Lightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis (Technical Report)
Loading...
No Access Until
Permanent Link(s)
Collections
Other Titles
Abstract
Hardware-based mechanisms for software isolation are becoming
increasingly popular, but implementing these mechanisms correctly has
proved difficult, undermining the root of security.
This work introduces an effective way to formally verify important
properties of such hardware security mechanisms. In our approach,
hardware is developed using a lightweight security-typed hardware
description language (HDL) that performs static information flow analysis.
We show the
practicality of our approach by implementing and verifying a
simplified but realistic multi-core prototype of the ARM TrustZone
architecture.
To make the security-typed HDL expressive enough to verify
a realistic processor, we develop new type system features.
Our experiments suggest that information flow analysis
is efficient, and programmer effort is modest. We also show that information
flow constraints are an effective way to detect hardware
vulnerabilities, including several found in commercial processors.
Journal / Series
Volume & Issue
Description
Sponsorship
This research has been sponsored by NSF grant 1513797 and NASA grant
NNX16AB09G.
Date Issued
2017-01-29
Publisher
Keywords
hardware security, information flow
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
Lightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis
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
Rights URI
Types
technical report