Formalization of Troupe's single-process information-flow meta-theory in Lean 4

Troupe is a functional programming language for concurrent and distributed programs. A Troupe program is a collection of processes in the actor style: a process has a mailbox, receives messages from it, and sends messages to other processes, on the same node or on another one. The language enforces information-flow control at run time. Every value carries a label, the runtime propagates labels through computation, and a monitor refuses the operations that would move information against the order on labels. The compiler translates a program to an intermediate representation, and the runtime executes that representation with the monitor on.

In this report we present a formalization, in Lean 4, of the information-flow meta-theory of one Troupe process. Our formal model is a single thread that runs the intermediate representation under the monitor, reads messages from its mailbox, and emits outputs. The messages in the mailbox are the input of a run; the outputs and the internal events of a run are what an observer sees. The model has no instruction that starts a second thread and no scheduler.

The result is a security condition on runs, stated over consistent inputs, with separate bounds for downgrades, and a theorem (Theorem 1) that every run of the monitored machine satisfies it. As a corollary, a well-formed program that contains no instruction that may emit a downgrade is noninterfering under the monitor: at every level and after every step, the consistent inputs of an observer of its outputs are those of the empty trace (Lemma 14).

The report is organized as follows. §1 and §2 define labels, authorities and the flow order. §3 defines the intermediate representation, the labelled values, the events of a run and the input supplies. §4 defines the monitored machine. §5 defines what an observer sees of values, traces and inputs, and §6 the security condition. §7 states the theorem and presents its proof; §8 collects what the theorem guarantees and derives from it noninterference for downgrade-free programs (§8.1); §9 is a reference to the Lean lemmas of the proof. We discuss the relation of the development to the work of Bay and Askarov [BA20] in §10.

The report is a transcription of the Lean development (Troupe/), made by an LLM; the Lean is the source of truth, and the mathematics here is the Lean’s. Under each heading a grey line records the Lean files from which the section was transcribed, with their checksums. Each definition and lemma names its Lean declaration. Every example is pinned by a runnable file of the repository, named in the grey line that closes it; a sentence between blue guillemets, or a block marked as LLM narrative, has a docstring of the development as its only source.

1 Labels

A label records who may read a piece of data and who vouches for it. We take labels from the DC-label model of Stefan, Russo, Mazières and Mitchell (Disjunction Category Labels, NordSec 2011; cited below as DC). A label there is a pair of formulas in conjunctive normal form (DC Definition 1): the first names the principals who may observe the data, the second the principals who created it and may modify it. The Lean development keeps the pair and abstracts the formulas to an arbitrary carrier.

A label over a carrier \(P\) is a pair of two elements of \(P\), its confidentiality projection and its integrity projection (Label, the type \(P\times P^{\mathrm{op}}\)). The constructor Label.mk builds the label \[\ell \triangleq\langle c \,;\, i \rangle, \qquad c, i \in P,\] and the functions Label.conf and Label.integ return \(\mathsf{conf}(\ell ) = c\) and \(\mathsf{integ}(\ell ) = i\). The relations of this section and the next carry the names of the DC model: can-flow-to (DC Definition 2), the join (DC Definition 3), can-flow-to given privileges (DC Definition 4) and can-delegate (DC Definition 5, here acts-for). Each is stated over whatever order structure on \(P\) it needs, and we say which as we go.

Throughout the report we illustrate the definitions over one concrete carrier, the finite sets of the three principals \(\mathsf{alice}\), \(\mathsf{bob}\) and \(\mathsf{charlie}\) ordered by inclusion (PLabel). We write \(A\) for the label \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \top \rangle\). Intuitively, \(A\) is the secret of \(\mathsf{alice}\): the examples use a message of presence \(A\) as the secret that an observer at \(\bot\) must not learn.

Distinguished labels

When the carrier is bounded, four labels have both projections at an extreme. The right column gives the name of the matching constant of the Troupe implementation (rt/src/levels/DCLabels/dclabel.mts). \[\begin{array}{r@{\;}c@{\;}l@{\qquad}l} \bot&=& \langle \bot \,;\, \top \rangle & \texttt{IFC\_BOT}\\ \top&=& \langle \top \,;\, \bot \rangle & \texttt{IFC\_TOP}\\ \ensuremath{\mathsf{rootauth}}&=& \langle \top \,;\, \top \rangle & \texttt{TRUST\_ROOT}\\ \ensuremath{\mathsf{trustnull}}&=& \langle \bot \,;\, \bot \rangle & \texttt{TRUST\_NULL} \end{array}\] Over PLabel these are \(\bot=\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}},\ensuremath{\mathsf{charlie}}\} \rangle\), the public and fully trusted label, and \(\top\) with the two sets exchanged; \(\ensuremath{\mathsf{rootauth}}\) has both sets full and \(\ensuremath{\mathsf{trustnull}}\) both empty. The labels \(\bot\) and \(\top\) are the bottom and the top of the flow order of §2. The other two are the extremes of a second order, defined next.

Authorities and the acts-for order

A label has a second use in the formal model, as an authority. Every downgrade instruction of §3 takes an authority as an operand, and the authority says which downgrades the instruction may perform (Definition 4). We compare two authorities by the acts-for relation.

Intuitively, an authority is the stronger the more principals it carries in each projection. For example, \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) acts for \(\langle \emptyset \,;\, \emptyset \rangle\), since \(\emptyset\subseteq\emptyset\) and \(\emptyset\subseteq\{\ensuremath{\mathsf{alice}}\}\), and not the other way round. The two authorities \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \emptyset \rangle\) and \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) are incomparable: neither acts for the other. The label \(\ensuremath{\mathsf{rootauth}}\) acts for \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\), and \(\top\) does not, since its integrity projection is empty. The relation is reflexive and transitive over a preordered carrier (Label.actsFor.refl, Label.actsFor.trans) and antisymmetric over a partially ordered one (Label.actsFor_antisymm), so it is a partial order (Label.actsFor.instIsPartialOrder). Over a bounded carrier \(\ensuremath{\mathsf{rootauth}}\) acts for every label (Label.actsFor_root) and every label acts for \(\ensuremath{\mathsf{trustnull}}\) (Label.actsFor_null); we call \(\ensuremath{\mathsf{rootauth}}\) the root authority and \(\ensuremath{\mathsf{trustnull}}\) the null authority. We check the instances of this section and the next in examples/labels_orders.lean.

Formalized: examples/labels_orders.lean • run: scripts/run-example.sh labels_orders

The authority join

We will need to combine two authorities into one that acts for both. The machine does so when it closes a receive region (rule close, Fig. 4), and the security condition does so in its bound on the close event (Definition 17, case 4).

For example, \[\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \emptyset \rangle \mathbin{\curlyvee} \langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle = \langle \{\ensuremath{\mathsf{alice}}\} \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle ,\] and this label acts for each of the two. The authority join is the least upper bound in the acts-for order: it acts for both operands (Label.actsFor_authJoin_left, Label.actsFor_authJoin_right), and any label that acts for both acts for the join (Label.authJoin_actsFor). It is monotone in both arguments (Label.authJoin_actsFor_mono) and associative (Label.authJoin_assoc), and over a bounded carrier the null authority is its right unit, \(a \mathbin{\curlyvee} \ensuremath{\mathsf{trustnull}} = a\) (Label.authJoin_bot). Note that the authority join is not the join of the flow order; we define that join in the next section and return to this pair of authorities there.

2 The information-flow order

Information may move from one label to another only in the direction of the flow order. This section defines the order and its join, which the monitor of §4 uses in its checks and in labelling results, and then the privileged can-flow-to relation, which adds an authority and is the check of every downgrade. Data becomes more confidential when a principal is added to its confidentiality projection and less trusted when one is removed from its integrity projection, so the order is the product order on \(P\times P^{\mathrm{op}}\).

In the Lean development the relation \(\sqsubseteq\) is the order \(\le\) of the product type, and the lemma Label.flowsTo_iff states the displayed equivalence. For example, \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle \sqsubseteq\langle \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\} \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) holds, because \(\{\ensuremath{\mathsf{alice}}\}\subseteq{}\)\(\{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\}\) and the integrity projections are equal; and \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\} \rangle \sqsubseteq\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) holds, because the confidentiality projections are equal and \(\{\ensuremath{\mathsf{alice}}\}\subseteq{}\)\(\{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\}\). Neither converse holds. Note that the flow order and the acts-for order run in opposite directions on the integrity projection: \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle \sqsubseteq\langle \emptyset \,;\, \emptyset \rangle\), while \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) acts for \(\langle \emptyset \,;\, \emptyset \rangle\). In particular the null authority \(\ensuremath{\mathsf{trustnull}}=\langle \emptyset \,;\, \emptyset \rangle\) flows neither to \(\ensuremath{\mathsf{rootauth}}\) nor to \(\bot\), and \(\bot\sqsubseteq\ensuremath{\mathsf{trustnull}}\).

The join of the flow order joins the confidentiality projections and meets the integrity projections: \[\langle c_1 \,;\, i_1 \rangle \sqcup \langle c_2 \,;\, i_2 \rangle = \langle c_1 \sqcup c_2 \,;\, i_1 \sqcap i_2 \rangle\] (Label.conf_sup, Label.integ_sup). The value operations of §3 label the result of a binary operator by the join of the data labels of its arguments: the result of adding a value of \(\mathsf{alice}\) to a value of \(\mathsf{bob}\) is labelled \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle \sqcup \langle \{\ensuremath{\mathsf{bob}}\} \,;\, \{\ensuremath{\mathsf{bob}}\} \rangle = \langle \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\} \,;\, \emptyset \rangle\), at least as confidential and at most as trusted as either operand. This is also why authorities are not combined by the join of the flow order. The join of the authorities \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \emptyset \rangle\) and \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) in the flow order is \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \emptyset \rangle\), which does not act for the second of them, whereas their authority join \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) acts for both (§1).

Privileged can-flow-to

An authority permits flows that the order does not. We capture this by a relation with the authority as a third argument. It is the relation that the downgrade check \(\ensuremath{\mathsf{okDown}}\) of §3 tests, and it is also how an observer who holds an authority \(a\) at a level \(\ell\) sees a label \(x\): the observer sees \(x\) when \(x \sqsubseteq_{a} \ell\) (§5).

Both joins in the display are joins of the carrier \(P\). Intuitively, the authority \(a\) may remove the principals of \(\mathsf{conf}(a)\) from a confidentiality projection and add the principals of \(\mathsf{integ}(a)\) to an integrity projection. For example, the flow from \(\langle \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\} \,;\, \emptyset \rangle\) to \(\langle \{\ensuremath{\mathsf{bob}}\} \,;\, \emptyset \rangle\) does not hold in the flow order, but it holds under the authority \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \emptyset \rangle\): the first conjunct is \(\{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\}\subseteq{}\)\(\{\ensuremath{\mathsf{bob}}\}\cup\{\ensuremath{\mathsf{alice}}\}\). Under the same authority the flow from \(\langle \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\} \,;\, \emptyset \rangle\) to \(\langle \emptyset \,;\, \emptyset \rangle\) does not hold, since \(\mathsf{bob}\) is not in \(\emptyset\cup\{\ensuremath{\mathsf{alice}}\}\). On the integrity side, the flow from \(\langle \emptyset \,;\, \emptyset \rangle\) to \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) holds under the authority \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\), with the second conjunct \(\{\ensuremath{\mathsf{alice}}\}\subseteq{}\)\(\emptyset\cup\{\ensuremath{\mathsf{alice}}\}\), and not under \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \emptyset \rangle\); and \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) does not permit the confidentiality flow of the first example. Under the null authority neither flow holds.

The last observation is general: under the null authority the privileged relation is the flow order, \(\ell _1 \sqsubseteq_{\ensuremath{\mathsf{trustnull}}} \ell _2\) if and only if \(\ell _1 \sqsubseteq\ell _2\) (Label.privFlowsTo_bot), and every flow of the flow order is a privileged flow under every authority (Label.le_imp_privFlowsTo). A stronger authority permits every flow that a weaker one does, where strength is measured in the acts-for order of §1, not in the flow order.

To see that the flow order would be the wrong measure, take \(a=\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\) and \(b=\ensuremath{\mathsf{trustnull}}\). In the flow order \(a \sqsubseteq a \sqcup b\), and yet the flow from \(\langle \emptyset \,;\, \emptyset \rangle\) to \(\langle \emptyset \,;\, \{\ensuremath{\mathsf{alice}}\} \rangle\), which holds under \(a\), does not hold under \(a \sqcup b=\langle \emptyset \,;\, \emptyset \rangle\): the join has met the integrity projections and lost \(\mathsf{alice}\). The label \(a \sqcup b\) does not act for \(a\) (a checked \(\mathsf{decide}\) example in the PLabel block of Troupe/Label.lean), while the authority join is \(a \mathbin{\curlyvee} b=a\) (Label.authJoin_bot). The development keeps this instance as a witness.

Formalized: _working_notes/soundness-witnesses/close_charge_join_drops_integrity_privilege.lean • run: scripts/run-example.sh close_charge_join_drops_integrity_privilege

The next section puts labels on the values that programs compute and on the events that their runs emit.

3 The intermediate representation

This section presents the programs that the machine of §4 runs, the labelled values that they compute with, the events that their steps emit, and the input supplies that they read. The security condition of §6 is stated over the events of a run and the supply that the run starts from.

3.1 Grammar

The formal model runs the closure-converted intermediate representation of the Troupe compiler.¹ A program (Syntax.Program) is a function table, which is a list of bodies, together with a main body. A body is a list of instructions followed by one terminator. A local variable \(\ensuremath{\mathsf{loc}}\,n\) carries a number \(n\) that identifies it, and an instruction binds the local with such a number, which we write to the left of \(:=\). The operands of an expression, of every other instruction and of a terminator are atoms.

\[\begin{array}{r@{\;}c@{\;}l@{\qquad}l} \rlap{\text{(variables, atoms, types, operators)}}\\[2pt] x&::=& \ensuremath{\mathsf{loc}}\,n \mid \ensuremath{\mathsf{env}}\,i \mid \ensuremath{\mathsf{self}}& \texttt{Var}\\ t&::=& x \mid b \mid \ensuremath{\mathsf{pc}}\mid \ensuremath{\mathsf{root}}& \texttt{Atom}\\ \tau&\in& \{\ensuremath{\mathsf{unit}},\ensuremath{\mathsf{int}},\ensuremath{\mathsf{level}},\ensuremath{\mathsf{authority}},\ensuremath{\mathsf{closure}},\ensuremath{\mathsf{tuple}},\ensuremath{\mathsf{list}},\ensuremath{\mathsf{capability}}\} & \texttt{Ty}\\ \oplus&\in& \{+,-,=,<,\sqcup,\sqcap,/\} & \texttt{BinOp}\\ \odot&\in& \{\ensuremath{\mathsf{levelOf}},\ensuremath{\mathsf{typeOf}}\} & \texttt{UnOp}\\ d&\in& \{\ensuremath{\mathsf{conf}},\ensuremath{\mathsf{integ}},\ensuremath{\mathsf{both}}\} & \texttt{Dim}\\ g&\in& \{\ensuremath{\mathsf{value}},\ensuremath{\mathsf{typeOnly}},\ensuremath{\mathsf{valueOnly}}\} & \texttt{Gran}\\[6pt] \rlap{\text{(expressions, instructions, terminators, bodies, programs)}}\\[2pt] e&::=& t \mid t \mathbin{\oplus} t \mid \odot\,t \mid \ensuremath{\mathsf{attenuate}}(t_{\mathit{auth}},t_{\mathit{lev}}) & \texttt{Expr}\\ & \mid& \ensuremath{\mathsf{tuple}}(\overline{t}) \mid \ensuremath{\mathsf{proj}}(i,t) \mid \ensuremath{\mathsf{list}}(\overline{t}) \mid \ensuremath{\mathsf{head}}\,t \mid \ensuremath{\mathsf{tail}}\,t &\\ \iota&::=& n \mathrel{:=} e \mid n \mathrel{:=} \ensuremath{\mathsf{outputToEndpoint}}(t_{\mathit{chan}},t_{\mathit{val}}) & \texttt{Inst}\\ & \mid& n \mathrel{:=} \ensuremath{\mathsf{tyrecv}}(t_{\mathit{pres}},\tau) &\\ & \mid& n \mathrel{:=} \ensuremath{\mathsf{peek}}(t_{\mathit{idx}},t_{\mathit{lowb}},t_{\mathit{highb}}) \mid n \mathrel{:=} \ensuremath{\mathsf{consume}}(t_{\mathit{idx}},t_{\mathit{lowb}},t_{\mathit{highb}},t_{\mathit{auth}}) &\\ & \mid& \overline{n} \mathrel{:=} \ensuremath{\mathsf{mkClosures}}(\overline{n}_{\mathit{fn}},\overline{x}) &\\ & \mid& n \mathrel{:=} \ensuremath{\mathsf{downgrade}}_{d,g}(t_{\mathit{val}},t_{\mathit{auth}},t_{\mathit{lev}}) \mid n \mathrel{:=} \ensuremath{\mathsf{blockDowngrade}}_{d}(t_{\mathit{auth}},t_{\mathit{lev}}) &\\ & \mid& n \mathrel{:=} \ensuremath{\mathsf{enableRangedReceive}}(t_{\mathrm{lo}},t_{\mathrm{hi}},t_{\mathit{auth}}) \mid n \mathrel{:=} \ensuremath{\mathsf{rangedConsume}}(t_{\mathit{idx}},t_{\mathrm{lo}},t_{\mathrm{hi}}) &\\ & \mid& n \mathrel{:=} \ensuremath{\mathsf{disableRangedReceive}}(t_{\mathit{cap}}) &\\ \mathit{tm}&::=& \ensuremath{\mathsf{ret}}\,t \mid \ensuremath{\mathsf{branch}}(t,B_{\mathit{thn}},B_{\mathit{els}}) \mid \ensuremath{\mathsf{stackExpand}}(n,B_{\mathit{body}},B_{\mathit{cont}}) \mid \ensuremath{\mathsf{tailCall}}(t_{f},t_{\mathit{arg}}) & \texttt{Term}\\ B&::=& \ensuremath{\mathsf{bb}}(\overline{\iota},\mathit{tm}) & \texttt{Body}\\ \mathit{prog}&=& (\overline{B},\ B) & \texttt{Program} \end{array}\] The subscripts on the operands are the Lean argument names. The atom \(\ensuremath{\mathsf{root}}\) evaluates to the root authority, the atom \(\ensuremath{\mathsf{pc}}\) to a label of the monitor (§4), and a base value \(b\) in atom position is a constant. The function \(\mathsf{toInt}\) (Ty.toInt) numbers the runtime types \(\ensuremath{\mathsf{unit}}\mapsto 0\), \(\ensuremath{\mathsf{int}}\mapsto 1\), \(\ensuremath{\mathsf{level}}\mapsto 2\), \(\ensuremath{\mathsf{authority}}\mapsto 3\), \(\ensuremath{\mathsf{closure}}\mapsto 4\), \(\ensuremath{\mathsf{tuple}}\mapsto 5\), \(\ensuremath{\mathsf{list}}\mapsto 6\), \(\ensuremath{\mathsf{capability}}\mapsto 7\).

The step rules of §4 give the instructions and terminators their meaning. For orientation, the following table says what one step of each does and names its rule.

The three remaining instructions, \(\ensuremath{\mathsf{enableRangedReceive}}\), \(\ensuremath{\mathsf{rangedConsume}}\) and \(\ensuremath{\mathsf{disableRangedReceive}}\), together with the runtime type \(\ensuremath{\mathsf{capability}}\), belong to the receive regions, which we present as a whole in §4.5.

Bodies of this grammar are verbose, so we write the example programs of this report in the notation of the program builder of the development (Troupe/Builder.lean), one binding per line. Consider the program that receives an integer at the presence {alice}, compares it with zero, and returns \(100\) or \(200\); we return to it many times as the secret branch.

secret <- tyrecv {alice} int
c      <- 0 < secret
r      <- if c then ret 100 else ret 200
ret r

The builder turns these four lines into the following body, which we print as the development prints it; $\(n\) is the local \(\ensuremath{\mathsf{loc}}\,n\), and the conditional has become a \(\ensuremath{\mathsf{stackExpand}}\) whose inner body is a \(\ensuremath{\mathsf{branch}}\) and whose continuation returns the result.

$0 = receive(`{alice}`, int)
$1 = 0 < $0
stackexpand
  body:
    branch $1
      then:
        ret 100
      else:
        ret 200
  cont $2:
    ret $2

Formalized: examples/program_notation_and_ir.lean • run: scripts/run-example.sh program_notation_and_ir

The listings of this report print labels and values as the development does. A label whose integrity projection is the top of the carrier prints as its confidentiality projection alone: {alice} is the label \(A=\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \top \rangle\), and {} is the label \(\bot\). Every other label prints both projections: <{};{}> is the null authority \(\ensuremath{\mathsf{trustnull}}\). A labelled value prints as value@lev%tlev, base value, data label, type label, as in 42@{alice}%{alice}. An authority value prints its label after an exclamation mark: the root authority value prints as !{alice, bob, charlie}@{}%{}. The listings use two spellings of the builder notation, which denote the same instructions. The lines x <- tyrecv {alice} int and let x \(\leftarrow\) tyrecv {alice} .int both denote \(n \mathrel{:=} \ensuremath{\mathsf{tyrecv}}(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \top \rangle,\ensuremath{\mathsf{int}})\), and 0 < s and lt 0 s both denote the expression \(0<s\). The surface instructions declassify and blockdeclto are \(\ensuremath{\mathsf{downgrade}}\) at the granularity \(\ensuremath{\mathsf{value}}\) and \(\ensuremath{\mathsf{blockDowngrade}}\), both in the dimension \(\ensuremath{\mathsf{conf}}\) (declassify and blockDeclassify in Troupe/Builder.lean).

3.2 Values

