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.

Area-Efficient Near-Associative Memories on FPGAs

FPGA '13, Feb. 11-13, Monterey, CA, USA. Authors: Udit Dhawan, André DeHon