Introduction to Formal Compiler Security

This blog-post tries to give a formal introduction to compiler security. If you are already familiar with the term robust preservation, this blog-post is likely not for you. The post is accompanied by a Coq mechanization, i.e., all proofs presented in this blog-post are machine-checked. Find the link for it at the bottom of the post.

Preliminaries

Why formal methods?

Starting out in computer science, I’ve been very much into practical stuff. Writing “cool” algorithms, optimizing the hell out of the classic raytracer that everyone has to write at some point, and, well, designing a compiler. My first ever compiler was for a subset of the C programming language and it was inherently incorrect: It failed to faithfully translate the recursive version of Fibonacci: The compiler just wrote to some static memory location and forgot about the contents of the variables by overwriting the old location. In other words, my compiler did not make use of the stack at all, neither did it simulate it somehow, ending up with compiled programs that don’t behave the way I expected them to behave.

This expectation for program behavior should be written down somewhere, e.g., the C programming language dictates in its standard ( Citation: WG14/N1256 2007 September WG14/N1256. 2007 September . Programming languages — C ) the way a C program should run. In there, one can see a bunch of Backus-Naur-Forms defining the concrete syntax. Moreover, prose describes the semantics (what should happen under certain consequences, e.g., calling a function pointer is the same as dereferencing and then calling it). These rules give a more or less precise understanding how the programming language works and what programmers expect. Even though there have been studies that suggest differently ( Citation: Xu et.al. 2023 Jianhao Xu and Kangjie Lu and Zhengjie Du and Zhu Ding and Linke Li and Qiushi Wu and Mathias Payer and Bing Mao. 2023 . Silent Bugs Matter: A Study of Compiler-Introduced Security Bugs ) , the point I’m trying to make here is that every C programmer has some kind of mental model of how their program behaves. It turns out that specifying the semantics of programming languages is itself a tricky problem. As an example, for C, in certain contexts, the evaluation order is left implementation-defined, so there can be differences in the result of the expression f() + g() for the following program when compiled with different C compilers:

int x = 0;
int f() { x = x - 1; return x; }
int g() { x = x + 1; return x; }

If f() is evaluated first, the value of f() + g() is -1. If g() is evaluated first, the value of f() + g() is 1.

A formal, mathematical, specification gives a precise understanding on how something works. While it do can be ambiguous by design (by introducing non-determinism as a “feature” to the language), it cannot be ambiguous “by language”. It is also the most convincing argument one can do: Starting with stuff that is irrefutably obvious, inducing other facts from these by means of rules given by the logic we do reasoning in, there is no chance to say “your argument doesn’t make sense” without questioning the logic to begin with. It is the very core reason why we do math/logic.

Utilizing formal methods to prove that programs adhere to a specification is also much more powerful than unit- or property-based testing. Consider the following program:

void add(int x, int y) {
  if(x == 17290001 && y == 29171373) {
    return x - y;
  }
  return x + y;
}

For almost all inputs x and y, it is correct. A :shit:ton of tests are still very unlikely to find the bug where the function does not fulfill the intended specification “add number x and y”.

What are properties?

So, we want to verify programs. One way of looking at programs is to do so abstractly: Programs may perform some events that may have an effect to the “outside world”, like reading from or writing to memory. These events are also known as atomic propositions, commonly referred to as $\operatorname{AP}$. This post will only use the terminology “event”. The formal description of an event can be done with a Backus-Naur-Form without any metavariable/non-terminal symbol:

This is an example of a formal definition for concrete events: the empty event ($\varepsilon$), the event signaling that a program starts ($\text{Start}$), and the event signaling program termination ($\text{End}\ v$). The empty event is usually included to refer to unimportant/unobservable/internal actions (you may see this being referred to as $\lambda$ instead of $\varepsilon$ in the literature, some even use $\tau$). Note that $\text{End}$ carries a parameter $v$, which I have not defined precisely, but which is supposed to be “just some value”, like true, false, or 1729.

A program may emit multiple events (written $\overline{a}$) and, depending on what properties interest us, the concrete events wanted from program execution may need to change. In the verification domain, programs yield (potentially) infinitely sized lists of events, which are known as traces.

Even in this very simple setting where the only “interesting” events are $\text{Start}$ and $\text{End}\ v$, it is possible to define interesting properties for programs, which will be done soon. First up, it is necessary to make sense of the term property from the formal perspective: A trace property ($\pi$) is simply a set of traces (e.g., Trace -> Prop in Coq). For example, the property “termination” may be formulated as “any trace $\overline{a}$ which at some point contains an $\text{End}\ v$ event”. More formally:

Hereby, the $\vDash$ means “satisfies” and the $\diamond$ is a unary operator reading “eventually”. $\pi_{\text{term}}$ is an example for a liveness property, which intuitively concerns that “something good happens”. Even if the good thing did not happen yet, it could still happen at some point!

Having seen a liveness property, let us see an example for another class of properties, the safety properties. For this, let’s try to formulate “non-termination”: “any trace $\overline{a}$ which never contains an $\text{End}\ v$ event”. Formally:

The $\square$ reads “always” and the $\neg$ is simply “not”.

Safety and liveness are the two big properties, but there also exist properties which are neither safety nor liveness (because they are both!). But anyhow, the crucial bit to keep in mind for the rest of the blog post is that properties are sets of traces.

(Robust) Satisfaction

Suppose $\gamma$ is a compiler that translates from language $\src{S}$ to language $\trg{T}$.

Def. Property Satisfaction

A program $w$ satisfies a property $\pi$ ($w\vdash\pi$) if its execution yields a trace $\overline{a}$ such that $\overline{a}\in\pi$.

It is easy for a compiler to make sure target programs never go wrong: Just always emit a program that corresponds to the constant $\trg{42}$. But, this is very much not satisfactory. The intuition of programmers is that compiled $\trg{T}$-level programs behave similar to the original $\src{S}$ program! This “behaves similar” is precisely the intuition for preservation, given some compiler $\gamma$:

Def. Preservation of Property Satisfaction

For any property $\pi$ and $\src{S}$-level program $\src{w}$, if $\src{w}\vdash\pi$, then $\gamma(\src{w})\vdash\pi$.

Notice how $\src{w}\vdash\pi$ has a hidden assumption: program execution of $\src{w}$ can actually yield a trace. The issue is that this is not how a programmer writes a program. To illustrate why, consider this C function:

void foo() {
  printf("hello");
}

A very basic C function that makes crucial use of printf, a function that is not defined in the above excerpt! In fact, one would have to compile this snippet and then link the result with an implementation of the C standard library, which provides a definition for printf. While this is only one of many possible scenarios, in reality, people use libraries daily, no questions asked. To accurately model preservation of properties with this in mind, the blog-post refers to programs written by the programmer as components and to any library providing definitions for, e.g., undefined functions, as contexts. Property satisfaction is only defined on whole programs, so it does not work for components, because they are partial programs where not every symbol has an accompanying definition. A natural extension to make is to generalize this to arbitrary contexts. To this end, revisit property satisfaction and take arbitrary contexts into account:

Def. Robust Property Satisfaction

A component $p$ robustly satisfies a property $\pi$ ($p\vdash_R\pi$) if there is a whole program $w$ that is the result of linking an arbitrary context $C$ with the component $p$ such that the execution of $w$ yields a trace $\overline{a}$ that fulfills $\overline{a}\in\pi$.

Consider this C function and the compiled ARM64 output:

extern int arr[5];

int foo(int idx) {
  return arr[idx];
}

foo(int):
  adrp x1, arr
  add x1, x1, arr
  ldr w0, [x1, w0, sxtw 2]
  ret

Looking at the code, the compiler translates this as expected: perform an array access to some pre-defined constant arr. However, it is easy to see that there is a potential memory safety issue: A context that somewhere invokes foo(1729) will lead to an out-of-bounds memory access, which is a spatial memory safety violation. This means $\texttt{foo}\vdash_R\text{smssafe}$ does not hold, since $\texttt{foo}$ does not satisfy the property $\text{smssafe}$ (no out-of-bounds accesses) for all possible contexts.

A potential fix is to make it robust by inserting a bounds-check:

extern int arr[5];

int foo(int idx) {
  if(0 <= idx && idx < 5) {
    return arr[idx];
  }
  abort();
}

Now, $\texttt{foo}\vdash_R\text{smssafe}$ holds.

Secure Compilation

The lifting of preservation of a source behavior in the target simply uses robust satisfaction :

Def. Robust Trace Property Preservation

For any property $\pi$ and $\src{S}$-level program $\src{p}$, if $\src{p}\vdash_R\pi$, then $\gamma(\src{p})\vdash_R\pi$.