Every value carries two labels: the data label \(\ell_v\) guards its content, and the type label \(\ell_\tau\) guards its runtime type, which a dynamically typed program may learn without learning the content. A labelled value (LVal) is a base value (BaseVal) together with the two labels, written \({b}^{\,\ell_v}_{\,\ell_\tau}\); the two types are mutually recursive. \[\begin{array}{r@{\;}c@{\;}l@{\qquad}l} b&::=& ()\mid n \mid \ensuremath{\mathsf{lev}}\,\ell \mid {!}\ell & \text{unit, integer, level, authority}\\ & \mid& \ensuremath{\mathsf{clos}}(\mathit{id},\mathit{fn},\overline{n},\overline{v}) & \text{closure}\\ & \mid& \ensuremath{\mathsf{tuple}}\,\overline{v} \mid \ensuremath{\mathsf{list}}\,\overline{v} & \text{tuple, list}\\ & \mid& \ensuremath{\mathsf{cap}}(\ell_{\mathrm{lo}},\ell_{\mathrm{hi}},\mathit{ok},\mathit{pc}_{\mathrm e},\ell_a,s_\Delta,s_\Phi,s_{\Delta\mathrm{lab}},s_{\Phi\mathrm{lab}},\mathit{prev},\mathit{uid}) & \text{region capability}\\ v&=& {b}^{\,\ell_v}_{\,\ell_\tau} & \text{labelled value} \end{array}\] Levels and authorities are first-class values: a level \(\ell\) is a label used as data, and an authority \({!}\ell\) is a label used as a capability for downgrading. In a closure, \(\mathit{id}\) is a pair \((\ell,n)\) of a label and a number that identifies the closure, \(\mathit{fn}\) is the index of its body in the function table, \(\overline{n}\) is the group of indices it was allocated with, and \(\overline{v}\) is the list of captured values. The last form of base value, the region capability, belongs to the receive regions of §4.5.

We write \(\mathsf{val}(v) = b\), \(\mathsf{lev}(v) = \ell_v\) and \(\mathsf{tlev}(v) = \ell_\tau\) for the projections of \(v= {b}^{\,\ell_v}_{\,\ell_\tau}\) (LVal.val, LVal.dataLabel, LVal.typeLabel), and \(\mathsf{type}(v)\) for its runtime type, the type of the constructor of the base value (BaseVal.ty, LVal.ty). The children of a base value (BaseVal.children) are the captured values of a closure and the components of a tuple or a list; every other base value has no children. To see the two labels at work, let \(A = \langle \{\ensuremath{\mathsf{alice}}\} \,;\, \top \rangle\) and take the integer \(5\) with data label \(A\) and type label \(\bot\): its content is the secret of \(\mathsf{alice}\), its type is public. The two reflection operators of §3.3 read one label each, with \(1\) for \(\mathsf{toInt}(\ensuremath{\mathsf{int}})\): \[\ensuremath{\mathsf{typeOf}}\,{5}^{\,A}_{\,\bot} = {1}^{\,\bot}_{\,\bot}, \qquad \ensuremath{\mathsf{levelOf}}\,{5}^{\,A}_{\,\bot} = {A}^{\,A}_{\,\bot}.\] The type is public and comes out public, and the data label comes out labelled by itself.

Intuitively, any operation on the content of a value reveals its type, so we require the type label to flow to the data label. Every step of the machine preserves this well-formedness of the values in a configuration (Config.WF, step_preserves_WF), and we require it of the payloads of a supply (Definition 9).

The second clause is stated in the Lean by recursion over the list of children (BaseVal.envWF); the quantified form is BaseVal.WF_clos_iff, BaseVal.WF_tuple_iff and BaseVal.WF_list_iff. For example, the value \({5}^{\,A}_{\,\bot}\) above is well-formed, since \(\bot\sqsubseteq A\), and the value \({5}^{\,\bot}_{\,A}\) with the two labels exchanged is not, since \(A\not\sqsubseteq\bot\); on the latter \(\ensuremath{\mathsf{typeOf}}\) would yield \({1}^{\,A}_{\,\bot}\), a secret type on a public content.

When a value is sent, everything inside it goes along, including the captured values of a closure and the components of a tuple. The label that an output has to clear is therefore the join of the data labels at every depth, which we call the send label. Rule outputToEndpoint of §4 tests it against the level of the channel, and Definition 9 tests it against the presence of a message.

For example, a closure labelled \(\bot\) that captures the value \({5}^{\,A}_{\,\bot}\), \(v={\ensuremath{\mathsf{clos}}(\mathit{id},\mathit{fn},\overline{n},[{5}^{\,A}_{\,\bot}])}^{\,\bot}_{\,\bot}\), has \(\mathsf{lev}(v)=\bot\) but \(\ensuremath{\mathsf{sendLabel}}(v)=A\): it can be sent to \(A\) and not to \(\bot\). Note that type labels do not enter the send label; only data labels do.

Formalized: examples/labelled_value_operations.lean • run: scripts/run-example.sh labelled_value_operations

3.3 Value operations

The evaluation functions and the step rules of §4 build labelled values from labelled values by the operations of the following table, three of which take a label \(\ell\) as a parameter. The table gives the base value, the data label and the type label of each result.

\[\begin{array}{l@{\quad}l@{\quad}l@{\quad}l@{\quad}l} \text{operation} & \text{base value} & \text{data label} & \text{type label} & \text{Lean}\\[2pt] \ensuremath{\mathsf{pub}}\,b & b& \bot & \bot & \texttt{LVal.pub}\\ \ensuremath{\mathsf{atPc}}_{\ell}\,v & \mathsf{val}(v) & \ell\sqcup\mathsf{lev}(v) & \ell\sqcup\mathsf{tlev}(v) & \texttt{LVal.atPc}\\ \ensuremath{\mathsf{raiseData}}_{\ell}\,v & \mathsf{val}(v) & \ell\sqcup\mathsf{lev}(v) & \mathsf{tlev}(v) & \texttt{LVal.raiseData}\\ \ensuremath{\mathsf{readTainted}}_{\ell}\,v & \mathsf{val}(v) & \ell\sqcup\mathsf{lev}(v) & \ell\sqcup\mathsf{lev}(v) & \texttt{LVal.readTainted}\\ \ensuremath{\mathsf{levelOf}}\,v & \mathsf{lev}(v) & \mathsf{lev}(v) & \bot & \texttt{LVal.levelOf}\\ \ensuremath{\mathsf{typeOf}}\,v & \mathsf{toInt}(\mathsf{type}(v)) & \mathsf{tlev}(v) & \bot & \texttt{LVal.typeOf}\\ \oplus(v_1,v_2) & \ensuremath{\mathsf{binCore}}(\oplus,\mathsf{val}(v_1),\mathsf{val}(v_2)) & \mathsf{lev}(v_1)\sqcup\mathsf{lev}(v_2)\sqcup\ell_{=} & \bot & \texttt{LVal.binOp} \end{array}\] The first four operations relabel. The operation \(\ensuremath{\mathsf{pub}}\) makes a public value of a base value; \(\ensuremath{\mathsf{atPc}}\) raises both labels of a value to a context label \(\ell\), which is how a constant created under a raised program counter is labelled; \(\ensuremath{\mathsf{raiseData}}\) raises the data label alone; and \(\ensuremath{\mathsf{readTainted}}\) sets both labels to the raised data label, which is how a value read from the mailbox is bound (rules peek, consume and rangedConsume). For example, with \(B = \langle \{\ensuremath{\mathsf{bob}}\} \,;\, \top \rangle\) and \(AB = \langle \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\} \,;\, \top \rangle\), \[\ensuremath{\mathsf{atPc}}_{B}\,{5}^{\,A}_{\,\bot} = {5}^{\,AB}_{\,B}, \qquad \ensuremath{\mathsf{raiseData}}_{B}\,{5}^{\,A}_{\,\bot} = {5}^{\,AB}_{\,\bot}, \qquad \ensuremath{\mathsf{readTainted}}_{B}\,{5}^{\,A}_{\,\bot} = {5}^{\,AB}_{\,AB}.\]

In the last row of the table, \(\ell_{=}\) is \(\ensuremath{\mathsf{eqLabel}}(\mathsf{val}(v_1),\mathsf{val}(v_2))\) (Definition 7) when \(\oplus\) is \({=}\) and is \(\bot\) for every other operator (LVal.binOpDataLabel), and the operation is undefined when \(\ensuremath{\mathsf{binCore}}\) is. The unary operation \(\odot\,v\) (LVal.unOp) is \(\ensuremath{\mathsf{levelOf}}\,v\) or \(\ensuremath{\mathsf{typeOf}}\,v\) according to the operator. The root authority value is \(\ensuremath{\mathsf{pub}}\,({!}\langle \top \,;\, \top \rangle)\) (LVal.rootAuth); its label is the root authority \(\ensuremath{\mathsf{rootauth}}\) of §1.

Equality

The operator \({=}\) compares two values by the function \(\ensuremath{\mathsf{refEq}}\), which ignores labels and compares closures by identity, and labels its result with \(\ensuremath{\mathsf{eqLabel}}(\cdot,\cdot)\). The result of comparing two tuples depends on the components up to the first pair that differs, and on no later component; the label \(\ensuremath{\mathsf{eqLabel}}(\cdot,\cdot)\) joins the data labels of exactly those components.

For example, the values \({5}^{\,A}_{\,\bot}\) and \({5}^{\,B}_{\,\bot}\) are not equal as labelled values, and \(\ensuremath{\mathsf{refEq}}\) of the two is true. Write a component without a label for a component labelled \(\bot\) on both labels, and let the compared tuples themselves carry \(\bot\). Comparing \(\ensuremath{\mathsf{tuple}}\,[1,\ {5}^{\,A}_{\,}]\) with \(\ensuremath{\mathsf{tuple}}\,[1,\ 9]\) yields \(0\) at the data label \(A\). Comparing \(\ensuremath{\mathsf{tuple}}\,[{5}^{\,A}_{\,},\ {7}^{\,B}_{\,}]\) with \(\ensuremath{\mathsf{tuple}}\,[9,\ 8]\) also yields \(0\) at \(A\): the first components already differ, so the label \(B\) of the second pair does not enter the result. Comparing \(\ensuremath{\mathsf{tuple}}\,[{5}^{\,A}_{\,}]\) with \(\ensuremath{\mathsf{tuple}}\,[{5}^{\,B}_{\,}]\) yields \(1\) at \(\langle \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\} \,;\, \top \rangle\).

The partial function \(\ensuremath{\mathsf{binCore}}\) (BaseVal.binCore) is defined on the following arguments and on no others. \[\begin{array}{r@{\;}c@{\;}l@{\qquad}l} \ensuremath{\mathsf{binCore}}(+,\,n_1,\,n_2) &=& n_1 + n_2\\ \ensuremath{\mathsf{binCore}}(-,\,n_1,\,n_2) &=& n_1 - n_2\\ \ensuremath{\mathsf{binCore}}(<,\,n_1,\,n_2) &=& 1 \text{ if } n_1 < n_2,\ \text{else } 0\\ \ensuremath{\mathsf{binCore}}(/,\,n_1,\,n_2) &=& n_1 / n_2 & \text{if } n_2 \neq 0 \text{ (the Lean division on } \mathbb{Z}\text{)}\\ \ensuremath{\mathsf{binCore}}(\sqcup,\,\ell_1,\,\ell_2) &=& \ell_1 \sqcup \ell_2\\ \ensuremath{\mathsf{binCore}}(\sqcap,\,\ell_1,\,\ell_2) &=& \ell_1 \sqcap \ell_2\\ \ensuremath{\mathsf{binCore}}(=,\,b_1,\,b_2) &=& 1 \text{ if } \ensuremath{\mathsf{refEq}}(b_1,b_2),\ \text{else } 0 \end{array}\] Every result of \(\ensuremath{\mathsf{binCore}}\) is a well-formed base value (BaseVal.binCore_WF) and contains no capability (BaseVal.binCore_capsSat, for the predicate \(\ensuremath{\mathsf{capsSat}}_Q\) of Definition 10 at every \(Q\)).

Attenuation and the downgrade check

The remaining two operations act on labels. Attenuation is the operation of the expression \(\ensuremath{\mathsf{attenuate}}\): it derives from an authority \(a\) the weaker authority \(t\), provided \(a\) acts for \(t\), and yields \(\bot\) otherwise. The predicate \(\ensuremath{\mathsf{okDown}}\) is the check of every downgrade, in the rules downgrade, blockDowngrade, consume and open of §4: it asks whether the authority \(\ell_a\) permits the flow from a from-label \(\ell_f\) to a to-label \(\ell_t\), and in the dimensions \(\ensuremath{\mathsf{conf}}\) and \(\ensuremath{\mathsf{integ}}\) it further requires that the other projection is unchanged. \[\begin{array}{r@{\;}c@{\;}l@{\qquad}l} \ensuremath{\mathsf{attenuate}}(a,t) &\triangleq& t \ \text{if}\ a \succcurlyeq t,\ \text{else}\ \bot & \texttt{attenuate}\\[2pt] \mathsf{off}_{\ensuremath{\mathsf{conf}}}(\ell_f,\ell_t) &\triangleq& \mathsf{integ}(\ell_f) = \mathsf{integ}(\ell_t) & \texttt{Dim.offPreserved}\\ \mathsf{off}_{\ensuremath{\mathsf{integ}}}(\ell_f,\ell_t) &\triangleq& \mathsf{conf}(\ell_f) = \mathsf{conf}(\ell_t)\\ \mathsf{off}_{\ensuremath{\mathsf{both}}}(\ell_f,\ell_t) &\triangleq& \mathsf{true}\\[2pt] \ensuremath{\mathsf{okDown}}_{d}(\ell_f,\ell_t,\ell_a) &\triangleq& \mathsf{off}_{d}(\ell_f,\ell_t) & \texttt{okToDowngrade}\\ && {}\wedge \mathsf{conf}(\ell_f) \le \mathsf{conf}(\ell_t)\sqcup\mathsf{conf}(\ell_a)\\ && {}\wedge \mathsf{integ}(\ell_t) \le \mathsf{integ}(\ell_f)\sqcup\mathsf{integ}(\ell_a) \end{array}\] Here \(a \succcurlyeq t\) is the acts-for order of Definition 1, and the two inequalities of \(\ensuremath{\mathsf{okDown}}\) are in the order of the carrier \(P\); they are the two conjuncts of privileged can-flow-to, so that in the dimension \(\ensuremath{\mathsf{both}}\) the check is exactly \(\ell_f \sqsubseteq_{\ell_a} \ell_t\) (Label.privFlowsTo_iff_okToDowngrade). Attenuating the root authority to \(t\) yields \(t\) (attenuate_root); attenuating \(a=\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \emptyset \rangle\) to \(\langle \{\ensuremath{\mathsf{bob}}\} \,;\, \emptyset \rangle\) yields \(\bot\), since \(a\) does not act for it. Under this \(a\) the check from \(A\) to \(\bot\) holds in the dimensions \(\ensuremath{\mathsf{conf}}\) and \(\ensuremath{\mathsf{both}}\), the two labels having the same integrity projection, and fails in the dimension \(\ensuremath{\mathsf{integ}}\), their confidentiality projections being different; and the check from \(\langle \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\} \,;\, \top \rangle\) to \(\bot\) fails in every dimension, because \(\mathsf{bob}\) is not in the confidentiality projection of \(a\).

Formalized: examples/labelled_value_operations.lean • run: scripts/run-example.sh labelled_value_operations

3.4 Events

A step of the machine emits at most one event, and the events of a run, oldest first, form its trace (Trace, a list of events). An observer sees a run through its trace (§5), and the security condition of §6 bounds what each event of a trace reveals. The events record outputs, mailbox reads, downgrades and the binding of values; the three forms of the last line below are emitted by the rules of a receive region (§4.5). The Lean constructors of the four downgrade events are downgradeVal, downgradeType, downgradeValType and downgradeBl, which we shorten to \(\ensuremath{\mathsf{dVal}}\), \(\ensuremath{\mathsf{dType}}\), \(\ensuremath{\mathsf{dValType}}\) and \(\ensuremath{\mathsf{dBl}}\). \[\begin{array}{r@{\;}c@{\;}l} \alpha&::=& \ensuremath{\mathsf{output}}(c,v) \mid \ensuremath{\mathsf{consumeInput}}(p,v) \mid \ensuremath{\mathsf{dgConsumeInput}}(a,\ell_{\mathrm{lo}},p_m,k)\\ &\mid& \ensuremath{\mathsf{dVal}}(d,a,\ell_t,v) \mid \ensuremath{\mathsf{dType}}(d,a,\ell_t,\ell,\tau) \mid \ensuremath{\mathsf{dValType}}(d,a,\ell_t,\ell_{\mathit{occ}},v,\ell_\tau,\tau) \mid \ensuremath{\mathsf{dBl}}(d,a,\ell_t)\\ &\mid& \ensuremath{\mathsf{assign}}(v) \mid \ensuremath{\mathsf{bind}}(\ell,\overline{v})\\ &\mid& \ensuremath{\mathsf{regionOpen}}(\ell_{\mathit{occ}},\ell_{\mathrm{lo}},\ell_{\mathrm{hi}},v) \mid \ensuremath{\mathsf{confinedConsumeInput}}(\ell_{\mathit{taint}},p_m,k) \mid \ensuremath{\mathsf{regionClose}}(a,a_{\mathrm{in}},\ell_{\mathrm{lo}},\ell,D) \end{array}\] The metavariables \(c\), \(p\), \(p_m\), \(a\), \(a_{\mathrm{in}}\) and every \(\ell\) range over labels, \(k\) over natural numbers, and \(D\) over lists of pairs \((p_m,k)\) of a label and a natural number. The step rules of §4 fill the fields. A pair \((p_m,k)\) is a removal descriptor; we define it together with the mailbox operator that computes it (§4.3).

In the listings a trace prints as a list of events: send \(c\) \(\triangleleft\) \(v\) and recv \(p\) \(\triangleright\) \(v\) are \(\ensuremath{\mathsf{output}}\) and \(\ensuremath{\mathsf{consumeInput}}\) events, assign \(\Rightarrow\) \(v\) is an \(\ensuremath{\mathsf{assign}}\) event, downgradeValType[conf] and blockDowngrade[conf] are \(\ensuremath{\mathsf{dValType}}\) and \(\ensuremath{\mathsf{dBl}}\) events in the dimension \(\ensuremath{\mathsf{conf}}\), and dgRecv and confinedRecv are \(\ensuremath{\mathsf{dgConsumeInput}}\) and \(\ensuremath{\mathsf{confinedConsumeInput}}\) events.

Every event has a level, and an observer at a label sees the events whose level flows to that label. For an output the level is the channel, for a mailbox read the presence of the message or the lower bound of the interval that was read, and for a blocking-label downgrade its target.

Several events carry an authority, the one under which the step was performed, and the security condition names it in its bound on the event. The authority of an event (Event.authOf, Troupe/Meta/SecurityTheorem.lean) is \(a\) for the four downgrade events and for \(\ensuremath{\mathsf{dgConsumeInput}}\), is the authority join \(a \mathbin{\curlyvee} a_{\mathrm{in}}\) (Definition 2) for \(\ensuremath{\mathsf{regionClose}}\), and is the null authority \(\ensuremath{\mathsf{trustnull}}\) for the remaining six forms. We return to concrete traces, their levels and their authorities when the machine is in place (§4.4).

3.5 Input supplies

A program receives its input as messages. A message (Message) pairs a label, its presence, with a labelled value, its payload: \[m = \langle \mathsf{presence}(m),\ \mathsf{payload}(m)\rangle, \qquad \mathsf{presence}(m)\in\mathcal{L},\quad \mathsf{payload}(m)\ \text{a labelled value.}\] The presence is the label of the fact that the message is there at all; the receive instructions select messages by it (§4.3), and an observer who sees the presence sees that the message exists. The payload has labels of its own, which decide whether the observer sees its content.

The input supply \(\mathcal{I}\) of a run (Inputs) and a mailbox \(\mathcal{M}\) (Mailbox) are both lists of messages, and the mailbox of an input supply is that list (Mailbox.ofInputs). The supply is what a run starts from, and the consistent inputs of §6 are sets of supplies; the mailbox is the component of the machine state that the receive instructions read and shorten. The per-presence projection (Inputs.atPresence) collects the payloads present at exactly \(p\), in order: \[\mathcal{M}{\restriction}p \;\triangleq\; \mathsf{map}\ \mathsf{payload}(\cdot)\ \big(\mathsf{filter}\ (\lambda m.\ \mathsf{presence}(m)=p)\ \mathcal{M}\big).\]

The security condition assumes that the supply of a run is well-formed in the following sense, and its sets of consistent inputs contain well-formed supplies only (Definitions 18 and 15). The Lean names the notion Inputs.Wf; we say well-formed supply.

The third condition concerns region capabilities, which may not arrive from outside; Definition 10 of §4.5 defines the predicate \(\ensuremath{\mathsf{capFree}}\). For example, the one-message supply \([\langle A,\ {42}^{\,\bot}_{\,\bot}\rangle]\) is well-formed: the send label \(\bot\) of the payload flows to the presence \(A\), the payload is a well-formed value, and it contains no capability. This is the supply that the secret branch of §3 runs on; note that the payload itself is public and that the label \(A\) sits on the message. The one-message supply \([\langle \bot,\ v\rangle]\), where \(v\) is the closure of the send-label example above, is not well-formed, because \(\ensuremath{\mathsf{sendLabel}}(v)=A\) does not flow to \(\bot\). Every sublist of a well-formed supply is well-formed (Inputs.Wf.sublist), and a well-formed supply is capability-free (Inputs.Wf.capFree).

Formalized: examples/labelled_value_operations.lean • run: scripts/run-example.sh labelled_value_operations

The next section defines the machine that runs a program on a supply.

4 The monitored machine

