TY - GEN
T1 - Verification of a practical Hardware security architecture through static information flow analysis
AU - Ferraiuolo, Andrew
AU - Xu, Rui
AU - Zhang, Danfeng
AU - Myers, Andrew C.
AU - Suh, G. Edward
N1 - Funding Information:
We thank Daniel Lo and the anonymous reviewers for their review of and suggestions about this paper. This work was partially sponsored by NSF grant CNS-1513797 and NASA grant NNX16AB09G. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of NSF or NASA.
Publisher Copyright:
© 2017 ACM.
PY - 2017/4/4
Y1 - 2017/4/4
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85022087578&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85022087578&partnerID=8YFLogxK
U2 - 10.1145/3037697.3037739
DO - 10.1145/3037697.3037739
M3 - Conference contribution
AN - SCOPUS:85022087578
T3 - International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS
SP - 555
EP - 568
BT - ASPLOS 2017 - 22nd International Conference on Architectural Support for Programming Languages and Operating Systems
PB - Association for Computing Machinery
T2 - 22nd International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2017
Y2 - 8 April 2017 through 12 April 2017
ER -