# Secure Compilation

In this post, I want to shed some light on what, why, and how to do I'm focusing on robust trace preservation. Neither does this post discuss full abstraction or even mention it in any way, nor do we look at hyperproperties as means to talk about confidentiality. It's solely meant as a lightweight intro to robust trace preservation. . It’s more on the light-weight side of things, so if you are already familiar with parts of the topic, you likely don’t want to read this.

Computer programs are written in text-form by programmers. This text needs to be processed in some way, which is referred to as “compilation”. We can view this as translating from one language to another. For example, you may write down code in C, which subsequently the compiler translates to some data-representation that your processor can understand, referred to as machine language. So, abstractly, compilers are just functions which we’ll write down more or less handwavingly as $\llbracket\src{\bullet}\rrbracket^{\src{S}\to\trg{T}}$. The idea is that $\llbracket\src{\bullet}\rrbracket^{\src{S}\to\trg{T}}$ is a compiler from language $\src{S}$ to language $\trg{T}$.

Programming languages usually have some kind of formal or at least informal specification. This is necessary to ensure functional correctness of compilers, so that they faithfully translate from e.g. $\src{S}$ to $\trg{T}$. Formally, we can phrase this correctness in terms of whole programs as follows:

$$\forall \src{w}\in\src{P}, \forall \bm{t}\in\text{Outputs}, \text{if } \src{w}\to\bm{t} \text{, then } \llbracket \src{w}\rrbracket^{\src{S}\to\trg{T}}\to\bm{t}$$

Hereby, $\bm{t}$ is some final “state” of the program, which may simply be a value, like 42. So, given an $\src{S}$ program evaluates under the semantics of $\src{S}$ to some output $\bm{t}$, we want that it’s compiled version $\llbracket \src{p}\rrbracket^{\src{S}\to\trg{T}}$ evaluates to the same configuration. You may think that configurations are different, given that the programs run under different semantics, and you’d be correct. For sake of simplicity, let us assume that programming languages $\src{S}$ and $\trg{T}$ have a semantics that yields an output of the We could relax this formally by building some kind of relation $\sim$ between outputs. So, we'd have to define what it means for an "output object" of language $\src{S}$ to be equal to an "output object" of language $\trg{T}$. The statement then may look like: $$\forall \src{w}\in\src{P}, \text{if } \src{w}\to\src{\bm{t}} \text{, then } \llbracket \src{w}\rrbracket^{\src{S}\to\trg{T}}\to\trg{\bm{t}} \text{ and } \src{\bm{t}}\sim\trg{\bm{t}}$$

In our setting, we require the output to contain a Traces are potentially infinite long lists of actions. An action is something like "Read value 4 at location 0xdeadbeef". Basically, any side-effect is tracked in the trace. Such properties are sets of all such traces that fulfill a certain condition, like “No use after free” or “The letter x is printed exactly once”. Thus, a program satisfies a property $\pi$ if the trace it’s output contains is part of $\pi$. Formally: $$\src{p}\text{ satisfies }\pi \text{ iff given }\forall\bm{t}\in\text{Outputs},\src{p}\to\bm{t}\text{ then }\bm{t}\in\pi$$ With that, we can finally talk about security and why correctness is inadequate as a criterion for it. First of all, security is always about violating a particular kind of property. We never want something bad to happen. So, we may think to phrase a “secure” compiler as simply preserving property satisfaction: $$\forall \pi\in\text{Properties}, \forall \src{w}\in\src{P}, \text{if } \src{w} \text{ satisfies }\pi \text{, then } \llbracket \src{w}\rrbracket^{\src{S}\to\trg{T}}\text{ satisfies }\pi$$ In the setting of security, there is always this distinction between “the good people” and “the bad people”, the latter commonly referred to as “attackers”.

Security researchers will always have to consider a so-called To give you an example of a particular weak threat-model, consider some office application that understands "security" as "the user cannot give some program input that will crash the program". The only thing an attacker can do in this setting is to provide some input to the program. which simply describes the power of an attacker. What could be the most powerful attacker in terms of programs? Considering a program $p$ written in some programming language, the most powerful attacker is able to interact with $p$ in any way that the programming language allows. For example, a C program may call some library function, like strcmp. strcmp may have been swapped out by some malicious attacker. Instead of just comparing strings, it overwrites some parts of your memory by means of pointer arithmetic on the pointer you provide as an argument. In this simple example, the attacker even controls parts of the internal state that we have, which is something pretty difficult to protect us against. Any attack carried out by an evil-person will always be written as some kind of exploit, some other program that is linked, provides inputs, or overwrites stuff by means of what the processor’s language allows them to overwrite. So, the most powerful attacker can run arbitrary code at the same language level. This is not something that the correctness criterion captures. It only talks about whole programs, programs without open definitions and - therefore - without any interaction with the outside world.

