| Autor: |
Li, Xun, Kashyap, Vineeth, Oberg, Jason K, Tiwari, Mohit, Rajarathinam, Vasanth Ram, Kastner, Ryan, Sherwood, Timothy, Hardekopf, Ben, Chong, Frederic T |
| Rok vydání: |
2014 |
| Předmět: |
|
| Zdroj: |
ACM SIGARCH Computer Architecture News, vol 42, iss 1 |
| Popis: |
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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