Notably, in the assumption $\src{p}\vdash_R\pi$ , the context is at $\src{S}$-level, while for the goal $\gamma(\src{p})\vdash_R\pi$ the context is at $\trg{T}$-level. Now, if you think of $\trg{T}$ as something like ARM64, program contexts easily appear much more powerful than for $\src{S}$, which could be something like Rust. In Rust, one is not able to just guess some memory address (without unsafe), while this works without issue in ARM64, assuming one guesses correctly.

Lets see how one could try to prove robust preservation . On the left there are the assumptions that we are allowed to work with, on the right there is the goal we need to prove. The diagram is supposed to be read from top to bottom.

Looking at the proof context, i.e., the assumptions that we have, we have to show that this trace $\overline{a}$ is part of whatever property $\pi$, where the only thing we know about $\overline{a}$ is that it is the result of the execution $\trg{link\ C\ }\llbracket\src{p}\rrbracket^{\src{S}\to\trg{T}}\to\overline{a}$. Since $\pi$ is arbitrary, there is little hope to show that $\overline{a}$ is an element of it by decomposing this $\trg{T}$-level execution. But, note that there is also assumption $H_1'$ . We certainly can specialize it with $\overline{a}$, but then we need to provide an $\src{S}$-level context as well as an execution $\src{link\ C\ p}\to\overline{a}$, both of which we do not have. This is the crucial part in these kinds of robust preservation proofs: somehow coming up with an $\src{S}$-level context $\src{C}$ whose runtime behavior when linked with $\src{p}$ is similar to that of $\trg{link\ C\ }\llbracket\src{p}\rrbracket^{\src{S}\to\trg{T}}$.

In the rest of this post, we’ll see how to do this on the basis of backtranslating the trace $\overline{a}$.

$\src{S}$ Definitions

$\src{S}$ Syntax

(** Possible binary operations. *)
Variant binopsymb : Type :=
| Badd : binopsymb
| Bsub : binopsymb
| Bmul : binopsymb
| Bdiv : binopsymb
| Bless : binopsymb
.
(** Value *)
Inductive value : Type :=
| Vnat : nat -> value
| Vbool : bool -> value
.
(** Variables are just strings. *)
Definition vart := string.

(** Expression *)
Inductive expr : Type :=
| Xval (v : value) : expr
| Xvar (x : vart) : expr
| Xbinop (symb : binopsymb) (lhs rhs : expr) : expr
| Xif (c e0 e1 : expr) : expr
| Xabort : expr
.
(** Type *)
Inductive ty : Type :=
| Tnat : ty
| Tbool : ty
| Tfun : ty -> ty -> ty
.

Hereby, $\src{x}$ is some kind of string and $\src{\oplus}$ is one of the following binary operations: $\src{<}$, $\src{+}$, $\src{\times}$, $\src{/}$, and $\src{-}$. We do not encode precedence or anything into this formal description, because it is more meant to be a generator for abstract syntax trees instead of a context free grammar. That being said, the precedences of the binary operators are “as usual”.

Another rather syntactic comment I have to make is the fact that some metavariables appear “free” in the above definition, e.g., $\src{e_1}$ in the binary operation rule. I sketch the “basename” of the metavariable $\src{e}$ and add subscripts as a means to signal that both branches in an expression like $\src{e_1\oplus e_2}$ can be different. If I’d have written it as $\src{e\oplus e}$, there could be confusion that you have to insert the same syntactic block into each branch, i.e., you can only have expressions like $\src{val\ 1+val\ 1}$, but not $\src{val\ 1+val\ 2}$. Admittedly, the rule for expressions should quantify over all used metavariables, i.e., the full, formal definition of the Backus-Naur-Form rule would look like $\src{Exprs}\ni\src{e_1,e_2,e_3}::=\dots$, where "$\dots$" as above. $\src{Exprs}$ hereby describes a set that contains all words adhering to the syntax on the righthandside of the ::= operator. Anyhow, I think this notation is still somewhat understandable while lessening the burden of parsing what I’ve written.

While we have expressions now, we still lack contexts and whole programs. The following definitions make this precise:

(** Symbols look like `fn foo x : τ := e` *)
Definition symbol : Type := vart * ty * ty * expr.

(** Viable contexts that can be linked against a symbol. *)
Inductive LinkageContext : Type :=
(* basically models `let y = call foo e__pre in e__post` *)
| LContext (y : vart) (e__pre e__post : expr) : LinkageContext
.

