Blame-aware Recomposition for Secure Compilation Proofs of Low-Level Compartment Isolation

Blame-aware Recomposition for Secure Compilation Proofs of Low-Level Compartment Isolation Basile Schlosser1,3

arXiv:2610.26054v1 [cs.PL] 19 Oct 2026

1

ENS Paris-Saclay, France

Jérémy Thibault2,3 2

EPFL, Lausanne, Switzerland

Abstract—The security guarantees of existing formally verified compilers for compartmentalized programs in unsafe languages like C stop at a rather high level, assuming a built-in protection mechanism and a block-based memory model. Verifying a concrete, low-level enforcement mechanism for compartment isolation is still a major challenge for current proof techniques. In particular, Abate et al.’s proof technique fails because one of their proof steps, recomposition, essentially requires hiding all information about the code of each compartment, which is not practically achievable at a low level. We propose an extension of their proof technique to a low-level setting where compartments can fully observe each other’s code. To do so, we introduce an overlay semantics that allows us to characterize these observations as a form of undefined behaviour, and we use a novel variant of recomposition that we call blame-aware recomposition, which essentially allows recomposing executions as needed in the original high-level proof technique, even if the low-level context observes the code, because this context is ultimately going to be discarded. We apply this new proof to a compartment isolation mechanism that uses a programmable tag-based reference monitor.

1

Introduction

Vulnerabilities in software systems can lead to devastating attacks when exploited by malicious attackers. In particular, unsafe languages such as C call out many undefined behaviours (UB), which include various memory safety vulnerabilities that account for 70% of high-severity security bugs, according to both Microsoft and Chrome [8, 29]. Compartmentalization [12, 14, 25, 32, 36] is an often proposed practical countermeasure against vulnerabilities that relies on the principle of least privilege: programs are split into mutually distrustful compartments that interact through protected interfaces. If one compartment is compromised, the security impact on the rest of the program is limited. Compartmentalization is widely deployed in web browsers, which use process-level isolation to protect web sites from each other [25, 26] and software-fault isolation (SFI) [28, 32, 36] to sandbox WebAssembly code and third-party libraries [15, 22]. In order to characterize precisely the security guarantees a compilation chain for compartmentalized source programs should satisfy in the presence of undefined behaviour, Abate et al. [1, 2] propose a criterion: secure compilation should restrict undefined behaviours both spatially (to just the compartments that encounter undefined behaviour), and temporally (compartments are protected until they encounter an undefined behaviour). They reduce their criterion to a variant of a secure compilation criterion known as Robust Safety Preservation

Cătălin Hrit, cu3 3

MPI-SP, Bochum, Germany

(RSP) [3, 24] that they call RSCDC MD , standing for Robustly Safe Compilation with Dynamic Compromise and Mutual Distrust. Their variant states that any attack mounted by low-level attackers (i.e., low-level compartments that may have been dynamically compromised by undefined behaviour) against a safety property of a compiled program can also be mounted by source attackers (i.e., source-level compartments) against the source program. In addition, they formally verify that a compiler for a simple compartmentalized source language is secure according to this criterion. Since then, this result has been extended to incorporate memory sharing [10], to prove stronger secure compilation criteria [31], and most prominently to build SECOMP [30], a formally secure compiler based on CompCert for a C variant with compartments. However, a common limitation of these works is that they do not verify secure compilation all the way down to the actual machine; instead, they stop at a relatively high-level assembly language with an abstract view of memory and with an abstract model of compartments built into the semantics. Instead of a realistic flat memory model, where code is laid out in memory, they assume a block-based memory model [20] which only allows for a limited amount of memory unsafety (for instance, they cannot model heap overflows), and have code in a separate part of the state (so it cannot be modified or even read during execution). Hence, their abstract model of compartments is just a specification of what an actual compartment isolation mechanism should do at a lower level. Abate et al. [1] implement this specification in two lowerlevel compiler backends: one based on SFI [25, 28, 32], and another one based on a compartment isolation micropolicy [4], a programmable tag-based reference monitor. They leave verifying these backends open, and instead systematically test their SFI backend. Similarly, SECOMP [30] proposes an unverified lower-level backend targeting a variant of the CHERI RISC-V capability machine [35]. These works cannot verify such realistic backends because their proof technique relies on a step called recomposition [2], which allows one to split two whole programs (obtained by linking partial programs together, denoted by a bowtie ▷◁) that produce the same event trace (calls, returns and outputs; written ⇝ m) into two parts each, and then recombine these parts into a new whole program that produces the same event trace. In their proof, recomposition lets them replace a target-

level context CT with a compiled one CS↓:1 ) CT ▷◁ P↓ ⇝ m =⇒ CS↓ ▷◁ P↓ ⇝ m ∀ m, CS↓ ▷◁ P′↓ ⇝ m This step relies on the event traces capturing all possible interactions between compartments, meaning that the traces need to be “fully abstract” [13, 17, 23], and for this, compartments cannot observe other compartments’ code. This has little chance to hold at a low level, because there are many new observations compartments can make that are invisible (i.e. they don’t appear on event traces) and hard to prevent. A simple example would be reading code directly. Example 1 (Reading code directly). Consider the following function f belonging to a compartment C1: C1.f() { x := 100; // guesses an address if (*x < 1000) { // reads at it ... } else { ... } }

This function exploits the fact that there is no difference between a pointer and an integer in the low-level language to read memory at an arbitrary location, and branch on the result. That is a problem, because after code is laid out in memory, address 100 may point to the code of another compartment, so the branch taken by f depends on the code of the compartments C1 is linked with! Hence, compartment C1 learns information about other compartments’ code, which is not recorded on the trace. A second example shows observations through allocation.

behaviour into defined low-level behaviour, so even a compartment compiled from source can perform such observations once it has been compromised by undefined behaviour, which is exactly the dynamic compromise scenario that RSCDC MD is designed to protect against. We propose a significant extension of the recompositionbased proof technique of Abate et al. [2] that enables the verification of a secure compilation backend targeting a lowlevel assembly with a realistic memory model and a compartmentalization mechanism, which we call the low-level backend. Our technique is based on two observations: first, that the partial programs kept in recomposition are both compiled, so they do not trigger undefined behaviours along the considered trace; and second, that one can characterize most behaviours that break recomposition at the lower level as undefined behaviours w.r.t. an overlay semantics [11, 27]. Specifically, we introduce an intermediate language that is all but equal to the low-level language targeted by the backend, except that it considers these behaviours undefined. We write ⇝ov for the overlay semantics (whereas we use ⇝ for the low-level semantics). We then replace the use of recomposition by a new variant we call blame-aware recomposition. This variant allows recomposing partial programs just like before, with the added precondition that three out of the four partial programs behave in a defined way according to the overlay semantics, i.e., do not have the behaviours that would break recomposition. More specifically, blame-aware recomposition takes two executions: if CS↓ ▷◁ P′↓ ⇝ov m

in the overlay semantics

and either CT ▷◁ P↓ ⇝ov m

in the overlay semantics

Example 2 (Observation through allocation).

or CT ▷◁ P↓ ⇝ m

in the low-level semantics,

C1.f() { x := malloc(1); // allocates one byte C2.g(); y := malloc(1); // allocates another byte if (y - x > 1) { // compares the two addresses ... } else { ... } }

but

all undefined behaviours

This function allocates a byte, calls a function from another compartment, C2.g, and then allocates another byte. By comparing the addresses of the two allocations, C1 obtains information about the internal behaviour of another compartment, and can branch on it; this breaks recomposition, because allocating and comparing the two addresses are not events that are recorded on the event trace. With a high-level memory model such as the block-based one of CompCert [20], these observations are not possible, even in CompCert’s Asm: subtracting or ordering pointers to different blocks is undefined behaviour, and so is dereferencing an integer. This is why previous recomposition proofs [2, 30] did not run into them: executions stop with undefined behaviour before performing such observations. Compiling further down to a flat memory model turns this undefined 1 We use bold, dark blue for source objects, and thin, red for target objects.

in this execution happen in CT and yields an execution of the recomposed program CS↓▷◁P↓: CS↓ ▷◁ P↓ ⇝ov m

in the overlay semantics.

The preconditions ensure that the observations that would break recomposition can only occur in CT , which is discarded, while CS↓ cannot perform such an observation, at least along the trace m, because it executes in the overlay semantics. This allows proving blame-aware recomposition for low-level backends that don’t explicitly prevent these observations. Our blame-aware recomposition proof technique is strong enough to deal with observations that can be cleanly characterized in an overlay semantics, such as Example 1. The observations of Example 2 would be difficult to characterize as undefined behaviour in an overlay semantics without overly restricting acceptable behaviours (for instance, comparing pointers to the same block is allowed in CompCert-like memory models, and we would like to preserve this ability) or resorting to very complex tracking schemes. Hence, instead of dealing with Example 2 using overlay semantics, we address it with a compiler-based masking scheme to hide compartments’ heap usage: each compartment is statically assigned its own

space in memory, ensuring that all of a compartment’s memory allocations are contiguous independently of other compartments. An advantage of this solution is that it prevents the allocation channel from leaking information not only about other compartments’ code, but also about their data; the latter would be required to extend our guarantees beyond robust safety preservation in the future [3]. We updated the formerly unverified micro-policy backend of Abate et al. [1] to close leaks of this kind, with an allocator that uses our masking scheme. We prove that the resulting backend satisfies blame-aware recomposition using an overlay semantics. Our overlay semantics is constructed as a variant of the micro-policy used at the lowest level: in addition to using the enforcement from the concrete backend, the overlay semantics calls reading and writing to code in memory and executing data undefined behaviours. To prove blame-aware recomposition in this instance, we reuse the proof diagrams introduced to prove recomposition in SECOMP [30]. While proving the main diagrams of blameaware recomposition, we are, as expected, forced to reason about the concrete implementation of the compartment isolation mechanism, which is highly relevant for security. In summary, we put forward the following contributions: 1) We introduce blame-aware recomposition, a novel variant of recomposition that relies on an intermediate overlay semantics and gives rise to a proof technique that allows one to prove the security of a compiler targeting a lowlevel backend with a flat memory model. 2) We generically prove that blame-aware recomposition can be used to replace recomposition and obtain RSCDC MD . Our technique is formalized in the Rocq proof assistant. 3) We apply our methodology to the micro-policy backend of Abate et al. [2], modified as described above, proving blame-aware recomposition and as a consequence the security of this backend, in the Rocq proof assistant. Outline: The rest of this paper is structured as follows: in §2, we describe our new approach in a generic setting. In §3, we discuss our adaptation of the micro-policy backend to make the proofs work. In §4, we discuss how we prove blame-aware recomposition for this backend. Finally, §5 and §6 discuss related and future work. Artifact: Our formal development is available at the following URL: https://github.com/secure-compilation/ when-good-components-go-bad/tree/mp-transitional

