CRASH/SAFE: Clean-slate Co-design of a Secure Host Architecture

An important cause for the insecurity of today’s computer systems is security–performance trade-offs made decades ago, which are now deeply embedded in the hardware and software ecosystem, but which are based on assumptions that are now obsolete. We are now living in an era in which security is no longer a side issue, hardware resources are abundant, and formal methods are more practical, so the time is ripe for a redesign.

The CRASH/SAFE project brings together academics (University of Pennsylvania, Harvard, and Northeastern) and industry (BAE Systems and Clozure Associates), with the very ambitious goal of designing a significantly more secure network host from scratch, without any legacy constraints. In this DARPA-funded project, we have undertaken a clean-slate co-design of novel hardware, operating system, programming language, and verification strategy based on modern cost structure and capabilities.

The SAFE hardware and a very thin layer of privileged software (a zero-kernel operating system), provide a run-time system for Breeze, a safe high-level language in which application software is written. This simpler design eliminates some of the traditional sources of complexity in operating systems and makes formal analysis more tractable. Moreover, safety and security are enforced at all layers of the system, not just at the programming language level. The SAFE hardware and runtime system dynamically enforce type and memory safety as well as fine-grained dynamic information-flow control (IFC) and label-based access control (clearance).

I’m going to talk about the CRASH/SAFE project in general and about a couple of specific research problems on which I’ve been working. I will focus on the novel exception handling mechanism in Breeze, which allows IFC violations to be recoverable exceptions as opposed to fatal stop-the-world failures. This work identifies public labels and delayed exceptions as the crucial ingredients for making all errors recoverable in a sound and usable language with fine-grained dynamic IFC. Finally, I’m going to discuss several directions for future research.