Title: Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract),
Abstract: We propose a new formal criterion for secure compilation, providing strong
security guarantees for components written in unsafe, low-level languages with
C-style undefined behavior. Our criterion goes beyond recent proposals, which
protect the trace properties of a single component against an adversarial
context, to model dynamic compromise in a system of mutually distrustful
components. Each component is protected from all the others until it receives
an input that triggers an undefined behavior, causing it to become compromised
and attack the remaining uncompromised components. To illustrate this model, we
demonstrate a secure compilation chain for an unsafe language with buffers,
procedures, and components, compiled to a simple RISC abstract machine with
built-in compartmentalization. The protection guarantees offered by this
abstract machine can be achieved at the machine-code level using either
software fault isolation or tag-based reference monitoring. We are working on
machine-checked proofs showing that this compiler satisfies our secure
compilation criterion.