Secure compartment isolation proofs handle shared low-level code views
Blame-aware Recomposition for Secure Compilation Proofs of Low-Level Compartment Isolation
Programming LanguagesCryptography and Security
Summary
Proving security for programs that isolate pieces of code, called compartments, is hard when those compartments can see each other’s code at a low level. Previous methods assumed the code was hidden, which is unrealistic for real computers. The authors extend these proofs by treating the observation of other compartments’ code as a special kind of undefined behavior. They introduce a new proof step called blame-aware recomposition that lets them safely prove security even when code is fully visible. Their approach applies to systems that protect compartments using programmable tags on memory references.
What this means in practice
- •For compiler developers: Create verified compilers that guarantee security for compartmentalized C code even when compartments can see each other's low-level code.
- •For operating system engineers: Design compartment isolation mechanisms using tag-based reference monitors with formal security proofs that hold against realistic low-level threats.
A theory result. No direct application yet.
Authors
Basile Schlosser, Jérémy Thibault, Catalin Hritcu
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.