(** Top-level programs *)
Inductive prog : Type := Cprog (C : LinkageContext) (foo : symbol) : prog.

Again, this is meant to be abstract syntax. The intuitive understanding for compontents is simply a function, in imaginative syntax, $\src{fn(x : \tau) : \tau := e}$. Similarily, contexts are simply a let-expression that “calls” into this function, again in imaginative syntax, $\src{let\ y\ =\ call\ p\ e_{pre}\ in\ e_{post}}$. We’ll see the dynamic semantics of this soon, but first, let’s take a look at the static semantics, i.e., what it means for a program to be considered valid/safe.

$\src{S}$ Static Semantics

(** Type system spec *)
Reserved Notation "'[' Γ '|-' e ':' τ  ']'" (at level 81, Γ at next level, e at next level, τ at next level).
Inductive check : Gamma -> expr -> ty -> Prop :=
| T_var : forall (Γ : Gamma) (x : vart) (τ : ty),
  nodupinv Γ ->
  Min Γ x τ ->
  [Γ |- Xvar x : τ]
| T_abort : forall (Γ : Gamma) (τ : ty),
  [Γ |- Xabort : τ]
| T_vnat : forall (Γ : Gamma) (n : nat),
  [Γ |- Xval(Vnat n) : Tℕ]
| T_vbool : forall (Γ : Gamma) (b : bool),
  [Γ |- Xval(Vbool b) : Tbool]
| T_binop : forall (Γ : Gamma) (b : binopsymb) (e1 e2 : expr),
  b <> Bless ->
  [Γ |- e1 : Tℕ] ->
  [Γ |- e2 : Tℕ] ->
  [Γ |- Xbinop b e1 e2 : Tℕ]
| T_binop_less : forall (Γ : Gamma) (e1 e2 : expr),
  [Γ |- e1 : Tℕ] ->
  [Γ |- e2 : Tℕ] ->
  [Γ |- Xbinop Bless e1 e2 : Tbool]
| T_if : forall (Γ : Gamma) (e0 e1 e2 : expr) (τ : ty),
  [Γ |- e0 : Tbool] ->
  [Γ |- e1 : τ] ->
  [Γ |- e2 : τ] ->
  [Γ |- Xif e0 e1 e2 : τ]
where "'[' Γ '|-' e ':' τ ']'" := (check Γ e τ)
.

The typing rules for expressions are rather straightforward. Typechecking binary operations is split into $\src{S}\text{-t-binop}$ and $\src{S}\text{-t-less}$ , since comparisons should return a boolean value and anything else a number.

Typechecking contexts, components, and whole programs closely follows the standard “let”-rule when typechecking more complicated programming languages.

(** Checking of symbols. A symbol may use the identifier x, because a symbol
  in this language is basically fn(x) ↦ e. *)
Inductive check_symb : symbol -> Prop :=
| check_symb_c : forall (e : expr) (x : vart),
  check (x ↦ Tℕ ◘ [⋅]) e Tℕ ->
  check_symb (x, Tℕ, Tℕ, e)
.
(** Similarily, contexts are like `let y = call foo e__pre in e__post` *)
Inductive check_ctx : LinkageContext -> Prop :=
| check_ctx_c : forall (y : vart) (e__pre e__post : expr),
  [[⋅] |- e__pre : Tℕ] ->
  [y ↦ Tℕ ◘ [⋅] |- e__post : Tℕ] ->
  check_ctx (LContext y e__pre e__post)
.
(** Checking a top-level program just means checking both context and component *)
Definition prog_check (p : prog) : Prop :=
let '(Cprog C foo) := p in
check_symb foo /\ check_ctx C
.

$\src{S}\text{-t-whole}$ restricts components to be of type $\src{\mathbb{N}\to\mathbb{N}}$.

$\src{S}$ Dynamic Semantics

Since the language is so simple, the dynamic semantics are also simple, like the typing rules. The semantics is done small-step style with evaluation contexts, thereby sidestepping the need for congruence rules. Evaluation does not happen on expressions themselves, but rather on “runtime expressions”. Moreover, execution may give visible events (something like syscalls), which warrants a trace-model:

(** A runtime program is just an expression or a crashed state. *)
Inductive rtexpr : Type :=
| RTerm (e : expr)
| RCrash
.
#[global]
Notation "'▷' e" := ((RTerm e) : rtexpr) (at level 81, e at next level).
#[global]
Notation "'▷↯'" := (RCrash).

