Secure Compilation and Robust Property Preservation

Prerequisites. Direct starred prerequisites: Chapter 134. No later core chapter depends on this route.

A semantics-preservation theorem quantifies over whole programs. Compile a component instead, and link it with a context, and the theorem is silent unless the context is the image of a source context.

Here is what that silence costs. Let a source language have a partial program that receives a boolean or a natural from its context and outputs a natural, and let the target have only naturals, with $\mathsf{true}$ and $\mathsf{false}$ compiled to $0$ and $1$. Compile $P=f(x:\mathsf{Bool})\mapsto e$ to On an input a source context could have produced — $0$ or $1$ — the compiled function runs the compiled body. On the input $2$ it diverges, and on every larger input it outputs $42$, whatever $P$ was. A whole-program correctness theorem is untouched: no whole source program ever supplies $2$. A user linking $P\downarrow$ with untrusted target code has lost every guarantee $P$ had.

The question this chapter answers is what a compiler must satisfy so that a property of the source component survives linking with an arbitrary target context, and how the resulting criteria are related to each other and to full abstraction. The development follows Abate, Blanco, Garg, Hriţcu, Patrignani and Thibault (2019).

The setting

The distinction is the one that makes the chapter necessary. A trace property is satisfied or violated by one execution; a hyperproperty may require comparing two, as noninterference does.

Robust preservation of trace properties

Definition 136.3 quantifies over all properties, which makes it awkward to prove for a particular compiler. It has an equivalent statement that mentions no property at all.

Proof of Theorem 136.5 — RTP and RTC are equivalent

Proof. The mechanism is worth naming once, because every other equivalence in this chapter uses it: from $\mathrm{RTP}$ to $\mathrm{RTC}$ one instantiates the universally quantified property with the strongest property the source program robustly satisfies; from $\mathrm{RTC}$ to $\mathrm{RTP}$ one uses the produced source context to transport the hypothesis.

$\mathrm{RTP}⟹\mathrm{RTC}$. Fix $P$, and apply $\mathrm{RTP}$ to the property ${\pi }_0=\{t\mid \mathrm{\exists }{C}_S.C_S[P]\Downarrow t\}$. Its hypothesis is $\mathrm{\forall }{C}_S,t.C_S[P]\Downarrow t⟹\mathrm{\exists }{C}_S^{\prime }.C_S^{\prime }[P]\Downarrow t$, which holds by taking $C_S^{\prime }=C_S$. Its conclusion is $\mathrm{\forall }{C}_T,t.C_T[P\downarrow ]\Downarrow t⟹t\in {\pi }_0$, and $t\in {\pi }_0$ is by definition the existence of a source context producing $t$. That is $\mathrm{RTC}$.

$\mathrm{RTC}⟹\mathrm{RTP}$. Fix $\pi$ and $P$ and assume $$\mathrm{\forall }{C}_S,t.C_S[P]\Downarrow t⟹t\in \pi .$$ Take any $C_T$ and $t$ with $C_T[P\downarrow ]\Downarrow t$. By $\mathrm{RTC}$ there is $C_S$ with $C_S[P]\Downarrow t$, and (136.1) instantiated at that $C_S$ and $t$ gives $t\in \pi$. ◻

Theorem 136.5 is what makes the criterion usable: to establish $\mathrm{RTP}$ one exhibits, for each target context, a source context that explains the same trace. Constructing that source context is called back-translation, and section 136.6 describes the two shapes it takes.

Safety, density, and their criteria

A safety property is refuted by a finite prefix: once the bad prefix has occurred, no continuation repairs it. A dense property can be refuted only by an infinite trace, and plays here the role liveness plays elsewhere.

Proof of Theorem 136.8 — Both characterizations are equivalent to their criteria

Proof. $\mathrm{RSP}⟹\mathrm{RSC}$. Fix $P$ and a finite prefix $m_0$ with $C_T[P\downarrow ]\Downarrow m_0$, and suppose no source context produces $m_0$. Put ${\pi }_1=\{t\mid m_0\nleqq t\}$. Then ${\pi }_1\in \mathrm{Safety}$: if $t\notin {\pi }_1$ then $m_0\le t$, and every $t^{\prime }\ge m_0$ also fails ${\pi }_1$, so $m_0$ is the required bad prefix. The hypothesis of $\mathrm{RSP}$ at ${\pi }_1$ holds, since a source context producing some $t\ge m_0$ would produce the prefix $m_0$, contrary to assumption. Its conclusion applied to the target trace extending $m_0$ gives a trace in ${\pi }_1$ that has $m_0$ as a prefix, a contradiction. So some source context produces $m_0$.

$\mathrm{RSC}⟹\mathrm{RSP}$. Fix $\pi \in \mathrm{Safety}$, $P$ satisfying (136.1), a target context $C_T$ and a trace $t$ with $C_T[P\downarrow ]\Downarrow t$; suppose $t\notin \pi$. Safety gives a bad prefix $m\le t$ with every extension outside $\pi$. Since $C_T[P\downarrow ]$ produces $t$, it produces $m$, so $\mathrm{RSC}$ gives $C_S$ with $C_S[P]\Downarrow m$. Extend: $C_S[P]$ produces some $t^{\prime }\ge m$, and (136.1) puts $t^{\prime }\in \pi$, contradicting the choice of $m$. Hence $t\in \pi$.

