Show simple item record

dc.contributor.authorFerraiuolo, Andrew
dc.date.accessioned2018-08-18T21:58:13Z
dc.date.available2018-08-18T21:58:13Z
dc.date.issued2017-12
dc.identifier.urihttps://hdl.handle.net/1813/57673
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.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 in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Except where otherwise noted, this item's license is described as CC0 1.0 Universal

Statistics