Library

eCommons

 

Lightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis (Technical Report)

Simple item page
dc.contributor.authorFerraiuolo, Andrew
dc.contributor.authorXu, Rui
dc.contributor.authorZhang, Danfeng
dc.contributor.authorMyers, Andrew C.
dc.contributor.authorSuh, G. Edward
dc.date.accessioned2017-01-29T15:29:10Z
dc.date.available2017-01-29T15:29:10Z
dc.date.issued2017-01-29
dc.description.abstractHardware-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.en_US
dc.description.sponsorshipThis research has been sponsored by NSF grant 1513797 and NASA grant NNX16AB09G.en_US
dc.identifier.urihttps://hdl.handle.net/1813/45898
dc.language.isoen_USen_US
dc.relation.hasversionLightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysisen_US
dc.subjecthardware security, information flowen_US
dc.titleLightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis (Technical Report)en_US
dc.typetechnical reporten_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
techreport.pdf
Size:
293.72 KB
Format:
Adobe Portable Document Format
Description:
Download

Collections

Computer Science Technical Reports