2

General Machine-Checked Proof Technique Using Blame-Aware Recomposition

We start by presenting the proof technique of Abate et al. [2] in a generic setting, then explain why the same technique doesn’t work fully in low-level settings, and finally describe a way to adapt this proof technique to such a setting. 2.1

Setting and Background

The generic setting we consider is as follows: we have an unsafe source language S and a target language T . Both

languages have a notion of contexts (C ∈ CS or C ∈ CT ) and partial programs (P ∈ PS or P ∈ PT ) that can be linked together to obtain whole programs W = C▷◁P or W = C▷◁P. Both languages are equipped with semantics that produce finite traces for whole programs: W ⇝ m and W ⇝ m. The traces record stuckness with an event ⊥P or ⊥C , depending on whether the stuckness occurred while executing in the partial program or the context. Other than this, we do not require a particular structure for the traces, but a common choice is for them to record calls and returns between the partial program and the context. We write ≤ for the prefix relation between finite traces, and m′ ≺P m (resp. m′ ≺C m) to mean ∃ m′′ ≤ m, m′ = m′′ · ⊥P (resp. ⊥C ): it captures m being a refinement of an undefined behaviour that appears at the end of m′ while executing inside the partial program (resp. the context). Additionally, our proof technique relies on small-step operational semantics at the target level to be able to define and to construct intermediate semantics that will be used in our replacement of recomposition. Hence, we require the semantics of T , which we call low-level semantics, to be e described by a small-step relation between runtime states − → where e can be either an event or nothing (for silent steps). m We write −→∗ to denote the transitive reflexive closure of that relation, producing the trace m. We suppose the initial state of a program W is given by initial(W) and we see m W ⇝ m as a shorthand for ∃ s, initial(W)−→∗ s. Importantly, target-level runtime states should also be classified as belonging either to the program or the context, depending on which of the components is currently executing, written s ∈ P or s ∈ C. On the other hand, it doesn’t matter how the semantics of S is defined, except for the fact that the back-translation and compiler correctness lemmas below have to be provable. Our goal is to prove that a compiler ↓ST from S to T is secure, in the sense that it satisfies RSCDC MD [1]. Definition 1 (RSCDC MD ). ∀ P ∈ PS , C ∈ CT , m, C ▷◁ P↓ST ⇝ m =⇒ ∃ C ∈ CS , m′ , C ▷◁ P ⇝ m′ ∧ (m ≤ m′ ∨ m′ ≺P m). We refer the interested reader to [1] for a detailed explanaDC tion of what makes RSCDC MD interesting, but in short, RSCMD captures the fact that a low-level attack by a low-level context C, represented by a trace m, can be explained in terms of a source context C that can perform an attack m′ that is either longer than m (m ≤ m′ ), or that can be blamed on (explained in terms of) an undefined behaviour triggered in the source program P (m′ ≺P m). The second disjunct rules out vacuous back-translations: the constructed context has defined behaviour, so any UB of C ▷◁ P comes from P. To use the proof technique from Abate et al., we need four components: compiler correctness, a correct back-translation from finite traces to source whole programs, the recomposition theorem, and the blame theorem. Following the proof of Abate et al., we start from the hypothesis C ▷◁ P↓ST ⇝ m and apply the back-translation lemma:

Proposition 1 (Back-translation). There exists ↑, a function from finite traces to whole programs, such that: ∀ P ∈ PT , C ∈ CT , m, C ▷◁ P ⇝ m =⇒ ∃ CS ∈ CS , P′ ∈ PS , m↑ = (CS ▷◁ P′ ) ∧ CS ▷◁ P′ ⇝ m. The back-translation allows one to take a (well-formed) finite trace m and obtain a whole source program that produces this exact trace. With this, we obtain a new CS and a new P′ in the source. The next step is to compile these back to the target, and to apply the forward direction of compiler correctness, which states that a compiled program produces all traces that were produced by the source program.

C1.f() { r = C2.g(27); if (r > 1) { E.print(1); } else { E.print(0); } } C2.g(x) { E.print(27); return 12; }

C1.f() { if (C2.g(27) > 1) { E.print(1); } else { E.print(0); } } C2.g(x) { E.print(x); return 12; }

(b) Second program W'

(a) First program W

Fig. 1. Two programs that recompose well

Proposition 2 (Compiler Correctness (forward direction)). ∀P ∈ PS , C ∈ CS , m, C ▷◁ P ⇝ m =⇒ C↓ST ▷◁ P↓ST ⇝ m. After applying this theorem, we now have both C ▷◁ P↓ST ⇝ m (from the hypothesis) and CS↓ST ▷◁P′↓ST ⇝ m (from compiler correctness). This is where recomposition gets applied: Definition 2 (Recomposition). ) C ▷◁ P ⇝ m ∀m, ′ =⇒ C′ ▷◁ P ⇝ m. C ▷◁ P′ ⇝ m Recomposition takes executions of two target-level whole programs that produce the same trace, and requires proving that one can “recompose” these programs, taking the context of one and the partial program of the other and linking them, to obtain a recomposed execution of the recomposed program that produces the same trace. Applying recomposition at this point yields CS↓ST ▷◁P↓ST ⇝ m, which can be sent back to the source language using another compiler correctness theorem: Proposition 3 (Compiler Correctness (backward direction)). ∀ P ∈ PS , C ∈ CS , m, C↓ST ▷◁ P↓ST ⇝ m =⇒ ∃ m′ , C ▷◁ P ⇝ m′ ∧ (m ≤ m′ ∨ m′ ≺ m)

2.2

Recomposition and its Failings in Low-level Settings

So, how do Abate et al. [2] prove recomposition? Let us look at a concrete example where recomposition works well (Figure 1). This example is written in a hypothetical language whose syntax is similar to C, and which has a block-based memory model like the target of Abate et al. The programs W and W' are divided into two compartments, C1 with one procedure C1.f (written C1.f' in W') and C2 with one procedure C2.g (written C2.g' in W'), and we have an E.print external function that outputs values on the trace. Let us consider what happens in W in an execution starting in C1.f: first, C1.f calls C2.g with argument 27; C2.g calls E.print to output it, then returns 12 to C1.f. C1.f then branches on the returned value, and since 12 > 1, takes the first branch and calls E to print it. The second program W' does the same thing, with the sole exception being that C1.f' uses a temporary variable for storing the result of C2.g', and that C2.g' hardcodes the value to be printed, 27. The event traces can be represented visually as the following sequences of transitions, where →∗ represents a sequence of silent steps, and the labels correspond to calls, returns, or outputs via E.print.

where m′ ≺ m means that m refines an undefined behaviour happening at the end of m′ , but with no indication of where the undefined behaviour happened.

W

Using the last proposition, blame, we finally obtain RSCDC MD :

W'

∗ C2.g(27)

∗

27

∗

Ret 12

∗

1

∗ C2.g(27)

∗

27

∗

Ret 12

∗

1

Proposition 4 (Blame). ∀ P, P′ ∈ PS , C ∈ CS , m, C ▷◁ P ⇝ m ∧ C ▷◁ P′ ⇝ m′ ∧ m′ ≺ m =⇒ m′ ≺P m. Blame allows us to identify the component that triggers the undefined behaviour, as required by RSCDC MD . When all these theorems hold, we obtain RSCDC MD . However, as we hinted at previously, recomposition may not always hold as stated here. To explain how this may happen, and how we solve it, we must first explain how recomposition is proved.

Now, recomposition states that the two programs can be recomposed: one can build a program W½ by taking C1.f from W and C2.g' from W'. If we follow the execution of that program, we see that it produces the exact same trace, despite having different code from W and W'. The reason is that when executing inside C1.f, W½ takes the exact same steps as W, and when executing inside C2.g', the exact same steps as W', which can be represented as the

diagram below: ∗ C2.g(27)

W

∗

W½

C2 .g