With this, primitive reductions are defined as follows:

(** Evaluation of binary expressions. Note that 0 means `true` in S, so `5 < 42` evals to `0`. *)
Definition eval_binop (b : binopsymb) (n0 n1 : nat) : option value :=
Some((match b with
     | Bless => (if Nat.ltb n0 n1 then Vbool true else Vbool false)
     | Badd => Vnat(n0 + n1)
     | Bdiv => Vnat(Nat.div n0 n1)
     | Bsub => Vnat(n0 - n1)
     | Bmul => Vnat(n0 * n1)
     end))
.
(** Primitive evaluation steps. *)
Inductive pstep : (PrimStep rtexpr) :=
| e_binop : forall (n1 n2 : nat) v (b : binopsymb),
  Some(v) = eval_binop b n1 n2 ->
  ▷ Xbinop b n1 n2 --[]--> ▷ v
| e_if_true : forall (e1 e2 : expr),
  ▷ <( if true then (e1) else (e2) )> --[]--> ▷ e1
| e_if_false : forall (e1 e2 : expr),
  ▷ <( if false then (e1) else (e2) )> --[]--> ▷ e2
| e_abort :
  ▷ <( abort )> --[ Scrash ]--> ▷↯
.

All steps without an event above the arrow implicitly throw the empty event ($\src{\varepsilon}$). While these definitions allow us to evaluate a runtime expression like $\src{\rtexpr{}{val\ 1+val\ 2}}$, it fails to apply for stuff like $\src{\rtexpr{}{(val\ 1+val\ 2)+val\ 3}}$. In order to be able to reduce these more complicated expressions, we decompose them into evaluation contexts and primitive expressions. The idea of evaluation contexts is that of a continuation, i.e., “the remaining continuation”. When evaluating something like $\src{\rtexpr{}{(val\ 1+val\ 2)+val\ 3}}$, there is an outermost part that stays the same when evaluating, in this case $\src{\square+val\ 3}$. So, let’s define evaluation contexts:

(** We proceed to define the dynamic semantics via evaluation contexts/environments. *)
Inductive evalctx : Type :=
| Khole : evalctx
| KbinopL (b : binopsymb) (K : evalctx) (e : expr) : evalctx
| KbinopR (b : binopsymb) (n : nat) (K : evalctx) : evalctx
| Kif (K : evalctx) (e0 e1 : expr) : evalctx
.

Filling the hole ($\src{\square}$) of an evaluation context with some expression $\src{e}$ is written $\src{E[e]}$. With that, define context-based reduction as follows:

(* Contextual steps may either have a subexpression that can do a primstep or
 have a subexpression that crashes. *)
Inductive estep : EctxStep rtexpr :=
| E_ectx : forall (e e' e0 e0' : expr) (o : option event) (K : evalctx),
  e0 = insert K e ->
  e0' = insert K e' ->
  ▷ e --[, o ]--> ▷ e' ->
  ▷ e0 ==[, o ]==> ▷ e0'
| E_stuck : forall (e e0 : expr) (K : evalctx),
  e0 = insert K e ->
  ▷ e --[ Scrash ]--> ▷↯ ->
  ▷ e0 ==[ Scrash ]==> ▷↯
.

To evaluate multiple steps, simply take the reflexive transitive closure $\src{\stepsarrow{\trace}}$. To evaluate multiple steps in $n$, simply count down $n$ for each transitive step and only if it is $0$ allow reflexive steps. When taking multiple steps, the trace $\src{\trace}$ only collects events that are non-empty - and, the way we have defined the relations, it’s either a singleton list containing the crash event (:zap:), or it is the empty list. The other events will become relevant for the top-level execution, which we define now.

