Verification of a practical Hardware security architecture through static information flow analysis

Andrew Ferraiuolo, Rui Xu, Danfeng Zhang, Andrew C. Myers, G. Edward Suh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Scopus citations

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 Trust Zone 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.

Original languageEnglish (US)
Title of host publicationASPLOS 2017 - 22nd International Conference on Architectural Support for Programming Languages and Operating Systems
PublisherAssociation for Computing Machinery
Pages555-568
Number of pages14
ISBN (Electronic)9781450344654
DOIs
StatePublished - Apr 4 2017
Event22nd International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2017 - Xi'an, China
Duration: Apr 8 2017Apr 12 2017

Publication series

NameInternational Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS
VolumePart F127193

Other

Other22nd International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2017
CountryChina
CityXi'an
Period4/8/174/12/17

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Verification of a practical Hardware security architecture through static information flow analysis'. Together they form a unique fingerprint.

Cite this