Caisson: a hardware description language for secure information flow

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 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-ev...

• Type: Journal
• Year: 2011
• Where: PLDI
• Authors: Xun Li 0001, Mohit Tiwari, Jason Oberg, Vineeth Kashyap, Frederic T. Chong, Timothy Sherwood, Ben Hardekopf
• Keywords: Hardware Architects, Hardware Description Language, Hardware Description Languages, PLDI 2011, Programming Languages