Verified Software-Based Fault Isolation

Presented as part of the 2013 HCSS conference.

ABSTRACT

Native Client (NaCL) is a new service provided by Google's Chrome for directly executing native binary code in the context of the browser.  The security of NaCL depends upon a binary checker that is meant to enforce a basic sandbox policy known as software-based fault isolation.  Recently, we built a new binary checker for NaCL and verified its correctness using the Coq proof assistant: If the checker says "yes" on a binary, and the binary is loaded into a suitable context, then the binary is guaranteed to respect the sandbox.

The primary challenge was building a model, in Coq, for an appropriate subset of the x86 architecture.  To support our desired theorem, the model needs to support symbolic reasoning about bit-level encodings of instructions and their semantics.  At the same time, the model needs to support efficient validation, so that we can compare its execution to real processors.  To address these problems, we embedded two domain specific languages into Coq, and used these languages to specify the syntax and semantics for the x86 respectively.  We then constructed provably correct compilers and interpreters to map these specifications to a relatively efficient executable model.