数字硬件通常在医疗、金融、基础设施和国防系统中扮演着重要的角色,随着信息和供应链的全球化,硬件设计会涉及到多个国家和团队,其安全性越来越受到人们的关注。硬件设计中不安全的端口和硬件木马都有可能引发安全漏洞,这些安全漏洞为攻击者提供了访问和篡改敏感信息的可能,因此,对硬件设计进行安全性分析具有重要的现实意义。本文基于信息流跟踪的方法,来检测电路是否有安全威胁。主要内容如下:（1）介绍了硬件安全和信息流相关的基础知识,包括硬件安全威胁和防护技术,信息流的分类和安全策略等。同时对安全验证方法进行了解,并总结了现有的安全验证方法与其各自的优缺点。（2）研究了基于信息流跟踪的硬件木马检测方法。根据信息流跟踪的原理,对输入输出端口添加污点标签,并对电路进行阴影逻辑的扩展,在对添加阴影逻辑的电路进行网表分级的操作之后,运用形式化验证工具对添加阴影逻辑的电路进行等价性验证,根据输入端的属性为输入端口污点标签进行赋值,通过观察输出端口污点标签的取值,来判断电路是否有敏感信息的泄露或篡改。同时,利用形式化验证工具验证失败会给出反例的原理,对形式化验证判断有安全威胁的电路进行木马功能电路起始逻辑的检测,检测其位置和取值。最后进行三个实验,对样本电路进行有无网表分级的对比测试,形式化验证检测电路是否有木马的测试,以及木马功能电路起始逻辑的位置和取值的测试,通过这三个实验来证明方法的有效性。（3）研究了基于形式化验证反推电路完整触发序列的方法。基于已知的木马功能电路起始逻辑及其取值,利用形式化验证失败后给出的反例,对原始电路进行触发序列的反推。首先,以木马功能电路起始逻辑作为回溯的起点,进行网表分级操作的优化,来降低反推复杂逻辑的时间复杂度。然后对划分好的每一级进行时序逻辑组合化,这样可以通过形式化验证回溯到电路的输入端口。最后对每一级中得到的序列进行完整性验证,以得到完整的触发序列。通过实验表明,网表分级优化操作是有效的,并且对于电路逻辑较简单的木马电路,方法可以在较短的时间内反推出电路全部的触发序列,对于电路逻辑复杂的处理器电路,方法可以尽可能地降低时间复杂度,并反推出完整的触发序列。