Using Security Invariant To Verify Confidentiality in Hardware Design
Using Security Invariant To Verify Confidentiality in Hardware Design
复制标题
使用安全不变式来验证硬件设计中的机密性
DOI：
10.1145/3060403.3060456
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Zhou, Hai
中科院分区：
文献类型：
--
作者：
Kong, Shuyu;Shen, Yuanqi;Zhou, Hai
由于设计过程、外包和第三方块的使用日益复杂，防止木马插入和其他恶意设计修改变得越来越困难。在本文中，我们建议部署安全不变式作为携带证明来预防和检测木马和恶意攻击，并确保硬件设计的安全性。对不干扰降级政策进行保密检查。与现有的类型检查方法相反，我们开发了一种对组合机器上的简单安全属性进行模型检查的方法。在模型检查中以更好的方式处理降级，并且我们的方法的有效性在各种 Verilog 基准测试中得到了证明。
Due to the increasing complexity of design process, outsourcing, and use of third-party blocks, it becomes harder and harder to prevent Trojan insertion and other malicious design modifications. In this paper, we propose to deploy security invariant as carried proof to prevent and detect Trojans and malicious attacks and to ensure the security of hardware design. Non-interference with down-grading policy is checked for confidentiality. Contrary to existing approaches by type checking, we develop a method to model-check a simple safety property on a composed machine. Down-grading is handled in a better way in model-checking and the effectiveness of our approach is demonstrated on various Verilog benchmarks.
DOI：
10.1007/11547662_24
发表时间：
2005-09
期刊：
--
影响因子：
--
作者：
Tachio Terauchi;A. Aiken
通讯作者：
Tachio Terauchi;A. Aiken