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.
Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos. Submitted to ICFP 2013. March 2013.
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.
Check out our motivational video at http://youtu.be/viCSLa7Njxs.
It gives a very high level motivation for why we need a clean slate approach to computer security, and then a simple demonstration of a few of the base hardware protections such as fat pointers and atomic group checks.