eCommons

 

Security Results for SIRRTL, A Hardware Description Language for Information Flow Security

dc.contributor.authorFerraiuolo, Andrew
dc.date.accessioned2018-08-18T21:58:13Z
dc.date.available2018-08-18T21:58:13Z
dc.date.issued2017-12
dc.description.abstractThis 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_US
dc.identifier.urihttps://hdl.handle.net/1813/57673
dc.language.isoen_USen_US
dc.rightsCC0 1.0 Universal*
dc.rights.urihttps://creativecommons.org/publicdomain/zero/1.0/*
dc.subjectinformation flow securityen_US
dc.subjecthardware securityen_US
dc.subjecttiming channelsen_US
dc.subjectchiselen_US
dc.subjectverilogen_US
dc.titleSecurity Results for SIRRTL, A Hardware Description Language for Information Flow Securityen_US
dc.typearticleen_US

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
paper.pdf
Size:
159.68 KB
Format:
Adobe Portable Document Format
Description: