Welcome to the SAFE project.

homemade FPGA enclosure booting SAFE

SAFE is a secure computing platform built on a tagged hardware architecture that supports maintenance, propagation, and per-instruction checking of arbitrary per-word metadata. The metadata rule engine can enforce a wide range of security policies, including memory safety, control flow integrity, information flow secrecy, capabilities, software fault isolation, language-specific dynamic typing, and more. The least-privilege runtime separates computation into threads that do not share memory, and values are communicated across hardware-supported, tagged streams.

Area-Efficient Near-Associative Memories on FPGAs

ACM Transactions on Reconfigurable Technology and Systems (TRETS) , Volume 7, Number 4, DOI: 10.1145/2629471, January, 2015.

Associative memories can map sparsely used keys to values with low latency but can incur heavy area overheads. The lack of customized hardware for associative memories in today’s mainstream FPGAs exacerbates the overhead cost of building these memories using the fixed address match BRAMs. In this article, we develop a new, FPGA-friendly, memory system architecture based on a multiple hash scheme that is able to achieve near-associative performance without the area-delay overheads of a fully associative memory on FPGAs. At the same time, we develop a novel memory management algorithm that allows us to statistically mimic an associative memory. Using the proposed architecture as a 64KB L1 data cache, we show that it is able to achieve near-associative miss rates while consuming 3–13× fewer FPGA memory resources for a set of benchmark programs from the SPEC CPU2006 suite than fully associative memories generated by the Xilinx Coregen tool. Benefits for our architecture increase with key width, allowing area reduction up to 100×. Mapping delay is also reduced to 3.7ns for a 1,024-entry flat version or 6.1ns for an area-efficient version compared to 17.6ns for a fully associative memory for a 64-bit key on a Xilinx Virtex 6 device.

Copyright Dhawan and DeHon 2015. This is the author’s version of the work. It is posted here for your personal use. Not for redistribution. The definitive version was published in ACM Transactions on Reconfigurable Technology and Systems (TRETS), http://dx.doi.org/10.1145/2629471

Architectural Support for Software-Defined Metadata Processing

Accepted into 20th International Conference on Architectural Support for Programming Languages and Operating Systems, March 14-18, 2015, Istanbul, Turkey.

Hardware for propagating and checking software-programmable metadata tags can achieve low runtime overhead when carefully implemented. We generalize prior work on hardware tagging by considering a generic architecture that supports software-defined policies over metadata of arbitrary size and complexity. We introduce several novel microarchitectural optimizations that keep the overhead of this rich processing low. Our model thus achieves the efficiency of previous hardware-based approaches with the flexibility of the software-based ones. We demonstrate this by using it to enforce four diverse safety and security policies—spatial and temporal memory safety, taint tracking, control-flow integrity, and code and data separation —plus a composite policy that enforces all of them simultaneously. Experiments on SPEC CPU2006 benchmarks show modest impact on runtime (typically under 10%) and power ceiling (less than 10%), in return for some increase in energy usage (typically under 60%) and area for on-chip memory structures (110%).


A Verified Information-Flow Architecture

In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, CA USA. January 22, 2014.

SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to control information flow in SAFE and an end-to-end proof of noninterference for this model.