We now present the machine that runs a program on an input supply. It is an abstract machine with a mailbox, and its state carries two labels of the monitor, the label \(\mathit{pc}\) and the blocking label \(\mathit{bl}\). The label \(\mathit{pc}\) is the usual program-counter label: constants are created at it, results are labelled by it, a branch on a secret raises it, and a return restores it. The blocking label \(\mathit{bl}\) is, intuitively, the label of whatever may have influenced whether the run got this far: the rules raise it whenever they raise \(\mathit{pc}\) and, in addition, by the labels of the operands on which an operation may fail or block, and only the instruction \(\ensuremath{\mathsf{blockDowngrade}}\) lowers it. The monitor checks \(\mathit{bl}\), not \(\mathit{pc}\), when the program outputs, and it labels the result of a finished run by \(\mathit{bl}\). One step of the machine is one function, \(\ensuremath{\mathsf{stepOutcome}}\), which we present as inference rules.

4.1 Configurations

A configuration is a running state, a halted result, or the stuck configuration: \[c ::= \langle s \rangle \mid \ensuremath{\mathsf{done}}\;v \mid \ensuremath{\mathsf{stuck}}.\] A running state has two components (State, with fields monitor and regions): \[s = (\,\underbrace{\mathit{mon}}_{\text{\texttt{MonitorState}}},\ \underbrace{{\color{var(--acct)}\mathcal{R}}}_{\text{\texttt{List RegionFrame}}}\,).\] The second component, the stack \({\color{var(--acct)}\mathcal{R}}\) of region frames, belongs to the receive regions of §4.5 and is empty in the initial configuration. We write a field of \(\mathit{mon}\) bare, \(\mathit{pc}\) for \(\mathit{mon}.\mathit{pc}\), and set the stack \({\color{var(--acct)}\mathcal{R}}\) in gray, so that a record update \(\{\,s\ \ensuremath{\mathsf{with}}\ \dots\,\}\) may name fields of either component.

The first ten fields of \(\mathit{mon}\) are those of an abstract machine with a mailbox, plus the two labels of the monitor: \[\mathit{mon} \supseteq (\,\underbrace{C}_{\text{ctrl}},\ \underbrace{E}_{\text{env}},\ \underbrace{W}_{\text{cenv}},\ \underbrace{\mathit{self}}_{\text{self}},\ \underbrace{\Phi}_{\text{funs}},\ \underbrace{K}_{\text{kont}},\ \mathit{pc},\ \mathit{bl},\ \underbrace{\mathcal{M}}_{\text{mailbox}},\ \underbrace{\nu}_{\text{nextId}}\,).\] The control \(C\) is the current body, the environment \(E\) is a list of pairs of a local id and its value, the captured environment \(W\) is a list of values, \(\mathit{self}\) is an optional value (the closure being run), and \(\Phi\) is the function table. The mailbox \(\mathcal{M}\) is the list of messages that the receive instructions read (§4.3). The continuation \(K\) is a stack of frames (Frame) \[(E_s,W_s,\mathit{self}_s,\mathit{pc}_s,\mathit{ch}_s,\mathit{br},n,B),\] with fields savedEnv, savedCenv, savedSelf, savedPc, savedCapHead, branched, resultVar, and cont. Rule stackExpand pushes a frame, and rule ret-frame pops it and continues with the body \(B\) after binding the result to \(n\) (Fig. 3). The fields \(\mathit{ch}_s\) and \(\mathit{br}\) belong to §4.5.

The counter \(\nu:\mathcal{L}\to\mathbb{N}\) supplies identities for closures and capabilities. An allocation identity (AllocId) is a pair \((\ell,k)\) of a level and a number; the rules mkClosures and open take the identity \((\mathit{pc},\nu(\mathit{pc}))\) and increment the counter at the level \(\mathit{pc}\). The remaining three fields of \(\mathit{mon}\), the region registers, the chain head and the root balance, also belong to §4.5.

4.2 Evaluation

Atom evaluation \(\mathcal{A}\llbracket t \rrbracket\) (evalAtom) yields an optional value. Expression evaluation \(\mathcal{E}\llbracket e \rrbracket=(v,\beta)\) (evalExpr) yields an optional value together with a label \(\beta\), the blocking-label raise (EvalResult, fields val and blRaise): the label of whatever could have made the evaluation fail. Both are taken against the \((E,W,\mathit{self},\mathit{pc})\) of \(s\): \[\begin{array}{r@{\;}c@{\;}l@{\qquad\qquad}r@{\;}c@{\;}l} \mathcal{A}\llbracket \ensuremath{\mathsf{loc}}\,n \rrbracket &=& E(n) & \mathcal{A}\llbracket b \rrbracket &=& \ensuremath{\mathsf{atPc}}_{\mathit{pc}}\,(\ensuremath{\mathsf{pub}}\,b)\\ \mathcal{A}\llbracket \ensuremath{\mathsf{env}}\,i \rrbracket &=& W[i] & \mathcal{A}\llbracket \ensuremath{\mathsf{pc}} \rrbracket &=& {\ensuremath{\mathsf{lev}}\,\mathit{pc}}^{\,\mathit{pc}}_{\,\bot}\\ \mathcal{A}\llbracket \ensuremath{\mathsf{self}} \rrbracket &=& \mathit{self}& \mathcal{A}\llbracket \ensuremath{\mathsf{root}} \rrbracket &=& \ensuremath{\mathsf{atPc}}_{\mathit{pc}}\,(\ensuremath{\mathsf{pub}}\,{!}\langle \top \,;\, \top \rangle) \end{array}\]

\[\begin{array}{r@{\;}c@{\;}l} \mathcal{E}\llbracket t \rrbracket &=& (\,\mathcal{A}\llbracket t \rrbracket,\ \bot\,)\\ \mathcal{E}\llbracket t_1 \mathbin{\oplus} t_2 \rrbracket &=& (\,\ensuremath{\mathsf{atPc}}_{\mathit{pc}}\,\oplus(v_1,v_2),\ \beta_{\oplus}\,)\\ \mathcal{E}\llbracket \odot\,t_1 \rrbracket &=& (\,\ensuremath{\mathsf{raiseData}}_{\mathit{pc}}\,(\odot\,v_1),\ \bot\,)\\ \mathcal{E}\llbracket \ensuremath{\mathsf{attenuate}}(t_1,t_2) \rrbracket &=& (\,\ensuremath{\mathsf{atPc}}_{\mathit{pc}}\,{{!}\ensuremath{\mathsf{attenuate}}(a,\ell)}^{\,\mathsf{lev}(v_1)\sqcup\mathsf{lev}(v_2)}_{\,\bot},\ \mathsf{tlev}(v_1)\sqcup\mathsf{tlev}(v_2)\,)\\ \mathcal{E}\llbracket \ensuremath{\mathsf{tuple}}(\overline{t}) \rrbracket &=& (\,\ensuremath{\mathsf{atPc}}_{\mathit{pc}}\,{\ensuremath{\mathsf{tuple}}\,\overline{v}}^{\,\bot}_{\,\bot},\ \bot\,)\\ \mathcal{E}\llbracket \ensuremath{\mathsf{list}}(\overline{t}) \rrbracket &=& (\,\ensuremath{\mathsf{atPc}}_{\mathit{pc}}\,{\ensuremath{\mathsf{list}}\,\overline{v}}^{\,\bot}_{\,\bot},\ \bot\,)\\ \mathcal{E}\llbracket \ensuremath{\mathsf{proj}}(i,t_1) \rrbracket &=& (\,\ensuremath{\mathsf{atPc}}_{\sigma}\,\overline{w}[i],\ \sigma\,) \qquad \text{where}\ \mathsf{val}(v_1)=\ensuremath{\mathsf{tuple}}\,\overline{w}\\ \mathcal{E}\llbracket \ensuremath{\mathsf{head}}\,t_1 \rrbracket &=& (\,\ensuremath{\mathsf{atPc}}_{\sigma}\,w,\ \sigma\,) \qquad \text{where}\ \mathsf{val}(v_1)=\ensuremath{\mathsf{list}}\,(w::\overline{w})\\ \mathcal{E}\llbracket \ensuremath{\mathsf{tail}}\,t_1 \rrbracket &=& (\,\ensuremath{\mathsf{raiseData}}_{\sigma}\,{\ensuremath{\mathsf{list}}\,\overline{w}}^{\,\bot}_{\,\bot},\ \sigma\,) \qquad \text{where}\ \mathsf{val}(v_1)=\ensuremath{\mathsf{list}}\,(w::\overline{w}) \end{array}\] Here \(v_i=\mathcal{A}\llbracket t_i \rrbracket\), \(\overline{v}=\overline{\mathcal{A}\llbracket t \rrbracket}\), \(\sigma=\mathsf{lev}(v_1)\), the expression \(\ensuremath{\mathsf{attenuate}}\) requires \(\mathsf{val}(v_1)={!}a\) and \(\mathsf{val}(v_2)=\ell\), and the blocking-label raise of a binary operator is \[\beta_{\oplus} = \begin{cases} \bot & \oplus= {=}\\ \mathsf{tlev}(v_1)\sqcup\mathsf{tlev}(v_2)\sqcup\mathsf{lev}(v_2) & \oplus= {/}\\ \mathsf{tlev}(v_1)\sqcup\mathsf{tlev}(v_2) & \text{otherwise.} \end{cases}\] The raise of a binary operator is the join of the type labels of the operands, since a type error is what can make it fail; division adds the data label of the divisor, since division by zero can fail too; and equality is total and raises nothing. A projection, head or tail raises \(\mathit{bl}\) by the data label of the aggregate, because the shape of the aggregate decides whether the operation succeeds. The value is absent when an operand atom has no value, when the operands of \(\ensuremath{\mathsf{attenuate}}\) are not an authority and a level, when the binary operator is undefined on its operands, when the projection index is out of bounds, and when the operand of \(\ensuremath{\mathsf{proj}}\), \(\ensuremath{\mathsf{head}}\), or \(\ensuremath{\mathsf{tail}}\) does not have the shape shown. In the last four cases the function still returns the displayed raise; when an operand atom has no value, the raise is \(\bot\). Rule assign is the one rule that applies \(\mathcal{E}\llbracket \cdot \rrbracket\): it requires the value and joins \(\beta\) into \(\mathit{bl}\) (Fig. 1).

4.3 The mailbox

The mailbox \(\mathcal{M}\) of a state is a list of messages (§3.5; the definitions of this subsection are those of Troupe/Trace.lean), and in the initial configuration it is the input supply of the run. The rules read it through partial operators, one for the instruction \(\ensuremath{\mathsf{tyrecv}}\), one for \(\ensuremath{\mathsf{peek}}\), and one for \(\ensuremath{\mathsf{consume}}\) and \(\ensuremath{\mathsf{rangedConsume}}\). The value \(\ensuremath{\mathsf{none}}\) marks an undefined result, on which the step is \(\ensuremath{\mathsf{stuck}}\).

The operator Mailbox.consumeFirst removes the first message that satisfies a predicate \(\varphi\): \[\begin{array}{r@{\;}c@{\;}l@{\qquad}l} \mathsf{consumeFirst}_{\varphi}(\varepsilon) &=& \ensuremath{\mathsf{none}}&\\ \mathsf{consumeFirst}_{\varphi}(m\cdot\mathcal{M}) &=& (\mathsf{payload}(m),\ \mathcal{M}) & \text{if}\ \varphi(m)\\ &=& (v,\ m\cdot\mathcal{M}') & \text{otherwise, where}\ (v,\mathcal{M}')=\mathsf{consumeFirst}_{\varphi}(\mathcal{M})\\ & & & \text{($\ensuremath{\mathsf{none}}$ if that is $\ensuremath{\mathsf{none}}$).} \end{array}\] Rule tyrecv instantiates \(\varphi(m)=(\mathsf{presence}(m)=p)\wedge{}\)\((\mathsf{type}(\mathsf{payload}(m))=\tau)\) and writes the operator \(\mathsf{consumeFirst}_{p,\tau}\).

The other two instructions read by position among the messages of an interval of presences. A message \(m\) is in the interval \([\ell_{\mathrm{lo}},\ell_{\mathrm{hi}}]\) when \(\ell_{\mathrm{lo}} \sqsubseteq\mathsf{presence}(m) \sqsubseteq\ell_{\mathrm{hi}}\) (Mailbox.inInterval). The operator Mailbox.atIntervalInt returns the \(i\)-th (\(0\)-based) in-interval message, in mailbox order, for an integer index \(i\): \[\mathsf{atInterval}_{[\ell_{\mathrm{lo}},\ell_{\mathrm{hi}}]}(\mathcal{M})[\,i\,] \;\triangleq\; \big(\mathsf{filter}\ (\lambda m.\ \ell_{\mathrm{lo}} \sqsubseteq\mathsf{presence}(m) \sqsubseteq\ell_{\mathrm{hi}})\ \mathcal{M}\big)[\,i\,] \quad (i\ge 0), \qquad \ensuremath{\mathsf{none}}\ \text{for}\ i<0 .\] The operator Mailbox.consumeAtIntervalIntD removes that message and returns it together with a natural number \(k\) and the residual mailbox. For \(i\ge 0\) it is \(\mathsf{consume}_{[\ell_{\mathrm{lo}},\ell_{\mathrm{hi}}]}(\mathcal{M})[\,i\,]\triangleq{}\)\(\mathsf{cD}_{i}(\mathcal{M})\) (Mailbox.consumeAtIntervalD), and it is \(\ensuremath{\mathsf{none}}\) for \(i<0\): \[\begin{array}{r@{\;}c@{\;}l@{\qquad}l} \mathsf{cD}_{i}(\varepsilon) &=& \ensuremath{\mathsf{none}}&\\ \mathsf{cD}_{i}(m\cdot\mathcal{M}) &=& (m,\ 0,\ \mathcal{M}) & \text{if}\ \ell_{\mathrm{lo}} \sqsubseteq\mathsf{presence}(m) \sqsubseteq\ell_{\mathrm{hi}},\ i=0\\ &=& \mathsf{cD}_{j}(\mathcal{M})\oplus m & \text{if}\ \ell_{\mathrm{lo}} \sqsubseteq\mathsf{presence}(m) \sqsubseteq\ell_{\mathrm{hi}},\ i=j{+}1\\ &=& \mathsf{cD}_{i}(\mathcal{M})\oplus m & \text{otherwise,} \end{array}\] where \((m_\star,k,\mathcal{M}')\oplus m = (m_\star,\ k{+}1,\ m\cdot\mathcal{M}')\) when \(\mathsf{presence}(m)=\mathsf{presence}(m_\star)\), \((m_\star,k,\mathcal{M}')\oplus m = (m_\star,\ k,\ m\cdot\mathcal{M}')\) otherwise, and \(\ensuremath{\mathsf{none}}\oplus m=\ensuremath{\mathsf{none}}\). The number \(k\) counts the messages of the same presence as \(m_\star\) that precede it. The pair \((\mathsf{presence}(m_\star),k)\) is the removal descriptor of the removal and \(k\) its rank; neither mentions the index \(i\) or the bounds of the interval. The events \(\ensuremath{\mathsf{dgConsumeInput}}\), \(\ensuremath{\mathsf{confinedConsumeInput}}\) and \(\ensuremath{\mathsf{regionClose}}\) carry removal descriptors (§3.4).

Let \(\mathsf{consume}_{[\ell_{\mathrm{lo}},\ell_{\mathrm{hi}}]}(\mathcal{M})[\,i\,]=(m_\star,k,\mathcal{M}')\). The removed message is the one that the operator of \(\ensuremath{\mathsf{peek}}\) returns, \(\mathsf{atInterval}_{[\ell_{\mathrm{lo}},\ell_{\mathrm{hi}}]}(\mathcal{M})[\,i\,]=m_\star\) (Mailbox.consumeAtInterval_fst, through Mailbox.consumeAtIntervalIntD_toConsumeAtInterval); it is in the interval (Mailbox.consumeAtIntervalIntD_inInterval) and a member of \(\mathcal{M}\) (Mailbox.consumeAtIntervalIntD_mem); \(\mathcal{M}'\) is a sublist of \(\mathcal{M}\) (Mailbox.consumeAtIntervalIntD_sublist); and \(\mathcal{M}'\) is \(\mathcal{M}\) without the message of presence \(\mathsf{presence}(m_\star)\) that has \(k\) messages of that presence ahead of it (Mailbox.consumeAtIntervalIntD_removeAtPresenceRank; the removal function is Inputs.removeAtPresenceRank). By the last fact the descriptor determines the residual at its presence: the messages of \(\mathcal{M}'\) at the presence \(\mathsf{presence}(m_\star)\) are those of \(\mathcal{M}\) with the \(k\)-th removed.

4.4 The step relation

The judgment \(c \xrightarrow{\,\alpha\,} c'\) denotes a step that emits the event \(\alpha\), or no event when \(\alpha=\epsilon\). In the Lean one step is a single function, \(\ensuremath{\mathsf{stepOutcome}}\), from configurations to outcomes (Outcome), and \(\ensuremath{\mathsf{step}}\) is its image under \(\ensuremath{\mathsf{toResult}}\), which returns the successor configuration paired with the optional event (StepResult): \[\ensuremath{\mathsf{stepOutcome}}(c) ::= \ensuremath{\mathsf{running}}\,(s',\alpha) \mid \ensuremath{\mathsf{done}}\,v\mid \ensuremath{\mathsf{stuck}}, \qquad \ensuremath{\mathsf{step}}(c) = \ensuremath{\mathsf{toResult}}(\ensuremath{\mathsf{stepOutcome}}(c)).\] The outcomes \(\ensuremath{\mathsf{done}}\,v\) and \(\ensuremath{\mathsf{stuck}}\) carry no event. We present \(\ensuremath{\mathsf{stepOutcome}}\) on a running state through two auxiliary judgments. When the control holds at least one instruction, the head instruction fires against the state and the block advances (rule instr), by the judgment \(s \vdash \iota \xrightarrow{\,\alpha\,} s'\) (Figs. 1, 2, and 4). When it holds none, the terminator produces the next configuration (rule term), by the judgment \(s \vdash \mathit{tm} \xrightarrow{\,\alpha\,} c'\) (Fig. 3). In the Lean every rule is an arm of the one \(\ensuremath{\mathsf{stepOutcome}}\) match. The rules read their fields against \(s\); a result \(\{\,s\ \ensuremath{\mathsf{with}}\ \dots\,\}\) shows the updated fields, and the other fields are unchanged. A running configuration to which no rule applies steps to \(\ensuremath{\mathsf{stuck}}\) with no event, and \(\ensuremath{\mathsf{stepOutcome}}\) maps each of \(\ensuremath{\mathsf{done}}\;v\) and \(\ensuremath{\mathsf{stuck}}\) to itself.

The rules set the contribution of the monitor in blue, in two kinds. A blocking check is a premise on labels or on an authority that can refuse the step; it is additionally \({\color{var(--mon)}\boxed{\text{boxed}}}\). Label tracking is every write to \(\mathit{pc}\), \(\mathit{bl}\), the region registers, the chain head, or a branch flag, together with the premises that compute the written value; it is unboxed. The stack \(\mathcal{R}\) and every premise or update that only reads or writes it are gray. The boxed premises are exactly the conditions that the step function stepWith nonBlocking (Troupe/Machine/Enforcement.lean) omits; that function keeps the label tracking, the gray updates, and the black premises. We call the machine that steps by it the non-blocking machine and the machine of the figures the monitored machine (the printed output of some examples says deployed monitor). The two agree until the monitor refuses a step: at every configuration the non-blocking step equals the monitored step, or the monitored step is \(\ensuremath{\mathsf{stuck}}\) with no event (stepWith_nonBlocking_eq_or_blocking_stuck), and the trace of the monitored run is a prefix of the trace of the non-blocking run at the same fuel (blocking_trace_prefix). We use the non-blocking machine in §6 to show programs that the security condition rejects. Note also that a step never lowers \(\mathit{bl}\) unless it emits a \(\ensuremath{\mathsf{dBl}}\) event (step_bl_le_or_downgradeBl), and never lowers \(\mathit{pc}\) unless the control is a \(\ensuremath{\mathsf{ret}}\) terminator (step_pc_le_or_ret).

Some parts of Figs. 1 and 3 concern receive regions and should be read after §4.5: the premise \({\color{var(--mon)}\boxed{\mathit{ch}=\ensuremath{\mathsf{none}}}}\) of the rules tyrecv and consume, the terms \(\mathit{\Delta}\sqcup\mathit{\Delta}_{\mathrm{lab}}\) of rule peek, and the boxed premises of the two return rules with the frame fields \(\mathit{ch}_s\) and \(\mathit{br}\) and the update \(\mathsf{flag}\). In a state with no open region these are inert: the premise holds and the two terms are \(\bot\) (State.ChainWF.folds_bot, under the chain invariant of §4.5).

Label tracking and the \(\mathsf{outputToEndpoint}\) check.

We illustrate the rules on the two programs that recur throughout the report. The first is the secret branch of §3.

secret <- tyrecv {alice} int      -- 42, or -1 in the second run
c      <- 0 < secret
r      <- if c then ret 100 else ret 200
ret r

The second program tries to output inside the branch.

secret <- tyrecv {alice} int
c      <- 0 < secret
if c then { outputToEndpoint bot 1; ret 0 } else ret 0

Mailbox reads.

The rules tyrecv, peek, and consume (Fig. 1) read the mailbox through the operators of §4.3. They write \(i_d\) for the data label of the index operand, \(\ell_d^{\mathrm{lo}}\) and \(\ell_d^{\mathrm{hi}}\) for the data labels of the two bound operands, and \(a_d\) for the data label of the authority operand. A plain receive takes a message at one presence \(p\), and its event is at the level \(p\). An interval read is more delicate: the message it selects depends on the index and on every message whose presence lies in \([\ell_{\mathrm{lo}},\ell_{\mathrm{hi}}]\), so what it reveals is at the level \(\ell_{\mathrm{hi}}\sqcup i_d\), while the event is emitted at the lower bound \(\ell_{\mathrm{lo}}\). Rule consume therefore requires, in the first boxed premise, that the context of the read flows to \(\ell_{\mathrm{lo}}\) (we call it the occurrence premise), and in the second that the authority \(a\) permits the flow from \(\ell_{\mathrm{hi}}\sqcup i_d\) to \(\ell_{\mathrm{lo}}\) (the selection premise, the privileged flow \(\ell_{\mathrm{hi}}\sqcup i_d\sqsubseteq_{a}\ell_{\mathrm{lo}}\) by Label.privFlowsTo_iff_okToDowngrade). When \(\ell_{\mathrm{hi}}\sqcup i_d\) flows to \(\ell_{\mathrm{lo}}\) without the authority, the consume is a plain read and emits \(\ensuremath{\mathsf{consumeInput}}\); otherwise it is a downgrade under \(a\), and its event \(\ensuremath{\mathsf{dgConsumeInput}}\) carries the removal descriptor (step_consume_running_iff). We call the latter a disclosing consume. The bound value is read through \(\ensuremath{\mathsf{readTainted}}\), so both its labels are \(q\sqcup\mathsf{lev}(v)\) for the taint \(q\) of the rule (LVal.readTainted_dataLabel, LVal.readTainted_typeLabel); the level of the \(\ensuremath{\mathsf{assign}}\) event of rule peek is the data label of the bound value (Event.lev_assign).

For example, over the mailbox [10@\(\bot\), 7@{alice}, 20@\(\bot\)] consider the two one-instruction programs, each run under the root authority:

v <- consume 0 bot bot     root    -- point: index 0 in [bot, bot]
v <- consume 2 bot {alice} root    -- interval: index 2 in [bot, {alice}]

In the first, the interval \([\bot,\bot]\) holds the two messages of presence \(\bot\), the message at index \(0\) is 10, and \(\ell_{\mathrm{hi}}\sqcup i_d=\bot\) flows to \(\ell_{\mathrm{lo}}=\bot\): the trace is [recv {} \(\triangleright\) 10@{}%{}], and the result 10@{}%{}. In the second, the interval \([\bot,\texttt{\{alice\}}]\) holds all three messages, and the message at index \(2\) is 20. One message of its presence \(\bot\) precedes it, so the rank is \(k=1\), which differs from the index. The join \(\ell_{\mathrm{hi}}\sqcup i_d=\texttt{\{alice\}}\) does not flow to \(\ell_{\mathrm{lo}}=\bot\), so the trace is [dgRecv !{alice, bob, charlie} @ {} \(\triangleright\) \(\langle\){}, 1\(\rangle\)], a \(\ensuremath{\mathsf{dgConsumeInput}}\) event with the descriptor \((\bot,1)\), and the result is 20@{alice}%{alice}.

Formalized: examples/consume_by_index_rank.lean • run: scripts/run-example.sh consume_by_index_rank

Downgrades.

The value and type downgrades are one rule, downgrade, parametric in the granularity \(g\) (Fig. 2). The note under the figure defines the occurrence level \(\ell_{\flat}\), the join of \(\mathit{pc}\) with the data labels of the authority and the target operands, and the effective target \(\ell_\star\), which is the requested target raised to the occurrence level: a downgrade never lowers a label below the context that performs it. At the granularity \(\ensuremath{\mathsf{value}}\) the check is on the data label of the value and the rule also lowers the type label, to \((\mathsf{tlev}(v)\sqcap\ell)\sqcup\ell_{\flat}\); the check on the data label covers this, since the type label of a well-formed value flows to its data label: for every label \(q\sqsubseteq\mathsf{lev}(v)\) and every label \(x\), the check \(\ensuremath{\mathsf{okDown}}_{d}(\mathsf{lev}(v),\ell,a)\) and the privileged flow \(q \sqcap \ell\sqsubseteq_{a}x\) give \(q\sqsubseteq_{a}x\) (okToDowngrade.typeLabel_visible, Unwinding/PrivLowEquiv), so that an observer who holds \(a\) sees the lowered type label only where the original one was visible. The event \(\ensuremath{\mathsf{dValType}}\) carries both the released value and the new type label, and its level is the occurrence level. The rule raises \(\mathit{bl}\) by the from-label and by the data labels of the two label operands, so that whether the check passed cannot be observed below those labels. Rule blockDowngrade is the one rule that lowers \(\mathit{bl}\); it sets \(\mathit{bl}\) to the target \(\ell\), provided the authority permits the flow from the current \(\mathit{bl}\) (joined with the operand labels) to \(\ell\), and \(\mathit{pc}\) and the operand labels flow to \(\ell\). Its event \(\ensuremath{\mathsf{dBl}}\) is at the level \(\ell\). A step that emits an event \(\alpha\) from a state with \(\mathit{pc}\sqsubseteq\mathit{bl}\) has \(\mathit{pc}\sqsubseteq\mathsf{lev}(\alpha)\) (step_event_pc_le), so events are only emitted at or above the context.

Consider first a declassification of a constant under an authority that was chosen by a secret:

secret <- tyrecv {alice} int
c      <- 0 < secret
a      <- if c then ret root else ret root   -- a_d = {alice}
pub    <- declassify 5 a bot
outputToEndpoint bot pub

Rule ret-frame binds a with the data label {alice} of the \(\mathit{pc}\) of the arm, so \(a_d=\texttt{\{alice\}}\). Rule downgrade joins \(a_d\) into the occurrence level and into \(\mathit{bl}\): the constant 5 is bound at the effective target \(\ell_\star=\bot\sqcup\ell_{\flat}=\texttt{\{alice\}}\), and \(\mathit{bl}\) contains {alice} at the output. The runs on the secrets 42 and -1 both have no result, the output being refused, and their \(\bot\)-observable output traces agree over the pool of integer secrets of the example file.

Formalized: examples/declassify_secret_authority.lean • run: scripts/run-example.sh declassify_secret_authority

The next two examples declassify the secret itself. They differ in what the program does afterwards, and together they show what the blocking label does: a declassification releases the value, and only \(\ensuremath{\mathsf{blockDowngrade}}\) releases the fact that the run got past it.

let secret ← tyrecv {alice} .int
let pub ← declassify secret root ⊥
let _ ← blockdeclto root ⊥      -- first variant only
ret pub

result, first variant:   42@{}%{}
result, second variant:  42@{alice}%{alice}
trace, second variant:   [recv {alice} ▷ 42@{}%{},
    downgradeValType[conf] !{alice, bob, charlie} → {} @ {} ⇒ 42@{}%{} ; int@{}]

let secret ← tyrecv {alice} .int
let pub ← declassify secret root ⊥
let _ ← blockdeclto root ⊥      -- second variant only
let _ ← outputToEndpoint ⊥ pub

first variant:   result none (secret 42);
                 the ⊥-observations agree over the secrets -1, 0, 1
second variant:  I/O trace, secret 42:
                 [recv {alice} ▷ 42@{}%{}, send {} ◁ 42@{}%{}]
                 the ⊥-observations of the secrets 42 and -1 differ

4.5 Receive regions

A plain receive takes a message at one presence, and a \(\ensuremath{\mathsf{consume}}\) over an interval of presences needs an authority for the flow from the upper bound to the lower bound at every read. A receive region lets a program make many reads over an interval under one authority, presented once. The instruction \(\ensuremath{\mathsf{enableRangedReceive}}\) opens the region over an interval \([\ell_{\mathrm{lo}},\ell_{\mathrm{hi}}]\) of presences under an authority and binds a capability; inside the region the instruction \(\ensuremath{\mathsf{rangedConsume}}\), the confined consume, removes messages with no authority operand; and \(\ensuremath{\mathsf{disableRangedReceive}}\) closes the region with the capability. The bounds \(\ell_{\mathrm{lo}}\) and \(\ell_{\mathrm{hi}}\) are the lower bound and the upper bound of the region. The monitor treats the region as a single downgrade whose disclosure happens at the close. While the region is open, every read is tainted by the upper bound, so that nothing read inside can be observed below it, and the event of a confined consume is at that tainted level. The close emits one event, at the lower bound, that carries the removal descriptors of all the removals made inside, together with the authority of the open. The authority is checked at the open, where it decides whether the region can be closed at all; it is not checked again at each read.

Consider a region with lower bound \(\bot\) and upper bound {alice} opened under the root authority, in which the program consumes the {alice} message and then closes:

lo  <- bot
hi  <- {alice}
e   <- enableRangedReceive lo hi root      -- ok = true
cap <- proj 1 e
v   <- rangedConsume 0 hi hi
_   <- disableRangedReceive cap
ret v

The open binds a pair e of an integer, the certification bit, and a capability, which the close takes. On the supply \([\langle \texttt{\{alice\}},\ 42\rangle]\) the trace has six events; omitting the three \(\ensuremath{\mathsf{assign}}\) events that bind lo, hi, and cap, they are

regionOpen @ {} [{}..{alice}] \(\Rightarrow\) tuple[2]@{}%{}
confinedRecv @ {alice} \(\triangleright\) \(\langle\){alice}, 0\(\rangle\)
regionClose !{alice, bob, charlie}\(\oplus\)<{};{}> \(\to\) {} @ {} \(\triangleright\) [\(\langle\){alice}, 0\(\rangle\)]

The \(\ensuremath{\mathsf{regionOpen}}\) event has level \(\bot\). The \(\ensuremath{\mathsf{confinedConsumeInput}}\) event has level {alice} and carries the removal descriptor \((\texttt{\{alice\}},0)\). The \(\ensuremath{\mathsf{regionClose}}\) event has level \(\bot\); its descriptor list holds the same descriptor, and its two authority fields print as !{alice, bob, charlie}\(\oplus\)<{};{}>, the root authority of the open beside the null authority. The result is 42@{alice}%{alice}. We call this program the certified region.

Formalized: examples/ranged_receive_lifecycle.lean • run: scripts/run-example.sh ranged_receive_lifecycle

The capability.

The value that an open binds contains a region capability, the last form of base value in the grammar of §3: \[\ensuremath{\mathsf{cap}}(\ell_{\mathrm{lo}},\ell_{\mathrm{hi}},\mathit{ok},\mathit{pc}_{\mathrm e},\ell_a,s_\Delta,s_\Phi,s_{\Delta\mathrm{lab}},s_{\Phi\mathrm{lab}},\mathit{prev},\mathit{uid}) .\] It records the bounds, the certification bit \(\mathit{ok}\), the \(\mathit{pc}\) and the authority level \(\ell_a\) of the open, the four register values \(s_\Delta\), \(s_\Phi\), \(s_{\Delta\mathrm{lab}}\), \(s_{\Phi\mathrm{lab}}\) to restore at the close, the identity \(\mathit{prev}\) of the enclosing region (optional) and its own identity \(\mathit{uid}\). The Lean names of the eleven fields are, in order, lo, hi, ok, pcEnable, aLev, s\(\Delta\), s\(\Phi\), s\(\Delta\)lab, s\(\Phi\)lab, sPrev and uid. Rule open fills them and rule close reads them. A capability has no children. The third condition of Definition 9 requires the payloads of a supply to contain no capability, through the following predicate, and the hypothesis of the soundness theorem requires the same of the constants of a program (§7).

The predicate \(\ensuremath{\mathsf{capsSat}}_Q\) is monotone in \(Q\) (LVal.capsSat_mono), so a capability-free value satisfies \(\ensuremath{\mathsf{capsSat}}_Q\) for every \(Q\) (LVal.capFree.capsSat); the quantified form of the third clause is BaseVal.envCapsSat_iff.

Registers and frames.

The last three fields of \(\mathit{mon}\) concern the open regions: \[\mathit{mon} \supseteq (\,\underbrace{\mathit{regs}=(\mathit{\Delta},\ \mathit{\Delta}_{\mathrm{lab}},\ \mathit{\Phi},\ \mathit{\Phi}_{\mathrm{lab}})}_{\text{regs}},\ \underbrace{\mathit{ch}}_{\text{capHead}},\ \underbrace{(\mathit{ch}_0,\ \mathit{br}_0)}_{\text{root}}\,),\] The region registers \(\mathit{regs}\) (RegionRegisters) have the fields clearance \(\mathit{\Delta}\), clearanceLabel \(\mathit{\Delta}_{\mathrm{lab}}\), evidenceLevel \(\mathit{\Phi}\), and evidenceLabel \(\mathit{\Phi}_{\mathrm{lab}}\). The active clearance \(\mathit{\Delta}\) is the join of the upper bounds of the open regions, the taint that every read inside them carries, and the active evidence level \(\mathit{\Phi}\) is the join of their lower bounds; \(\mathit{\Delta}_{\mathrm{lab}}\) and \(\mathit{\Phi}_{\mathrm{lab}}\) accumulate the data labels of the bound operands. (The register letters are italic; the upright \(\Phi\) is the function table.) The chain head \(\mathit{ch}\) is the identity of the innermost open region, an optional allocation identity. The root balance \((\mathit{ch}_0,\mathit{br}_0)\) (RootBalance, fields savedCapHead and branched) holds, for the configurations with \(K=[\,]\), the two fields \(\mathit{ch}_s\) and \(\mathit{br}\) that a frame of the continuation holds.

The second component of the state is the stack of region frames (RegionFrame), innermost first: \[{\color{var(--acct)}\mathcal{R}= [\,F_1,\dots,F_n\,]},\qquad {\color{var(--acct)}F = \langle \mathit{uid},\ell_{\mathrm{lo}},\mathit{regs}_e,\mathcal{M}_e,D,\mathit{acc},T\rangle }.\] The Lean names of the seven fields are uid, evidenceLevel, entryRegisters, entryMailbox, evidence, absorbedAuth, and absorbedClearances. A frame remembers the registers and the mailbox at the open, and collects the removal descriptors made since in its evidence \(D\); the list \(D\) is what the close discloses. The label \(\mathit{acc}\), the absorbed authority, collects the authorities of the regions that were opened and closed inside this one, and \(T\) is a list of pairs of labels that records their bounds. No monitor check reads the stack; the rules write it in gray. The open-time base \(\mathsf{outermostBase}(s)\) is the entry mailbox \(\mathcal{M}_e\) of the last frame of \(\mathcal{R}\), and the current mailbox \(\mathcal{M}\) when \(\mathcal{R}\) is empty (State.outermostBase); the state relation of Definition 21 compares it.

The rules of a region.

Fig. 4 gives the rules open, rangedConsume and close. The open computes the certification bit \(\mathit{ok}\): whether the authority permits the flow from the upper bound to the lower bound, each joined with the clearance already active, which is the privileged flow \(\ell_{\mathrm{hi}}\sqcup\mathit{\Delta}\sqsubseteq_{a}\ell_{\mathrm{lo}}\sqcup\mathit{\Delta}\) (Label.privFlowsTo_iff_okToDowngrade). The open fires whether or not the bit holds; it joins the bounds into the registers, mints the identity \(\mathit{uid}\), makes it the chain head, and pushes a frame. Its event is at the occurrence level \(\mathit{occ}\) of the open, the join of \(\mathit{pc}\) with the data labels of its operands and the register labels. A step of \(\ensuremath{\mathsf{enableRangedReceive}}\) has a running successor exactly when its three operands evaluate to two levels and an authority (step_enableRangedReceive_running_iff).

The confined consume has three boxed premises, which we call, in the order of the figure, the occurrence premise, the evidence premise and the selection premise. The first and the third are those of rule consume with the lower bound raised by the active clearance \(\mathit{\Delta}\) and with no authority: the authority was examined at the open. The evidence premise \(\mathit{\Phi}\sqsubseteq\ell_{\mathrm{lo}}\) keeps the lower bound of every read at or above the lower bounds of the enclosing opens. The bound value is tainted by \(\theta\), which we call the taint of the read, and the event is at that level (Event.lev_confinedConsumeInput); the removal descriptor is appended to the evidence of every open frame.

The close takes the capability, checks that the context flows to the \(\mathit{pc}\) of the open and to the lower bound, and requires \(\mathit{ok}=\ensuremath{\mathsf{tt}}\) and that the capability is the innermost open region, \(\mathit{ch}=\mathit{uid}\) (step_disableRangedReceive_running_iff). These last two premises are black: the non-blocking machine keeps them, since they are what makes the regions well-bracketed rather than a check of the monitor. The close restores the registers from the capability, sets the chain head to the enclosing region, and emits the \(\ensuremath{\mathsf{regionClose}}\) event with the evidence \(D\) of the head frame, the authority \(a\) of the open, and the absorbed authority \(\mathit{acc}_0\) of the frame, which we call the inner authority of the event. The level of the event is \(\ell_{\mathrm{lo}}\sqcup s_{\Delta}\sqcup s_{\Delta\mathrm{lab}}\), the lower bound raised by the clearance that was active when the region was opened (Event.lev_regionClose): the close of an inner region is only observable at the clearance of the regions enclosing it, and the outer close, through \(\mathsf{closeRegion}\), absorbs the inner authority into its own frame and, since \(\mathsf{recordRemoval}\) appends to every frame, carries the inner removals in its evidence.

In the certified region above the bit is \(\mathit{ok}=\ensuremath{\mathsf{tt}}\), since the root authority permits the flow from \(\ell_{\mathrm{hi}}\sqcup\mathit{\Delta}=\texttt{\{alice\}}\) to \(\ell_{\mathrm{lo}}\sqcup\mathit{\Delta}=\bot\). The confined consume is over the interval \([\texttt{\{alice\}},\texttt{\{alice\}}]\), its three premises hold with \(\mathit{\Delta}=\texttt{\{alice\}}\) and \(\mathit{\Phi}=\bot\), and its taint is \(\theta=\texttt{\{alice\}}\), the level of its event. The level of the close event is \(\ell_{\mathrm{lo}}\sqcup s_{\Delta}\sqcup s_{\Delta\mathrm{lab}}=\bot\), from the registers that the capability stored at the open. Now attenuate the authority of the open to the null authority:

lo  <- bot
hi  <- {alice}
na  <- atten root <bot;bot>
e   <- enableRangedReceive lo hi na        -- ok = false
cap <- proj 1 e
v   <- rangedConsume 0 hi hi
_   <- disableRangedReceive cap
ret v

The null authority does not permit the flow from {alice} to \(\bot\), so the open computes \(\mathit{ok}=\ensuremath{\mathsf{ff}}\). The open fires, and so does the confined consume, whose premises do not mention \(\mathit{ok}\). The trace (at fuel \(80\)) ends with the \(\ensuremath{\mathsf{regionOpen}}\), the \(\ensuremath{\mathsf{assign}}\) that binds the capability, printed uncertified as cap#{}/0[{}..{alice}]\(\times\), and the \(\ensuremath{\mathsf{confinedConsumeInput}}\) at the level {alice}. The premise \(\mathit{ok}=\ensuremath{\mathsf{tt}}\) of rule close fails, so the trace contains no \(\ensuremath{\mathsf{regionClose}}\) and the run has no result: a region opened without sufficient authority can be used but never closed, and nothing read inside it is ever disclosed.

Formalized: examples/ranged_uncertified_unclosable.lean • run: scripts/run-example.sh ranged_uncertified_unclosable

The chain invariant.

The registers, the chain head and the stack \(\mathcal{R}\) describe the same open regions, and the predicate State.ChainWF, the chain invariant, ties them together. It holds at the initial configuration of a program whose constants contain no capability on a capability-free supply (init_ChainWF), and runs preserve it (run_preserves_ChainWF); it is one of the single-run invariants of the proof (Definition 28). In a state that satisfies it, the chain head \(\mathit{ch}\) is the \(\mathit{uid}\) of the head frame of \(\mathcal{R}\), and \(\ensuremath{\mathsf{none}}\) when \(\mathcal{R}\) is empty (field head), so that \(\mathit{ch}=\ensuremath{\mathsf{none}}\) gives \(\mathcal{R}=[\,]\) (State.ChainWF.collapse) and \(\mathsf{outermostBase}(s)=\mathcal{M}\) (State.ChainWF.outermostBase_eq); the registers \(\mathit{regs}\) equal the \(\mathit{regs}_e\) of the head frame and are all \(\bot\) when \(\mathcal{R}\) is empty (field registersHead, hence State.ChainWF.folds_bot); the evidence of each frame is a suffix of the evidence of the next enclosing frame (field pendingNested, State.ChainWF.evidence_isSuffix); every frame’s \(\mathit{uid}=(\ell,k)\) satisfies \(k<\nu(\ell)\) (field fresh), and the identities of the frames are pairwise distinct (field nodup). The remaining fields order the frames and are listed in §9.2. The counters \(\nu\) do not decrease across a step (step_nextId_mono), and an identity \((\ell,k)\) with \(k<\nu(\ell)\) that is among the identities of the frames after a step was among them before it (step_uid_no_remint).

The evidence of the frames is determined by the trace. The function Trace.regionEvidence folds a trace over a stack of descriptor lists, starting from the empty stack: a \(\ensuremath{\mathsf{regionOpen}}\) pushes an empty list, a \(\ensuremath{\mathsf{confinedConsumeInput}}(\_,p,k)\) appends \((p,k)\) to every list, a \(\ensuremath{\mathsf{regionClose}}\) drops the head, and every other event leaves the stack unchanged. For every fuel at which the run from the initial configuration is at a running state \(s\), the value of the function on the trace of that run is the list of the evidence of the frames of \(s\) (run_regionEvidence_eq_regions_evidence).

The other mailbox rules inside a region.

The premise \({\color{var(--mon)}\boxed{\mathit{ch}=\ensuremath{\mathsf{none}}}}\) of the rules tyrecv and consume (Fig. 1) fails while a region is open, so every removal inside a region is a confined consume and is recorded in the evidence. Rule peek removes nothing and has no such premise; instead its taint and its raise of \(\mathit{bl}\) contain the two register terms \(\mathit{\Delta}\sqcup\mathit{\Delta}_{\mathrm{lab}}\), so that what a peek reads inside a region is confined like a confined consume. The next example shows why: a peek reads the residual that a confined consume left, and the residual depends on what was removed.