$\mathrm{RDP}⟺\mathrm{RDC}$. The same two moves with ${\pi }_0$ replaced by ${\pi }_2=\{t\mid t\text{ terminating}\}\cup \{t\mid \mathrm{\exists }{C}_S.C_S[P]\Downarrow t\}$, which is dense by construction, and with the observation that a dense property is violated only by a non-terminating trace, so only infinite traces need explaining. ◻

Proof of Theorem 136.9 — Decomposition

Proof. Let $\pi$ be arbitrary. Put $S(\pi )=\{t\mid \mathrm{\forall }m\le t.\mathrm{\exists }{t}^{\prime }\ge m.t^{\prime }\in \pi \}$ and $D(\pi )=\pi \cup \{t\mid t\notin S(\pi )\}$.

$S(\pi )$ is safety: if $t\notin S(\pi )$ there is $m\le t$ with no extension in $\pi$; every $t^{\prime }\ge m$ then also has $m$ as a prefix with no extension in $\pi$, so $t^{\prime }\notin S(\pi )$.

$D(\pi )$ is dense once terminating traces are read as those with a maximal finite prefix: a terminating $t$ either lies in $\pi$ or has a prefix with no extension in $\pi$, and in the second case $t\notin S(\pi )$, so $t\in D(\pi )$.

Finally $S(\pi )\cap D(\pi )=\pi$. For $\subseteq$: if $t\in S(\pi )$ and $t\in D(\pi )$, the second gives $t\in \pi$ or $t\notin S(\pi )$, and the first excludes the alternative. For $\supseteq$: $t\in \pi$ gives $t\in D(\pi )$ immediately, and $t\in S(\pi )$ because every prefix of $t$ extends to $t$ itself. ◻

Theorem 136.9 says that $\mathrm{RSP}$ and $\mathrm{RDP}$ together are not weaker than $\mathrm{RTP}$ for a fixed property — the property splits — but it does not say that the two criteria imply $\mathrm{RTP}$, because the hypothesis of $\mathrm{RTP}$ at $\pi$ does not give the hypotheses at $S(\pi )$ and $D(\pi )$ separately.

Hyperproperties

Proof of Theorem 136.11

Proof. $\mathrm{RHP}⟹\mathrm{RHC}$. Fix $P$ and apply $\mathrm{RHP}$ to $H_0=\{b\mid \mathrm{\exists }{C}_S.b=\mathrm{Behav}(C_S[P])\}$, whose hypothesis holds by taking the same context. The conclusion says that every target context’s behaviour is some source context’s behaviour, which is $\mathrm{RHC}$.

$\mathrm{RHC}⟹\mathrm{RHP}$. Given $H$, $P$ with $\mathrm{Behav}(C_S[P])\in H$ for all $C_S$, and any $C_T$, $\mathrm{RHC}$ supplies $C_S$ with equal behaviour, so $\mathrm{Behav}(C_T[P\downarrow ])\in H$.

The subset-closed pair is the same argument with $H_1=\{b\mid \mathrm{\exists }{C}_S.b\subseteq \mathrm{Behav}(C_S[P])\}$, which is subset-closed, in place of $H_0$; the conclusion then gives an inclusion rather than an equality, and in the converse direction subset-closure of $H$ is what turns the inclusion supplied by $\mathrm{RSCHC}$ into membership. ◻

Full abstraction is a different criterion

For determinate languages contextual equivalence coincides with equality of the trace sets produced in all contexts, so $\mathrm{OEP}$ coincides with robust preservation of trace equivalence. How that criterion relates to the ones above it is not what one might expect, and the next theorem settles one direction.

Proof of Theorem 136.14 — Full abstraction does not imply robust safety preservation

Proof. The compiler is the one displayed in the opening. Source partial programs take a boolean or a natural from the context and output naturals; the target has only naturals; $\mathsf{true}$ and $\mathsf{false}$ compile to $0$ and $1$; and a boolean-accepting $P=f(x:\mathsf{Bool})\mapsto e$ compiles to

Correctness. A whole source program supplies only $\mathsf{true}$ or $\mathsf{false}$, hence only $0$ or $1$, so the first branch is taken and the compiled program runs $e\downarrow$. Compilation is compositional in the function definitions, so separate compilation holds.

$\mathrm{OEP}$. Let $P_1$ and $P_2$ be contextually equivalent source programs. A target context can feed $P_1\downarrow$ and $P_2\downarrow$ an input below $2$, where both behave as the corresponding source programs under the corresponding source context and are therefore indistinguishable; the input $2$, where both diverge; or an input above $2$, where both output $42$. In every case the two compiled programs agree, so they are contextually equivalent.

Failure of $\mathrm{RSP}$. Take $P=f(x:\mathsf{Bool})\mapsto 0$ and the safety property $\pi =\{t\mid t\text{ contains no output }42\}$. Every source context linked with $P$ produces the single output $0$, so $P$ robustly satisfies $\pi$. The target context supplying $3$ makes $P\downarrow$ output $42$, violating $\pi$. Hence $\mathrm{RSP}$ fails. ◻