Inductive progstep : prog -> tracepref -> rtexpr -> Prop :=
| prog_step_success : forall (x__foo y : vart) (e__pre e__post e__foo : expr) (foo : symbol) (v v__pre v__foo : value)
                      (n__pre n__foo n__post : nat),
  check_symb foo ->
  (* with traces, we cheat a little. All steps of the language are internal (i.e., they do not produce an action)
     To actually emit traces, we just hardcode them at the top-level... *)
  x__foo = vart_of_symbol foo ->
  e__foo = expr_of_symbol foo ->
  (* setup the argument for the function call *)
  ▷ e__pre =( n__pre )=[ nil ]==> ▷ Xval v__pre ->
  (* do the function call *)
  ▷ (subst x__foo e__foo (Xval v__pre)) =( n__foo )=[ nil ]==> ▷ Xval v__foo ->
  (* something may happen after the function call *)
  ▷ subst y e__post (Xval v__foo) =( n__post )=[ nil ]==> ▷ Xval v ->
  progstep (Cprog (LContext y e__pre e__post) foo)
           (Sstart :: Scall Qctxtocomp (sv v__pre) :: Sret Qcomptoctx (sv v__foo) :: Send (sv v) :: nil)
           (RTerm (Xval v))
| prog_step_failure0 : forall (y : vart) (e__pre e__post : expr) (foo : symbol) (n__pre : nat),
  (* wether component is well-typed or not does not matter if the context yields a crash *)
  (* with traces, we cheat a little. All steps of the language are internal (i.e., they do not produce an action)
     To actually emit traces, we just hardcode them at the top-level... *)
  (* setup the argument for the function call ; fails *)
  ▷ e__pre =( n__pre )=[ Scrash :: nil ]==> (▷↯) ->
  progstep (Cprog (LContext y e__pre e__post) foo)
           (Sstart :: Scrash :: nil)
           (▷↯)
| prog_step_failure1 : forall (x__foo y : vart) (e__pre e__post e__foo : expr) (foo : symbol) (v__pre : value)
                       (n__pre n__foo : nat),
  check_symb foo ->
  (* with traces, we cheat a little. All steps of the language are internal (i.e., they do not produce an action)
     To actually emit traces, we just hardcode them at the top-level... *)
  x__foo = vart_of_symbol foo ->
  e__foo = expr_of_symbol foo ->
  (* setup the argument for the function call *)
  ▷ e__pre =( n__pre )=[ nil ]==> ▷ Xval v__pre ->
  (* do the function call ; fails *)
  ▷ (subst x__foo e__foo (Xval v__pre)) =( n__foo )=[ Scrash :: nil ]==> (▷↯) ->
  progstep (Cprog (LContext y e__pre e__post) foo)
           (Sstart :: Scall Qctxtocomp (sv v__pre) :: Scrash :: nil)
           (▷↯)
| prog_step_failure2 : forall (x__foo y : vart) (e__pre e__post e__foo : expr) (foo : symbol) (v__pre v__foo : value)
                       (n__pre n__foo n__post : nat),
  check_symb foo ->
  (* with traces, we cheat a little. All steps of the language are internal (i.e., they do not produce an action)
     To actually emit traces, we just hardcode them at the top-level... *)
  x__foo = vart_of_symbol foo ->
  e__foo = expr_of_symbol foo ->
  (* setup the argument for the function call *)
  ▷ e__pre =( n__pre )=[ nil ]==> ▷ Xval v__pre ->
  (* do the function call *)
  ▷ (subst x__foo e__foo (Xval v__pre)) =( n__foo )=[ nil ]==> ▷ Xval v__foo ->
  (* something may happen after the function call; fails *)
  ▷ subst y e__post (Xval v__foo) =( n__post )=[ Scrash :: nil ]==> (▷↯) ->
  progstep (Cprog (LContext y e__pre e__post) foo)
           (Sstart :: Scall Qctxtocomp (sv v__pre) :: Sret Qcomptoctx (sv v__foo) :: Scrash :: nil)
           (▷↯)
| prog_step_failure3 : forall (x__foo y : vart) (e__pre e__post e__foo : expr) (foo : symbol) (v__pre : value)
                       (n__pre : nat),
  (* this is a dirty hack to sidestep more formalization work. we want ill-typed components to "crash", but it's a hassle
     to extend small step and bigstep accordingly. So, instead, we do it at the top level execution relation of programs *)
  ~(check_symb foo) ->
  (* with traces, we cheat a little. All steps of the language are internal (i.e., they do not produce an action)
     To actually emit traces, we just hardcode them at the top-level... *)
  x__foo = vart_of_symbol foo ->
  e__foo = expr_of_symbol foo ->
  (* setup the argument for the function call *)
  ▷ e__pre =( n__pre )=[ nil ]==> ▷ Xval v__pre ->
  (* since the component is ill-typed, just crash immediately *)
  progstep (Cprog (LContext y e__pre e__post) foo)
           (Sstart :: Scall Qctxtocomp (sv v__pre) :: Scrash :: nil)
           (▷↯)