Programs are more often than not developed as one or multiple modules, which depend on other modules to ultimately yield a whole program. Whole programs do not have any open definition. For example, the following is a valid partial C program:

int foo(void);

int main(int argc, char** argv) {
return foo();
}


The program declares the symbol foo, but never ends up defining it. That is, unless we compile it together with another C file containing the following:

int foo(void) {
return 5;
}


Linking partial programs together to build up (eventually) a whole program usually happens on the target level. In the above example, you could compile both files with gcc, which will ultimately invoke the linker ld that glues the assembly of compiled partial programs together. Another option may be to simply take the definition from the one file and move it to the other. We’ll consider linking formally as a binary operator $\bowtie$. Now, we can say a program is robust with respect to an arbitrary attacker if it satisfies a property of interest. We’ve already seen satisfaction, and we can similarily define this new notion of robust satisfaction: $$\text{In language }\src{S},\ \src{p}\src{\text{ robustly satisfies }}\pi \text{ iff given }$$ $$\forall\bm{t}\in\text{Outputs},\forall K\in\src{P},\src{K\bowtie p}\to\bm{t}\text{ then }\bm{t}\in\pi$$

With that, we simply take compiler correctness and amend the statement to make use of this more security-centric notion of property satisfaction: $$\forall \pi\in\text{Properties}, \forall \src{p}\in\src{P}, \text{if } \src{p} \src{\text{ robustly satisfies }}\pi,$$ $$\text{then } \llbracket \src{p}\rrbracket^{\src{S}\to\trg{T}}\trg{\text{ robustly satisfies }}\pi$$

