Name
Abstract | ||
|---|---|---|
Privacy and integrity are important security concerns. These concerns are addressed by controlling information flow, i.e., restricting how information can flow through a system. Most proposed systems that restrict information flow make the implicit assumption that the hardware used by the system is fully ``correct'' and that the hardware's instruction set accurately describes its behavior in all circumstances. The truth is more complicated: modern hardware designs defy complete verification; many aspects of the timing and ordering of events are left totally unspecified; and implementation bugs present themselves with surprising frequency. In this work we describe Sapper, a novel hardware description language for designing security-critical hardware components. Sapper seeks to address these problems by using static analysis at compile-time to automatically insert dynamic checks in the resulting hardware that provably enforce a given information flow policy at execution time. We present Sapper's design and formal semantics along with a proof sketch of its security. In addition, we have implemented a compiler for Sapper and used it to create a non-trivial secure embedded processor with many modern microarchitectural features. We empirically evaluate the resulting hardware's area and energy overhead and compare them with alternative designs. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2541940.2541947 | ASPLOS |
Keywords | Field | DocType |
hardware-level security policy enforcement,novel hardware description language,resulting hardware,modern microarchitectural feature,security-critical hardware component,important security concern,alternative design,modern hardware design,proposed system,information flow,information flow policy,hardware description language | Programming language,Computer science,Instruction set,Static analysis,Real-time computing,Policy enforcement,Computer hardware,Sketch,Hardware description language,Information flow (information theory),Parallel computing,Compiler,restrict | Conference |
Volume | Issue | ISSN |
42 | 1 | 0163-5964 |
Citations | PageRank | References |
33 | 0.99 | 30 |
Authors | ||
9 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Xun Li | 1 | 95 | 12.91 |
| Vineeth Kashyap | 2 | 181 | 8.73 |
| Jason K. Oberg | 3 | 178 | 6.45 |
| Mohit Tiwari | 4 | 445 | 23.94 |
| Vasanth Ram Rajarathinam | 5 | 77 | 3.30 |
| Ryan Kastner | 6 | 1779 | 147.73 |
| Timothy Sherwood | 7 | 1921 | 123.28 |
| Ben Hardekopf | 8 | 444 | 22.12 |
| Frederic T. Chong | 9 | 1428 | 130.07 |