Security Results for SIRRTL, A Hardware Description Language for Information Flow Security
dc.contributor.author | Ferraiuolo, Andrew | |
dc.date.accessioned | 2018-08-18T21:58:13Z | |
dc.date.available | 2018-08-18T21:58:13Z | |
dc.date.issued | 2017-12 | |
dc.description.abstract | This 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.uri | https://hdl.handle.net/1813/57673 | |
dc.language.iso | en_US | en_US |
dc.rights | CC0 1.0 Universal | * |
dc.rights.uri | https://creativecommons.org/publicdomain/zero/1.0/ | * |
dc.subject | information flow security | en_US |
dc.subject | hardware security | en_US |
dc.subject | timing channels | en_US |
dc.subject | chisel | en_US |
dc.subject | verilog | en_US |
dc.title | Security Results for SIRRTL, A Hardware Description Language for Information Flow Security | en_US |
dc.type | article | en_US |
Files
Original bundle
1 - 1 of 1