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

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Hardware and Architecture

Cite this

Ferraiuolo, A., Xu, R., Zhang, D., Myers, A. C., & Suh, G. E. (2017). Verification of a practical Hardware security architecture through static information flow analysis. In ASPLOS 2017 - 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (pp. 555-568). (International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS; Vol. Part F127193). Association for Computing Machinery. https://doi.org/10.1145/3037697.3037739