i   <- tyrecv {alice} int              -- 0 or 1
e   <- enableRangedReceive bot {alice} root
cap <- proj 1 e
_   <- rangedConsume i bot {alice}
p   <- peek 0 bot bot
_   <- disableRangedReceive cap
ret p

The development keeps a witness that the register terms in the taint of rule peek are needed: on a read over \([\bot,\bot]\) at \(\mathit{pc}=\bot\) with public operands, inside a region with \(\mathit{\Delta}=\{\ensuremath{\mathsf{alice}}\}\) after a confined consume by a secret index, the peeked contents of two runs differ while the taint without the terms \(\mathit{\Delta}\sqcup\mathit{\Delta}_{\mathrm{lab}}\) flows to the observer level, and the taint with them does not (the file ranged_receive_peek_needs_region_fold_under_covered_occurrence.lean under _working_notes/soundness-witnesses/). The taint of the rule dominates the join \(\mathit{pc}\sqcup i_d\sqcup\ell_d^{\mathrm{lo}}\sqcup\ell_d^{\mathrm{hi}}\sqcup\ell_{\mathrm{hi}}\) (occLabels_le_peekTaintFull, in the witness file ranged_receive_peek_confined_by_bound_label_taint.lean).

The branch-balance checks.

The boxed premises of the rules ret-frame and ret-done (Fig. 3) require the regions opened in a branch to be closed in it: when the frame being popped (or the root balance, when the continuation is empty) has its branch flag \(\mathit{br}\) set, the chain head must equal the field \(\mathit{ch}_s\) saved when the frame was pushed. The notation \(\mathsf{flag}\) of the rules branch and tailCall sets the branch flag of the top frame: the update \(K:=\{\,f\ \ensuremath{\mathsf{with}}\ \mathit{br}:=\ensuremath{\mathsf{tt}}\,\}::K'\) when \(K=f::K'\), and the update \(\mathit{br}_0:=\ensuremath{\mathsf{tt}}\) when \(K=[\,]\). Two programs of Troupe/Examples.lean, checked by #guard, show the check at work. The program bbBranchOneSidedE opens a region in one arm of a branch on a secret and does not close it: its run on the secret that takes this arm has no result, and its run on the other secret completes. The program bbBalancedBranchE opens and closes a region inside an arm of a branch on a secret, and its runs on both secrets return 7@{alice}%{alice}.

4.6 Runs

A run starts from the initial configuration of a program on an input supply. The initial configuration (init, Troupe/Machine/Run.lean) runs the main body with empty environments, no self value, \(K=[\,]\), \(\mathit{pc}=\mathit{bl}=\bot\), the mailbox equal to the input supply, \(\nu=\lambda\_.\,0\), the four region registers at \(\bot\), \(\mathit{ch}=\ensuremath{\mathsf{none}}\), the root balance \((\ensuremath{\mathsf{none}},\ensuremath{\mathsf{ff}})\), and \(\mathcal{R}=[\,]\).

The functions run and exec (Troupe/Machine/Run.lean) iterate \(\ensuremath{\mathsf{step}}\) a given number of times, the fuel: the first returns the configuration reached, and the second records the configurations passed and the events emitted. The trace of a run is its list of events, oldest first (Run.trace). The statements of the later sections quantify over the fuel, so a run means the run to any number of steps. The functions runWith and execWith take the step function as a parameter, and at nonBlocking they are the runs of the non-blocking machine.

The two labels of the monitor keep the relation \(\mathit{pc}\sqsubseteq\mathit{bl}\) throughout a run, so the check of rule outputToEndpoint on \(\mathit{bl}\) alone gives \(\mathit{pc}\sqsubseteq c\) for every output, as step_event_pc_le states for every event.

Likewise, the mailbox of every state of a run from a well-formed supply is a well-formed supply (step_preserves_InputsWf), and the values of every configuration reached from a well-formed program on a well-formed supply are well-formed (Inputs.Wf.toInputsWF, init_WF, step_preserves_WF).

4.7 The formal model and the Troupe implementation

The following table collects the statements of this report about the Troupe implementation. Each row names an item of the formal model and the file of the implementation that holds its counterpart; the paths are relative to the root of the Troupe repository. The identifiers of the third column occur in the named files.

The docstrings of the Lean development state the following differences between the formal model and the implementation.

5 Indistinguishability

This section defines what an observer sees of a value, of an event, of a trace and of an input supply, and when the observer cannot tell two of them apart. The consistent inputs of §6 are built from these relations.

An observer is a pair \((a,\ell )\) of an authority \(a\) and a level \(\ell\), which we write \(a\,|\,\ell\) in subscripts. The observer tests a label \(x\) by privileged can-flow-to, \(x \sqsubseteq_{a} \ell\) (Definition 4); a label that passes the test is visible to the observer, and one that fails it is hidden. The observer \((\ensuremath{\mathsf{trustnull}},\ell )\) we call the observer at \(\ell\); its test is \(x\sqsubseteq\ell\) (Label.privFlowsTo_bot). We define the relations of this section for an arbitrary observer. The security condition uses the observer at a level for the events whose authority is the null authority, and an observer who holds the authority of the event for the others.

5.1 Values

We now define when an observer cannot distinguish two labelled values. Recall that a labelled value carries a data label and a type label. The definition accordingly has two parts: we compare the base values if the data label is visible to the observer, and the runtime types if the type label is visible.

To illustrate the definition, we take the observer at \(\bot\) and the label \(A=\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \top \rangle\), which is hidden from this observer. The integers \(5\) and \(7\), each with data label \(A\) and type label \(\bot\), are low-equivalent: the observer sees an integer in both and the content of neither. The integer \(5\) and the unit value, with the same two labels, are not low-equivalent, because both type labels are visible and the runtime types differ. When no label of either value is visible the definition asks for nothing, and any two values are low-equivalent, for instance the integer \(5\) with both labels \(A\) and the unit value with both labels \(\langle \{\ensuremath{\mathsf{bob}}\} \,;\, \top \rangle\).

A label that is visible in one value has to be the label of the other. The integer \(5\) with data label \(\bot\) and the integer \(5\) with data label \(A\) hold the same content and are not low-equivalent: the first data label is visible, and the two data labels differ. In a low-equivalent pair the data label of one value is therefore visible exactly when the data label of the other is, and the same holds of the type labels (LVal.PrivLowEq.dataLabel_privFlowsTo_iff, LVal.PrivLowEq.typeLabel_privFlowsTo_iff).

Low-equivalent values need not be equal even when their data labels are visible, since a tuple, a list or a closure holds labelled values of its own. The tuples \(\ensuremath{\mathsf{tuple}}\,[1,{5}^{\,A}_{\,\bot}]\) and \(\ensuremath{\mathsf{tuple}}\,[1,{7}^{\,A}_{\,\bot}]\), both labelled \(\bot\), are low-equivalent and differ in their second component; with \(2\) in place of \(1\) in one of them they are no longer low-equivalent, and the tuple \(\ensuremath{\mathsf{tuple}}\,[{5}^{\,A}_{\,A}]\) is not low-equivalent to the empty tuple \(\ensuremath{\mathsf{tuple}}\,[\,]\), the two lists of components having different lengths. Two low-equivalent values are equal when the observer sees all of one of them: if \(v_1\mathrel{\approx_{a\,|\,\ell }}v_2\), the value \(v_1\) is well-formed and its send label (Definition 6) is visible, then \(v_1=v_2\) (LVal.PrivLowEq.eq_of_sendLabel_le).

Low-equivalence is an equivalence relation (LVal.PrivLowEq.refl, .symm, .trans). Values that are low-equivalent at a level are low-equivalent at every level below it (LVal.PrivLowEq.mono), and values that are low-equivalent for an observer who holds an authority \(c\) are low-equivalent for the observer at the same level who holds any authority that \(c\) acts for (LVal.PrivLowEq.of_actsFor), the null authority among them (Label.actsFor_null). We check the pairs of this subsection with the Boolean function LVal.lowEqB (Troupe/Meta/LowEqChecker.lean), which decides the relation at the null authority (LVal.lowEqB_iff).

Formalized: examples/value_low_equivalence_pairs.lean • run: scripts/run-example.sh value_low_equivalence_pairs

A machine state keeps labelled values in the local environment, indexed by identifiers, in the captured environment, indexed by positions, and in the \(\mathit{self}\) slot. The proof relates these slots between two states, so we extend the relation to optional values, with the requirement that a slot which holds a visible value in one state holds one in the other.

Evaluation respects these relations: in two states whose environments and self values are related, an atom or an expression that evaluates in both evaluates to low-equivalent values.

5.2 Events and traces

Two events are low-equivalent when they have the same constructor and the observer cannot tell their fields apart. Fields that are labels are compared by equality; a value field is compared by Definition 11; and the descriptor list of a \(\ensuremath{\mathsf{regionClose}}\) event is compared after the descriptors of hidden presence are dropped, since the observer sees a removal only at the presence of the removed message.

For example, at the observer at \(\bot\) the outputs \(\ensuremath{\mathsf{output}}(\bot,(1,{5}^{\,A}_{\,\bot}))\) and \(\ensuremath{\mathsf{output}}(\bot,(1,{7}^{\,A}_{\,\bot}))\) are low-equivalent, their channels being equal and their values related, whereas \(\ensuremath{\mathsf{output}}(\bot,{5}^{\,\bot}_{\,\bot})\) and \(\ensuremath{\mathsf{output}}(\bot,{7}^{\,\bot}_{\,\bot})\) are not, and neither are two outputs of the same value on the channels \(\bot\) and \(A\). Two \(\ensuremath{\mathsf{regionClose}}\) events with the root authority, the lower bound \(\bot\) and the level \(\bot\) whose descriptor lists are \([(A,0)]\) and \([(A,1)]\) are low-equivalent: the presence \(A\) is hidden, and both lists are empty once the descriptors of hidden presence are dropped. The same holds of the lists \([(\bot,0),(A,0)]\) and \([(A,3),(\bot,0)]\), but not of \([(\bot,0)]\) and \([(\bot,1)]\), which differ in a descriptor that the observer sees. Two \(\ensuremath{\mathsf{regionClose}}\) events that differ only in the inner authority are low-equivalent, the inner authority not being compared. The Boolean functions Event.lowEqB and Trace.lowEqB decide the two relations at the null authority (Event.lowEqB_iff, Trace.lowEqB_iff). Note that two related events have the same level as soon as the first is observable (Event.privLowEq_lev_eq).

Formalized: examples/event_low_equivalence_pairs.lean • run: scripts/run-example.sh event_low_equivalence_pairs

An observer sees the events of a trace whose level is visible, in order.

At the null authority the two notions are observability at the level \(\ell\) (\(\mathsf{Event.observableAt}\), Definition 8) and the projection of a trace to the events observable at \(\ell\) (\(\mathsf{Trace.observableAt}\)); the lemmas are Event.observableAtPriv_bot and Trace.observableAtPriv_bot. A second projection at a level keeps the outputs only (Trace.observableIO):

\[\mathsf{observableAt}_\ell \ \text{keeps every event with}\ \mathsf{lev}(\alpha)\sqsubseteq\ell ;\qquad \mathsf{observableIO}_\ell \ \text{keeps every $\ensuremath{\mathsf{output}}$ event with}\ \mathsf{lev}(\alpha)\sqsubseteq\ell .\] The projection \(\mathsf{observableIO}\) is the view of an observer outside the process, who receives the messages sent on channels at or below its level; \(\mathsf{observableAt}\) is the view of an observer who also sees the internal events of the run. For example, the trace of the certified region of §4.5 has six events, of which the \(\ensuremath{\mathsf{confinedConsumeInput}}\) has the level {alice} and the other five the level \(\bot\). Its observable part at the observer \((\ensuremath{\mathsf{trustnull}},\bot)\) has five events, its observable part at the observer \((\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \emptyset \rangle,\bot)\) has six, since {alice} flows to \(\bot\) under that authority (§2), and its projection \(\mathsf{observableIO}_\bot\) is empty: the program outputs nothing.

Formalized: examples/event_low_equivalence_pairs.lean • run: scripts/run-example.sh event_low_equivalence_pairs

5.3 Visible sub-streams

An observer at \(\ell\) sees the messages of a supply whose presence flows to \(\ell\). The \(\ell\)-visible sub-stream of an input supply keeps these messages, in order (Inputs.visibleSub): \[\mathcal{I}{\downarrow}\ell \;\triangleq\; \mathsf{filter}\ (\lambda m.\ \mathsf{presence}(m)\sqsubseteq\ell )\ \mathcal{I}.\] Two input supplies are related by \(\mathrel{=^{\mathsf v}_{\ell }}\) when their \(\ell\)-visible sub-streams are equal (Inputs.EqVisible). For an observer \((a,\ell )\) the sub-stream keeps the messages \(m\) with \(\mathsf{presence}(m)\sqsubseteq_{a}\ell\) (Inputs.privVisibleSub), and the relation \(\mathcal{I}_1 \mathrel{=^{\mathsf v}_{a\,|\,\ell }} \mathcal{I}_2\) (Inputs.privEqVisible) holds when the two sub-streams are equal. These relations are the baselines of the consistent inputs of §6: a supply that the observer could already distinguish from the actual one by looking at the visible messages is not a candidate. The state relation of Definition 21 applies the second to mailboxes. At the null authority the privileged sub-stream is the \(\ell\)-visible sub-stream (Inputs.privVisibleSub_bot) and the privileged relation is \(\mathrel{=^{\mathsf v}_{\ell }}\) (Inputs.privEqVisible_bot); at any authority the relation \(\mathrel{=^{\mathsf v}_{a\,|\,\ell }}\) implies \(\mathrel{=^{\mathsf v}_{\ell }}\) (Inputs.privEqVisible.toEqVisible) and agreement of the two supplies at every single presence \(c\) with \(c\sqsubseteq_{a}\ell\) (\(\mathsf{Inputs.privEqBelow}\), Inputs.privEqVisible.toPrivEqBelow).

For example, the supplies \([\langle \texttt{\{alice\}},\ 42\rangle]\) and \([\langle \texttt{\{alice\}},\ -1\rangle]\) of the secret branch (Example 1) both have the empty \(\bot\)-visible sub-stream, so they are related by \(\mathrel{=^{\mathsf v}_{\bot}}\), while their {alice}-visible sub-streams differ. The two supplies of the region with a secret index (Example 5) hold an index, \(0\) or \(1\), of presence {alice} followed by the payloads 10 and 20 of presence \(\bot\); their \(\bot\)-visible sub-stream is the list of the last two messages in both, so they too are related by \(\mathrel{=^{\mathsf v}_{\bot}}\), whereas for the observer \((\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \emptyset \rangle,\bot)\) the visible sub-stream of each is the whole supply, and the two differ.

Formalized: examples/visible_substreams_of_supplies.lean • run: scripts/run-example.sh visible_substreams_of_supplies