(2 7

∗

Ret 12

∗

t

∗

1

∗

1

∗

1

12

Re

)

∗ C2.g(27)

W'

27

∗

27

∗

∗

27

∗

Ret 12

In fact, this diagram is exactly how the proof of recomposition goes for both Abate et al. [2] and Thibault et al. [30]: they prove a three-way simulation between the two original programs and the recomposed one. More precisely, they prove a series of simulation diagrams capturing the idea that silent steps in the parts that are kept are matched by equivalent silent steps (steps closer together between W/W' and W½ in the diagram), that silent steps in the parts that are discarded do not matter (steps further apart in the diagram), and that eventproducing steps are taken synchronously. C1.f() { C1.f() { if (C2.g(27) > 1) { r = C2.g(27); E.print(1); if (r > 1) { } else { 100: E.print(1); 100: E.print(0); } else { } E.print(0); } } } C2.g(x) { C2.g(x) { E.print(*50); E.print(27); if (*100 < 1000) { if (*100 < 1000) { return 0; return 12; } else { } else { return 12; return 0; } } } } (b) Second program W'

(a) First program W

Fig. 2. Two programs that don’t recompose well

Now, let us look at what could go wrong when we introduce lower-level observations. Consider the programs in Figure 2. The functions C1.f and C1.f' are unchanged, but C2.g and C2.g' have changed. In W, C2.g first reads the value to print at an arbitrary address (50), then reads at another arbitrary address (100), and chooses which value to return based on what it finds there. In W', C2.g' only does this second read (and always prints 27), but the branches are swapped. In the language from the example, reading memory at an arbitrary integer address is undefined behaviour, which is modelled by the execution stopping there, as depicted in the following diagram, in black. W W½

W'

∗ C2.g(27) ∗

∗ 27 ⊥

∗

∗

C2 .g (2 7)

∗ C2.g(27)

Ret 12

t

∗

1

∗

0

∗

1

0

Since the executions of the two programs end early, recomposition only requires recomposing W and W' up to the last shared event (the call to C2.g), and indeed W½ proceeds similarly up to that point. However, after compiling further down to a flat memory model, the programs are in a lower-level language where code is laid out in memory and any integer can be used as a pointer, thus reading at an arbitrary address isn’t undefined behaviour anymore.2 To illustrate the problems encountered when trying to prove recomposition at this lower level, let us assume that the compiler put the code of the compartments first in memory, and in particular that address 100 points to a particular instruction from compartment C1: in W, to the one responsible for calling E.print(0), and in W', to the one responsible for calling E.print(1); and let us assume that address 50 in W contains the integer 27. The execution of W starts the same as in the source, but instead of encountering undefined behaviour, the reads at arbitrary addresses succeed and the execution can continue, represented in red. C2.g first reads 27, prints it, then reads from address 100, obtains something that doesn’t satisfy the condition, and ends up returning 12. Now, W' behaves similarly: it prints 27, as before, then reads from address 100, obtaining this time something that satisfies the condition and returns 12. Hence, W and W' end up having the same event trace. Yet, if we try to recompose them, we run into an issue: C2.g' reads from address 100, gets a value that doesn’t pass the test, and so returns 0. Hence, W½’s execution extends the previous one with what’s depicted in red, which is clearly not the same trace: the simulation falls apart; recomposition cannot hold. This doesn’t mean RSCDC MD doesn’t hold anymore; indeed, the observations that break recomposition are observations about the code of other compartments, and, as explained by Abate et al. [3], criteria such as RSP and its derivatives (including RSCDC MD ) do not depend on the privacy of code. Moreover, in the proof of RSCDC MD , the kept function C2.g' can only come from two places: it is either part of the compiled partial program or part of the compiled back-translation. In the former case, that means the partial program exhibited undefined behaviour, and so we can use the blame conjunct ′ of RSCDC MD (m ≺P m) to stop early in reproducing the trace; in the latter case, C2.g' comes from a source program that the back-translation built to produce the whole trace m; since reading address 100 is undefined behaviour in the source, that read can only happen after m ends, so it cannot affect the recomposed execution along m. Similarly, we’re discarding C2.g, so what it actually does shouldn’t matter at all. This gives us a glimpse of the solution: our goal becomes to build a variant of recomposition that can be proved, because it excludes these cases, and can still be used to obtain RSCDC MD .

Re

∗

27

∗

27

∗ ⊥ ∗ ⊥

∗ ∗

Ret 12

2 We do not give out the code of the compiled programs explicitly, and for the purpose of this example, one can imagine the same syntax to be executed using a lower-level semantics.

2.3

Overlay Semantics

Our methodology starts by introducing overlay semantics [11, 27] that prevent these undesirable behaviours: a second smallstep semantics for T programs, using the exact same syntax for programs, but with runtime states carrying additional information, called ghost state. The difference is that the smalle step relation for the overlay semantics, − →ov , is made more restrictive by adding conditions that prevent these behaviours, t using the ghost state. We can then define → − ∗ov and ⇝ov similarly to those for the low-level semantics. Because the overlay semantics is defined to be more restrictive than the low-level semantics, we trivially have: e

e

∀ s, s′ , s − →ov s′ =⇒ s − → s′ and, as a consequence: e

e

∀ s, s′ , s − →∗ov s′ =⇒ s − →∗ s′ and ∀ W, m, W ⇝ov m =⇒ W ⇝ m for m free of UB e

In the other direction, there are cases where s − → s′ holds but e ′ ′ s− →ov s doesn’t hold (for any s ). We can illustrate that fact by thinking of our previous example. In the low-level semantics, the states s contain a memory m, i.e. a map from word to word, and loading from memory is essentially unconstrained: L OW-L EVEL -L OAD

m(w) = w′ ... Load(m, w) = w′

One can load from a location whenever it contains something, no matter what.3 The overlay semantics adds a bit of ghost state, here a rudimentary tag on every memory location recording whether it contains code, and uses it to restrict execution: OVERLAY-L OAD

m ⊢ w : data m(w) = w′ Load(m, w) = w′

...

Here, the notation “m ⊢ w : data” means that location w contains data, to be contrasted to the notation “m ⊢ w : code” that would appear on locations containing code. According to this rule, the reads performed by C2.g and C2.g' wouldn’t be allowed, because they target the code area of memory. In summary, our methodology starts by defining an overlay semantics that gets stuck when encountering the behaviours that break recomposition, essentially seeing the low-level semantics as refining undefined behaviour from the overlay semantics. Defining such overlay semantics is not always easy, and one can easily imagine settings where doing so would be prohibitively complex, or even impossible. As we will see in §3, which describes our concrete implementation of the proof technique, we propose combining our methodology with concrete enforcement at the lowest level, to eliminate some 3 Other conditions, such as not being allowed to read from another compartment’s data, are omitted, since they are not relevant to the discussion here, which is about distinguishing code from data in memory.

behaviours and stay in a setting where defining the overlay semantics is realistically feasible. Now that we have defined the overlay semantics, we can reduce the problem to proving two instances of RSCDC MD and composing them: (1) for the compiler from S to T with the overlay semantics, and (2) for the identity compiler from T with the overlay semantics to T with the low-level semantics. Because we eliminated all behaviours that invalidate recomposition in the overlay semantics, we can apply the proof technique of Abate et al. to prove (1), and this doesn’t require much additional work: by definition, we can still reuse the back-translation (traces in the low-level semantics can only become smaller in the overlay semantics) and compiler correctness (the overlay semantics only stops behaviours that were anyway not allowed in the source language). We will also see that the recomposition variant used to prove (2) also implies recomposition for the overlay semantics, so we need not duplicate this proof. We now focus on proving (2). 2.4

Undefined-behaviour-restricting semantics

In order to prove RSCDC MD between the two semantics for T , we introduce a novel variant of recomposition; but before we can do so, we need to build a third semantics that captures the high-level intuition of “undefined behaviour not happening in a certain program part”. The reason we want to do this is that our proofs are not manipulating arbitrary low-level objects: one component is indeed a low-level component, but the other one is obtained by compiling a source program, and so it has defined behaviour according to the overlay semantics, at least along the trace that is considered. This semantics should then allow us to reason about the linking of these two objects. We call the semantics we define undefined-behaviourrestricting semantics (UB-restricting semantics for short), because it allows some behaviours from the low-level semantics that are not allowed in the overlay semantics, but not all. We build this by combining the overlay semantics and the lowlevel semantics, at the small-step level. The semantics is parameterized by I, which can be either C or P, describing on which side undefined behaviours are allowed, and defined by the small-step relation →UB(I) with the following two rules: S-I N -I

s∈I e

e

s− → s′

s− →UB(I) s′

S-N OT I N -I

e

s− →ov s′

s∈ /I e

s− →UB(I) s′

Rule S-I N -I says that any low-level behaviour is allowed in the UB-restricting semantics, for runtime states belonging to I. The other rule, S-N OT I N -I, says that only behaviours that are possible in the overlay semantics are allowed in the UBrestricting semantics, for runtime states not belonging to I. e e Since s − →ov s′ implies s − → s′ , the UB-restricting semantics accepts any behaviour that can be expressed in the overlay semantics; but, additionally, it accepts low-level behaviours that are not possible in the overlay semantics (i.e. undefined behaviours w.r.t. the overlay semantics) as long as they happen in the right component.

Coming back to the example from Figure 2, we can execute the first program W with the UB-restricting semantics, in two ways depending on which compartment we assign to I: I ∋ C1 I ∋ C2

∗ C2.g(27) ∗ C2.g(27)

∗ C2.g(27) ∗

∗

27

∗

∗

27

∗

27

∗ ⊥ ∗ ⊥

∗

Ret 12

∗

1

C2

.g (

27

)

27

∗

∗

Ret 12

∗

1

W'

In the first execution, C2 doesn’t belong to I, so it must follow the overlay semantics, and triggers undefined behaviour when attempting to read code. On the other hand, when C2 belongs to I, in the second execution, these steps are allowed because the UB-restricting semantics does not constrain steps taken by compartments in I. 2.5

W W½

∗ ⊥ ∗

The recomposition diagram for this instantiation is:

Blame-aware recomposition

Using these definitions, we can now formulate a novel variant of recomposition, which we call blame-aware recomposition, that captures the ideas necessary to make the proof work in our setting. As we mentioned previously, there is no hope of proving recomposition (Definition 2). However, we repeat the two observations that guide the definition of our new property: ′ • C (and P ) are not used in the conclusion of recomposition, so in principle they may exhibit the recompositionbreaking behaviours of §2.2. ′ • Recomposition is used in a proof technique where C and ′ P are the compiled back-translation of m, so they do not exhibit the unwanted behaviours along m; and where P is compiled from a source program, so it can only exhibit them where the source program already has undefined behaviour, which the blame conjunct of RSCDC MD allows. These observations lead us to the definition of blame-aware recomposition, trying to capture these intuitions by using the UB-restricting semantics: Definition 3 (Blame-aware recomposition). ) C ▷◁ P ⇝UB(C) m =⇒ C′ ▷◁ P ⇝ov m ∀m, ′ C ▷◁ P′ ⇝ov m This property is similar to the recomposition property from Abate et al. [2], in that it allows putting together two similar executions from different programs to obtain a third execution. However, the difference with the previous version of recomposition lies in the semantics that are being used: C′ ▷◁P′ must execute according to the overlay semantics, while C ▷◁ P must execute according to the UB-restricting semantics. In the conclusion, we obtain an execution in the overlay semantics, which can trivially be lowered to the low-level semantics. The use of the UB-restricting semantics for C ▷◁ P means that C is allowed to have behaviours that are not allowed in the overlay semantics, i.e. it is allowed to perform the low-level behaviours that would invalidate standard recomposition. To illustrate this definition, let us take the example from Figure 2 and instantiate the components as follows: C1 ∈ P

