|
|
论文:2024,Vol:42,Issue(1):92-97 |
|
|
引用本文： |
|
|
张茜歌, 朱嘉诚, 马俊, 沈利香, 周佳慧, 慕德俊. 基于故障传播模型的硬件安全性与可靠性验证方法[J]. 西北工业大学学报 |
|
|
ZHANG Xige, ZHU Jiacheng, MA Jun, SHEN Lixiang, ZHOU Jiahui, MU Dejun. Hardware security and reliability verification based on fault propagation model[J]. Journal of Northwestern Polytechnical University |
|
|
|
|
|
|
|
| 基于故障传播模型的硬件安全性与可靠性验证方法 |
|
| 张茜歌1, 朱嘉诚2, 马俊1, 沈利香2, 周佳慧1, 慕德俊2 |
|
1. 北京智芯微电子科技有限公司, 北京 100000;
2. 西北工业大学深圳研究院, 广东 深圳 518057 |
| 摘要: |
| 大规模集成电路正面临着诸如设计脆弱性、侧信道、硬件木马等安全漏洞的威胁。传统的功能测试验证方法无法遍历所有的输入空间,同样无法检测侧信道安全漏洞。现有的形式化验证方法关注硬件设计的等价性和功能的正确性,难以满足安全性和可靠性验证需求。研究面向安全性和可靠性验证的形式化模型,形成有效的硬件安全性与可靠性形式化验证方法。该方法能够从门级对集成电路进行建模,生成细粒度的形式化模型,实现对安全性与可靠性的形式化验证,可以捕捉硬件设计中潜在的安全隐患。实验结果表明该验证方法对硬件设计中存在的侧信道和硬件木马导致的信息泄露和篡改有很好的检测效果。 |
| 关键词:
形式化模型
故障效应分析
漏洞检测
硬件安全
|
|
| Hardware security and reliability verification based on fault propagation model |
|
| ZHANG Xige1, ZHU Jiacheng2, MA Jun1, SHEN Lixiang2, ZHOU Jiahui1, MU Dejun2 |
|
1. Beijing Smart-Chip Microelectronics Technology Co., Ltd., Beijing 100000, China;
2. Shenzhen Research Institute of Northwestern Polytechnical University, Shenzhen 518057, China |
| Abstract: |
| Large scale integrate circuits is facing serious threat such as design vulnerabilities, side channels, and hardware Trojans. Traditional functional verification method is difficult to ensure high test coverage, and it is also difficult to detect security vulnerabilities such as side channels and stealthy hardware Trojans. Formal verification methods focus on the equivalence and functional correctness of design, and are difficult to meet security and reliability verification needs. The present work proposes a hardware security and reliability verification method from formal model. The present method can develop formal models for describing the security and reliability behaviour of hardware designs. It can detect potential security vulnerabilities in hardware designs. Experimental results show that the verification method is effective in detecting sensitive information leakage and modification caused by side channels and hardware Trojans. |
| Key words:
formal model
fault effect analysis
vulnerability detection
hardware security
|
|
| 收稿日期: 2023-02-14
修回日期:
|
| DOI: 10.1051/jnwpu/20244210092 |
| 基金项目: 北京智芯微电子科技有限公司实验室开放基金(SGSC0000SJQT2207164)资助 |
| 通讯作者: 朱嘉诚(1996-),博士研究生 e-mail:zhu_jc@mail.nwpu.edu.cn
Email：zhu_jc@mail.nwpu.edu.cn |
| 作者简介: 张茜歌(1978-),研究员
|
|
|
|
|
|
|
|
参考文献: |
|
|
[1] HORN J, HAAS W, PRESCHER T, et al. Meltdown: reading kernel memory from user space[C]//27th Security Symposium Security, 2018
[2] WEISSE O, NEAL I, LOUGHLIN K, et al. NDA: preventing speculative execution attacks at their source[C]//Proceedings of the 52nd Annual IEEE/ACM International Symposium on Microarchitecture, 2019
[3] BHUNIA S, HSIAO M S, BANGA M, et al. Hardware trojan attacks: threat analysis and countermeasures[J]. Proceedings of the IEEE, 2014, 102(8): 1229-1247
[4] SHAKYA B, HE T, SALMANI H, et al. Benchmarking of hardware trojans and maliciously affected circuits[J]. Journal of Hardware and Systems Security, 2017, 1: 85-102
[5] MAO B, HU W, ALTHOFF A, et al. Quantitative analysis of timing channel security in cryptographic hardware design[J]. IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems, 2018, 37(9): 1719-1732
[6] KAUSHIK P, MAJUMDAR R. Timing attack analysis on AES on modern processors[C]//6th International Conference on Reliability, Infocom Technologies and Optimization, 2017
[7] DINA G M, HU W, MIRJANA S. X-attack: remote activation of satisfiability don't-care hardware Trojans on shared FPGAs[C]//30th International Conference on Field-Programmable Logic and Applications, 2020
[8] GAO Y, LIU L, DU H, et al. Software and hardware co-verification technology based on virtual prototyping of RF SOC[C]//IEEE International Conference on Computer and Communication Engineering Technology, 2018
[9] FERN N, SAN I, CHENG K. Detecting hardware trojans in unspecified functionality through solving satisfiability problems[C]//2nd Asia and Sourth Pacitic Desigh Autowntion Canference, 2017
[10] TIWARI M, WASSEL H, MAZLOOM B, et al. Complete information flow tracking from the gates up[C]//Proceedings of the 14th International Conference on Architectural Support for Programing Languages and Operating Systems, 2009
[11] ARDESHIRICHAM A, WEI H, MARXEN J, et al. Register transfer level information flow tracking for provably secure hardware design[C]//Design, Automation ＆ Test in Europe Conference ＆ Exhibition, 2017 |
|
|
|
相关文献: |
|
|
1．黄兴利, 胡伟, 慕德俊, 郭蓝天, 李哲.一种精确故障效应传播的形式化模型[J]. 西北工业大学学报, 2014,32(5): 719-724 |
|
|
|
|
|
|
