Title: Whole-system security with machine-checked verification
Advisors: Xi Wang, Arvind Krishnamurthy, and Emina Torlak
Abstract: Chimera is a new framework for developing applications with formal, whole-system security guarantees. It employs a systematic approach to decomposing a security property and using a portfolio of theorem provers to discharge the result- ing proof obligations. It allows programmers to specify and verify cryptographic security properties about their applica- tions at the level of assembly code, without trusting the com- piler or runtime; it also allows programmers to invoke auto- mated provers when possible. To further reduce the proof burden, Chimera introduces a security kernel, which allows verified applications to safely reuse unverified components (e.g., off-the-shelf Linux) through sandboxing.
We have implemented Chimera for 64-bit ARM, and used it to build a set of five Chimera applications: a chat client, as well as a notary app, an incrementer app, a password hasher, and a differential privacy service ported from the Ironclad project. Our experience shows that these applications built using Chimera can provide both functional correctness and cryptographic security properties through formal verifica- tion, with a moderate proof effort.