W = C ▷◁ P = C2 ▷◁ C1

C2 ∈ C

W'= C′ ▷◁ P′ = C2′ ▷◁ C1′

∗ C2.g(27)

Since C▷◁P executes according to the UB-restricting semantics (⇝ UB(C) ), the low-level observations performed by C2.g go through, depicted in red. However, those are not allowed in C′ ▷◁ P′ , so the execution still gets stuck in C2.g', when reading at address 100. But now, note how we recompose: despite W technically triggering undefined behaviour before printing 27, we are still able to include this event in the recomposed execution, because inside W, it happens in the context that will be discarded! We also introduce an alternative formulation of blame-aware recomposition that takes into account what happens when the execution gets stuck while executing inside the program part P in the UB-restricting semantics: the recomposed execution also gets stuck while executing inside the program part. Definition 4 (Blame-aware recomposition with explicit undefined behaviour). ) C ▷◁ P ⇝UB(C) m · ⊥P ∀m, ′ =⇒ C′ ▷◁ P ⇝ov m · ⊥P C ▷◁ P′ ⇝ov m The purpose of this definition is to properly handle the undefined behaviour happening in the program, and to link it directly to the blame conjunct of RSCDC MD . To illustrate it, let us take the other assignment (C1 becomes the context and C2 becomes the program), and the other recomposition (we build W½' with C1 from W' and C2 from W). C1 ∈ C

W = C ▷◁ P = C1 ▷◁ C2

C2 ∈ P

W'= C′ ▷◁ P′ = C1′ ▷◁ C2′

For this assignment, the recomposition diagram is: W

∗ C2.g(27) 7)

∗ ⊥ ∗ ⊥

∗ C2.g(27)

∗

