硬件木马是指在集成电路设计或制造过程中恶意植入的电路结构,一旦芯片制造完成,硬件木马将长久存在。硬件木马具有极大的危害,其恶意功能包括但不限于信息泄露、功能篡改以及降低性能等。由于硬件木马种类繁多,植入环节多样,表现特征各异,尚没有一种普适的硬件木马检测技术能够保障集成电路的安全。本文首先论述了集成电路生命周期中的安全隐患问题,详细分析了硬件木马所带来的安全威胁,面向硅前(pre-silicon)阶段隐藏在第三方IP核中的硬件木马以及硅后(post-silicon)阶段在芯片加工制造中植入的硬件木马,开展了硬件木马检测技术研究。本文系统地研究了不同层级硬件木马的特点,建立了集成电路高层次形式化模型以及电磁辐射频谱指纹模型,有效解决硬件木马检测技术中的关键问题。在硅前阶段,重点开展了基于RTL代码的集成电路硬件形式化验证技术研究。对比了等价性验证(equivalent checking)、定理证明(theorem proving)以及模型检验(model checking)的方法差异,提出了一种电路信息完备的基于电路状态机(FSM)的形式化模型建模方法;改进了基于布尔可满足性计算(3-SAT solver)的电路状态机提取工具,开发了基于Python脚本的转译工具,完成了由状态机到形式化模型的自动建模。在此基础上,阐述了基于可计算逻辑树(computational tree logic,CTL)的Query安全属性描述语言的语义及属性,提出了面向硬件木马恶意行为检测的安全属性描述方法,涵盖信息流控制(确定性、不变性)和访问权限判定。完成了基于AMBA AXI4-Lite总线的多IP核So C系统构建,分别针对单IP级信息泄露型硬件木马以及系统级拒绝服务型硬件木马开展了硬件检测实验,实现了硬件木马恶意行为的检出;提出了一种递进式的安全属性验证策略,对电路状态反馈信息进行提取和二次验证,实现了硬件木马代码的精准定位。在硅后阶段,研究了利用RTL代码构建高层次电磁辐射模型的方法,生成了电磁辐射频谱指纹来强化侧信道(side channel)硬件木马检测技术。首先结合集成电路硬件中基本逻辑单元的驱动能力以及逻辑状态,形成了有权重的电磁辐射汉明重量(Hamming weight)理论模型;提出了基于电路RTL代码的电磁侧信道辐射模型,基于频谱因子分析,生成了可用于硅后硬件木马检测的电磁频谱指纹,解决了限制侧信道硬件木马检测技术实际应用的无参考芯片问题。深入研究了噪声、工艺偏差等非理想因素对于电磁频谱指纹的影响,完成了在±5%工艺偏差下的仿真验证,实验结果表明,仿真模型与实测数据在电磁频谱信息方面的相关性达到了98%以上。在Xilinx FPGA检测平台上,基于AES电路设计了11种硬件木马电路,并利用有基准参考的欧氏距离判别算法以及神经网络自适应检测算法,实现了最小占比在0.2%的硬件木马的有效检出,验证了模型的有效性,解决了基于形式化验证的硬件木马检测技术无法检测在芯片加工制造过程中植入的硬件木马的问题。