沈利香，慕德俊，曹 国，谢光前，束方勇

(1.西北工业大学 自动化学院，陕西 西安 710072；2.常州工学院 计算机信息工程学院，江苏 常州 213032；3.西北工业大学 网络空间安全学院，陕西 西安 710072；4.西北工业大学 管理学院，陕西 西安 710072；5.常州工学院 经济与管理学院，江苏 常州 213032)

伴随着集成电路供应链的全球化，硬件安全正越来越成为硬件设计中的一个巨大挑战。硬件安全漏洞会威胁电路的安全属性，包括保密性，完整性和有效性等。硬件木马是硬件安全中的一个主要问题。文献[1]指出硬件木马威胁了整个集成电路市场。当植入木马的芯片被用到各种系统时，硬件木马会导致严重的安全问题和经济损失，甚至是人身伤害。例如，2010年Stuxnet蠕虫使可编程逻辑控制器偏离了预定义行为，严重损害了伊朗核电站的离心机。

形式化验证是一种基于算法的验证方法，与仿真测试相比验证更加完备，但也更加耗时。形式化验证技术主要包含了定理证明和模型检测。在定理证明方面，JIN等使用定理证明技术验证Verilog代码安全。在文献[2-3]中，提出了一种测试框架。该框架结合了定理证明和信息流追踪技术[4-5]。文献[6]首先针对门级电路构造电路语义模型，然后定义验证定理，以人机交互方式利用定理证明器验证定理的合理性，从而确定门级电路的安全性。在模型检测方面，该技术穷举式地遍历验证模型的状态空间，以验证测试电路的各种属性。与定理证明相比，模型检测不需要证明，验证速度更快，这使得它比定理证明更为实用。……