Merge branch 'master' of https://github.com/TroupeLang/Troupe-user-guide

Author: Aslan Askarov

body.tex

@@ -303,6 +303,10 @@ \subsubsection{Example: updateable service}
 main thread finished with value: ()@{}%{}
 \end{verbatim}
 
+\subsection{Debugging concurrent programs}
+To help debugging concurrent programs, one can use a special primitive $\code{\_setProcessDebuggingName}$ that
+takes a string argument and uses that string when reporting errors in the process. By design, there is no mechanism
+for reading the process name other than causing an error; this prevents using process names to leak information.
 
 \section{Information flow control}
 \label{sec:infoflow}
@@ -404,16 +408,20 @@ \subsection{Monitoring for information flow}
 we also carry the information about the chosen branch into the type label.
 
 \paragraph{Implicit flows and I/O}
-The implicit information flows are further propagated between processes,
-as one can see in this modification of the previous example.
+The implicit information flows are further propagated between processes. 
+In the mailbox, each message is additionally tagged with a label that 
+corresponds to the blocking level of the sender at the time when the message was sent.
+Troupe supports filtering messages based on these tags.
+In the following example, \code{rcvp} is a form of receive statement that selects messages
+where the pc-tag set to the provided label argument.
 
 \begin{lstlisting}
 let val x = 10 raisedTo {secret}
     val p = self()
     val _ = spawn ( fn () => if x > 0 
     							then send (p, 1) 
     							else send (p, 0) )
-in receive [ hn x => x ]
+in rcvp ({secret}, [ hn x => x ])
 end
 \end{lstlisting}
 \begin{verbatim}
@@ -565,6 +573,53 @@ \subsubsection{Declassification of the blocking level}
 \code{pinipop} dynamically scope the part of the execution for which the blocking label is declassified.
 
 