(2 .g C2

W½' W'

∗ 27

∗ ⊥

Here, the undefined behaviour that happens in the first execution happens in the program part, hence it must also happen in the program part in W½'. As we will see in §2.6, we need this second formulation for programs P with undefined behaviour. Importantly, blame-aware recomposition directly implies recomposition at the level of the overlay semantics, which simplifies proving that the compiler to the overlay semantics satisfies RSCDC MD , i.e. instance (1) of §2.3. One may wonder why we chose to use the overlay semantics, and not the UB-restricting semantics, in the second

Overlay semantics UB-restricting semantics

C′ ▷◁ P′ ⇝ov m

C′ ▷◁ P ⇝ov m

C′ ▷◁ P ⇝ov m′ · ⊥P

(3) Blame-Aware Recomposition (1) Back-translation

Low-level semantics

(4) Blame-Aware Recomposition with Undefined Behaviour

C ▷◁ P ⇝UB(C) m

∨

C ▷◁ P ⇝UB(C) m′ · ⊥P and m′ ≤ m

C ▷◁ P ⇝ m (2) Maximum prefix lemma Fig. 3. Proof technique for RSCDC MD between the overlay semantics and the low-level semantics

execution, C′ ▷◁ P′ ⇝ov m. Indeed, it appears to be possible to replace it with ⇝UB(P) , since P′ is being discarded, just like C. We chose not to, because C′ ▷◁ P′ is the compiled backtranslation of m, so P′ has defined behaviour in the overlay semantics along m anyway. Because this semantics is more restrictive, it is intuitively easier to reason about it, and so we prefer using it there. 2.6

Replaying the proof

Using the two formulations of blame-aware recomposition, it becomes possible to replay the proof of Abate et al. [2] and obtain RSCDC MD . As mentioned in §2.3, we only need to prove RSCDC MD for instance (2), the “identity compiler” between T with the overlay semantics and T with the low-level semantics. We need one last additional lemma before proceeding: the maximum prefix lemma. Lemma 1 (Maximum prefix). ∀ P, C, m, C ▷◁ P ⇝ m =⇒ ∃ m′ , C ▷◁ P ⇝UB(C) m′ ∧ (m = m′ ∨ m′ ≺P m)

Theorem 1 (RSCDC MD between the overlay semantics and the low-level semantics). ∀ P ∈ PT , C ∈ CT , m, C ▷◁ P ⇝ m =⇒ ∃ C′ ∈ CT , m′ , C′ ▷◁ P ⇝ov m′ ∧ (m ≤ m′ ∨ m′ ≺P m). Proof. The proof is described in Figure 3. We start from the hypothesis C ▷◁ P ⇝ m and (1) apply the back-translation to it, to obtain a new target program P′ and a new target context C′ such that C′ ▷◁ P′ ⇝ov m. To the same hypothesis, (2) we also apply the maximum prefix lemma (Lemma 1), which yields two cases: either C ▷◁ P ⇝UB(C) m, or C ▷◁ P ⇝UB(C) m′ · ⊥P , with m′ ≺P m. In the first case, no undefined behaviour was triggered in P along the execution producing m. Hence, (3) we can apply blame-aware recomposition (Definition 3) to this execution and the one from the back-translation, obtaining exactly the ′ first disjunct of the conclusion of RSCDC MD : C ▷◁ P ⇝ov m. In the second case, P triggered undefined behaviour along that execution, so (4) we apply its variant with explicit undefined behaviour (Definition 4), obtaining the second disjunct directly: C′ ▷◁ P ⇝ov m′ · ⊥P with m′ ≺P m. 2.7

Proof. If C ▷◁ P ⇝UB(C) m, then we are trivially done. Otherwise, we know there exist states s and s′ , and a finite m′ e trace m′ < m such that initial(C ▷◁ P) −−→∗UB(C) s, s − → s′ , but e not s − →UB(C) s′ . By definition of the UB-restricting semantics, s ∈ P, and so we have C ▷◁ P ⇝UB(C) m′ · ⊥P . The maximum prefix lemma allows us to lift low-level executions to the UB-restricting semantics by making the following observation: if C ▷◁ P ⇝ m, then there exists some prefix m′ ≤ m that can also be produced in the UB-restricting semantics, and additionally, if it’s a strict prefix, then this is because P, not C, triggered an undefined behaviour. Depending on the case, we use one of the two formulations of blameaware recomposition, Definition 3 or Definition 4, respectively. We can now prove the result we want:

Formalization

We have formalized this generic proof technique in the Rocq proof assistant. More precisely, we have defined the lemmas for back-translation, for compiler correctness, and for blame. We have defined the UB-restricting semantics in a generic manner, and we prove that in that setting, the maximum prefix lemma holds and that blame-aware recomposition can be used to prove RSCDC MD .

3

A Low-Level Micro-Policy Backend

In this section, we discuss how our proof technique can be applied to a concrete low-level backend. 3.1

The low-level micro-policy backend of Abate et al.

Abate et al. [1] implement and verify a secure compiler for a compartmentalized C-like language. In their source language, programs are split into several compartments C that can

only interact with each other via function calls, mediated by interfaces that specify what procedures are exported and imported by each compartment. As we mentioned earlier, their compiler is only verified to be secure down to an intermediate language with built-in support for cross-compartment calls and returns (i.e., they are done with special instructions) and a CompCert-like block-based memory model. This gives them the freedom to target different backends, and they implement two of them: one backend based on software fault isolation (SFI) [32], and another one based on micro-policies [4], which are essentially programmable tag-based security monitors. This second backend is the one that is of direct interest to us here and the one we want to verify. In that backend, the memory forms a single contiguous block and the only datatype is that of machine words, which can act as both integers and pointers. Additionally, on a micropolicy machine, each memory location or register is given a tag; during execution, at each instruction, the tag of the current PC, the tags of the operands, the tag of the current instruction, as well as the opcode are all processed by a monitor that decides, based on these tags, whether the execution is allowed to continue, and if so, how to update the tags. The policy that Abate et al. implement is a compartmentalizing policy that mainly relies on two ideas: • Memory locations are assigned a colour that uniquely identifies the compartment they belong to. Compartments cannot read or write data to memory tagged with a colour other than their own. • The stack discipline is enforced using linear return capabilities [7]. The size of the stack is recorded in the tag of the PC, and incremented every time a cross-compartment call occurs. Return addresses are tagged with a level n that represents the size of the stack at the point where the return address was created. When jumping using such an address, the policy ensures that the stack has the right size, n + 1. The monitor also ensures return addresses cannot be duplicated (the “linear” part), which prevents reusing the same return address several times. Concretely, their backend consists of a few instructions given below, and its semantics is given by a small-step relation →, which itself depends on the compartmentalization micropolicy. i :=

| Nop | Const i → r | Bnz r i | Load ∗rp → rd | Jal l

| Halt | BinOp r1 ⊕ r2 → rd | Mov rs → rd | Store ∗rp ← rs | Jump r

Memory addresses, registers, and the PC are tagged slightly differently, using the following tags: Value tags tv := Ret n | ⊥ Register tags treg := tv Memory tags tm := (tv , c, entry point) PC tags tpc := (Level n, c).

The most basic tags, upon which the others are constructed, are value tags tv : Ret n is used to tag return addresses, and ⊥ for other values. The PC is tagged with a level, which records the size of the stack, and the current compartment c. Memory locations are tagged using a value tag, to track whether they contain a return address or not; the colour c is a compartment identifier that identifies which compartment owns the memory location; and entry point optionally records whether this is an address corresponding to the entry point of a function available to other compartments. These tags are manipulated according to the rules of the monitor such as the ones in Figure 4. Rules are of the form [P ] Instr [Q], meaning that Instr can only be executed when the precondition P holds, and updates tags according to postcondition Q. Those conditions are of the form d 7→ t where d is either a register r, the address contained in a register ∗r, or a code label l, and t is a tag of the appropriate kind, with some conditions on it. We use an underscore either when there’s no condition on part of the tag (in a precondition), or when that part of the tag isn’t modified (in a postcondition).   l 7→ (⊥, c′ , e ∈ allowed(c)) PC 7→ (Level n, c)  r 7→ Ret n ∗r 7→ ( , c′ , )  PC 7→ (Level n + 1, c)







 PC 7→ (Level n + 1, c′ ) RA 7→ Ret n



 PC 7→ (Level n, c′ ) r 7→ ⊥

Jal l

Jump r

   ∗rp 7→ (⊥, c, ) ∗rp 7→ (tv , c, ) Load ∗rp →rd PC 7→ ( , c) rd 7→ tv

Fig. 4. Micro-policy describing the linear return policy for Abate et al.’s backend

The three rules depicted in Figure 4 form the core of the linear return capability policy. The first rule, for Jal, describes what happens during a cross-compartment call (calls are made using the Jal instruction).4 The preconditions require the monitor to check that the label points to code belonging to a compartment c′ that the current compartment c (indicated by the tag of the PC: PC 7→ (Level n, c)) is allowed to call (e ∈ allowed(c)), the set allowed(c) being computed statically based on the interfaces. The postcondition indicates how the monitor updates the tags: the PC is now tagged with the new compartment c′ , and its level incremented. The new return capability created in the RA register must then be tagged with the former PC level, n. The next rule, for Jump, describes what happens when doing a jump using a return capability, i.e. a cross-compartment return. The precondition describes the current tags: the current compartment is c, and the stack is at level n + 1; meanwhile, the jump must use a return capability at just one level below, n, and this capability points to compartment c′ . The postcondition describes the updated tags after the return: the level of the PC 4 There are also rules for internal jumps that do not manipulate the tags other than checking that there is no change of compartment, but we don’t depict them here as they aren’t relevant to the cross-compartment concerns.

has been decremented, we are now in compartment c′ , and importantly the return capability has been invalidated, ensuring it can’t be used again in another return (r 7→ ⊥). Finally, the rule for Load is the one that ties everything together. The precondition requires reading at an address belonging to the same compartment c as the PC, and that it has a tag tv (∗rp 7→ (tv , c, )). The postcondition transfers that tag to the destination register (rd 7→ tv ) and invalidates the memory tag (∗rp 7→ (⊥, c, )). If tv was already ⊥, this doesn’t change anything. However, if tv was Ret n for some n, then the rule ensures that there only ever exists one copy of that capability, hence the name “linear”. The step relation → uses the monitor to check and modify the tags at every step. Otherwise, it is unsurprising, so it is not reproduced here. 3.2

Why recomposition doesn’t work

In order to apply our proof technique to Abate et al.’s backend, we start by identifying why recomposition doesn’t hold, i.e. what are the problematic behaviours programs can have that are not recorded on the trace, and allow compartments to learn something about other compartments. In this backend, these behaviours fall in two categories, corresponding to the two examples from the introduction. Direct code observations are of two kinds. The first corresponds to Example 1 and the example from the previous section. Compartments can freely use integers as pointers, so they read from arbitrary locations in the code, obtaining information either directly about the private implementation of other compartments, or indirectly by being able to observe the code layout. The second kind is that compartments have access to pointers to their own code, via the RA register for instance. By converting those to integers, they learn immediately where their code is laid out in memory, which is something that depends on the code of the other compartments. Note that this is not simply following a code pointer: here, the code pointer is just inspected by an operation or comparison. The other category is what we call leaky allocations, and corresponds to Example 2. These arise from the ability to cast dynamically allocated pointers to integers, which allows compartments to obtain information covertly, and from the memory allocation mechanism. The micro-policy backend’s allocator is a standard bump allocator: it allocates memory sequentially by keeping a pointer to the start of the not-yetallocated region, bumping it by the requested amount and tagging the region between with the colour of the compartment that allocates, which can leak information about the allocation behaviour. Recall Example 2: C1.f allocates x, calls C2.g, allocates y, and then compares them. If C2.g doesn’t allocate, we get the following memory layout: ...

C1

C1

x

y

...

y−x=1

In this case, x and y point to two locations next to each other, since nothing was allocated by C2.g. Hence, y − x = 1. On the other hand, if C2.g does allocate, we get the following memory layout: ...

C1

C2

C1

x

memory allocated by C2.g

y

...

y−x>1

After allocating some memory for x, the allocator has allocated a block of memory right next to it for C2.g, and then allocated again next to it for y. Hence, this time y−x > 1, an observation that breaks recomposition. We reiterate that these observations being possible should not affect the top-level theorem, because the top-level theorem, as a variant of RSP, is only concerned with safety properties, and these safety properties cannot capture attacks against the privacy of the code. We’ve seen in §2.3 that one solution would be to define an overlay semantics that prevents all these behaviours. However, leaks through the allocation mechanism are much harder than code observations to characterize in an overlay semantics. Indeed, it is difficult to accurately characterize all the observations through this kind of cast that break recomposition: doing so would already require a fine-grained dynamic analysis that tracks the provenance of pointers and how they are used, but it would also probably stop many legitimate behaviours that do not lead to leaks, thus strongly restricting the reach of our theorem. Thus, we took a path of lesser resistance and opted to slightly modify the backend to prevent those entirely. This is not entirely unreasonable: the backend is already preventing all kinds of undesirable behaviours, and our change is quite minimal, as it is only a slight change to the behaviour of the allocator. Furthermore, hiding the allocation pattern would be a required change if we wanted to prove a stronger security result that requires confidentiality of data. We describe this change in the next section. 3.3

Hiding the memory allocation pattern in the backend

We implement a masking protection in the allocator that stops compartments from obtaining information about other compartments’ behaviour by comparing dynamically allocated pointers. Our changes to the allocator are inspired by softwarefault isolation, a commonly deployed technique to implement compartmentalization [6, 22, 36]. Our allocator divides the memory into regions of equal size by reserving the first bits of each pointer to encode a unique compartment identifier. This means that for a compartment C, all pointers allocated by C will start with a specific bit pattern unique to that compartment. For instance, if we assign prefix 0001 to C1 and 000F to C2, the resulting memory layout is as follows:

C1’s space (prefix 0001) ...

...

0x00010000

...

x

y

0x0001FFFF

C2’s space (prefix 000F) ...

are pointers to the same block, so preventing all pointer comparisons seems too restrictive. Tightening this restriction would also be difficult: at the micro-policy machine level, we have already lost semantic information about which pointers used to point to the same block, and we can’t retrieve it from compilation, because not all the programs we consider are compiled. Hence, we believe this change to the allocator to be the most reasonable solution.

...

4 0x000F0000

0x000FFFFF

With this scheme, C1’s allocations will only ever live between addresses 0x00010000 and 0x0001FFFF, and C2’s allocations will only ever live between addresses 0x000F0000 and 0x000FFFFF, ensuring they are completely disjoint. Hence, we will always have y − x = 1: this partitioning hides each compartment’s allocation pattern. Note that contrary to some existing SFI implementations, we do not rewrite reads using masking, and the partitioning into several regions is not a substitute for the tagging mechanism: a compartment is free to try to access any memory location, and it is the micro-policy that stops it from accessing the other compartments’ data. We do not partition the code section of the program. The first reason for this is technical: jump labels appearing in the Jal instructions are encoded as immediates that are smaller than the full range of a pointer; redirecting those to the memory space of a compartment would require substantial changes to the semantics of Jal, which we explicitly wanted to avoid. Instead, we decided to put the code of all compartments contiguously at the beginning of the memory (starting with prefix 0000). The second reason is conceptual: observations that leak information about the code layout can be reasonably easily characterized as undefined behaviour in an overlay semantics, so unlike memory allocation, we don’t need to change the backend for this. Discussion One may wonder whether the changes to the allocator are too large. We do not believe this is the case. Indeed, while such protections are not necessary to prove RSP and its variants, including RSCDC MD , they are still desirable if one is interested in confidentiality, and are necessary to prove stronger security criteria. Moreover, protections such as using a custom allocator and masking are already commonly used [15, 21, 22, 36]. Finally, it is true that our custom allocator limits the possible number of compartments, and the memory available for such compartments. We believe this to be a necessary trade-off between security, performance, usability and proof engineering. The remaining question is whether we could have found a proper characterization of memory allocation-related leaks as undefined behaviour for the overlay semantics. We believe this task to be a difficult one and beyond the scope of this paper. Indeed, in the block-based memory model of CompCert, comparing and computing with pointers is allowed when they

Proving Blame-aware Recomposition

We are now ready to discuss how we can apply the proof technique to this modified backend. We start by describing the overlay semantics we introduce, and then how we prove blame-aware recomposition. 4.1

The Overlay Semantics

Our overlay semantics uses a variant of the low-level micropolicy, which we call the overlay micro-policy. Its goal is to prevent the code observations described in §3.2. To do so, we add a boolean b to memory tags that records whether a location contains code. tm := (tv , c, entry point, b) This boolean is set statically and is completely immutable, and our overlay micro-policy uses it to prevent leaking the layout of the code. The first major change in the overlay micro-policy is that it prevents reading code, whereas this is always allowed in the low-level micro-policy (code isn’t private).     ∗rp 7→ (tv , c, , false) Load ∗rp →rd . . . PC 7→ ( , c) To help with hiding the code layout, we also make the value tags more granular, so that the machine can distinguish more types of values: tv := Ret n | InternalJump | Inv | ⊥. The tags Ret n and ⊥ are unchanged, and we introduce two new tags, InternalJump, for return addresses of internal calls, and Inv, standing for “invalidated”, for crosscompartment return capabilities that have been used. The invariant our overlay micro-policy maintains is that all code pointers one gets during execution (i.e. return addresses) are tagged with either Ret n, InternalJump, or Inv. Then, we simply prevent values with such tags from being used in computations or comparisons. For instance, the Bnz rule becomes the following:   r 7→ ⊥  PC 7→ ( , c)  Bnz r i · . PC + i 7→ ( , c, , ) The tag of the operand is required to be ⊥, meaning it can’t be a pointer to code. To tag code pointers properly, we update the micro-policy rules for the instructions that create and use them. The only instruction that actually creates code pointers is Jal. The rule

for cross-compartment Jal already tags the return address as Ret n; now, the rule for internal Jal also tags the return address as InternalJump:     l 7→ (⊥, c, , ) PC 7→ ( , c) Jal l . PC 7→ ( , c) RA 7→ InternalJump Because this is an internal jump, there is no need to track its level. Now, recall the previous rule for cross-compartment Jump: it set the tag of the operand to ⊥, to prevent using it again, as required by the linear return policy. The issue is that ⊥-tagged values can still be used in comparisons and computations, so we have to change the cross-compartment Jump to invalidate it.     r 7→ Ret n ′  Jump r PC 7→ (Level n, c ) ∗r 7→ ( , c′ , , ) r 7→ Inv PC 7→ (Level n + 1, c) That way, we ensure that the return address will not be used. We need the same change for Load, Store, and Mov: they now invalidate return addresses. Finally, we need to change the rule for internal Jump to require having an InternalJump:   r 7→ InternalJump   Jump r · ∗r 7→ ( , c, , ) PC 7→ ( , c) We need this, because absolute jumps can leak information about the code layout, just like reading the code. Note that contrary to the cross-compartment jumps, internal jumps are not subject to the linear policy (the tags aren’t modified): a compartment is free to reuse the same return address several times. There are two additional mundane changes: the overlay micro-policy prevents executing instructions not tagged as code, and it prevents writing to code, which are needed to ensure the confidentiality of code. Note that we didn’t try to design the minimal overlay semantics: it is possible that some of these rules are not strictly necessary in our proof (for instance, preventing executing data may not be fully necessary). However, the overlay semantics is only a tool for proving RSCDC MD ; these rules make reasoning about the behaviour of the code simpler, and since the source language doesn’t allow executing data or rewriting code, these rules do not overly restrict the behaviours of compiled programs. 4.2

Proving Blame-Aware Recomposition, in Practice

Recall that our goal is to prove blame-aware recomposition: ) C ▷◁ P ⇝UB(C) m ∀m, ′ =⇒ C′ ▷◁ P ⇝ov m. C ▷◁ P′ ⇝ov m