.

Since the language only has one call, it can be hardcoded in the semantics by simulating the reduction of a nested let-expression, as done in $\src{S}\text{-eprog-success}$ .

The rules $\src{S}\text{-eprog-fail0}$ , $\src{S}\text{-eprog-fail1}$ , and $\src{S}\text{-eprog-fail2}$ encode all possibilities where either the context or the component crashes: the component could fail or the context can fail prior to calling in $\src{e_{pre}}$ or it can fail in $\src{e_{post}}$ after the component returned. Lastly, $\src{S}\text{-eprog-fail3}$ is a rather nasty/lazy rule that exists for technical reasons. The rule itself is “wrong” in the sense that not all ill-typed programs are able to reduce the first part of the context $\src{e_{pre}}$. So, pedantically, there should be yet another rule for ill-typed programs where $\src{e_{pre}}$ may fail. Anyhow, this situation could/should also be a lemma that is proven somewhere, i.e. the component should fail if the whole program is ill-typed, and this is something that is preferrable, but not done here, out of lazyness. The main secure compilation proof is not really affected by this. :sweat_smile:

Robust satisfaction , for $\src{S}$-level programs is now defined as:

Def. $\src{S}$-level Robust Property Satisfaction

$$\src{p}\text{ robustly satisfies }\pi \text{ iff } \forall \src{C},\text{if }\src{prog\ C\ p \progarrow{\trace} r}\text{, then }\trace\in\pi$$

$\trg{T}$ Definitions

$\trg{T}$ Syntax

To make compilation at least somewhat interesting, let’s make $\trg{T}$ a stack-machine. It is worth noting that, while we do have control here over the (formal) definition of the target language of the soon-to-be-defined compiler, in practice, it’s only $\src{S}$ that you have control over, if at all. More often than not for practically relevant languages, even $\src{S}$ is specified by, e.g., some ISO standard ( Citation: WG14/N1256 2007 September WG14/N1256. 2007 September . Programming languages — C ) . Anyways, the commands of $\trg{T}$ are as follows:

(** Values are numbers or booleans. *)
Inductive value : Type :=
| Vnat : nat -> value
| Vbool : bool -> value
.
(** _Dynamic_ Types of T *)
Inductive ty : Type :=
| Tnat : ty
| Tbool : ty
.
(** List of commands available in T. The abstract syntax is just a list *)
Inductive cmd : Type :=
| Cpush : value -> cmd
| Cbop : binopsymb -> cmd
| Cabort : cmd
| Chas : ty -> cmd
| Cquote : list cmd -> cmd
| Cunquote : cmd
| Cif : cmd
| Cget : vart -> cmd
| Cnegb : cmd
.
(** Components *)
Definition symbol : Type := vart * list cmd.

(** Viable contexts that can be linked against a symbol. *)
Inductive LinkageContext : Type :=
(* basically models `let y = call foo e__pre in e__post` *)
| LContext (y : vart) (cmds__pre cmds__post : list cmd) : LinkageContext
.
(** Top-level programs *)
Inductive prog : Type := Cprog (C : LinkageContext) (foo : symbol) : prog.

The notation $\trg{\overline{c}}$ means “list of $\trg{c}$”.

$\trg{T}$ Dynamic Semantics

As before, we first define runtime programs. Contrary to $\src{S}$, runtime programs in $\trg{T}$ depend on a stack and a heap:

(** Stack elements are either values or code. *)
Inductive stack_el : Type :=
| Sval : value -> stack_el
| Scode : list cmd -> stack_el
.
Definition stack : Type := list stack_el.
Definition store : Type := option (vart * value).

(** A runtime program is a stack and heap with a list of commands or a crashed state. *)
Inductive rtprog : Type :=
| RPTerm (Ψ : stack) (Δ : store) (cmds : list cmd)
| RPCrash
.

The “heap” is a singleton, it can store at most one variable. Stacks may either contain a list of commands as one element or a value.

Since the trace-models of $\src{S}$ and $\trg{T}$ are exactly the same, they are not listed in the above definition. Just color everything related to the trace model in the previous definition , red.

In terms of evaluation, the semantics does not need contexts, since it’s just popping off commands off of the list of commands in a given runtime program. The context is simply the remaining list of commands, but this is being taken care of by the reflexive-transitive closure as well as the step-indexed version. Most commands are straightforward: