当前，信息安全的重要性不言而喻，但信息安全的现状却不尽人意，针对信息安全的攻击技术和手段层出不穷，硬件木马的出现更是给信息安全带来了新的威胁。相对于软件恶意代码，硬件木马与系统底层密切相关，具有更强的隐蔽性和更严重的破坏性，开展硬件木马检测技术的研究对于全面保障信息系统的安全至关重要，具有重要的现实意义和理论意义。本文以指令诱发型硬件木马为研究对象，主要内容和创新点如下：1.构建一种指令诱发型硬件木马模型。在分析硬件木马特性的基础上，根据Thimbleby木马模型，提出基于Thimbleby方法的硬件木马模型；在此模型的基础上，结合指令诱发型硬件木马的特点，构建指令诱发型硬件木马模型。2.提出并实现指令诱发型硬件木马的检测技术。根据指令诱发型硬件木马模型，提出基于指令序列覆盖的指令诱发型硬件木马检测思想和相应算法；在深入分析模型检验方法的基础上，提出基于模型检验的指令诱发型硬件木马检测技术，并给出模型生成算法和待验证性质提取方法。实验结果表明，指令诱发型硬件木马检测技术能够有效检测硬件木马。3.提出基于抽象解释的二进制代码变量区间分析方法。基于抽象解释理论，结合固件二进制代码变量的特点，扩展区间抽象域，定义字级数据区间抽象域和位级数据区间抽象域；分别给出两种区间抽象域上的区间运算方法；提出不同变量区间抽象域间的转换算法；在转换过程中引入区间集的概念，保证运算的精度。实验结果表明基于抽象解释的二进制代码变量区间分析方法相对于传统依次运算方法在效率上有数量级倍数的提高；引入区间集的区间分析方法的运算精度高于不引入区间集的分析方法。4.提出基于敏感位置识别的状态缩减技术。为有效缓解硬件木马检测过程中的状态爆炸问题，结合固件代码的特点定义了敏感变量和敏感位置，给出敏感位置识别技术；在敏感位置识别过程中，为了提高识别效率，提出结合子过程摘要信息的敏感位置识别算法。实验结果表明，本文所提方法能够有效缩减状态规模，状态规模优化率最大为91.5%，有效缓解了状态爆炸问题。