What a Sandbox Proof Establishes and What It Assumes

An argument that a sandbox is secure is usually informal: a list of checks, a claim that they cover the operations that matter, and an assurance that the code performing them has been reviewed. Formal verification replaces the assurance with a machine-checked proof, and in doing so it makes visible something the informal argument hides: the set of things the proof assumes without proving them. That set is where the security actually lives.

The shape of the claim

A verified sandbox is stated as a theorem about an abstract machine. The theorem has the form: for any initial state satisfying the invariants, any sequence of steps the machine takes preserves the isolation property, where the isolation property is a relation between the states of two subjects.

The proof is by induction over the execution. The induction step requires showing that each instruction of the abstract machine preserves the invariant, which reduces to a lemma per instruction. The base case requires showing that the initial state satisfies the invariant, which reduces to a lemma about the initialization code. The lemmas are discharged by a proof assistant, and the assistant checks that each proof is a valid derivation in its logic.

The value of this construction is that it forces every step to be accounted for. An informal argument can skip a case, and the skip is invisible; a proof cannot, because the induction is total over the machine’s transition relation. The cost is that the abstract machine must be defined, and the definition is a specification, which is where the first gap appears.

The specification gap

The theorem is about the abstract machine. The running system is an implementation, and the connection between them is either a refinement proof or an assumption.

A refinement proof shows that the implementation’s observable behaviour is a behaviour of the abstract machine, and it is the expensive part. seL4’s verification is the standard example: the kernel’s C implementation is connected to an abstract specification through a chain of intermediate specifications, and the refinement proofs between them are machine-checked. The chain is long because each intermediate level abstracts a different concern: the executable specification, the design, and the abstract model with its security properties.

Without refinement, the theorem says something about a model and nothing about the binary. The gap is not hypothetical: an implementation can differ from its specification in ways the specification does not mention, and those ways are where defects live. A sandbox whose C code has an integer overflow in a bounds computation is a correct implementation of a specification that says “the index is checked”, and the specification is not wrong; it is silent about how the check is performed.

The second form of the gap is more common and harder to close. The specification itself may be weaker than the property the user cares about. A proof that a tenant cannot write another tenant’s memory is not a proof that the tenant cannot read it, cannot infer it through timing, or cannot exhaust the shared allocator. Each of those is a separate property requiring a separate specification, and a verification effort that establishes one does not establish the others. The timing property in particular is the one that formal methods handle worst, for the reasons the covert-channel discussion sets out: the proof is about states, and a duration is not a state. The enumeration of properties is therefore part of the trusted base: someone decided which properties to prove, and the decision is not checked by the proof.

Proof-carrying code and the untrusted producer

Necula’s proof-carrying code inverts the usual arrangement. Instead of the consumer verifying the producer’s code by analyzing it, the producer supplies a proof alongside the code, and the consumer checks the proof. The check is cheap relative to the analysis, because checking a derivation is easier than finding one.

The security property is stated as a safety predicate on the code, and the proof demonstrates that the code satisfies it. For memory safety, the predicate might be that every load and store is within a declared region; for control flow, that every branch target is a declared entry point. The consumer’s trusted base is the proof checker and the specification of the safety predicate, not the compiler that produced the code.

The mechanism is attractive because it removes the compiler from the trusted base. A code producer may use any compiler, including one with bugs, and if the produced code carries a valid proof, the consumer can run it safely. The proof is checked against the code as it exists, not against the source the compiler claims to have compiled.

The costs are substantial and explain why the technique is not widespread. Generating the proofs requires the compiler to be instrumented to emit them, which means the compiler must be modified and the modification must be correct enough to produce checkable derivations. The proofs are large, so the transmission cost is real. And the safety predicate must be expressive enough to be useful and simple enough to check cheaply, which is a narrow window.

The trusted base, restated for a verified system

For a verified sandbox, the trusted base is not smaller in kind; it is different in composition.

The proof checker. A defect in the checker means an invalid proof is accepted, and the checker is a large program. The standard mitigation is to have a small kernel in the checker that validates the derivation, with the rest of the system as heuristics that propose proofs. This is the architecture of the major proof assistants: a small trusted kernel, a large elaborator.

The specification. The properties proved are the properties someone wrote down. A verified kernel that proves non-interference between its own partitions says nothing about a device driver that writes to memory the kernel did not mediate, unless the driver’s behaviour is in the model.

The hardware and firmware. The abstract machine assumes an execution model: memory that behaves as an array, instructions that do what the model says, and no faults outside the model. Rowhammer, speculative execution, and microarchitectural faults are all outside that model, and each has been demonstrated to break isolation in systems whose software was correct by its own specification.

The compiler and runtime that produce the binary. Unless the refinement chain reaches the machine code, the compiler is assumed correct. A verified compiler exists for a substantial subset of C, but it is an exception rather than a norm, and the verification of a compiler is a separate large effort.

The configuration. A verified mechanism enforces the policy it is given, and the policy is data. A system that proves “no subject can access memory outside its granted regions” proves nothing about whether the grants are correct, and misconfigured grants are the common cause of real isolation failures.

The last item is the one most often overlooked. The proof is about the mechanism; the security outcome depends on the policy; and the policy is written by people using an interface whose semantics may be misunderstood. A verified microkernel with a capability system still fails if a component is given a capability it should not have, and the proof of the mechanism does not detect the mistake.

What verification buys in practice

Three concrete benefits, each of which is real and none of which is “the system is secure”.

It eliminates a class of defect. Memory-safety bugs in the verified component are excluded by the proof, which means the component’s attack surface is its specification and its interface, not its implementation. For a kernel, that removes a large class of privilege-escalation defects from the verified component.

It makes the assumptions explicit. A verification effort must state its model, its invariants, and its refinement chain, and each statement is a document that a reviewer can attack. The informal alternative leaves the assumptions implicit, and implicit assumptions are the ones that turn out to be false.

It survives refactoring. A proof is a property of the code, and a change that breaks the property fails to verify. This is a stronger guarantee than a test suite, which only checks the cases it enumerates, and it is why verified components can be maintained by people who did not write them.

The corresponding limits are equally concrete. Verification does not establish that the policy is right, that the model matches the hardware, that the properties chosen are the ones that matter, or that the unverified components in the same system are safe. A verified sandbox surrounded by unverified code has the security of the unverified code, because the sandbox’s guarantee is conditional on the boundary it is given.

The practical reading for runtime design

The lesson for a language runtime is not that verification is required. It is that the structure a verification effort demands is the structure a careful design should have anyway.

Enumerate the mediated operations. A verifier must define the machine’s transition relation, and doing so forces a complete list of the ways state can change. The list is exactly what the reference-monitor argument needs, and most sandbox defects are operations that were omitted from the list rather than operations that were checked incorrectly.

State the property precisely. “The tenant cannot reach another tenant’s data” must be made into a relation over states, and the act of formalizing it exposes the ambiguities: does “reach” include reading through a shared buffer, does it include inferring through timing, does it include affecting availability. Each answer is a different property with a different cost.

Identify the assumptions. The model, the hardware, the compiler, the policy. Writing them down converts an implicit trust into a reviewable claim, and the review is where the design improves.

Keep the trusted base small enough to argue about. This is the same principle as economy of mechanism, restated in the terms a verification effort uses: every component in the base is a component whose correctness must be established, and the argument for the whole system is only as strong as the weakest of them. The articles in this cluster have each described one boundary and its costs; the reason to prefer several boundaries over one is that a defect must then defeat all of them, and the reason to keep each boundary small is that a boundary nobody can analyze is a boundary nobody can trust.