Note that the sub-stream keeps the order of the visible messages across presences. A weaker relation, \(\mathrel{=_{\ell }}\), compares the visible messages presence by presence: \(\mathcal{I}_1{\restriction}c=\mathcal{I}_2{\restriction}c\) for every \(c\sqsubseteq\ell\) (Inputs.eqBelow, with the per-presence projection of §3.5). It does not imply \(\mathrel{=^{\mathsf v}_{\ell }}\): the development keeps the witness of two supplies holding the integer \(7\) at the presence \(\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \top \rangle\) and the integer \(8\) at the presence \(\langle \{\ensuremath{\mathsf{bob}}\} \,;\, \top \rangle\) in opposite orders, which are related by \(\mathrel{=_{\ell }}\) at \(\ell =\langle \{\ensuremath{\mathsf{alice}},\ensuremath{\mathsf{bob}}\} \,;\, \top \rangle\) and whose \(\ell\)-visible sub-streams differ, as do the lists of messages with presence in \([\bot,\ell ]\) that an interval read would select (interval_receive_needs_ordered_visible.lean under _working_notes/soundness-witnesses/). The ordered relation is the one the interval reads respect: an interval read with \(\ell_{\mathrm{hi}}\) visible returns the same message from two mailboxes with the same visible sub-stream (Mailbox.atIntervalInt_congr_privVisible), and a removal over an interval whose lower bound is hidden leaves the visible sub-stream unchanged, that is, if \(\mathsf{consume}_{[\ell_{\mathrm{lo}},\ell_{\mathrm{hi}}]}(\mathcal{M})[\,i\,]=(m_\star,k,\mathcal{M}')\) and \(\ell_{\mathrm{lo}}\not\sqsubseteq_{a}\ell\), the visible sub-streams of \(\mathcal{M}\) and \(\mathcal{M}'\) for the observer \((a,\ell )\) are equal (Mailbox.consumeAtIntervalIntD_privVisibleSub_invisible). A removal at a visible presence does change the visible sub-stream, and which message goes depends on the index: removing at index \(0\) and at index \(1\) from a mailbox of two messages at one presence \(p\) leaves residuals that differ on \(\cdot{\restriction}p\) (witness consume_secret_index_unsound.lean), which is why the index of a read is accounted for in the rules of §4 and the rank of a removal is disclosed by the events that carry a descriptor.

The next section defines the consistent inputs of an observer from these relations.

6 The security condition

We define security in the manner of the knowledge-based conditions, by sets of consistent inputs. The consistent inputs of an observer after an observation are the input supplies from which the program could have produced that observation; the more the observation separates, the smaller the set. At an observer whose level has the integrity projection \(\bot\), the set is what the literature calls the knowledge of the observer about the secret inputs; the condition also quantifies over levels with a non-trivial integrity projection, where the inputs that the set leaves free include the inputs that the level does not trust. The security condition bounds, for each event of a run, how much smaller the set may become, and the bound depends on the kind of the event. This section defines the consistent inputs, the per-event bounds, and the condition itself, TroupeSecurityCondition (abbreviated TSS); Theorem 1 states that every run of the monitored machine satisfies it.

6.1 Consistent inputs

Throughout the section, \(\mathit{prog}\) is a program and \(i\) an input supply. The trace of the run of \(\mathit{prog}\) from \(i\) after \(n\) steps, \((\ensuremath{\mathsf{exec}}\;n\;(\mathit{prog}.\ensuremath{\mathsf{init}}\;i)).\ensuremath{\mathsf{trace}}\), is written \(\mathsf{tr}\,(n,i)\). We write the three projections of §5 as follows; each is a filter of a trace \(t\) that keeps the order of the events. \[\begin{array}{l@{\quad}l@{\quad}l} \mathsf{obsIO}_\ell (t) & \text{the outputs $\alpha$ with $\mathsf{lev}(\alpha)\sqsubseteq\ell $} & \texttt{Trace.observableIO}\\ \mathsf{obsInt}_\ell (t) & \text{the events $\alpha$ with $\mathsf{lev}(\alpha)\sqsubseteq\ell $} & \texttt{Trace.observableAt}\\ \mathsf{obsInt}^{a}_\ell (t) & \text{the events $\alpha$ with $\mathsf{lev}(\alpha)\sqsubseteq_{a}\ell $} & \texttt{Trace.observableAtPriv} \end{array}\] An output is an event built by the constructor \(\ensuremath{\mathsf{output}}\) (Event.isOutput). The functions obsIO and obsInternal apply the first two projections to the trace of a run: \(\texttt{obsIO}(\mathit{prog},\ell ,i,n) = \mathsf{obsIO}_\ell (\mathsf{tr}\,(n,i))\) and \(\texttt{obsInternal}(\mathit{prog},\ell ,i,n) = \mathsf{obsInt}_\ell (\mathsf{tr}\,(n,i))\).

To see what an observation does and does not separate, take the two supplies \(i\) and \(i'\) that hold one message each at the presence \(A=\langle \{\ensuremath{\mathsf{alice}}\} \,;\, \top \rangle\), the integer \(42\) in \(i\) and \(-1\) in \(i'\); their \(\bot\)-visible sub-streams are equal (§5.3). The secret branch (Example 1) returns 100@{alice}%{alice} on \(i\) and 200@{alice}%{alice} on \(i'\), and its \(\bot\)-observations \(\mathsf{obsIO}_\bot\) are equal, both empty: nothing an observer at \(\bot\) sees tells the two apart. The second variant of Example 4, which declassifies the secret, lowers the blocking label and outputs the result on \(\bot\), has the \(\bot\)-observation [send {} \(\triangleleft\) 42@{}%{}] on \(i\) and a different one on \(i'\): here the observation separates the two supplies, and the declassification is the step at which the condition allows it to.

Formalized: examples/low_equivalent_twins_agree.lean • run: scripts/run-example.sh low_equivalent_twins_agree

Besides the program, the level, the supply and the observed trace, the definition of the consistent inputs is parametric in three things: a relation on supplies, the baseline, which fixes the candidates the observer starts from; a relation on traces, by which observations are compared; and a projection, which says what part of a trace the observer sees. We also define the progress-consistent inputs, the set of candidates from which the run goes on to produce one more observable event.

The security condition uses the following five instances; the supply \(i\) and the program are left implicit in the notation.

\[\begin{array}{l@{\;\;\triangleq\;\;}l@{\qquad}l} \Omega^{\mathsf{ext}}_{\ell }(o) & \Omega(\mathrel{=^{\mathsf v}_{\ell }},\,\mathrel{\approx_{\ell }},\,\mathsf{obsIO})(\mathit{prog},\ell ,i,o) & \texttt{Ω\_ext}\\[2pt] \Omega^{\mathsf{int}}_{\ell }(o) & \Omega(\mathrel{=^{\mathsf v}_{\ell }},\,\mathrel{\approx_{\ell }},\,\mathsf{obsInt})(\mathit{prog},\ell ,i,o) & \texttt{Ω\_internal}\\[2pt] \Omega^{\mathsf{int}}_{\ell ,\to}(o) & \Omega_{\!\to}(\mathrel{=^{\mathsf v}_{\ell }},\,\mathrel{\approx_{\ell }},\,\mathsf{obsInt})(\mathit{prog},\ell ,i,o) & \texttt{Ω\_internal\_prog}\\[2pt] \Omega^{\mathsf{priv}}_{a\,|\,\ell }(o) & \Omega(\mathrel{=^{\mathsf v}_{a\,|\,\ell }},\,\mathrel{\approx_{a\,|\,\ell }},\,\mathsf{obsInt}^{a})(\mathit{prog},\ell ,i,o) & \texttt{Ω\_internal\_priv}\\[2pt] \Omega^{\mathsf{priv}}_{a\,|\,\ell ,\to}(o) & \Omega_{\!\to}(\mathrel{=^{\mathsf v}_{a\,|\,\ell }},\,\mathrel{\approx_{a\,|\,\ell }},\,\mathsf{obsInt}^{a})(\mathit{prog},\ell ,i,o) & \texttt{Ω\_internal\_prog\_priv} \end{array}\] The baselines \(\mathrel{=^{\mathsf v}_{\ell }}\) and \(\mathrel{=^{\mathsf v}_{a\,|\,\ell }}\) are the relations on supplies of §5.3, and the relations \(\mathrel{\approx_{\ell }}\) and \(\mathrel{\approx_{a\,|\,\ell }}\) are trace low-equivalence at the null authority and at the authority \(a\) (Definition 13). The instances are three observers. The external observer of \(\Omega^{\mathsf{ext}}_{\ell }\) sees the outputs at or below \(\ell\), as a process outside the machine would. The internal observer of \(\Omega^{\mathsf{int}}_{\ell }\) sees every event at or below \(\ell\), including the reads, the bindings and the downgrades; its consistent inputs are included in the external observer’s (Ω_internal_subset_Ω_ext), since it sees more. The privileged observer of \(\Omega^{\mathsf{priv}}_{a\,|\,\ell }\) is the observer \((a,\ell )\) of §5, an internal observer who holds the authority \(a\); at the null authority it is the internal observer (Ω_internal_priv_bot, Ω_internal_prog_priv_bot). No progress form of the external consistent inputs is defined. The progress-consistent inputs are included in the consistent inputs (Ω_internal_prog_subset), and one more event can only shrink the internal consistent inputs (Ω_internal_extend_subset):

The sets of consistent inputs are infinite, so we compute them in the examples over a finite family of supplies. For a list \(F\) of supplies and a fuel, the function Ω_idx (Troupe/Meta/Falsifier.lean) returns the indices of the members of \(F\) that have, at some number of steps up to the fuel, a projected trace low-equivalent to the projection of the given trace, and Ω_prog_idx does the same for the progress-consistent inputs. Both take the step function and the projection as parameters, compare traces by Trace.lowEqB at the null authority, and do not evaluate the baseline or the well-formedness of the members, which the families of the examples satisfy by construction. We write an index set as a list.

Consider the family of the three supplies holding one message of presence {alice} with the payload \(-1\), \(0\) or \(1\), at the indices \(0\), \(1\) and \(2\), and the level \(\bot\). For the secret branch, at the trace of the run on member \(2\), the index sets of \(\Omega^{\mathsf{ext}}_{\bot}\) and \(\Omega^{\mathsf{int}}_{\bot}\) are both \([0,1,2]\): no run rules out a supply. For the program declassifyReleaseOutputToEndpointE (Example 4), let \(t\) be the trace of the run on member \(2\), whose four events are the receive, the \(\ensuremath{\mathsf{dValType}}\) event, the \(\ensuremath{\mathsf{dBl}}\) event and the output. At the first event of \(t\) the index sets of \(\Omega^{\mathsf{int}}_{\bot}\) and of \(\Omega^{\mathsf{int}}_{\bot,\to}\) are \([0,1,2]\). At the first two events of \(t\) the index set of \(\Omega^{\mathsf{int}}_{\bot}\) is \([2]\): the \(\ensuremath{\mathsf{dValType}}\) event has level \(\bot\) and carries the value 1@{}%{}, which only the run on member \(2\) produces. At the whole of \(t\) the index set of \(\Omega^{\mathsf{ext}}_{\bot}\) is \([2]\). An internal observer at the level \(\ensuremath{\mathsf{rootauth}} \sqcup \bot\), who sees the receive, has the index set \([2]\) already at the first event. For the blocked output (Example 2), at the empty trace the index set of \(\Omega^{\mathsf{int}}_{\bot}\) is \([0,1,2]\), and the index set of \(\Omega^{\mathsf{int}}_{\bot,\to}\) is empty on the monitored machine, where no run of the family emits an event observable at \(\bot\), and \([2]\) on the non-blocking machine, where the run on the positive secret outputs.

Formalized: examples/consistent_inputs_over_a_family.lean • run: scripts/run-example.sh consistent_inputs_over_a_family

6.2 The per-event bounds

Armed with the consistent inputs, we define the bound that the condition places on an event. Every bound has the form \(B \supseteq A\): the set \(B\) is a set of consistent inputs after the event, or before it, and \(A\) is a set of consistent inputs before the event, or at a prefix of the trace before it. The event may shrink the observer’s consistent inputs to \(B\) but not below \(A\). The kind of the event selects the two sets. The bound of a value or type downgrade uses a third combinator of consistent inputs, which restricts the further event of \(\Omega_{\!\to}\) by a predicate.

The docstring of Ω_prog_Q names the progress impact \(P_i^{+n}\) of Hansen, Larsen and Askarov (The Downgrading Semantics of Memory Safety, PLDI 2026) as the origin of the combinator. The bound of a value or type downgrade event \(\alpha\) uses the combinator with the predicate \(\mathsf{dr}\,\alpha\) (dr), which holds of the events that are a downgrade of the same kind: \(\mathsf{dr}\,\alpha\,\beta\) holds when \(\alpha\) and \(\beta\) are both \(\ensuremath{\mathsf{dVal}}\) events, both \(\ensuremath{\mathsf{dType}}\) events, or both \(\ensuremath{\mathsf{dValType}}\) events, with the same dimension, the same authority and the same target, and is false in every other case. The inputs consistent with \(\mathsf{dr}\,\alpha\)-progress are thus the supplies from which the run goes on to a downgrade like \(\alpha\), whatever value it releases.

The Lean definition states the progress part of case 3 before the privileged part, and has an arm of its own for the \(\ensuremath{\mathsf{dgConsumeInput}}\) event, with the privileged part alone. Case 2 is the baseline: an event that carries no authority (other than an output) may teach the internal observer nothing beyond the fact that the run reached it, which the progress-consistent inputs already express. The privileged part of case 3 says that a value or type downgrade, or a disclosing consume, may teach the internal observer at most what an observer who holds the authority of the event already knew, up to progress; the progress part says that every supply from which the run goes on to one more event observable at \(\ell\) goes on to a downgrade like \(\alpha\), with the same kind, dimension, authority and target. Case 4 says the same as the privileged part of case 3 of a region close, at the authority join of the authority of the open and the inner authority of the regions closed inside it (§4.5). The authority at which cases 3 to 5 take their privileged sets is the authority of the event (Event.authOf, §3.4). Case 5 splits the blocking-label downgrade in two: (5b) is the bound of case 2 for the event itself, and (5a) says that reaching the downgrade may teach the internal observer at most what the observer who holds its authority knew at an earlier point of the trace. The internal part of case 1 is the bound of case 2 for the output. The external part bounds an output not by the internal consistent inputs before it but by the progress-disclosure bound \(\Omega^{\mathsf{pd}}_{\langle \bot \,;\, \bot \rangle\,|\,\ell }(t)\) of the observer at \(\ell\) with the null authority, the privileged consistent inputs at the longest prefix of \(t\) that a certificate covers, and (5a) uses the same bound at the authority \(a\). We define the certificate and the bound in §6.5 and return to the two cases there; on the monitored machine the bound before an output is the internal consistent inputs at the whole trace, so that the external part of case 1 reads \(\Omega^{\mathsf{ext}}_{\ell }(t^{+}) \supseteq{}\)\(\Omega^{\mathsf{int}}_{\ell }(t)\): an output may teach the external observer nothing that the internal observer did not already know.

6.3 The condition

The function eventAt gives the event of the step taken after \(n\) steps of the run from \(i\), when that step emits one: \(\mathsf{eventAt}(\mathit{prog},i,n) \triangleq{}\)\((\ensuremath{\mathsf{step}}\;(\ensuremath{\mathsf{run}}\;n\;(\mathit{prog}.\ensuremath{\mathsf{init}}\;i))).\ensuremath{\mathsf{event}}\), a value of type \(\ensuremath{\mathsf{Option}}\;\ensuremath{\mathsf{Event}}\).

The condition is a property of the single run from \(i\); other supplies occur in it only as members of the sets of consistent inputs. It quantifies over every level \(\ell\), including levels with a non-trivial integrity projection, and over every step of the run, and it constrains an event only at the levels that see it. At a supply that is not well-formed it holds by its premise.

The falsifier.

We evaluate the condition in the examples with the falsifier of the development (Troupe/Meta/SecurityFalsifier.lean). The falsifier takes a step function, a level, a finite family \(F\) of supplies and a fuel. For each member of the family and each step of its run that emits an event observable at the level, it evaluates the bound of Definition 17 for that event with the index sets of Ω_idx, Ω_prog_idx and Ω_prog_Q_idx in place of the sets of consistent inputs (eventRefuted). The verdict refuted (refutedFamily, and refutedFamilyLevels over a list of levels) is true when some such bound fails as an inclusion of index sets; a refutation exhibits a member of the family and a step at which the condition fails. The verdict not refuted states that no bound fails on the family within the fuel; it is not a proof.

Two further caveats apply to the bounds with an authority. In the privileged part of case 3 and in case 4 the falsifier does not compute the privileged sets of the definition. For an event with authority \(a\) it evaluates, in place of the privileged progress-consistent inputs \(\Omega^{\mathsf{priv}}_{a\,|\,\ell ,\to}(t)\), the internal consistent inputs at the raised level \(a \sqcup \ell\), a set of the form \(\Omega\) and not \(\Omega_{\!\to}\) (docstring of eventRefuted). The raised level tests a label \(x\) by \(x\sqsubseteq a \sqcup \ell\), where the privileged observer tests it by \(x\sqsubseteq_{a}\ell\). The two tests agree on the confidentiality projection and differ on integrity, and no lemma of the development relates the consistent inputs of the two forms; a verdict of the falsifier in one of these cases is a verdict about the bound with the raised level. The falsifier computes the progress-disclosure bound of the external part of case 1 and of (5a) at the privileged observer, with the index sets Ω_internal_priv_idx and Ω_internal_prog_priv_idx, which also evaluate the baseline, and it decides the certificate of §6.5 over the same index sets (okProgTableWith); no lemma relates the prefix that it computes (progressDisclosurePrefixB) to the progress-disclosure prefix of the definition (module docstring of Troupe/Meta/SecurityFalsifier.lean).

In the examples of this report every label that is tested has the integrity projection \(\top\) of the carrier (these are the labels that print as a bare set, such as {alice}), and on such labels the two tests agree at every authority and level, which we check over all 64 labels of PLabel; on labels in general they do not.

Formalized: examples/privileged_test_at_top_integrity.lean • run: scripts/run-example.sh privileged_test_at_top_integrity

let secret ← tyrecv {alice} .int
let c ← lt 0 secret
ifte c (outputToEndpoint ⊥ 1; ret 0) (ret 0)

refuted at ⊥, non-blocking machine:                true
first refuting level, non-blocking machine:        ⊥
refuted at any swept level, deployed monitor:      false
\(\Omega\)_ext at ⊥, trace of the run with secret 1:        [2]
\(\Omega\)_ext at ⊥, trace of the run with secret -1:       [0, 1, 2]

6.4 Cases 2 to 4 on the examples

The events of case 2 are those whose authority is the null authority, other than outputs. The bound by the progress-consistent inputs accepts a receive whose reachability depends on a secret: the program implicitRecvE (Troupe/Examples.lean) receives a message of presence \(\bot\) in one branch of a test on a secret, and the falsifier does not refute it on the non-blocking machine, over three secrets (a #guard beside the program). The receive tells the internal observer that the branch was taken, and the progress-consistent inputs already account for that; what it does not account for is a later output that depends on it, and the external part of case 1 is where such a program is refuted (Example 10).

For case 3, return to the trace \(t\) of declassifyReleaseOutputToEndpointE on member \(2\) of the family of §6. The \(\ensuremath{\mathsf{dValType}}\) event has the root authority. The internal consistent inputs after it are \([2]\). The progress-consistent inputs of the internal observer before it are \([0,1,2]\), which are not included in \([2]\); the bound of case 2 would reject the event, and it is not the bound that applies. The internal consistent inputs at the level \(\ensuremath{\mathsf{rootauth}} \sqcup \bot\), the set that the falsifier takes for the privileged progress-consistent inputs, are \([2]\), and the privileged part of case 3 holds. The bound still constrains reachability: the program declassifySecretOccurrenceE (Troupe/Examples.lean) reaches a declassification only if a loop on a secret terminates, and the falsifier does not refute it, on the monitored and on the non-blocking machine (#guards beside the program), because the bounding set of each part is a set of progress-consistent inputs.

For case 4 we take the region with a secret index of Example 5, with the \(\ensuremath{\mathsf{peek}}\) moved after the close.

let i ← tyrecv {alice} .int
let (ok, cap) ← enableRangedReceive ⊥ {alice} root
let _ ← rangedConsume i ⊥ {alice}
let _ ← disableRangedReceive cap
peek 0 ⊥ ⊥

⊥-observation, i = 0:  [regionOpen ..., assign ...,
    regionClose !{alice, bob, charlie}⊕<{};{}> → {} @ {} ▷ [⟨{}, 0⟩],
    assign ⇒ 20@{}%{}]
⊥-observation, i = 1:  [regionOpen ..., assign ...,
    regionClose !{alice, bob, charlie}⊕<{};{}> → {} @ {} ▷ [⟨{}, 1⟩],
    assign ⇒ 10@{}%{}]
refuted, deployed monitor: false      refuted, non-blocking machine: false

let i ← tyrecv {bob} .int
let (_, capA) ← enableRangedReceive ⊥ {alice,bob} root
let (_, capB) ← enableRangedReceive {alice} {alice,bob} root
let _ ← rangedConsume i {alice} {alice}
let _ ← disableRangedReceive capB
let _ ← disableRangedReceive capA

{alice}-observation, i = 0:
    [regionOpen ..., assign ..., regionOpen ..., assign ...,
     regionClose !{alice, bob, charlie}⊕{alice, bob, charlie} → {} @ {}
                 ▷ [⟨{alice}, 0⟩], ...]
second variant, i = 0:
    [..., regionClose !{alice, bob, charlie}⊕{alice} → {} @ {}
                      ▷ [⟨{alice}, 0⟩], ...]
refuted at {alice}, deployed monitor: false
refuted at {alice}, non-blocking machine: false

6.5 The certified progress-disclosure prefix

The bounding sets of the external part of case 1 and of the bound (5a) are taken at a prefix of the trace before the event. The prefix is the longest one that a certificate covers, and the certificate is built along the trace: a visible event extends a certified prefix when every supply that the observer still considered possible at the earlier prefix goes on to produce the observation up to the event and one more observable event. On the monitored machine the certified prefix reaches past the last visible event of the trace, as we show at the end of this subsection; on the non-blocking machine it stops before an event whose reachability depends on a secret, and the external part of case 1 then catches an output that depends on the secret through that reachability. In the rules below, \(s\preceq t\) says that the trace \(s\) is a prefix of the trace \(t\) (List.IsPrefix).

Rule nil certifies the empty trace. Rule ordinary extends a certified prefix \(s\) to a trace that ends with an event \(e\) visible to the observer \(h\,|\,\ell\); the trace \(t\) before \(e\) is any extension of \(s\), and the premise on the sets asks that every supply which the observer considered possible at \(s\) produces the observation of \(t\) followed by one more event that the observer sees, so that the events of \(t\) after \(s\), and the progress past them, rule out no supply that \(s\) left open. Rule block does the same for a visible blocking-label downgrade with authority \(a\) and target \(\mathit{tgt}\), with the earlier certificate and the consistent inputs at \(s\) taken for the observer who holds the authority join \(h \mathbin{\curlyvee} a\) (Definition 2); the visibility of the event and the progress-consistent inputs at \(t\) stay those of the observer \(h\,|\,\ell\), and the authority \(a\) is the whole authority of the event, whatever its dimension \(d\).

Rule nil certifies the prefix of length \(0\), so the greatest length exists. The bound is what the observer \(h\,|\,\ell\) knows at the end of the longest certified prefix. Every certified length is at most the progress-disclosure prefix (le_progressDisclosurePrefix), and if the events of \(t\) after some certified prefix are all invisible to the observer \(h\,|\,\ell\), the bound is the privileged consistent inputs at the whole trace (progressDisclosureBound_eq_of_ok; both lemmas are in Troupe/Meta/SecurityConditionLemmas.lean). At the null authority, which the external part of case 1 uses, the privileged observer is the internal observer: its visibility test is \(\mathsf{lev}(\alpha)\sqsubseteq\ell\) (Event.observableAtPriv_bot) and its sets are \(\Omega^{\mathsf{int}}_{\ell }\) and \(\Omega^{\mathsf{int}}_{\ell ,\to}\) (Ω_internal_priv_bot, Ω_internal_prog_priv_bot).

The next three examples compute the progress-disclosure prefix on runs of the non-blocking machine, where it can stop short of the trace. In each, the program ends with an output on \(\bot\) whose reachability depends on a secret, and the external part of case 1 at that output is what refutes the program.

let hAuth ← atten root {alice,bob}
let s1 ← tyrecv {alice,bob} .int;   let s2 ← tyrecv {alice,bob} .int
let _ ← blockdeclto hAuth ⊥
let c ← lt 0 s1;   ifVal c (call loop 0; ret 0) (ret 0)
let _ ← declassify s2 hAuth ⊥
let _ ← outputToEndpoint ⊥ 1

length of t:                          9
progressDisclosurePrefix at ⊥:        7
event at position 6 of t:             a downgradeBl event
event at position 8 of t:             a downgradeValType event
refuted, deployed monitor:            false
refuted, non-blocking machine:        true

let _ ← outputToEndpoint ⊥ 0
let s ← tyrecv {alice,bob} .int
let c ← lt 0 s
ifVal c (tyrecv ⊥ .int; ret 0) (call loop 0; ret 0)
let _ ← outputToEndpoint ⊥ 1

length of t:                          7
progressDisclosurePrefix at ⊥:        4
event at position 3 of t:             an output event
event at position 6 of t:             a consumeInput event of presence ⊥
refuted, deployed monitor:            false
refuted, non-blocking machine:        true

The third program has no receive and no downgrade after its secret branch, only an assignment and a blocking-label downgrade before the output. The two visible events after the branch do not extend the certificate.

let lAuth ← atten root ⊥
let s1 ← tyrecv {alice,bob} .int
let c ← lt 0 s1;   ifVal c (ret 0) (call loop 0; ret 0)
let y ← 7
let _ ← blockdeclto lAuth ⊥
let _ ← outputToEndpoint ⊥ 7

length of t:                          8
⊥-visible positions of t:            [0, 1, 2, 3, 6, 7]
progressDisclosurePrefix at ⊥:        4
event at position 4 of t:             a consumeInput event of presence {alice,bob}
event at position 6 of t:             an assign event
event at position 7 of t:             a downgradeBl event with authority ⊥
refuted, deployed monitor:            false
refuted, non-blocking machine:        true

On the monitored machine the progress-disclosure bound before an output is the internal consistent inputs at the whole trace, and the bound before a \(\ensuremath{\mathsf{dBl}}\) event with authority \(a\) is the privileged consistent inputs at the whole trace. For a well-formed program and a well-formed supply, if the run is at a running state \(s\) after \(n\) steps with \(s.\mathit{bl}\sqsubseteq_{h}\ell\), then some certified prefix of \(\mathsf{tr}\,(n,i)\) is followed only by events that are invisible to the observer \(h\,|\,\ell\) (okProg_visible_prefix_of_bl_low, Troupe/Meta/ProgressCertification.lean), and therefore \(\Omega^{\mathsf{pd}}_{h\,|\,\ell }(\mathsf{tr}\,(n,i)) = \Omega^{\mathsf{priv}}_{h\,|\,\ell }(\mathsf{tr}\,(n,i))\) (progressDisclosureBound_eq_of_bl_low). The state that emits an output observable at \(\ell\) has \(\mathit{bl}\sqsubseteq\ell\) (output_emit_bl_le), which is the hypothesis at the null authority (Label.privFlowsTo_bot), and the state that emits a \(\ensuremath{\mathsf{dBl}}\) event with authority \(a\) and a target that flows to \(\ell\) has \(\mathit{bl}\sqsubseteq_{a}\ell\) (blockdecl_emit_bl_low_priv).

The proof of okProg_visible_prefix_of_bl_low is by induction on \(n\), for every held authority at once. A step either does not lower the blocking label or emits a \(\ensuremath{\mathsf{dBl}}\) event (step_bl_le_or_downgradeBl). In the first case the blocking label before the step is visible as well, and an event that the step emits and that the observer \(h\,|\,\ell\) sees extends the certified prefix by rule ordinary, whose premise on the sets holds because a second run with the observation so far takes one more bridge (Ω_internal_prog_priv_supset_of_emit, by bridge_progress). In the second case, with authority \(a\), the blocking label before the step flows to \(\ell\) under \(h \mathbin{\curlyvee} a\) (blockdecl_emit_bl_low_authJoin), the induction hypothesis gives a certificate for the observer \((h \mathbin{\curlyvee} a)\,|\,\ell\), and the event extends it by rule block, whose premise on the sets holds by Ω_internal_prog_priv_supset_authJoin_of_blockdecl (by bridge_constructed_blockdecl). In other words, on the monitored machine a visible blocking label at an output or at a blocking-label downgrade certifies every visible event of the trace before it.

The next section states that every run of the monitored machine satisfies the condition.

7 Soundness

We now state the main result, that every run of the monitored machine satisfies the security condition, and present its proof.

The hypothesis \(\mathit{prog}.\mathsf{WF}\) (Program.WF, Troupe/Meta/Defs/ValueWf.lean) requires, of the main body and of every body of the function table, that every constant is a well-formed base value (Body.WF) and that no constant contains a capability (Body.CapFree). The statement \(\mathsf{TSS}(\mathit{prog},i)\) is Definition 18, with the monitored step function of §4 in \(\mathsf{eventAt}\) and in the traces of the sets of consistent inputs; its own hypothesis is the well-formedness of the supply \(i\). The keyword theorem occurs once in the Lean sources under Troupe/, on this declaration; every other statement is a lemma. It depends on the axioms propext, Classical.choice and Quot.sound and on no other, which a #guard_msgs-checked #print axioms at the end of the file pins. The monitored runs of Examples 6, 7, 8, 9, 10 and 11 are instances, as far as the falsifier can tell: it does not refute their families (in the privileged part of case 3 and in case 4 for the bound with the raised level, and in the external part of case 1 and in (5a) for the certificate decided over the family, §6).

The shape of the proof.

Every bound of Definition 17 is an inclusion \(B \supseteq A\) of sets of consistent inputs, and we prove it by taking a supply \(i'\) of \(A\) and showing that \(i'\) is in \(B\). We call the run from the supply \(i\) of the theorem the reference run and the run from \(i'\) the second run. Membership of \(i'\) in \(A\) says that the second run has, for the observer in question, the same observation as the reference run up to the event; membership in \(B\) asks for the same observation including the event, or including one more event. The proof therefore has to show that two runs which agree on what the observer has seen so far go on to agree on the next observable event.

The argument runs as follows. We cut each run into bridges, stretches that emit no observable event and end with one (§7.2). Two runs with the same observation pass through the same number of bridges with low-equivalent events, and we show that at the end of each pair of bridges the two states are related by a state relation (§7.1) together with a set of invariants (§7.3); the relation and the invariants are carried from one pair of bridges to the next as the per-bridge invariant (§7.4). Operational security (§7.5) is then a statement about one bridge of the reference run and a related state of the second run: that the second run takes a bridge to a low-equivalent event, or that every bridge it takes has one. The unwinding lemma states that operational security holds at every bridge length, and §7.7 derives each bound from it. §9 tabulates the Lean lemmas of each step.

7.1 State relations

We first define when two states, one of the reference run and one of the second run, look the same to an observer. The relation has to say what the observer sees of each component of a state, and it has to be weak enough to hold while the two runs are inside a branch on a secret, where their controls differ, yet strong enough that when the two runs are at a visible \(\mathit{pc}\) the next observable event is the same in both. Most clauses accordingly have the form “if a certain label is visible, then the components it guards agree”.

We write the fields of the monitor of a state \(s_i\) as \(s_i.\mathit{pc}\), \(s_i.\mathit{bl}\), \(s_i.\Phi\), …; its four region registers as \(s_i.\mathsf{clearance}\), \(s_i.\mathsf{clearanceLabel}\), \(s_i.\mathsf{evidenceLevel}\), \(s_i.\mathsf{evidenceLabel}\); and \(s_i.\mathit{regions}\) for its list of region frames (\(\mathsf{State.regions}\)). The definition uses the following notions.

• The mailbox \(\mathsf{outermostBase}(s)\) (\(\mathsf{State.outermostBase}\)) is the open-time base of §4.5: the mailbox at the opening of the outermost region, or the current mailbox when no region is open.

• The relation \(\mathcal{I}_1 \mathrel{=^{\mathsf v}_{a\,|\,\ell }} \mathcal{I}_2\) (\(\mathsf{Inputs.privEqVisible}\)) is the relation of §5.3, applied to mailboxes.

• The list \(\mathsf{privVisibleFrames}_{a\,|\,\ell }(F)\) (\(\mathsf{Inputs.privVisibleFrames}\)) replaces each descriptor list \(D\) of the list of lists \(F\) by \(D{\restriction}_{a\,|\,\ell }\), the filter of the \(\ensuremath{\mathsf{regionClose}}\) row of Definition 13.

• The stack \(\mathsf{privLowFrames}_{a\,|\,\ell }(K)\) (\(\mathsf{Kont.privLowFrames}\)) drops frames from the head of the continuation \(K\) for as long as their saved \(\mathit{pc}\) is hidden, and keeps the rest: the frames pushed since the run entered a hidden context are not compared. Two frames are related (\(\mathsf{Frame.PrivLowEq}\)) when their saved local environments, saved captured environments, and saved \(\mathit{self}\) slots are related by the relations of Definition 12, and their saved \(\mathit{pc}\), saved chain head, branch flag, result destination, and continuation body are equal. Two stacks are related (\(\mathsf{Kont.PrivLowEq}\)), written \(\mathrel{\approx_{a\,|\,\ell }}\), when they have equal length and are related frame by frame.

The clauses fall into three groups. The first group concerns the control: the two program counters are visible together (pcSync), the function tables are equal, and when the program counter is visible the controls, the program counters, the environments and the self values agree (whenLow); the frames of the continuation below the hidden ones agree (kontLow), and the counters of fresh identities agree at every visible level (nextId). The second group concerns the mailbox, compared through the open-time base (inputs); the invariants of §7.3 compare the current mailbox when no region is open. The third group concerns the regions. The registers are compared under their own labels (clearanceLabelSync to evidenceLevelEqLow), the two runs have the same number of open regions (regionDepth), the same chain head and frame identities when the program counter is visible, and the same visible evidence in every frame when the active clearance and its label are visible (framesEqLow); the entry registers of each pair of frames are compared like the registers themselves. The clause (framesEqLow) compares the evidence after dropping the descriptors of hidden presence, and only when the clearance and its label are visible. The development checks the clause and two variants of it by #guard in Troupe/Examples.lean, at the observer at \(\bot\), on every pair of states that two runs of one program reach after the same number \(k<40\) of steps. On the two runs of the region with a secret index (Example 5) the clause holds at every pair (framesVisEqClearanceGuardB), and so does the variant that compares the full descriptor lists under the same premise (framesEqClearanceGuardB), the clearance \(\{\ensuremath{\mathsf{alice}}\}\) being hidden; but the variant that compares the full lists under the premise \(s_1.\mathsf{clearanceLabel}\sqsubseteq_{a}\ell\) alone fails (framesEqLabGuardB), since the label of the literal clearance is \(\bot\). On the program v2StressE, which opens a region with both bounds \(\bot\) and performs, in a branch on a secret index \(i\), the confined consume at index \(i\) over the interval \([\{\ensuremath{\mathsf{alice}}\},\{\ensuremath{\mathsf{alice}}\}]\), the clause holds at every pair and both variants fail.

The relation of operational security is a strong form that adds the blocking label and the domains of the environments.

With the domains agreeing, an atom that evaluates in one of two strongly related states at a visible \(\mathit{pc}\) evaluates in the other, to a related value (State.PrivLowEqCS.evalAtom_some); this is what lets the proof construct a step of the second run from a step of the reference run.

Synchronized bridging, defined in the next subsection, needs a weaker relation that only says that two states execute the same code.

Two low-equivalent states at a visible \(\mathit{pc}\) whose continuations hold only visible saved program counters are in same-control (State.PrivLowEqC.toSameControl).

7.2 Bridges

An observer sees a run as a sequence of observable events; the steps between them are invisible. A bridge is a number of steps that emit no observable event, followed by one step that emits one. The proof compares the reference run and the second run one bridge at a time. The step function \(\ensuremath{\mathsf{step}}\) maps a configuration \(c\) to an optional event \((\ensuremath{\mathsf{step}}\,c).\mathsf{event}\) and a successor configuration \((\ensuremath{\mathsf{step}}\,c).\mathsf{next}\) (§4.4).

The predicate \(\mathit{obs}\) is a parameter. The instance at \(\mathit{obs}=\mathsf{vis}_{a\,|\,\ell }\) (Definition 14), written with the subscript \(a\,|\,\ell\), is the bridge of an observer \((a,\ell )\). The instance at \(\mathit{obs}\,\alpha\triangleq{}\)\(\mathsf{lev}(\alpha)\sqsubseteq\ell\) (\(\mathsf{Event.observableAt}\)), written with the subscript \(\ell\), is the abbreviation \(\mathsf{BridgeStep}\). Note that a bridge always ends with an observable event: a run that halts or gets stuck without emitting one takes no further bridge.

_      <- outputToEndpoint bot 0
secret <- tyrecv {alice} int
c      <- 0 < secret
_      <- if c then { x <- 1 + 1; y <- x + 1; ret y } else ret 0
_      <- blockdeclto root bot
_      <- outputToEndpoint bot 1
ret 0

secret 42:   length 0: send {} ◁ 0@{}%{}
             length 7: blockDowngrade[conf] !{alice, bob, charlie} → {}
             length 0: send {} ◁ 1@{}%{}
secret -1:   length 0: send {} ◁ 0@{}%{}
             length 5: blockDowngrade[conf] !{alice, bob, charlie} → {}
             length 0: send {} ◁ 1@{}%{}

An observable event is only ever emitted from a state whose \(\mathit{pc}\) is visible, so the two runs of a bridge pair, however they diverge in between, are back at a visible \(\mathit{pc}\) when they emit.

The outcome of a step that emits an event is a running state (Outcome.running_of_event).

Synchronized bridging.

Two runs with the same observation take the same number of bridges with low-equivalent events. Synchronized bridging records this: it relates the pair of states at which two runs start to the pair they reach after the same number of bridges each, and asks that at every step of the way the two end states are in same-control.

The instance for an observer \((a,\ell )\) takes \(\mathit{obs}=\mathsf{vis}_{a\,|\,\ell }\) and \(\mathit{eqEv}={\mathrel{\approx_{a\,|\,\ell }}}\) on events (Definition 13). In Example 12 the two runs have, bridge by bridge, the lengths \(n_1\) and \(n_2\) of \(0\) and \(0\), \(7\) and \(5\), \(0\) and \(0\), and low-equivalent events; these are the premises of rule step other than same-control, at the observer at \(\bot\). A relation \(R\) on states that is preserved by every pair of bridge steps to running configurations with \(\mathit{eqEv}\)-related events is preserved by synchronized bridging: if \(R\,s_1\,s_2\) and \((s_1,s_2)\mathrel{\Rightarrow^{\,\overline\alpha}_{\,\mathit{obs}}}(s_1',s_2')\) then \(R\,s_1'\,s_2'\) (SyncBridgeObs.lowEqGen).

The indistinguishability restriction.

For a downgrade, the second state of operational security is not an arbitrary related state but one from which the two runs synchronize along the events that the observer who holds the authority of the downgrade sees. The restriction of a relation \(I\) along a list of events keeps the pairs that \(I\) relates and from which a synchronized bridging along that list starts.

7.3 Invariants

Besides the state relation, every statement of operational security assumes an invariant of each of the two states and two invariants of the pair. The single-run invariant collects the properties that every reachable state has.

The field regions says that the current mailbox is the entry mailbox of each open region with the removals of its evidence applied, so that the evidence of a frame determines the mailbox from the open-time base; its \(\mathsf{Forall}_2\) form over the projected lists is regionReplay_packed. A step preserves the invariant (StInv.step), and so does a run of any length (StInv.run). The preservation of the field regions (step_preserves_regionReplay) needs the chain invariant: the development keeps a state with \(\mathit{ch}=\ensuremath{\mathsf{none}}\) and a nonempty list of region frames that satisfies the field and whose step, a \(\ensuremath{\mathsf{tyrecv}}\), leads to a state that does not (region_replay_needs_chain_invariant.lean under _working_notes/soundness-witnesses/).

The two invariants on a pair of states compare the evidence of the region frames of the two states segment by segment, where the segment of a frame is the part of its evidence that the frame inside it does not hold. For a state \(s\) and an index \(j\), write \(\mathsf{seg}_j(s)\) for the \(j\)-th entry of \(\mathsf{regionSegs}\,(s.\mathsf{regions}.\mathsf{map}\,\mathsf{evidence})\), and the empty list when there is no such entry. The function regionSegs maps a list of descriptor lists \(F_0, F_1, \ldots\) to the list whose \(j\)-th entry is the first \(|F_j|-|F_{j-1}|\) descriptors of \(F_j\), with \(F_{-1}=[\,]\). For a list \(X\) of descriptors \((p,k)\), write \(X{\downarrow}_{o\,|\,\ell }\) for the sublist of those with \(p\sqsubseteq_{o}\ell\). The matched regions say that the visible descriptors of each segment agree whenever the clearance that covers the segment is visible.

The premise of segsRec is the premise of the clause (framesEqLow) of Definition 21, read from the entry registers of the frame; the premise of segs adds the clearances of the regions that were closed inside the frame and the frames enclosing it. The join over the frames at \(j, j{+}1, \ldots\) is needed: the variant that takes the absorbed clearances of the frame at \(j\) alone is false on two runs of the program freshRegionAfterAbsorbE (Troupe/Examples.lean) at the level {alice}, where the check matchedDeltasAbsorbedB evaluates to false and the check matchedDeltasAbsorbedJoinB for the joined form to true.

The charged regions concern the authority. A close discloses the evidence of its frame under the authority of the open, joined with the authorities absorbed from the regions closed inside it (§4.5); the observer who holds that authority has to find the visible segments equal. We say that the frame at \(j\) is charged for the observer when some enclosing frame has a visible clearance label and the observer acts for the absorbed authority of every frame in between.

The field segsCharged at \(j=0\) is what relates the two \(\ensuremath{\mathsf{regionClose}}\) events of a pair of related states (matched_close’P, Unwinding/PrivLowStep.lean). From basesVis and segsCharged at \(j=0\) and the field regions of \(\mathsf{StInv}\) in both states, the two current mailboxes are related by \(\mathrel{=^{\mathsf v}_{o\,|\,\ell }}\) (State.ChargedRegions.privEqVisible_mailbox, Unwinding/MatchedRegionsStep.lean). Both invariants hold of every pair of states in which neither state has a region frame and the mailboxes are related (matchedRegions_of_empty, chargedRegions_of_empty), in particular of the two initial states.

The two invariants carry information that the state relation alone does not. The development keeps two witness programs for this, one for the binding arm and one for the close arm of operational security (Definition 31). In each, two runs reach a pair of states that agree on every component the state relation compares, with hidden clearance so that the clause (framesEqLow) asks nothing, and whose visible frame evidence differs; the runs then produce events that are not low-equivalent, so that a statement of operational security whose hypothesis on the pair were the state relation alone would be false at that pair. The checks of both files are #guards on machine runs, evaluating Boolean forms of the state components listed; they do not contain a Lean proof that the pair satisfies \(\mathrel{\approx^{\mathsf{cs}}_{o\,|\,\ell }}\), nor that no bridge of the second state exists.

s     <- tyrecv {charlie} int
eo    <- enableRangedReceive bot bot root          -- outer region
capO  <- proj 1 eo
capOL <- declassify capO root bot
ei    <- enableRangedReceive bot {charlie} root    -- inner region
capI  <- proj 1 ei
capIL <- declassify capI root bot
_     <- if s then { rangedConsume 0 bot bot; ret 0 } else { peek 0 bot bot; ret 0 }
_     <- disableRangedReceive capIL
_     <- blockdeclto root bot
ew    <- enableRangedReceive {charlie} {charlie} root   -- third region
capW  <- proj 1 ew
capWL <- declassify capW root bot
_     <- disableRangedReceive capWL                -- the step at 16
_     <- peek 0 bot bot                            -- the step at 17
_     <- disableRangedReceive capOL
ret 0

fnBranch(s):
  x <- declassify s root {alice}
  _ <- if x then { rangedConsume 0 bot bot; ret 0 } else { peek 0 bot bot; ret 0 }
  ret 0

hi   <- tyrecv {bob} level
s    <- tyrecv {bob} int
aA   <- atten root {alice}
e    <- enableRangedReceive bot hi aA
cap  <- proj 1 e
capL <- declassify cap root bot
fnc  <- mkClosures fnBranch
_    <- call fnc s
_    <- blockdeclto root bot            -- closePSE only
_    <- disableRangedReceive capL       -- the step at 16 (closePSE), at 15 (closePIE)
ret 0

7.4 The per-bridge invariant

The proof carries the state relation and the three invariants from one pair of bridges to the next as one Lean structure, the per-bridge invariant PrivBridgeInvS (Unwinding/PrivBridgePreserves.lean). Given an observer \(a\,|\,\ell\) and two states \(s_1\) and \(s_2\), it is the conjunction of ten fields: \(s_1\mathrel{\approx^{\mathsf{cs}}_{a\,|\,\ell }}s_2\); \(\mathsf{StInv}\,\ell \,s_1\); \(\mathsf{StInv}\,\ell \,s_2\); every saved program counter of the continuation stack of \(s_1\) flows to \(\ell\) under \(a\), and likewise for \(s_2\); the first component of the identifier of every region frame of \(s_1\) flows to \(\ell\) under \(a\), and likewise for \(s_2\); the two lists of frame identifiers are equal; \(\mathsf{MR}_{a\mid\ell }(s_1,s_2)\); and \(\mathsf{CR}_{a\mid\ell }(s_1,s_2)\). It holds of the two initial states of a well-formed program on two well-formed supplies related by \(\mathrel{=^{\mathsf v}_{a\,|\,\ell }}\) (init_privBridgeInvS, Unwinding/RunsSynchronize.lean), and it follows from the hypotheses that every statement of operational security places on its pair of states, namely \(s_1.\mathit{pc}\sqsubseteq_{a}\ell\), the invariant \(\mathsf{StInv}\) of both states, \(s_1\mathrel{\approx^{\mathsf{cs}}_{a\,|\,\ell }}s_2\), and the matched and the charged regions at \(a\,|\,\ell\) (privBridgeInvS_of_premises, Unwinding/Lemma2.lean).

Item 1 is proved by strong induction on the sum of the two bridge lengths, by cases on whether \(s_1.\mathit{pc}\) is visible. At a visible \(\mathit{pc}\) the two runs are at the same control, and a step of one is matched by a step of the other: both emit, or both are silent and stay at a visible \(\mathit{pc}\), or both enter a hidden context. In the last case, and whenever \(\mathit{pc}\) is hidden, the two runs may do different things for a while, and the following lemma cuts the pair of bridges at the point where both are back at a visible \(\mathit{pc}\), in a related pair of states: the remainders of the second bridges of Example 12, from the states after the branch, are such a pair.

The states \(p_i\) are reached by a return: the continuation of \(p_i\) is the tail of that of \(s_i\), and rule ret-frame restores the saved \(\mathit{pc}\), which the hypotheses say is visible.

7.5 Operational security

Operational security is the single-bridge statement at the heart of the proof. It is about one bridge of a state \(s_1\), the reference state, and a state \(s_2\), the second state, that is related to \(s_1\), and it is stated by cases on the event that the bridge emits, in six arms. Two kinds of statement occur. A universal statement says that every bridge of \(s_2\) emits an event low-equivalent to that of \(s_1\) and ends in a related state. It serves the bounds whose bounding set is a set of progress-consistent inputs: a supply in that set has a bridge, and the bridge must match. An existential statement says that \(s_2\) takes such a bridge. It serves the inclusions of a set of consistent inputs in a set of progress-consistent inputs, in the external part of case 1 and in the bound (5a), where a bridge of the second run has to be constructed; it comes with the hypothesis that the blocking label at the end of the reference bridge is visible. For the downgrades the second state is taken from an indistinguishability restriction (Definition 27) at the authority of the event, and the conclusions are at that authority. We call such a statement restricted. The universal statements are (1a), (2), (3b-i), (4b-i), (5) and (6a); the existential ones (1b), (3a), (3b-ii), (4a), (4b-ii) and (6b); the restricted ones (3b), (4b), (5) and (6b).

The definition writes the observer as \(o\,|\,\ell\), with \(o\) for its authority, and writes \(a\) for the authority of a downgrade event. The observer \(o\,|\,\ell\) sees an event \(\beta\) when \(\mathsf{vis}_{o\,|\,\ell }(\beta)\) holds (Definition 14), and its bridges and bridge chains are those of Definition 24 at that predicate, written \(\langle s \rangle\mathrel{\curvearrowright^{\,n,\alpha}_{\,o\,|\,\ell }}\langle s' \rangle\) (BridgeStepObs (Event.observableAtPriv \(o\) \(\ell\))) and \(\langle s \rangle\mathrel{\curvearrowright^{\,*,\overline\beta}_{\,o\,|\,\ell }}\langle s' \rangle\) (BridgeChainObs). The relation \(\alpha\mathrel{\approx_{c\,|\,\ell }}\alpha'\) is event low-equivalence (Event.PrivLowEq, Definition 13), the relation \(s\mathrel{\approx^{\mathsf{cs}}_{c\,|\,\ell }}s'\) is the strong state relation (Definition 22), and \(\langle \mathrel{\approx^{\mathsf{cs}}_{c\,|\,\ell }}\rangle^{\,\overline\beta}_{\,c\,|\,\ell }\) is the restriction of Definition 27 (IndRestrictionObs) at the observation \(\mathsf{vis}_{c\,|\,\ell }\), the event relation \(\mathrel{\approx_{c\,|\,\ell }}\) and the base relation \(\mathrel{\approx^{\mathsf{cs}}_{c\,|\,\ell }}\). The relation \(c \succcurlyeq o\) is Label.actsFor \(c\) \(o\) (Definition 1), and \(a \mathbin{\curlyvee} a'\) is the authority join (Definition 2). The relation \(\mathrm{dr}\,\alpha\,\alpha'\) is the predicate of the progress part of case 3 of Definition 17 (dr, Troupe/Meta/Defs/SecurityCondition.lean). The arms say that a blocking label is low when it is visible to the observer, and call a value or type downgrade a declassify.

Arm 1 pairs the universal statement with an existential one, since the external part of case 1 of Definition 17 bounds an output by a set of consistent inputs, and its internal part and case 2 bound an output and a receive by a set of progress-consistent inputs. Arm 2 has the universal statement only. Arm 3 says two things about a declassify. The statement (3a) concerns its reachability: a related state reaches a declassify of the same kind, whatever value it releases, which is what the progress part of case 3 asks; the proof of that part does not apply (3a) but a lemma about a given bridge of the second run (§7.7). The statement (3b) concerns its content, at the authority \(a\): for the observer who holds \(a\) the released values are low-equivalent. The two \(\ensuremath{\mathsf{dValType}}\) events of the second variant of Example 3 on the secrets 42 and -1,

downgradeValType[conf] !{alice, bob, charlie} → {} @ {} ⇒ 42@{}%{} ; int@{}
downgradeValType[conf] !{alice, bob, charlie} → {} @ {} ⇒ -1@{}%{} ; int@{}

both have the level \(\bot\), the dimension \(\ensuremath{\mathsf{conf}}\), the root authority and the target \(\bot\), so the predicate \(\mathrm{dr}\) holds of the pair, as (3a) concludes; they carry the values 42 and -1 at the data label \(\bot\) and are not low-equivalent at \(\bot\); (3b) does not apply to this pair of runs, whose states after the receive are not related for the observer who holds the root authority and sees the secret.

Formalized: examples/downgrade_events_of_two_secrets.lean • run: scripts/run-example.sh downgrade_events_of_two_secrets

Arm 4 treats the disclosing consume like a declassify, and arm 5 treats the region close at the authority join of its two authorities, with the universal statement only. Arm 6 is the blocking-label downgrade: (6a) is the universal statement at the observer, and (6b) the existential one at the authority of the event; (6b) has no hypothesis on the blocking label of \(s_1'\), since the step that emits a \(\ensuremath{\mathsf{dBl}}\) event with authority \(a\) and a target that flows to \(\ell\) starts from a blocking label that flows to \(\ell\) under \(a\) (blockdecl_emit_bl_low_priv). Under the hypothesis \(a \succcurlyeq o\) of a restricted statement, a label that is visible to the observer \(o\,|\,\ell\) is visible to the observer \(a\,|\,\ell\) (Label.privFlowsTo.mono_auth), so a bridge of the observer \(o\,|\,\ell\) is a chain of bridges of the observer \(a\,|\,\ell\); at the empty list \(\overline\beta\) the restriction holds of every pair that the strong state relation relates (rule restr-nil).

7.6 The unwinding lemma

The proof is a case analysis on the constructor of the event \(\alpha\) and contains no induction of its own; the inductions are in the lemmas it applies, which couple the silent steps of the reference bridge with steps of the second state by induction on their number, and in Lemma 8. §9.3 lists, for each statement of Definition 31, the lemmas that the proof applies.

7.7 From the unwinding lemma to the theorem

The proof of monitorSatisfiesTSS is a case analysis on the emitted event, one case for each kind of bound. Each case is one application of a bound lemma, and each bound lemma is one application of the lemma in the last column. The sets of consistent inputs are written by their Lean names, at the trace \(t\) before the event and the trace \(t\alpha\) that includes it (Definition 17).

Each lemma of the last column takes a supply \(i'\) of the bounding set and shows that it is in the bounded set. The first step is the same in all of them: the two runs, which agree on their observation so far, are brought to a pair of states that carries the per-bridge invariant.

The states \(e_1\) and \(e_2\) are where the two runs are after their last pair of bridges. The steps of the reference run from \(e_1\) to \(s_1\), followed by the step of \(s_1\) that emits the event \(\alpha\), are one bridge of the observer \(a\,|\,\ell\) from \(e_1\) (bridge_of_silent_run). The unwinding lemma is applied to this bridge and the pair \((e_1,e_2)\), through the corollaries of the next table, which are at the end of Lemma2.lean. Each corollary takes a pair of states that carries the per-bridge invariant at an observer \(a\,|\,\ell\), the hypothesis \(e_1.\mathit{pc}\sqsubseteq_{a}\ell\), and a bridge of \(e_1\) at that observer.

Composing the two tables gives, for each case of the theorem, the statements of Definition 31 that its proof applies and the authority of the observer at which it applies them; §9.1 lists the calls in between.

Three cases also apply lemmas of Lemma2.lean that are not statements of Definition 31. The progress part of case 3 is proved by declassify_progress_translate with bridge_given_dr, which states that every bridge of the second run from the synchronized pair emits an event \(\alpha'\) with \(\mathrm{dr}\,\alpha\,\alpha'\), at \(\langle \bot \,;\, \bot \rangle\). The cases for \(\ensuremath{\mathsf{output}}\) and \(\ensuremath{\mathsf{dBl}}\) rewrite the progress-disclosure bound to the privileged consistent inputs at the whole trace (progressDisclosureBound_eq_of_bl_low, §6.5); its proof applies bridge_progress, which states that the second run takes a bridge when the blocking labels of the emitting state and of the end state of the reference bridge are visible, at each earlier visible event, and bridge_constructed_blockdecl at each earlier \(\ensuremath{\mathsf{dBl}}\) event, at the held authority of the certificate. Of the three, only bridge_constructed_blockdecl is also applied in the body of lemma2 (§9.3).

The three corollaries are the only declarations under Troupe/ that apply lemma2, so their bodies and their callers show how much of operational security the theorem uses. The next table gives, for each corollary, the statements that its body applies, by cases on the event, and the one lemma that calls it.

Every application of a restricted statement, (3b), (4b), (5) or (6b), is at the observer’s own authority: the authority of the event is the authority \(a\) of the observer (for (5), the authority join of the two authorities of the close), the acts-for hypothesis holds by Label.actsFor.refl, the list \(\overline\beta\) is empty, the chain is the one bridge (BridgeChainObs.cons hb .nil), and the restriction holds by its rule IndRestrictionObs.nil. Every corollary keeps the event relation of the conclusion and discards the relation between the end states. It follows that no call reaches the statements (1b) at \(\ensuremath{\mathsf{consumeInput}}\), (3a), (3b-ii), (4a) and (4b-ii), and that no call uses a restricted statement at a non-empty \(\overline\beta\) or at an authority other than the observer’s.

8 The guarantee of the theorem

We close by reading Theorem 1 back through the definitions: which bound holds of which event, for which observer, and what the statement leaves out. §8.1 then states the corollary of the theorem for programs without downgrades.

The guarantee.

Let \(\mathit{prog}\) be a well-formed program and \(i\) a well-formed supply, let the step of the monitored run after \(n\) steps emit an event \(\alpha\), and let \(\ell\) be a level that the level of \(\alpha\) flows to. Write \(t\) for the trace before the event and \(t^{+}\) for the trace with it. By Theorem 1 and Definitions 18 and 17:

• if \(\alpha\) is an output, the consistent inputs of the external observer at \(\ell\) after the output contain the internal consistent inputs before it, \(\Omega^{\mathsf{ext}}_{\ell }(t^{+}) \supseteq{}\)\(\Omega^{\mathsf{int}}_{\ell }(t)\), since on the monitored machine the progress-disclosure bound at the null authority is the internal consistent inputs at the whole trace (§6.5): a message that leaves the process tells its recipient nothing that an observer of the internal events at that level did not know; and the consistent inputs of the internal observer after the output contain the progress-consistent inputs before it, as for an event of case 2;

• if \(\alpha\) is a receive, a binding, a region open or a confined consume (case 2), the consistent inputs of the internal observer after it contain the progress-consistent inputs of that observer before it: the event tells the observer no more than that the run reached it;

• if \(\alpha\) is a value or type downgrade, a disclosing consume or a region close, the consistent inputs of the internal observer after it contain the progress-consistent inputs, before it, of the privileged observer who holds the authority of the event (Event.authOf): the downgrade releases to the observer at \(\ell\) what an observer with the authority already knew, and nothing else; for a value or type downgrade, moreover, every supply from which the run goes on to one more event observable at \(\ell\) goes on to a downgrade of the same kind, dimension, authority and target (the progress part of case 3);

• if \(\alpha\) is a blocking-label downgrade with authority \(a\), the consistent inputs of the internal observer after it contain the progress-consistent inputs before it (5b), and the progress-consistent inputs of the internal observer before it contain the consistent inputs of the privileged observer at \(a\,|\,\ell\) before it (5a), the progress-disclosure bound at the authority \(a\) being, on the monitored machine, the privileged consistent inputs at the whole trace (§6.5): the fact that the run gets past the downgrade is released under the authority \(a\).

What the statement permits.

The bounds are weaker than noninterference in three places, each visible in the examples. Case 2 bounds by the progress-consistent inputs, so a receive whose reachability depends on a secret is accepted: the program implicitRecvE, whose receive of presence \(\bot\) is in one branch of a test on a secret, is not refuted on the non-blocking machine (§6). Cases 3 and 4 bound by the consistent inputs of a privileged observer, so a downgrade under sufficient authority may separate supplies that the observer at \(\ell\) could not separate before: in the monitored run of declassifyReleaseOutputToEndpointE (§6) the internal consistent inputs at \(\bot\) over the family go from three supplies to one at the \(\ensuremath{\mathsf{dValType}}\) event. Case 3 bounds by progress-consistent inputs, so the reachability of a downgrade is itself a progress leak: the program declassifySecretOccurrenceE, which reaches a declassification only if a loop on a secret terminates, is not refuted on either machine. Finally, the condition bounds the events that a run emits and says nothing about a run that stops: the monitored run of Example 2 is stuck before its \(\mathsf{outputToEndpoint}\) step and emits no output, and the condition holds of it.

What the statement does not cover.

The following are facts about the definitions that the theorem is stated with. The model is one process: a configuration has one control and one continuation (§4), and the grammar of §3 has no instruction that starts a second thread, so the theorem says nothing about the interaction of several processes or about a scheduler. The supply of a run is fixed before the run: the initial configuration takes it as the mailbox, and no step rule adds a message to the mailbox, so a message that arrives during the run is not modelled. A set of consistent inputs contains a supply when some number of steps of its run gives the observation (Definition 15); the number of steps is not part of an observation, and an event has no field for time: the condition does not speak of time. The sets of consistent inputs contain well-formed supplies that the baseline relates to the supply of the run, and the condition has the well-formedness of that supply as its premise. The verdicts of the falsifier in the examples are about finite families of supplies, in the privileged part of case 3 and in case 4 about the bound with the raised level, and in the external part of case 1 and in (5a) about a certificate decided over the family (§6). The theorem is about the formal model; §4.7 lists the counterparts of its items in the Troupe implementation and the differences that the Lean development states.

8.1 Noninterference for downgrade-free programs

The bounds of cases 3 to 5 of Definition 17 let a downgrade shrink the consistent inputs of an observer below what the observer knew before it. When a run emits no such event, Theorem 1 gives more: at every level, the outputs of the run separate no supply that the visible messages of the supply do not already separate. We first name the events and the instructions in question, then state the corollary, first for a trace, then for a program.

The downgrade events are the events of cases 3, 4 and 5 of Definition 17: those whose bound takes the consistent inputs of a privileged observer, and the blocking-label downgrade. Every other event is an output or an event of case 2, and its bound contains the inclusion \(\Omega^{\mathsf{int}}_{\ell }(t^{+}) \supseteq{}\)\(\Omega^{\mathsf{int}}_{\ell ,\to}(t)\), the internal part of case 1 for an output and the whole bound of case 2 otherwise (Ω_internal_supset_prog_of_not_isDowngrade).

The four instructions are those whose rules emit the downgrade events: rule downgrade (Fig. 2) emits a \(\ensuremath{\mathsf{dVal}}\), \(\ensuremath{\mathsf{dType}}\) or \(\ensuremath{\mathsf{dValType}}\) event, rule blockDowngrade a \(\ensuremath{\mathsf{dBl}}\) event, rule close (Fig. 4) a \(\ensuremath{\mathsf{regionClose}}\) event, and rule consume (Fig. 1) a \(\ensuremath{\mathsf{dgConsumeInput}}\) event when it is a disclosing consume. A \(\ensuremath{\mathsf{consume}}\) is excluded whether or not it discloses: whether its event is \(\ensuremath{\mathsf{consumeInput}}\) or \(\ensuremath{\mathsf{dgConsumeInput}}\) depends on the labels of its operands at run time (step_consume_running_iff, §4), and the predicate is syntactic. The other reads stay: a downgrade-free program may contain \(\ensuremath{\mathsf{tyrecv}}\), \(\ensuremath{\mathsf{peek}}\), \(\ensuremath{\mathsf{enableRangedReceive}}\) and \(\ensuremath{\mathsf{rangedConsume}}\), whose events are of case 2, and it may open a receive region but contains no instruction that closes one. The docstring of Program.NoDowngrade gives the reason for the function table: a closure value names its code by an index into the function table, so the main body and the function table are all the code that a run can reach.

For the proof, the predicate is lifted to machine states: a state is downgrade-free (State.CodeNoDowngrade) when its control, every body of its function table and the continuation of every frame of its continuation stack are downgrade-free, and a configuration that is done or stuck is downgrade-free (Config.CodeNoDowngrade).

The right-hand side is the set of well-formed supplies that the baseline relates to \(i\); it is the internal consistent inputs at the empty trace (Ω_internal_nil), and it contains every set \(\Omega^{\mathsf{ext}}_{\ell }(o)\) (Ω_ext_subset_nil). The lemma thus says that after any prefix of a run without downgrade events, the external observer at \(\ell\) considers possible every supply it could not tell apart from \(i\) by the visible messages alone: the outputs of the run separate no further supply. The lemma speaks of the external consistent inputs only; it states nothing about the internal ones, which an event of case 2 may shrink.

The proof is by induction on \(n\). At \(n=0\) the trace is empty, and the two sets are equal by Ω_internal_nil and Ω_internal_subset_Ω_ext. At a step that emits no event, or an event that is not an output with a level that flows to \(\ell\), the projection \(\mathsf{obsIO}_\ell\) of the trace does not change, nor does the set (Ω_ext_congr_observableIO), and the induction hypothesis applies. At a step that emits an output observable at \(\ell\), the external part of case 1 bounds the external consistent inputs after the output from below by the progress-disclosure bound \(\Omega^{\mathsf{pd}}_{\langle \bot \,;\, \bot \rangle\,|\,\ell }(t)\) at the trace \(t\) before it (Definition 20), and that bound is the right-hand side (progressDisclosureBound_bot_eq_nil). The last equality rests on the certificate of Definition 19. At the null authority, every certified prefix \(s\) of the trace has the privileged consistent inputs of the empty trace, \(\Omega^{\mathsf{priv}}_{\langle \bot \,;\, \bot \rangle\,|\,\ell }(s) = \Omega^{\mathsf{priv}}_{\langle \bot \,;\, \bot \rangle\,|\,\ell }([\,])\) (okProg_Ω_internal_priv_eq_nil), by induction on the certificate. Rule nil is the empty trace. Rule block ends with a \(\ensuremath{\mathsf{dBl}}\) event, a downgrade event, which the hypothesis excludes. Rule ordinary extends a certified prefix \(s\) to \(t\mathbin{+\!\!+}[e]\); the event \(e\) is emitted at some step of the run (exists_eventAt_of_append_singleton_prefix), it is not a downgrade event, and it is visible at \(\ell\) (Event.observableAtPriv_bot), so \(\mathsf{TSS}\) gives \(\Omega^{\mathsf{int}}_{\ell }(t\mathbin{+\!\!+}[e]) \supseteq{}\)\(\Omega^{\mathsf{int}}_{\ell ,\to}(t)\). The premise of the rule gives \(\Omega^{\mathsf{int}}_{\ell ,\to}(t) \supseteq{}\)\(\Omega^{\mathsf{int}}_{\ell }(s)\) (at the null authority the privileged sets are the internal ones, Ω_internal_priv_bot, Ω_internal_prog_priv_bot), and the induction hypothesis says that \(\Omega^{\mathsf{int}}_{\ell }(s)\) is the set of the empty trace. The chain of inclusions bounds \(\Omega^{\mathsf{int}}_{\ell }(t\mathbin{+\!\!+}[e])\) from below by the set of the empty trace, which contains it. The progress-disclosure prefix is certified, since rule nil makes the greatest certified length exist (Nat.findGreatest_spec), so the progress-disclosure bound is the set of the empty trace.

The hypothesis of Lemma 12 is about the trace of the run. A downgrade-free program meets it at every supply and every number of steps: the initial configuration is downgrade-free (init_CodeNoDowngrade), every step keeps it so (step_preserves_CodeNoDowngrade), and a step from a downgrade-free state emits no downgrade event (step_event_not_isDowngrade_of_CodeNoDowngrade); together they give exec_trace_not_isDowngrade_of_noDowngrade.

With Theorem 1 in place of the hypothesis \(\mathsf{TSS}(\mathit{prog},i)\), the statement holds of every well-formed downgrade-free program under the monitor.

The statement quantifies over every level, including levels with a non-trivial integrity projection, and over every step of the monitored run, and its only hypotheses beyond those of Theorem 1 are that the program is downgrade-free and that the supply is well formed. It is declared as a lemma, as are the other two, and like the theorem it depends on the axioms propext, Classical.choice and Quot.sound only, which a #guard_msgs-checked #print axioms at the end of Troupe/Meta/Noninterference.lean pins.

let _ ← outputToEndpoint ⊥ 0
let s ← tyrecv {alice,bob} .int
let c ← lt 0 s
ifVal c (tyrecv ⊥ .int; ret 0) (call loop 0; ret 0)
let _ ← outputToEndpoint ⊥ 1

\(\Omega\)_ext at the empty trace:            [0, 1, 2]
monitored, member 0: ⊥ outputs [send {} ◁ 0@{}%{}]
  \(\Omega\)_ext at the whole trace:          [0, 1, 2]
monitored, member 1: ⊥ outputs [send {} ◁ 0@{}%{}]
  \(\Omega\)_ext at the whole trace:          [0, 1, 2]
monitored, member 2: ⊥ outputs [send {} ◁ 0@{}%{}]
  \(\Omega\)_ext at the whole trace:          [0, 1, 2]
non-blocking, member 2: ⊥ outputs
  [send {} ◁ 0@{}%{}, send {} ◁ 1@{}%{}]
  \(\Omega\)_ext at the whole trace:          [2]

9 Lean lemmas of the proof

This section is reference material for §7: for each step of the proof we tabulate the Lean lemma that proves it and the lemmas that this lemma calls, so that a reader of the Lean can find the place where a step of the account is carried out. The modules are under Troupe/Meta/; in the tables a label is called low when it is visible to the observer at hand.

9.1 Calls from the theorem to the unwinding lemma

The theorem monitorSatisfiesTSS (SecurityTheorem.lean) case-splits on the emitted event and calls one lemma named *_bound in each case (§7.7). The table follows the calls from these lemmas down to the three corollaries of lemma2 and to the lemmas of Lemma2.lean that the proof applies directly.

Where one of the three synced_* lemmas applies a restricted statement, the chain of one bridge is BridgeChainObs.cons hb .nil.

9.2 The invariants

The chain invariant.

Besides the fields listed in §4.5, the structure State.ChainWF (RegionChain.lean) has four fields that order the frames, and it is preserved by a step (step_preserves_ChainWF).

The remaining fields are kontSavedFresh, rootSavedFresh, kontScope, rootScope, headUnflaggedPc, rootUnflaggedPc, kontUnflaggedPc, lastUnflaggedPc, mailboxCapFree, tie, ctrlCapFree, funsCapFree and kontCapFree.

Equivalent forms of clauses of the state relation.

Three clauses of Definition 21 have an equivalent form over the lists of projected frame fields, which the one-step lemmas use. The base of the clause (inputs) is \(\mathsf{getLastD}\) of \(s_i.\mathit{regions}.\mathsf{map}\,({\cdot}.\mathsf{entryMailbox})\) with default \(s_i.\mathcal{M}\) (State.PrivLowEqC.inputs_packed); the clause (regionDepth) is equivalent to equal lengths of \(s_i.\mathit{regions}.\mathsf{map}\,({\cdot}.\mathsf{evidence})\) (State.PrivLowEqC.regionDepth_packed); and the clause (entryRegistersSync) is equivalent to the same position-by-position relation on \(s_i.\mathit{regions}.\mathsf{map}\,({\cdot}.\mathsf{entryRegisters})\) (State.PrivLowEqC.entryRegistersSync_packed).

The per-bridge invariant.

The fields of PrivBridgeInvS are named le, inv1, inv2, kont1, kont2, caps1, caps2, chainEq, regions and charged, in the order of §7.4.

The cases of bridgePreservesPrivS_lowStart:

The region invariants in one step.

The two lock-step lemmas (Unwinding/MatchedRegionsStep.lean) are stated for a pair in the relation State.PrivLowEqC with \(s_1.\mathit{pc}\sqsubseteq_{a}\ell\), one step of each state, and the hypothesis that the two emitted events, when the first is observable, are low-equivalent for \(a\,|\,\ell\). Each matches on the head instruction of \(s_1\).

In the \(\ensuremath{\mathsf{tyrecv}}\) and \(\ensuremath{\mathsf{consume}}\) rows of the right column the premise \(\mathit{ch}=\ensuremath{\mathsf{none}}\) of the rule gives, by State.ChainWF.collapse, that neither state has a region frame, and the obligation that remains is the conclusion of the field mailboxEmpty at the successors. Of the lemmas in the table only the two for \(\ensuremath{\mathsf{disableRangedReceive}}\) take the hypothesis on the emitted events; the \(\ensuremath{\mathsf{consume}}\) row of chargedRegions_lockstep uses it in the proof body.

9.3 The unwinding lemma

The body of lemma2 applies the following lemmas of Lemma2.lean to prove the statements of Definition 31.

The inductions are in lemmas that the body reaches: silentTail_couple_asym and silentTail_couple_forward, each by strong induction on the number of silent steps of the reference bridge, and bridgePreservesPrivS_lowStart (§9.2).