Name
Abstract | ||
|---|---|---|
Information flow is an important security property that must be incorporated from the ground up, including at hardware design time, to provide a formal basis for a system's root of trust. We incorporate insights and techniques from designing information-flow secure programming languages to provide a new perspective on designing secure hardware. We describe a new hardware description language, Caisson, that combines domain-specific abstractions common to hardware design with insights from type-based techniques used in secure programming languages. The proper combination of these elements allows for an expressive, provably-secure HDL that operates at a familiar level of abstraction to the target audience of the language, hardware architects. We have implemented a compiler for Caisson that translates designs into Verilog and then synthesizes the designs using existing tools. As an example of Caisson's usefulness we have addressed an open problem in secure hardware by creating the first-ever provably information-flow secure processor with micro-architectural features including pipelining and cache. We synthesize the secure processor and empirically compare it in terms of chip area, power consumption, and clock frequency with both a standard (insecure) commercial processor and also a processor augmented at the gate level to dynamically track information flow. Our processor is competitive with the insecure processor and significantly better than dynamic tracking. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/1993498.1993512 | PLDI |
Keywords | Field | DocType |
secure information flow,hardware design time,hardware architect,insecure processor,information-flow secure programming language,hardware design,secure processor,new hardware description language,commercial processor,provably information-flow secure processor,secure hardware,state machine,verification,provable security,chip,hardware description language,programming language,information flow | Pipeline (computing),Information flow (information theory),Programming language,Cache,Computer science,Real-time computing,Finite-state machine,Theoretical computer science,Compiler,Verilog,Clock rate,Hardware description language | Conference |
Volume | Issue | ISSN |
46 | 6 | 0362-1340 |
Citations | PageRank | References |
38 | 1.09 | 40 |
Authors | ||
7 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Xun Li | 1 | 127 | 5.94 |
| Mohit Tiwari | 2 | 445 | 23.94 |
| Jason K. Oberg | 3 | 178 | 6.45 |
| Vineeth Kashyap | 4 | 181 | 8.73 |
| Frederic T. Chong | 5 | 1428 | 130.07 |
| Timothy Sherwood | 6 | 1921 | 123.28 |
| Ben Hardekopf | 7 | 444 | 22.12 |