transition systems, the fact that we use different semantics in our statement is not a problem and we can apply the generic result from SECOMP in our setting. To understand the general intuition behind these diagrams, recall the recomposition diagrams from §2, and let us zoom in on a call and its surrounding execution.

W W½

∗

∗

∗ C2.g(27)

∗

∗

∗ C2 .g (

∗

∗

∗

∗

∗

∗

∗

∗

∗

27

)

∗

W’

∗ C2.g(27)

∗

The executions represented by this diagram start in C1.f, and after a few silent steps, there is a call to C2.g, after which there are a few more silent steps. The middle execution is that of W½, built by taking C1 from W and C2 from W'. What happens is the following: when executing W½ within C1.f, since W½ took C1 from W, the execution will be more similar to the one of W, and conversely, when executing within C2.g, it will be more similar to W'. This is because we’re executing the same code, and the behaviour of a compartment can only be influenced by what it can observe from other compartments, i.e. what appears on the trace. To formalize this intuition, SECOMP (taking inspiration from the ideas of El-Korashy et al. [9, 10]) puts forward the idea of proving a three-way simulation using three relations: a strong simulation relation ≡, a weak simulation relation ∼, and a mixed simulation relation M. When executing within C1, the strong relation ≡ relates the states of W and W½, and the weak relation ∼ relates the states of W' and W½. The mixed relation M is a ternary relation that relates all three states, to capture invariants that are common to the three executions, such as the shape of the cross-compartment stack. Then, SECOMP gives several diagrams to prove, such that together they imply recomposition, or in our case blame-aware recomposition. Figure 5 depicts the core three diagrams. In that figure, each row corresponds to one of the three executions, with the recomposed execution being at the bottom; arrows are steps (or their reflexive transitive closure); in thick dark blue are hypotheses, and in light green are conclusions to prove; and the double line represents equality. To illustrate their use, we have overlaid these diagrams on top of the recomposition diagram: executing C2.g

executing C1.f ∗

W ≡

W½

Approach We prove that result (and its variant with undefined behaviour) by reusing the simulation diagrams that Thibault et al. [30] introduced to prove recomposition in SECOMP and that we reproduce in Figure 5. Because these diagrams were originally phrased in terms of arbitrary labelled

executing C2.g

executing C1.f

∗

∗ C2.g(27)

∗ ≡

∗

≡

∗ C2 .g

∼

(2 7

∼

W’

∼

∼ ∗

Figure 5a

∗

∗

∗ ∼

∗ ∼

)

∗ ∗ C2.g(27)

Figure 5c

≡

∗

≡

∗

∗

∗

∗

Figure 5b

s2

≡

s2

≡

=

s1

ε

s′2

∼

ε s3

s1

≡

∼

∼ M

s′1

ε

s1

s′3

M

(a) Silent step in strongly related states

M

s3

s2

≡

a

s′1

a

s′2

∼

∼ =

s1

s3

M

M

(b) Silent step in weakly related states

∼

≡ a

s3

s′3

M

(c) Non-silent step with swapping relations

Fig. 5. Recomposition diagrams from SECOMP [30]