At this point, we may ask ourselves: Why? And the quesiton is relevant, given there exist several, practical source code instrumentations that will make sure a certain property of interest is not violated: Softbound ( Citation: , & al., , , & (). SoftBound: Highly compatible and complete spatial memory safety for c. Association for Computing Machinery. https://doi.org/10.1145/1542476.1542504 ) , CETS ( Citation: , & al., , , & (). CETS: Compiler enforced temporal safety for c. Association for Computing Machinery. https://doi.org/10.1145/1806651.1806657 ) , BaggyBounds ( Citation: , & al., , , & (). Baggy bounds checking: An efficient and backwards-compatible defense against out-of-bounds errors. USENIX Association. ) , (Low-)FatPointers ( Citation: , & al., , , , & (). Low-fat pointers: Compact encoding and efficient gate-level implementation of fat pointers for spatial safety and capability-based security. Association for Computing Machinery. https://doi.org/10.1145/2508859.2516713 ) , DangSan ( Citation: , & al., , & (). DangSan: Scalable use-after-free detection. Association for Computing Machinery. https://doi.org/10.1145/3064176.3064211 ) , to cite a few. We can just use those to fix our code, right? The issue at hand with these approaches is manyfold. Either they fail to interact with other code at all or they simply trust library code to behave correctly. So, their threat-model is internal, the situation is similar to the security we get out of compiler correctness. Library code could, if the programming language allows it, just overwrite our component’s memory with some arbitrary garbage. With a robustly preserving compiler you have reassurance that this cannot happen. Lastly, you have no guarantee these approaches are correct. They test this on a certain set of benchmarks and identify X% of memory safety issues. For sure, this goes some part of the mile, but certainly not the whole. If we want to have a truly secure program, we better go the whole mile. Pretty much the only way to establish 100% is by means of a mathematical proof.

Now, another question we may still ask is: Why all this formal nonsense and why do we really need the proof? The answer is surprisingly simple, but also intriguing. We want to get this right! We want to have a formal guarantee, a mathematical proof, that we have full-blown security, maybe not for all kinds of properties, but at least for a particular property or class of properties of interest. If we write a secure program to begin with, the compiler will make goddamn sure it stays secure at the target level. And writing a secure program may sound harder than it is: Rust enforces certain security guarantees Please just ignore unsafe. Calling external code with unsafe allows that external code to overwrite arbitrary, allegedly safe memory. The syntactic choice of guarding unsafe actions inside a block suggests that anything outside this block is safe, but parts wrapped in unsafe can easily escape by means of pointer arithmetic shenanigans. This could be circumvented by means of memory isolation. and this renders any Rust program as secure with respect to those properties. If the compiler robustly preserves them, any compiled Rust program will benefit from the original robust satisfaction of the properties of interest.

Ok, finally, the how. How does one prove this? Obviously, first of all, both source and target language and the compiler itself need a mathematical specification that we can work with. I’m glossing over this as if it were that easy, but formalizing these three things is already quite a feat. Given that, proving a compiler robustly preserving requires quite a bunch of rather technical setup. I’ll try to give an overview of how it works, but the precise details depend on the actual programming languages of consideration.

We look at the “robustly safe compiler” criterion. On the left, you can see the assumptions that we are allowed to work with, on the right, the current goal. Let’s make things easier notationally by immediately assuming anything that is quantified with $\forall$ or in front of a $\text{then}$: $$\begin{array}{rlll} \pi&:&\text{Properties}&\\ \src{p}&:&\src{P}&\\ H_1&:&\src{p\text{ robustly satisfies }}\pi&\\ &&& \llbracket\src{p}\rrbracket^{\src{S}\to\trg{T}}\trg{\text{ robustly satisfies }}\pi\\ \end{array}$$ Unfolding the defition of $\text{ robustly satisfies }$: $$\begin{array}{rlll} \pi&:&\text{Properties}&\\ \src{p}&:&\src{P}&\\ H_1&:&\forall\bm{t}\in\text{Outputs},&\\ &&\forall\src{K}\in\src{P},&\\ &&\text{if }\src{K\bowtie p}\to\bm{t}\text{, then }\bm{t}\in\pi&\\ \bm{t}&:&\text{Trace}&\\ &&& \forall\bm{t}\in\text{Outputs},\forall\trg{K}\in\trg{P},\\ &&& \text{if }\trg{K\bowtie}\llbracket\src{p}\rrbracket^{\src{S}\to\trg{T}}\to\bm{t}\text{, then }\bm{t}\in\pi\\ \end{array}$$ We can again introduce anything that is universally quantified or a premise: $$\begin{array}{rlll} \pi&:&\text{Properties}&\\ \src{p}&:&\src{P}&\\ H_1&:&\forall\bm{t}\in\text{Outputs},&\\ &&\forall\src{K}\in\src{P},&\\ &&\text{if }\src{K\bowtie p}\to\bm{t}\text{, then }\bm{t}\in\pi&\\ \bm{t}&:&\text{Trace}&\\ \trg{K}&:&\trg{P}&\\ H_2&:&\trg{K\bowtie}\llbracket\src{p}\rrbracket^{\src{S}\to\trg{T}}\to\bm{t}&\\ &&& \bm{t}\in\pi\\ \end{array}$$ Now it’s easy to see that we can apply $H_1$ as long as we can construct a $\src{K}$ from either $\bm{t}$ or $\trg{K}$. This is a crucial part of this whole criterion:

The compiler inserts countermeasures so that $\trg{\text{target level}}$ attackers can only do the same attacks that $\src{\text{source level}}$ attackers can do.

If $\src{S}=\trg{T}$, we can simply put $\trg{K}$ for $\src{K}$ and the only thing left to argue is that $\src{K\bowtie p}$ and $\trg{K\bowtie}\llbracket\src{p}\rrbracket^{\src{S}\to\trg{T}}$ produce similar output. Even if the languages are different, it can still be a viable option to take $\trg{K}$ and go over it’s syntactic structure and construct a similar behaving $\src{K}$. However, for $\src{S}$ and $\trg{T}$ very different, pretty much the only option at hand is $\bm{t}$. Here, one would make use of a so-called backtranslation, which takes a $\trg{T}$-level trace and translates that trace into an $\src{S}$-level context.

In practice, we also have some kind of filter operation hidden in there, which may mark $\bm{t}$ actions as context action or component action. That way, a context that trivially dissatisfies a property of interest can be ignored, i.e. we only consider properties inside components. A context that just immediately tries to deallocate a random address is certainly ill-behaving with respect to memory safety. Moreover, these are also not meaningful attackers, an attacker tries to trip up the component somehow, i.e. violating the property.

I hope this little intro has been helpful. That being said, I’m sure you can get quite a lot more out of the following papers:

## References

Kouwe, Nigade & Giuffrida (2017)
, & (). DangSan: Scalable use-after-free detection. Association for Computing Machinery. https://doi.org/10.1145/3064176.3064211
Kwon, Dhawan, Smith, Knight & DeHon (2013)
, , , & (). Low-fat pointers: Compact encoding and efficient gate-level implementation of fat pointers for spatial safety and capability-based security. Association for Computing Machinery. https://doi.org/10.1145/2508859.2516713
Nagarakatte, Zhao, Martin & Zdancewic (2009)
, , & (). SoftBound: Highly compatible and complete spatial memory safety for c. Association for Computing Machinery. https://doi.org/10.1145/1542476.1542504
Nagarakatte, Zhao, Martin & Zdancewic (2010)
, , & (). CETS: Compiler enforced temporal safety for c. Association for Computing Machinery. https://doi.org/10.1145/1806651.1806657
Patrignani, Ahmed & Clarke (2019)
, & (). Formal approaches to secure compilation: A survey of fully abstract compilation and related work. 1–36. https://doi.org/10.1145/3280984
Patrignani & Garg (2021)
& (). Robustly safe compilation, an efficient form of secure compilation. 1–41. https://doi.org/10.1145/3436809
Akritidis, Costa, Castro & Hand (2009)
, , & (). Baggy bounds checking: An efficient and backwards-compatible defense against out-of-bounds errors. USENIX Association.