一句话：提出安全类型 HDL，通过静态信息流分析验证 ARM TrustZone 多核原型等硬件安全机制，并能发现漏洞。
硬件隔离机制日益常用，但正确实现困难，威胁安全根基。本文提出用带安全类型的硬件描述语言开发硬件，并通过静态信息流分析形式化验证硬件安全机制的关键性质。为验证真实处理器，作者扩展了类型系统特性，使之足够表达复杂硬件。案例实现并验证了简化但真实的 ARM TrustZone 多核原型。实验表明信息流分析高效、程序员负担适中；信息流约束还能有效检测硬件漏洞，包括商用处理器中已发现的若干漏洞。
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.
@inproceedings{FerraiuoloXZMS17,
title = {Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis},
author = {Andrew Ferraiuolo and Rui Xu and Danfeng Zhang and Andrew C. Myers and G. Edward Suh},
booktitle = {ASPLOS},
year = {2017},
doi = {10.1145/3037697.3037739}
}