Figure 5a states that strongly-related executions proceed in lockstep. In the example, we are currently executing C1.f, the states of W and W½ are strongly related while the states of W½ and W' are weakly related, and W takes a silent step. We must prove that W½ takes a silent step, and reestablish the relations: the new states of W and W½ are strongly related, while the new state of W½ is still weakly related to that of W'. Figure 5b captures the fact that the weakly-related execution can step silently. In the example, we are currently executing C2.g, the states of W' and W½ are strongly related while the states of W½ and W are weakly related, and W takes a silent step. We must prove that this step preserves the weak relation, i.e. that the new state of W is still related to the state of W½. Informally, this diagram allows the weakly related execution to catch up to the other two. Finally, Figure 5c captures what happens during a step that produces an event: all executions must produce the same event, and the relations must be reestablished. In the example, we are switching from C1 to C2, which is exactly the boundary between the two parts that make W½ up, and as a result the relations are swapped: before the call, the states of W and W½ were strongly related and the states of W½ and W' were weakly related, and now it must be the opposite: the new states of W and W½ are now weakly related, and the states of W½ and W' are now strongly related. In particular, Figure 5b is the key to understanding why blame-aware recomposition works: running C ▷◁ P can only exhibit undefined behaviour within C, and the state of C ▷◁ P is then weakly related to the recomposed one. This means what happens in that execution doesn’t really matter: what matters is that the weak and mixed relations are preserved, and those only need to be precise enough to prove Figure 5c when needed, which in practice lets us use relations that don’t mention the internal state of the weakly related execution in a way that would be invalidated by undefined behaviour happening. Together with a proof that the initial states satisfy the simulation relations, these diagrams can be composed one by one to imply the existence of the recomposed execution, and so they imply blame-aware recomposition. Defining the Simulation Relations We can now describe how we instantiate these three simulation relations concretely. In our micro-policy machine, states are triples s = (m, regs, PC), and we use notations such as colour or code to inspect fields of the tags. How do we define the strong relation? First, the strong

and weak relations should only describe one side of the split between partial program and context, so we parameterize them with I = P|C, and we use ≡P and ∼C when the execution is in P, and ≡C and ∼P when the execution is in C, as depicted below. C ▷◁ P ≡P

∼P

C′ ▷◁ P ∼C

≡C

C′ ▷◁ P′

We define ≡I as follows: colour(PC) = colour(PC′ ) = c

c ∈ I (1)

′

PC = PC + offset(c) (2) regs ≃I regs′ (3)

m ≃I m′ (4)

(m, regs, PC) ≡I (m′ , regs′ , PC′ ) During the simulation, strongly related states are always in the same compartment, one that belongs to I, as captured by condition (1). More than this, strongly related states are always executing the same instruction, since they follow the same code. However, the condition PC′ = PC would be incorrect. Indeed, the code layout might have changed, and so actually there is a fixed offset for each compartment c, offset(c), between the original programs and the recomposed one. Hence condition (2). Then, to know that the same instructions are going to lead to the same results (otherwise the two strongly related executions would not be in lockstep), we need to know that the content of the registers and of the memory is the same: this is captured by (3) and (4). The relations ≃I on registers and memories relate the content of these registers and memories: for instance, we define ≃I on memories to be: m ≃I m′ ≜ (∀w d. colour(d) ∈ I ∧ ¬code(d) =⇒ m(w) = d =⇒ m′ (w) = d) ∧ ′

(∀w d . colour(d′ ) ∈ I ∧ ¬code(d′ ) =⇒ m′ (w) = d′ =⇒ m(w) = d′ ) ∧ . . . We have elided some well-formedness predicates on the memories and registers that state that the return addresses stored in registers and in memory point to code belonging to the same compartment. Any piece of data in m belonging to a compartment that is in I can be found at the same address in

m′ : this captures the fact that strongly related compartments have done the exact same sequence of memory operations, and is enabled by the allocation mechanism hiding the data layout of each compartment. The weak relation is defined in a similar manner: colour(PC) = colour(PC′ ) = c c ∈ / I (1)

m ≃I m′ (4)

(m, regs, PC) ∼I (m′ , regs′ , PC′ ) Note that we keep (1) (except that the states that are related are the ones not executing) and (4), but we drop the requirements on the PC and on the registers. Indeed, in the weakly related states, the execution doesn’t proceed in lockstep (recall the diagrams from the previous section), and so the internal details don’t need to be synchronized. We keep conditions on the memory, but note that the weak relation mentions state outside the one that is executing. The key takeaway for both these relations is that they only quantify over the parts of the programs that are actually kept in the recomposed execution: when the execution is inside P, then ≡P is used for the strong relation and relates the parts of the state that belong to P, and ∼C is used for the weak relation and relates the parts of the state that belong to C′ . tag(PC) = tag(PC′ ) = tag(PC′′ ) = (Level n, c) (a) Sn (s, m, m′ , m′′ ) (b)

...

Ms (m, regs, PC) (m′ , regs′ , PC′ ) (m′′ , regs′′ , PC′′ ) Finally, we also have a mixed relation, which is parameterized by a shadow stack s, where stack frames quadruples containing three return addresses and one colour. The shadow stack keeps track of the cross-compartment return addresses, ensuring they are in sync. This is captured by the two conditions (a), which enforce that the stack is at the same level in all three executions, and (b), which is defined by the two following rules. S0 (·, m, m′ , m′′ ) c ∈ P =⇒ vc = v c ∈ C =⇒ vc = v ′ (c) ′′ v = vc + offset(c) codec (m, v)

codec (m′ , v ′ ) codec (m′′ , v ′′ ) (d) Sn (s, m, m′ , m′′ )

Sn+1 ((v, v ′ , v ′′ , c) :: s, m, m′ , m′′ ) The rule for the empty stack is clear. For adding a stack frame on the stack, the rule is slightly more involved. Conditions (d) capture the fact that the return addresses point to code inside c. Then, following (c), how the return addresses are related depends on which compartment they target. If they target a compartment in P, then the return address v ′′ in the recomposed execution must be related to v, so that they point to the same instruction (with an offset because the code layout has changed). Conversely, if they target a compartment in C, then v ′′ must be related to v ′ , not v.

Reasoning about these three relations actually requires reasoning about the compartmentalization mechanism that is implemented: for instance, one of the key invariants that we need to establish to prove blame-aware recomposition is the uniqueness of the linear return capabilities. Another one is that we need to reason about the memory layout and consider various edge cases, such as adding conditions on the size of the code (it should not be too large or it would overflow into the data region). This supports our argument that blame-aware recomposition allows us to reason about a lower-level backend compared to the previous proof technique. 4.3

Formalization

We have implemented the allocator changes to the micropolicy backend of Abate et al. We have used our technique to prove RSCDC MD between our overlay semantics and the lowlevel semantics of our updated backend. We have also proved RSCDC MD between the source language of Abate et al. and our updated micro-policy backend, under a few additional assumptions, mainly that the source executions do not go beyond the limits of the machine (our source uses unbounded integers, whereas our backend uses concrete 32-bit integers). Everything is done within the Rocq proof assistant, and the full development can be found as supplementary materials.

5

Related Work

We build on top of the work of Abate et al. [1, 2]. Researchers have since developed various other extensions of this work focused on adding new features or proving stronger results. For instance, SECOMP [30] focuses on scaling to a realistic source language, by extending CompCert [18] with a compartmentalization mechanism and proving it secure. Thibault et al. [31] propose an extension of the back-translation that lets them prove a stronger security result that requires code confidentiality. El-Korashy et al. [10] add the possibility for components to share memory by exchanging pointers. Both of these extensions are seemingly incompatible with our work: the first one requires recomposition to hold at the lowest level considered, while with the second one, exchanging pointers irremediably leaks some of the components’ internal behaviour if they can be freely compared. Building and verifying low-level backends for compilers is a long-standing research problem. The state-of-the-art verified C compiler, CompCert [18, 19], targets relatively high-level backends that use a block-based memory model. As a result, it is impossible to model many behaviours such as buffer overflows or stack overflows. Various extensions of CompCert make progress towards more realism: CompCertMC [33] extends CompCert with lower-level backends that have flat memory spaces. Its successor CompCertELF [34] adds a verified assembler that produces ELF object files, concatenating the code together with data. However, all these works focus on correct compilation only, and in particular they do not support linking with arbitrary code. Other verification projects have focused on low-level compartmentalization, and in particular the verification of SFI

schemes, either at the assembly level [21, 37] or at higher levels [5, 16]. The techniques SFI uses to isolate different compartments’ memory regions from each other are similar to the changes we make to the backend’s memory allocation scheme. In our setting, however, because we have access to a monitor and a tagging mechanism, we do not need to introduce all the complexity that is inherent to SFI-based solutions. Overlay semantics were introduced by Skorstengaard et al. [27] in the context of secure compilation, to formally characterize the security of their calling convention: their overlay semantics has built-in local-state encapsulation and wellbracketed control flow. Later, Georges et al. [11] also added temporal elements to their overlay semantics, allowing them to characterize some temporal aspects of the stack safety. In both works, the authors prove that their concrete implementation of the calling convention is fully abstract w.r.t. their overlay semantics. In [15], Kolosick et al. use overlay semantics to characterize the well-behavedness of Wasm programs. They use this semantics to justify the correctness of the removal of some protections in the Wasm binaries. The main difference between all these works and ours is that while they use overlay semantics as a characterization of the expected behaviour of their programs, we use them merely as a proof technique. More plainly, our RSCDC MD theorem is a direct statement about the kind of properties that are preserved by the compiler, while one needs to understand and trust their overlay semantics in order to understand their theorems.

6

Conclusion and Future Work

