基于携带证明代码的IP核安全性验证方法

针对集成电路在RTL代码级设计阶段由于使用第三方IP软核引入的安全性问题,现有的功能测试方法较难实现全覆盖检测无法保障电路安全性。本文在已有基于携带证明代码思想的基础上改进提出一种安全性验证方法。该方法结合形式化验证平台coq,运用形式化逻辑描述电路代码和安全性假设,构造证明过程并采用系统的证明检查器验证证明过程。通过在DES电路代码的实验,说明了该验证方法能有效检测出电路中后门路径类型的硬件木马。相比较于测试类方法覆盖率不能达到100%而无法确定电路是非安全性,本文提出的方法可以确定电路是安全或非安全,能够保证电路代码级的安全可信性。