Ferraiuolo, Andrew2018-08-182018-08-182017-12https://hdl.handle.net/1813/57673This document establishes security results for SIRRTL, a secure variant of the FIRRTL intermediate language. We developed ChiselFlow, a variant of the Chisel hardware design language [1] for information flow security. ChiselFlow extends Chisel, a hardware description language embedded in Scala. ChiselFlow allows the hardeware designer to describe security policies about the hardware that are checked at design-time. Much like Chisel, ChiselFlow gains much of the expressive power of the rich host language, Scala. However, security enforcement is done by a small intermediate language called SIRRTL, so the trusted component of ChiselFlow is small. ChiselFlow emits SIRRTL, a variant of the FIRRTL intermediate language augmented with an information flow type system. ChiselFlow supports security policies that depend on the run-time values of signals, though these policies are checked purely at design-time by SIRRTL. In this document, we prove that well-typed SIRRTL modules enforce a timing safe variant of noninterference. We constructed the HyperFlow processor using ChiselFlow thereby establishing high assurance in the implementation of the processor.en-USCC0 1.0 Universalinformation flow securityhardware securitytiming channelschiselverilogarticle