We have proposed a proof technique for verifying low-level secure compiler backends. Our proof technique is a variant of a previous proof technique from the literature, and relies on blame-aware recomposition, a technical lemma that allows recomposing programs together. The idea behind it is to characterize some problematic behaviours for the previous proof technique as undefined behaviours w.r.t. an overlay semantics, and to exploit the fact that some of the programs that are manipulated are actually compiled, and thus free of such undefined behaviours. We have reported on the application of that proof technique to an existing backend using micro-policies (essentially tag-based monitors) as a protection mechanism to implement compartmentalization. There are still several questions that we believe are worth studying, and it would be nice to investigate how far one can take our proof technique, in different directions. For instance, how does the proof technique scale to larger and more realistic projects? SECOMP [30] showed that it is possible to prove RSCDC MD for a realistic compartmentalizing compiler; is it still the case if one wishes to go lower-level? Another question is whether we could adapt our proofs to the SFI backend of Abate et al. The difficulty here is that the invariants of SFI are much more complex than ours, since we benefit from having fine-grained tags. Another direction would be to study what criteria can be proved with this proof technique. The one we consider in this work, RSCDC MD , does not depend on the confidentiality of

the data or the code being run. Yet, the backend must still enforce some confidentiality of data for the proof technique to be applicable; can one then also obtain a stronger security criterion, in the manner of [31]? A final direction is what features can be added to the languages while preserving the ability to apply the proof technique. Memory sharing [9, 10] is one such feature: while it would be desirable to share memory directly between compartments, directly sharing pointers might re-introduce leaks concerning the allocation pattern of compartments. Finally, as we mentioned, recomposition and blame-aware recomposition still rely on code confidentiality, or at least the ability to build an overlay semantics with code confidentiality. It would be more satisfying to have a direct proof technique that doesn’t require this.

Acknowledgments This work was in part funded by the European Research Council under ERC Starting Grant SECOMP (715753), and by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under Germany’s Excellence Strategy – EXC 2092 CASA – 390781972. This research is supported by armasuisse Science and Technology. AI Usage GenAI tools were not used to write this paper, except for fixing grammar and spelling, for improving readability and tightening some existing paragraphs, for LaTeX programming, and for generating some of the figures from pen-and-paper sketches. Most of the proof work, including the generic proof technique and the main recomposition diagrams, was initially completed by the authors without GenAI tools. Claude Opus was later used to prove auxiliary technical lemmas (results about machine word arithmetic and bitwise operations) as well as to prove symmetric variants of some of the diagrams and clean up proofs.

References [1] C. Abate, A. Azevedo de Amorim, R. Blanco, A. N. Evans, G. Fachini, C. Hriţcu, T. Laurent, B. C. Pierce, M. Stronati, and A. Tolmach. When good components go bad: Formally secure compilation despite dynamic compromise. CCS. 2018. [2] C. Abate, A. Azevedo de Amorim, R. Blanco, A. N. Evans, G. Fachini, C. Hritcu, T. Laurent, B. C. Pierce, M. Stronati, J. Thibault, and A. Tolmach. When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise, 2019. Extended version of a paper previously published at CCS’18. Updates the proof technique to use recomposition. [3] C. Abate, R. Blanco, D. Garg, C. Hriţcu, M. Patrignani, and J. Thibault. Journey beyond full abstraction: Exploring robust property preservation for secure compilation. CSF, 2019. [4] A. Azevedo de Amorim, M. Dénès, N. Giannarakis, C. Hriţcu, B. C. Pierce, A. Spector-Zabusky, and A. Tol-

mach. Micro-policies: Formally verified, tag-based security monitors. Oakland S&P. 2015. [5] F. Besson, S. Blazy, A. Dang, T. Jensen, and P. Wilke. Compiling sandboxes: Formally verified software fault isolation. ESOP, 2019. [6] M. Castro, M. Costa, J. Martin, M. Peinado, P. Akritidis, A. Donnelly, P. Barham, and R. Black. Fast bytegranularity software fault isolation. SOSP. 2009. [7] S. Chiricescu, A. DeHon, D. Demange, S. Iyer, A. Kliger, G. Morrisett, B. C. Pierce, H. Reubenstein, J. M. Smith, G. T. Sullivan, A. Thomas, J. Tov, C. M. White, and D. Wittenberg. SAFE: A clean-slate architecture for secure systems. HST, 2013. [8] C. Cimpanu. Microsoft: 70 percent of all security bugs are memory safety issues. ZDNet, 2019. [9] A. El-Korashy, S. Tsampas, M. Patrignani, D. Devriese, D. Garg, and F. Piessens. CapablePtrs: Securely compiling partial programs using the pointers-as-capabilities principle. CSF. 2021. [10] A. El-Korashy, R. Blanco, J. Thibault, A. Durier, D. Garg, and C. Hriţcu. SecurePtrs: Proving secure compilation with data-flow back-translation and turntaking simulation. CSF, 2022. [11] A. L. Georges, A. Trieu, and L. Birkedal. Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities. PACMPL, 6 (OOPSLA), 2022. [12] K. Gudka, R. N. M. Watson, J. Anderson, D. Chisnall, B. Davis, B. Laurie, I. Marinos, P. G. Neumann, and A. Richardson. Clean application compartmentalization with SOAAP. CCS. 2015. [13] A. Jeffrey and J. Rathke. Java Jr: Fully abstract trace semantics for a core Java language. ESOP. 2005. [14] D. Kilpatrick. Privman: A library for partitioning applications. USENIX FREENIX. 2003. [15] M. Kolosick, S. Narayan, E. Johnson, C. Watt, M. LeMay, D. Garg, R. Jhala, and D. Stefan. Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI. PACMPL, 6(POPL), 2022. [16] J. Kroll, G. Stewart, and A. Appel. Portable software fault isolation. CSF. 2014. [17] J. Laird. A fully abstract trace semantics for general references. ICALP. 2007. [18] X. Leroy. Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. POPL. 2006. [19] X. Leroy. A formally verified compiler back-end. JAR, 43(4), 2009. [20] X. Leroy and S. Blazy. Formal verification of a Clike memory model and its uses for verifying program transformations. JAR, 41(1), 2008. [21] G. Morrisett, G. Tan, J. Tassarotti, J.-B. Tristan, and E. Gan. RockSalt: Better, faster, stronger SFI for the x86. PLDI. 2012. [22] S. Narayan, C. Disselkoen, T. Garfinkel, N. Froyd, E. Rahm, S. Lerner, H. Shacham, and D. Stefan.

Retrofitting fine grain isolation in the Firefox renderer. USENIX Security. 2020. [23] M. Patrignani and D. Clarke. Fully abstract trace semantics for protected module architectures. CL, 42, 2015. [24] M. Patrignani and D. Garg. Robustly safe compilation, an efficient form of secure compilation. ACM Trans. Program. Lang. Syst., 43(1), 2021. [25] C. Reis and S. D. Gribble. Isolating web programs in modern browser architectures. EuroSys. 2009. [26] C. Reis, A. Moshchuk, and N. Oskov. Site isolation: Process separation for web sites within the browser. USENIX Security. 2019. [27] L. Skorstengaard, D. Devriese, and L. Birkedal. StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. PACMPL, 3 (POPL), 2019. [28] G. Tan. Principles and implementation techniques of software-based fault isolation. FTSEC, 1(3), 2017. [29] The Chromium Project. Memory safety. chromium.org, 2022. [30] J. Thibault, R. Blanco, D. Lee, S. Argo, A. Azevedo de Amorim, A. L. Georges, C. Hriţcu, and A. Tolmach. SECOMP: Formally secure compilation of compartmentalized C programs. CCS. 2024. [31] J. Thibault, J. Lenormand, and C. Hriţcu. Nanopass backtranslation of call-return trees for mechanized secure compilation proofs. ITP. 2025. [32] R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficient software-based fault isolation. SOSP, 1993. [33] Y. Wang, P. Wilke, and Z. Shao. An abstract stack based approach to verified compositional compilation to machine code. PACMPL, 3(POPL), 2019. [34] Y. Wang, X. Xu, P. Wilke, and Z. Shao. CompCertELF: verified separate compilation of C programs into ELF object files. PACMPL, 4(OOPSLA), 2020. [35] R. N. M. Watson, P. G. Neumann, J. Woodruff, M. Roe, H. Almatary, J. Anderson, J. Baldwin, G. Barnes, D. Chisnall, J. Clarke, B. Davis, L. Eisen, N. W. Filardo, R. Grisenthwaite, A. Joannou, B. Laurie, A. T. Markettos, S. W. Moore, S. J. Murdoch, K. Nienhuis, R. Norton, A. Richardson, P. Rugg, P. Sewell, S. Son, and H. Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8). Technical Report UCAM-CL-TR-951, University of Cambridge, Computer Laboratory, 2020. [36] B. Yee, D. Sehr, G. Dardyk, J. B. Chen, R. Muth, T. Ormandy, S. Okasaka, N. Narula, and N. Fullagar. Native Client: A sandbox for portable, untrusted x86 native code. CACM, 53(1), 2010. [37] L. Zhao, G. Li, B. De Sutter, and J. Regehr. ARMor: Fully verified software fault isolation. EMSOFT. 2011.

Related documents

• CauSec: Unboxing the Causal Drivers of Static Vulnerability Analysis Performance#467075
• BiShield-TEE: On the (In-)Security of Unilateral Weight Obfuscation in On-Device TEE-Shielded LLM Partition#1356901
• BiShield-TEE: On the (In-)Security of Unilateral Weight Obfuscation in On-Device TEE-Shielded LLM Partition#1348767
• Halting problem proofs refuted on the basis of software engineering ?#98758
• Security Requirements for the Unidirectional Lightweight Encapsulation (ULE) Protocol#501050