Security Results for SIRRTL, A Hardware Description Language for Information Flow Security
Loading...
No Access Until
Permanent Link(s)
Collections
Other Titles
Authors
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.
Journal / Series
Volume & Issue
Description
Sponsorship
Date Issued
2017-12
Publisher
Keywords
information flow security; hardware security; timing channels; chisel; verilog
Location
Effective Date
Expiration Date
Sector
Employer
Union
Union Local
NAICS
Number of Workers
Committee Chair
Committee Co-Chair
Committee Member
Degree Discipline
Degree Name
Degree Level
Related Version
Related DOI
Related To
Related Part
Based on Related Item
Has Other Format(s)
Part of Related Item
Related To
Related Publication(s)
Link(s) to Related Publication(s)
References
Link(s) to Reference(s)
Previously Published As
Government Document
ISBN
ISMN
ISSN
Other Identifiers
Rights
CC0 1.0 Universal
Types
article