Theorem 136.14 is the reason the chapter’s criteria are not a reformulation of full abstraction. Full abstraction constrains only which programs the target can distinguish; it permits the compiled program to do anything at all, provided it does the same anything to equivalent programs.

This is Theorem 5.1 of the frozen source, with the mechanized proof in its Coq development. It is imported at exactly those hypotheses: determinacy of both languages, input totality of the target — if the target accepts one input value it accepts every other — and the property, also proved there, that a whole program producing every finite prefix of an infinite trace produces that trace. Nothing weaker is claimed, and no direction of theorem 136.14 is affected by it.

Back-translation

The characterizations of section 136.2, section 136.4 all require producing a source context from a target context. Two techniques do this, and they trade strength for generality.

The trade is exact. The first technique must embed an arbitrary target context, which requires knowing enough about the target language to simulate all of it; the second only has to replay a finite interaction, so it depends on the calls-and-returns interface between context and program and on nothing else. The first yields the strongest criterion; the second does not yield $\mathrm{RHC}$.

Limits and seminar

The frozen source is Abate, Blanco, Garg, Hriţcu, Patrignani and Thibault (2019). Definition 136.3, Definition 136.4, Definition 136.6, Definition 136.7, Definition 136.10, Definition 136.13 and theorem 136.5, theorem 136.8, theorem 136.11, theorem 136.14, theorem 136.15 are its definitions and theorems, at their exact statements; the proofs of theorem 136.5, theorem 136.8, theorem 136.11, theorem 136.14 are written out here. Theorem 136.9 is its Theorem B.7, proved here. Theorem 136.15 is imported and not reproved.

Five boundaries. First, every criterion is a statement about a compilation chain and a fixed notion of trace; changing what an event records changes every criterion, and no result here says which events a real compiler should emit. Second, none of the criteria is a theorem about any particular compiler: this chapter proves equivalences between criteria and one separation, and exhibits no verified secure compiler. Third, the criteria say nothing about cost: a compiler can satisfy $\mathrm{RSP}$ by inserting arbitrary dynamic checks, and exercise 136.3 is exactly that observation. Fourth, theorem 136.14 separates full abstraction from robust safety preservation for determinate languages only; the relationship in the presence of internal nondeterminism is not settled here. Fifth, the two back-translation techniques of section 136.6 are described, not carried out: no universal embedding is constructed in this chapter.

[4]

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 136.5, then complete exercise 136.8.

Exercise 136.5¶

★★☆ Order $\mathrm{RTP}$, $\mathrm{RSP}$, $\mathrm{RDP}$, $\mathrm{RHP}$ and $\mathrm{RSCHP}$ by implication, proving each implication from the property-free characterizations and giving a counterexample chain for each non-implication you claim. State which orderings your argument leaves open.

Referenced from 3 locations

• Secure Compilation and Robust Property Preservation

Exercise 136.6¶

★★★ Termination-insensitive noninterference is a hyperproperty, not a trace property. Write it as a set of sets of traces for a language whose events record public outputs, show that it is subset-closed, and conclude which of the criteria of this chapter suffice to preserve it robustly. Then exhibit a compiler satisfying $\mathrm{RSP}$ that does not preserve it.

Referenced from 2 locations

• Secure Compilation and Robust Property Preservation

Exercise 136.7¶

★★★ For a source language with first-order functions over naturals and a target that adds arbitrary jumps, sketch a universal embedding of target contexts into source contexts, or identify the target feature that makes one impossible. If it is impossible, give the strongest criterion of this chapter that a trace-based back-translation still yields.

Referenced from 2 locations

• Secure Compilation and Robust Property Preservation

Exercise 136.8 — Practical: criteria checker¶

★★★ Practical project.sec-criteria-checker Complete project sec-criteria-checker. For a finite model — a finite set of traces, finitely many source and target contexts, and a table giving the traces each linked program produces — implement (i) the predicates $\mathrm{Safety}$ and $\mathrm{Dense}$ of definition 136.6, (ii) the criteria $\mathrm{RTP}$, $\mathrm{RSP}$ and $\mathrm{RHP}$ and the characterizations $\mathrm{RTC}$, $\mathrm{RSC}$ and $\mathrm{RHC}$ by exhaustive search over the finite model, and (iii) the decomposition $\pi \mapsto (S(\pi ),D(\pi ))$ of theorem 136.9. The invariant the implementation must maintain is that on every model in the fixture the criterion and its characterization agree, which is theorem 136.5, theorem 136.8, theorem 136.11 restricted to that model. The named cases print

rtp-iff-rtc: ok
rsp-iff-rsc: ok
rhp-iff-rhc: ok
decomposition: ok
fa-model-violates-rsp: confirmed

The checker is independent evidence on the finite models in the fixture; it does not prove theorem 136.5, theorem 136.8, theorem 136.11, theorem 136.9, which quantify over all traces and all properties, and it contains no compiler, no back-translation and no infinite traces.

Referenced from 3 locations

• Secure Compilation and Robust Property Preservation