Constructing formal verification models for hardware Trojans |
| |
Authors: | SHEN Lixiang MU Dejun CAO Guo XIE Guangqian SHU Fangyong |
| |
Affiliation: | 1. School of Automation,Northwestern Polytechnical University,Xi’an 710072,China;2. School of Computer Information and Engineering,Changzhou Institute of Technology,Changzhou 213032,China;3. School of Cybersecurity,Northwestern Polytechnical University,Xi’an 710072,China;4. School of Management,Northwestern Polytechnical University,Xi’an 710072,China;5. School of Economics and Management,Changzhou Institute of Technology,Changzhou 213032,China |
| |
Abstract: | The effectiveness of hardware security verification is affected by the way of constructing formal verification models.To solve this problem,this paper proposes a method which can automatically construct formal verification models for hardware Trojans detection.First,the method traverses the control flow graphs of the register transfer level design to extract the path conditions of assignment statements and the corresponding expressions.The constraint relations of the Kripke’ state transition are generated based on the path conditions and the expressions.Second,the constraint relations of the Verilog grammar are transformed to the grammar of the model checker and generate the formal verification models.Finally,a model checker verifies the models and detects the hardware Trojans when a predefined specification is verified as false.In experiments,the hardware Trojans in the Trust-HUB benchmarks are detected,which shows that the models constructed by our method can effectively detect hardware Trojans in register transfer level design. |
| |
Keywords: | formal verification model checking hardware security hardware Trojan security verification |
|
| 点击此处可从《西安电子科技大学学报》浏览原始摘要信息 |
|
点击此处可从《西安电子科技大学学报》下载全文 |
|