基于携带证明代码的IP核安全性验证方法
|
摘要
针对集成电路在RTL代码级设计阶段由于使用第三方IP软核引入的安全性问题,现有的功能测试方法较难实现全覆盖检测无法保障电路安全性。本文在已有基于携带证明代码思想的基础上改进提出一种安全性验证方法。该方法结合形式化验证平台coq,运用形式化逻辑描述电路代码和安全性假设,构造证明过程并采用系统的证明检查器验证证明过程。通过在DES电路代码的实验,说明了该验证方法能有效检测出电路中后门路径类型的硬件木马。相比较于测试类方法覆盖率不能达到100%而无法确定电路是非安全性,本文提出的方法可以确定电路是安全或非安全,能够保证电路代码级的安全可信性。
The introduction of a large number of third party IP cores(3 PIPs)in the design stage of RTL code-level,Integrated Circuits are easy to be implanted with hardware Trojan. But the existing functional test methods are difficult to achieve full-coverage detection and can't guarantee the safety of the circuit.This paper proposes a formal verification method based on the idea of proof carrying code. The method combining formal verification platform coq,uses formal logic to describe circuit code and security assumption,constructs the proof process and uses the system certification checker to verify the proof process. The verification experiment on the DES circuit shows that by performing code-level analysis on the circuit,it is possible to effectively detect the hardware Trojan that changes the signal path type in the circuit. Compared with test methods,because the coverage cannot reach 100%,it is impossible to determine that the circuit is insecure.But the method proposed in this paper can be sure that the circuit is secure or non-secure,and can ensure the safety and trustworthy of the code level of circuits.
The introduction of a large number of third party IP cores(3 PIPs)in the design stage of RTL code-level,Integrated Circuits are easy to be implanted with hardware Trojan. But the existing functional test methods are difficult to achieve full-coverage detection and can't guarantee the safety of the circuit.This paper proposes a formal verification method based on the idea of proof carrying code. The method combining formal verification platform coq,uses formal logic to describe circuit code and security assumption,constructs the proof process and uses the system certification checker to verify the proof process. The verification experiment on the DES circuit shows that by performing code-level analysis on the circuit,it is possible to effectively detect the hardware Trojan that changes the signal path type in the circuit. Compared with test methods,because the coverage cannot reach 100%,it is impossible to determine that the circuit is insecure.But the method proposed in this paper can be sure that the circuit is secure or non-secure,and can ensure the safety and trustworthy of the code level of circuits.
引文
[1] SalmaniH,Tehranipoor M. Analyzing circuit vulnerability to hardware Trojan insertion at the behavioral level[J]. IEEE International Symposium onDefect and Fault Tolerance in VLSI and Nanotechnology Systems,2013,79(2):190-195.
[2]李杰,肖立伊,赤诚,等.基于SoC系统的IP核评测平台开发[J].微电子学与计算机,2017,34(6):45-48.
[3]周昱,于宗光.硬件木马威胁与识别技术综述[J].信息网络安全,2016(1):11-17.
[4] Reece T,Robinson W H. Detection of hardwaretrojans in third-party intellectual property usinguntrusted modules[J]. IEEE Transactions onComputer-aided Design of Integrated Circuits andSystems,2016,35(3):357-366.
[5] Waksman A,Suozzo M,Sethumadhavan S. FANCI:identification of stealthy malicious logic usingboolean functional analysis[C]//Proceedings of ACMSigsac Conference on Computer&Communications Security,2013:697-708.
[6]闫淑梅,邹明亮. IP软核测试策略及验证方法研究[J].电子设计工程,2013,21(4):98-100.
[7] Rajendran J,Dhandayuthapany A,Vedula V,et al.Formal security verification of third partyintellectual property cores for information leakage[C]//Proceedings of 29th International Conferenceon VLSI Design&15th International Conference onEmbedded Systems. 2016:547-552.
[8] Guo X,Dutta R G,Jin Y,et al. Pre-silicon security verification and validation:a formal perspective[J]. 2015,146(1-3):1-6.
[9]侯刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[J].计算机科学,2013,40(s1):77-86.
[10]Guo X,Dutta R G,Jin Y. Hierarchy-preservingformal verification methods for pre-silicon securityassurance[C]//International Workshop on Microprocessor and Soc Test and Verification. IEEE,2016:48-53.
[11]陶钧.基于定理证明的数字系统验证研究[D].杭州:浙江大学,2013.
[12]Veeranna N,Schafer B C. Hardware trojan detection in behavioral intellectual properties(IP's)using property checking techniques[J]. IEEE Transactions on Emerging Topics in Computing,2017,5(4):576-585.
[13]张臻婷,李兆鹏,陈意云,等.一种出具证明编译器中的汇编级断言和证明生成的方法[J].小型微型计算机系统,2011,32(6):1164-1169.
[14]Jin Y,Yang B,MakrisY. Cycle-accurate information assurance by proof-carrying based signal sensitivity tracing[C]//Proceedings of IEEE International Symposium on Hardware-Oriented Securityand Trust. IEEE,2013:99-106.
[15]Borrione D,Eveking H. Formal verification of hardware designs[J].Journal of the Brazilian ComputerSociety,2016,2(2):27-48.
[16]INRIA. The coq proof assistant[EB/OL].[2018-4-10]. http://coq.inria.fr/.
[17]Bidmeshki M M,Makris Y. VeriCoq:a Verilog-to-Coq converter for proof-carrying hardwareautomation[J].IEEE International Symposium onCircuits&Systems,2015:29-32.
[2]李杰,肖立伊,赤诚,等.基于SoC系统的IP核评测平台开发[J].微电子学与计算机,2017,34(6):45-48.
[3]周昱,于宗光.硬件木马威胁与识别技术综述[J].信息网络安全,2016(1):11-17.
[4] Reece T,Robinson W H. Detection of hardwaretrojans in third-party intellectual property usinguntrusted modules[J]. IEEE Transactions onComputer-aided Design of Integrated Circuits andSystems,2016,35(3):357-366.
[5] Waksman A,Suozzo M,Sethumadhavan S. FANCI:identification of stealthy malicious logic usingboolean functional analysis[C]//Proceedings of ACMSigsac Conference on Computer&Communications Security,2013:697-708.
[6]闫淑梅,邹明亮. IP软核测试策略及验证方法研究[J].电子设计工程,2013,21(4):98-100.
[7] Rajendran J,Dhandayuthapany A,Vedula V,et al.Formal security verification of third partyintellectual property cores for information leakage[C]//Proceedings of 29th International Conferenceon VLSI Design&15th International Conference onEmbedded Systems. 2016:547-552.
[8] Guo X,Dutta R G,Jin Y,et al. Pre-silicon security verification and validation:a formal perspective[J]. 2015,146(1-3):1-6.
[9]侯刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[J].计算机科学,2013,40(s1):77-86.
[10]Guo X,Dutta R G,Jin Y. Hierarchy-preservingformal verification methods for pre-silicon securityassurance[C]//International Workshop on Microprocessor and Soc Test and Verification. IEEE,2016:48-53.
[11]陶钧.基于定理证明的数字系统验证研究[D].杭州:浙江大学,2013.
[12]Veeranna N,Schafer B C. Hardware trojan detection in behavioral intellectual properties(IP's)using property checking techniques[J]. IEEE Transactions on Emerging Topics in Computing,2017,5(4):576-585.
[13]张臻婷,李兆鹏,陈意云,等.一种出具证明编译器中的汇编级断言和证明生成的方法[J].小型微型计算机系统,2011,32(6):1164-1169.
[14]Jin Y,Yang B,MakrisY. Cycle-accurate information assurance by proof-carrying based signal sensitivity tracing[C]//Proceedings of IEEE International Symposium on Hardware-Oriented Securityand Trust. IEEE,2013:99-106.
[15]Borrione D,Eveking H. Formal verification of hardware designs[J].Journal of the Brazilian ComputerSociety,2016,2(2):27-48.
[16]INRIA. The coq proof assistant[EB/OL].[2018-4-10]. http://coq.inria.fr/.
[17]Bidmeshki M M,Makris Y. VeriCoq:a Verilog-to-Coq converter for proof-carrying hardwareautomation[J].IEEE International Symposium onCircuits&Systems,2015:29-32.