+\subsection{Information flow control with I/O primitives}
+This section may be omitted upon first read as it has a number of information flow subtleties that 
+can be omitted when first starting to use the system.
+\subsubsection{Generalized receive and mailbox clearances}
+
+I/O operations such as send and receive introduce additional concerns w.r.t. 
+information flow control. In particular, because mailbox acts as a mutable state, an extra
+care needs to be taken to control information flows through the mailbox structure.
+
+
+Every message in a mailbox carries an extra label -- the blocking level of the sender.
+Receiving a value furthermore propagates the taint of the blocking level from the sender to the receiver. 
+In order to constrain a receive operation from an accidental raise of the blocking level, Troupe
+provides a general receive primitive in the form 
+\code{rcv(lev1,lev2,hns)}. Here, \code{lev1} and \code{lev2}
+indicate the to and from-levels of the pc-tags on the messages, and \code{hns} is the list of 
+handlers as before.
+The \code{receive} operation we introduced earlier is equivalent to \code{rcvp}
+at the level of the current pc label.
+
+While such a form of general receive over an interval of levels is useful, it is also too powerful 
+and needs to be further constrained. Consider the following snippet
+
+
+\begin{lstlisting}
+let val _ = if (secret) then rcv ({}, {alice}, [hn x => x] else ()
+in val x = rcv ({}, {}, [hn x => x ])
+end
+\end{lstlisting}
+
+Because the receive in the high branch is on an interval, the value of \code{x} may 
+depend on the secret value. In general, one can encode an entire secret in the structure 
+of the mailbox. To prevent such programs, Troupe provides a special notion of \emph{mailbox clearance}
+that constrains receives on an interval. The mailbox clearance is a proxy for an authority. 
+It can be raised using a dedicated command \code{raisembox (lev)} that returns a lowering
+capability and lowered with command \code{lowermbox(c, authority)}. 
+There are a few constraints related to the mailbox clearance.
+
+\begin{enumerate}
+    \item In order to receive on an interval $(\ell_1, \ell_2)$ under $\mathit{pc}$ 
+    with mailbox clearance $\ell_{\mathit{clear}}$ it must hold that $\ell_2 \sqcup \mathit{pc} \sqsubseteq \ell_1 \sqcup \ell_{\mathit{clear}}$. 
+    This constraint ensures that the mailbox clearance is sufficient for the interval receives. When mailbox clearance is $\bot$ -- as it is in the beginning of the program -- only point intervals of the form $(\ell, \ell)$ where $\mathit{pc} \sqsubseteq \ell$ are allowed.
+
+    \item The $\mathit{pc}$-label of the program point where the mailbox clearance is raised affects the lower bound of the intervals. In particular, if the clearance is raised when the $\mathit{pc}$ counter is $\mathit{pc}_{\mathit{raise}}$, the mailbox structure cannot be influenced by receives that are not as restrictive as $\mathit{pc}_{\mathit{raise}}$; in other words: $ \mathit{pc}_\mathit{raise} \sqsubseteq \mathit{pc} \sqcap \ell_1$, where $\ell_1$ is the lower bound of the interval receive. 
+    \item If the process mailbox clearance is raised in a branch, it must be lowered back before reaching the join point of the branch.
+\end{enumerate}
+
 
 
 
@@ -613,7 +668,16 @@ \subsubsection{Registering and looking up processes}
 end    
 \end{lstlisting}
 
+\subsubsection{Aliases}
+Aliases is a mechanism that allows us to avoid having hardcoded node identifiers in the source code. 
+The alias mechanism operates in the way of the traditional Unix hosts files.
+To use this mechanism, we need to provide the path to a special alias file that contains a mapping between
+alias strings and network identifiers. In the text of the program, an alias string must start with character~"@".
+
 
+\begin{verbatim}
+$TROUPE/rt/troupe out.js --aliases=<path_to_aliases_file>
+\end{verbatim}
 
 \subsection{Node trust levels}
 
@@ -623,7 +687,6 @@ \subsection{Node trust levels}
 passing a trust map file that include the identity of the nodes and their maximum
 trust level.
 
-
 
 \subsection{Remote spawning}
 If we know of a node identifier, we can spawn a thread on that node. Remote spawning is 
@@ -695,6 +758,14 @@ \subsubsection{\code{declassify}}
 
 \end{description}
 
+\subsubsection{\code{lowermbox}}
+\begin{description}
+    \item [Description] Lowers the clearance of the current process' mailbox. 
+    \item [Arguments] A tuple of the raise capability and authority 
+    \item [Returns] Unit. 
+    \item [Failure behavior] Fails if the type of the argument is invalid (dynamic type checking). Fails if the authority is insufficient for this lowering, or the provided capability does not match the stack scoping discipline. 
+\end{description}
+
 
 \subsubsection{\code{mkuuid}}
 \begin{description}
@@ -775,6 +846,16 @@ \subsubsection{\code{send}}
 \end{description}
 
 
+\subsubsection{\code{\_setProcessDebuggingName}}
+\begin{description}
+    \item [Description] Sets the process name that is used in debugging.
+    \item [Argument] A string value.
+    \item [Returns] Unit.
+    \item [Failure behavior] Fails if the type of the argument is invalid (dynamic type checking).
+\end{description}
+
+
+
 \subsubsection{\code{sleep}}
 
 \begin{description}
@@ -806,6 +887,31 @@ \subsubsection{\code{raisedTo}}
     \item [Example usage] $\code{42\ raisedTo\ \{alice\}}$
 \end{description}
 
+\subsubsection{\code{raiseTrust}}
+\begin{description}
+    \item [Description] Dynamically raise the trust level of a node.
+    \item [Arguments] A triple of a node identifier, root-level authority, and the intended trust level.
+    \item [Returns] Unit.
+    \item [Failure behavior]. Fails if the argument type is invalid. Fails if the authority argument is not top.
+ Fails if the blocking level is not $\bot$.
+    \item [Example usage] $\code{raiseTrust("@alicescomputer", authority, \{alice\})}$
+\end{description}
+Note that the top-level authority is required because this is a privileged operation with system-wide consequences. 
+
+
+
+
+\subsubsection{\code{raisembox}}
+\begin{description}
+    \item [Description] Raises the clearance of the current process' mailbox. 
+    \item [Arguments] A security level
+    \item [Returns] A capability for lowering the mailbox level back to the previous value. 
+    \item [Failure behavior] Fails if the type of the argument is invalid (dynamic type checking).
+\end{description}
+
+
+
+
 \subsubsection{\code{readInput}}
 \begin{description}
 \item[Description] Reads a  line from the console.
@@ -831,10 +937,11 @@ \subsubsection{\code{register}}
 $\mathit{authority}$ is the top authority value.
     \item [Returns] Unit.
     \item [Blocking behavior] Synchronous. 
-    \item [Failure behavior] Crashes if the provided authority is not top.
-    \item [Example usage]\textcode{register ("auctionServer", self())}
+    \item [Failure behavior] Crashes if the provided authority is not top, or if the blocking level is not $\bot$.
+    \item [Example usage]\textcode{register ("auctionServer", self(), authority)}
 \end{description}
 
+Note that this is a privileged operation with system-wide consequences. 
 
 
 \subsubsection{\code{rcv}}