|
|
论文:2024,Vol:42,Issue(3):506-513 |
|
|
引用本文： |
|
|
秦茂源, 侯佳滢, 李家乐, 唐时博, 邰瑜. 寄存器传输级硬件设计信息流建模与安全验证[J]. 西北工业大学学报 |
|
|
QIN Maoyuan, HOU Jiaying, LI Jiale, TANG Shibo, TAI Yu. Register transfer level hardware design information flow modeling and security verification method[J]. Journal of Northwestern Polytechnical University |
|
|
|
|
|
|
|
| 寄存器传输级硬件设计信息流建模与安全验证 |
|
| 秦茂源1, 侯佳滢1, 李家乐1, 唐时博2, 邰瑜2 |
|
1. 西安工业大学 计算机科学与工程学院, 陕西 西安 710021;
2. 西北工业大学 网络空间安全学院, 陕西 西安 710072 |
| 摘要: |
| 近年来,已有大量研究证明信息流分析能够有效地对设计安全属性与安全行为进行建模。然而,现有的门级抽象层次的信息流分析方法往往受制于算力和验证效力等因素难以应对大规模设计,而RTL抽象层次的信息流分析方法需借助类型系统等形式化语言对硬件设计进行重新描述。因此,提出了一种寄存器传输级硬件设计信息流建模与安全验证方法。该方法在寄存器传输级功能模型的基础上构建附加安全属性的信息流跟踪逻辑模型,从信息流角度建模设计安全行为和安全属性,并利用EDA测试验证工具,以无干扰为策略捕捉违反安全策略的有害信息流,检测硬件设计安全漏洞。以Trust-Hub硬件木马测试集为测试对象的实验结果表明:所提方法能够有效检测设计内潜藏的硬件木马。 |
| 关键词:
硬件安全
信息流安全模型
信息流安全验证
安全漏洞检测
|
|
| Register transfer level hardware design information flow modeling and security verification method |
|
| QIN Maoyuan1, HOU Jiaying1, LI Jiale1, TANG Shibo2, TAI Yu2 |
|
1. School of Computer Science and Engineering, Xi'an Technological University, Xi'an 710021, China;
2. School of Cybersecurity, Northwestern Polytechnical University, Xi'an 710072, China |
| Abstract: |
| Information flow analysis can effectively model the security behavior and security properties of hardware design. However, the existing gate level information flow analysis methods cannot deal with large-scale designs due to computing power and verification effectiveness, and the register transfer level (RTL) information flow analysis methods require formal languages to rewrite hardware designs. This paper proposes a RTL hardware design information flow modeling and security verification method. Based on the RTL functional model, this method develops an information flow tracking logical model to model security behavior and security properties of RTL hardware designs from the perspective of information flow. This method can be integrated into EDA flows and uses EDA testing and verification tools to capture security property violations and detect security vulnerabilities based on non-interference security policy. The results on experiments with Trust-Hub hardware Trojan benchmarks show that the proposed method can effectively detect hardware Trojans. |
| Key words:
hardware design
information flow security model
information flow security verification
security vulnerability detection
|
|
| 收稿日期: 2023-05-27
修回日期:
|
| DOI: 10.1051/jnwpu/20244230506 |
| 基金项目: 国家自然科学基金(U23B2041,62074131)、西安市碑林区科技计划(GX2136)与陕西省科技计划(2022JM-379)资助 |
| 通讯作者: 邰瑜(1982—),助理研究员 e-mail:taiyu@nwpu.edu.cn
Email：taiyu@nwpu.edu.cn |
| 作者简介: 秦茂源(1985—),讲师
|
|
|
|
|
|
|
|
参考文献: |
|
|
[1] 毛保磊, 慕德俊, 胡伟, 等. RSA时间信道滑动窗口攻击方法及量化分析[J]. 西安电子科技大学学报, 2017, 44(5): 115-120 MAO Baolei, MU Dejun, HU Wei, et al. Quantitative analysis of sliding windows attack for the RSA timing channel[J]. Journal of Xidian University, 2017, 44(5): 115-120(in Chinese)
[2] HU W, WU L, TAI Y, et al. A unified formal model for proving security and reliability properties[C]//2020 IEEE 29th Asian Test Symposium, 2020: 1-6
[3] HU W, MAO B, OBERG J, et al. Detecting hardware trojans with gate-level information-flow tracking[J]. Computer, 2016, 49(8): 44-52
[4] ZHANG Q, HE J, ZHAO Y, et al. A formal framework for gate-level information leakage using z3[C]//2020 Asian Hardware Oriented Security and Trust Symposium, 2020: 1-6
[5] ZHANG D, WANG Y, SUH G E, et al. A hardware design language for timing-sensitive information-flow security[J]. ACM Sigplan Notices, 2015, 50(4): 503-516
[6] BIDMESHKI M M, MAKRIS Y. VeriCoq: a Verilog-to-Coq converter for proof-carrying hardware automation[C]//2015 IEEE International Symposium on Circuits and Systems, 2015: 29-32
[7] HU W, ARDESHIRICHAM A, KASTNER R. Hardware information flow tracking[J]. ACM Computing Surveys, 2021, 54(4): 1-39
[8] ARDESHIRICHAM A, HU W, KASTNER R. Clepsydra: modeling timing flows in hardware designs[C]//2017 IEEE/ACM International Conference on Computer-Aided Design, 2017: 147-154
[9] ARDESHIRICHAM A, HU W, MARXEN J, et al. Register transfer level information flow tracking for provably secure hardware design[C]//Design, Automation ＆ Test in Europe Conference ＆ Exhibition, 2017: 1691-1696
[10] GUO X, DUTTA R G, HE J, et al. QIF-Verilog: quantitative information-flow based hardware description languages for pre-silicon security assessment[C]//2019 IEEE International Symposium on Hardware Oriented Security and Trust, 2019: 91-100
[11] JIN Y, MAKRIS Y. Proof carrying-based information flow tracking for data secrecy protection and hardware trust[C]//2012 IEEE 30th VLSI Test Symposium, 2012: 252-257
[12] 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 |
|
|
|
|
|
|
|
