Skip to main content

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis

Publication ,  Conference
Ferraiuolo, A; Xu, R; Zhang, D; Myers, AC; Suh, GE
Published in: ACM SIGPLAN Notices
May 12, 2017

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.

Duke Scholars

Altmetric Attention Stats
Dimensions Citation Stats

Published In

ACM SIGPLAN Notices

DOI

EISSN

1558-1160

ISSN

0362-1340

Publication Date

May 12, 2017

Volume

52

Issue

4

Start / End Page

555 / 568

Publisher

Association for Computing Machinery (ACM)

Related Subject Headings

  • Software Engineering
 

Citation

APA
Chicago
ICMJE
MLA
NLM
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 ACM SIGPLAN Notices (Vol. 52, pp. 555–568). Association for Computing Machinery (ACM). https://doi.org/10.1145/3093336.3037739
Ferraiuolo, Andrew, Rui Xu, Danfeng Zhang, Andrew C. Myers, and G Edward Suh. “Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis.” In ACM SIGPLAN Notices, 52:555–68. Association for Computing Machinery (ACM), 2017. https://doi.org/10.1145/3093336.3037739.
Ferraiuolo A, Xu R, Zhang D, Myers AC, Suh GE. Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis. In: ACM SIGPLAN Notices. Association for Computing Machinery (ACM); 2017. p. 555–68.
Ferraiuolo, Andrew, et al. “Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis.” ACM SIGPLAN Notices, vol. 52, no. 4, Association for Computing Machinery (ACM), 2017, pp. 555–68. Crossref, doi:10.1145/3093336.3037739.
Ferraiuolo A, Xu R, Zhang D, Myers AC, Suh GE. Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis. ACM SIGPLAN Notices. Association for Computing Machinery (ACM); 2017. p. 555–568.

Published In

ACM SIGPLAN Notices

DOI

EISSN

1558-1160

ISSN

0362-1340

Publication Date

May 12, 2017

Volume

52

Issue

4

Start / End Page

555 / 568

Publisher

Association for Computing Machinery (ACM)

Related Subject Headings

  • Software Engineering