Welcome

Welcome to the home page of the SAFE project, funded under the DARPA CRASH program. We are creating a clean-slate design of a secure computing system, including tagged hardware, fine-grained checking, and formal verification.


SAFE Video on YouTube!

Check out our January 2014 video explaining the SAFE project, and why it is so important:

A Verified Information-Flow Architecture

Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach. To appear in 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 2014.

SAFE: A Clean-Slate Architecture for Secure Systems

SAFE is a large-scale, clean-slate co-design project encompassing hardware architecture, programming languages,and operating systems. Funded by DARPA, the goal of SAFE is to create a secure computing system from the ground up. SAFE hardware provides memory safety, dynamic type checking,and native support for dynamic information flow control. The Breeze programming language leverages the security features of the underlying machine, and the "zero kernel" operating system avoids relying on any single privileged component for overall system security.

Low-Fat Pointers: Compact Encoding and Efficient Gate-Level Implementation of Fat Pointers for Spatial Safety and Capability-based Security

By Albert Kwon, Udit Dhawan, Jonathan M. Smith, Thomas F. Knight, Jr., and André DeHon
To appear in the proceedings of the 20th ACM Conference on Computer and Communications Security, November 4-8, 2013, Berlin, Germany.

Testing Noninterference, Quickly

Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos. In 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 455-468, ACM. September 2013.

All Your IFCException Are Belong To Us

Cătălin Hriţcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett. IEEE Symposium on Security and Privacy (Oakland), pages 3-17, IEEE Computer Society Press, May 2013.

Initial release of bluespec source for SAFE processor (Oct. 2012)

Visit the page at Penn's Implementation of Computation Group to find releases of the bluespec source for the SAFE Processor. As of October 2012, that page includes the bluespec source and a few documents.

Pages

Subscribe to crash-safe.org RSS