# HG changeset patch
# User wenzelm
# Date 1546456801 -3600
# Node ID 09a6a7c04b45ef8f4aec3c4cba2e414e134c7db8
# Parent  676182f2e3757d632a48aceac66d89ac56b230b0
more robust system channel via options that are private to the user;

diff -r 676182f2e375 -r 09a6a7c04b45 etc/options
--- a/etc/options	Wed Jan 02 12:50:32 2019 +0100
+++ b/etc/options	Wed Jan 02 20:20:01 2019 +0100
@@ -302,3 +302,9 @@
 option build_log_ssh_port : int = 0
 option build_log_history : int = 30  -- "length of relevant history (in days)"
 option build_log_transaction_size : int = 1  -- "number of log files for each db update"
+
+
+section "Isabelle/Scala/ML system channel"
+
+option system_channel_address : string = ""
+option system_channel_password : string = ""
diff -r 676182f2e375 -r 09a6a7c04b45 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Wed Jan 02 12:50:32 2019 +0100
+++ b/src/Pure/ML/ml_process.scala	Wed Jan 02 20:20:01 2019 +0100
@@ -22,7 +22,6 @@
     env: Map[String, String] = Isabelle_System.settings(),
     redirect: Boolean = false,
     cleanup: () => Unit = () => (),
-    channel: Option[System_Channel] = None,
     sessions_structure: Option[Sessions.Structure] = None,
     session_base: Option[Sessions.Base] = None,
     store: Option[Sessions.Store] = None): Bash.Process =
@@ -89,6 +88,7 @@
 
     // options
     val isabelle_process_options = Isabelle_System.tmp_file("options")
+    Isabelle_System.bash("chmod 600 " + File.bash_path(File.path(isabelle_process_options)))
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
@@ -120,13 +120,7 @@
     val eval_process =
       if (heaps.isEmpty)
         List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
-      else
-        channel match {
-          case None =>
-            List("Isabelle_Process.init_options ()")
-          case Some(ch) =>
-            List("Isabelle_Process.init_protocol " + ML_Syntax.print_string_bytes(ch.server_name))
-        }
+      else List("Isabelle_Process.init ()")
 
     // ISABELLE_TMP
     val isabelle_tmp = Isabelle_System.tmp_dir("process")
diff -r 676182f2e375 -r 09a6a7c04b45 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Wed Jan 02 12:50:32 2019 +0100
+++ b/src/Pure/PIDE/prover.scala	Wed Jan 02 20:20:01 2019 +0100
@@ -82,8 +82,6 @@
 
   private def output(kind: String, props: Properties.T, body: XML.Body)
   {
-    if (kind == Markup.INIT) channel.accepted()
-
     val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
     val reports = Protocol_Message.reports(props, body)
     for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
@@ -155,7 +153,7 @@
       system_output("process_manager terminated")
       exit_message(result)
     }
-    channel.accepted()
+    channel.shutdown()
   }
 
 
diff -r 676182f2e375 -r 09a6a7c04b45 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Jan 02 12:50:32 2019 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Jan 02 20:20:01 2019 +0100
@@ -10,9 +10,9 @@
   val protocol_command: string -> (string list -> unit) -> unit
   val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
-  val init_protocol: string -> unit
   val init_options: unit -> unit
   val init_options_interactive: unit -> unit
+  val init: unit -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
@@ -173,7 +173,7 @@
 val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
 val default_modes2 = [isabelle_processN, Pretty.symbolicN];
 
-val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn socket =>
+val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
   let
     val _ = SHA1.test_samples ()
       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
@@ -184,7 +184,8 @@
       Unsynchronized.change print_mode
         (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
 
-    val (in_stream, out_stream) = Socket_IO.open_streams socket;
+    val (in_stream, out_stream) = Socket_IO.open_streams address;
+    val _ = Byte_Message.write_line out_stream password;
     val msg_channel = init_channels out_stream;
     val _ = loop in_stream;
     val _ = Message_Channel.shutdown msg_channel;
@@ -211,4 +212,17 @@
   Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0);
   Printer.show_markup_default := true);
 
+
+(* generic init *)
+
+fun init () =
+  let
+    val address = Options.default_string \<^system_option>\<open>system_channel_address\<close>;
+    val password = Options.default_string \<^system_option>\<open>system_channel_password\<close>;
+  in
+    if address <> "" andalso password <> ""
+    then init_protocol (address, password)
+    else init_options ()
+  end;
+
 end;
diff -r 676182f2e375 -r 09a6a7c04b45 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Wed Jan 02 12:50:32 2019 +0100
+++ b/src/Pure/System/isabelle_process.scala	Wed Jan 02 20:20:01 2019 +0100
@@ -49,10 +49,13 @@
     val channel = System_Channel()
     val process =
       try {
-        ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes, cwd = cwd,
-          env = env, sessions_structure = sessions_structure, store = store, channel = Some(channel))
+        val channel_options =
+          options.string.update("system_channel_address", channel.address).
+            string.update("system_channel_password", channel.password)
+        ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
+            cwd = cwd, env = env, sessions_structure = sessions_structure, store = store)
       }
-      catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
+      catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
     process.stdin.close
 
     new Prover(receiver, xml_cache, channel, process)
diff -r 676182f2e375 -r 09a6a7c04b45 src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Wed Jan 02 12:50:32 2019 +0100
+++ b/src/Pure/System/system_channel.scala	Wed Jan 02 20:20:01 2019 +0100
@@ -20,14 +20,27 @@
 {
   private val server = new ServerSocket(0, 50, Server.localhost)
 
-  val server_name: String = Server.print_address(server.getLocalPort)
-  override def toString: String = server_name
+  val address: String = Server.print_address(server.getLocalPort)
+  val password: String = UUID.random().toString
+
+  override def toString: String = address
+
+  def shutdown() { server.close }
 
   def rendezvous(): (OutputStream, InputStream) =
   {
     val socket = server.accept
-    (socket.getOutputStream, socket.getInputStream)
-  }
+    try {
+      val out_stream = socket.getOutputStream
+      val in_stream = socket.getInputStream
 
-  def accepted() { server.close }
+      if (Byte_Message.read_line(in_stream).map(_.text) == Some(password)) (out_stream, in_stream)
+      else {
+        out_stream.close
+        in_stream.close
+        error("Failed to connect system channel: bad password")
+      }
+    }
+    finally { shutdown() }
+  }
 }