Secure information flow verification with mutable dependent types
Andrew Ferraiuolo, Weizhe Hua, Andrew C. Myers, and G. Edward Suh

54th Design Automation Conference
June 2017, Austin, TX, USA


This paper presents a novel secure hardware description language (HDL) that uses an information flow type system to ensure that hardware is secure at design time. The novelty of this HDL lies in its ability to securely share hardware modules and storage elements across multiple security levels. Unlike with previous secure HDLs, secure sharing is achieved at a fine granularity and without implicitly adding hardware for security enforcement; this is important because the implicitly added hardware can break functionality and harm efficiency. The new HDL enables practical hardware designs that are secure, correct, and efficient. We demonstrate the practicality of the new HDL by using it to design and type-check a synthesized pipelined processor with protection rings and instructions that change modes.