指令诱发型硬件木马检测技术研究

论文摘要

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

论文目录

• 摘要
• Abstract
• 图录
• 表录
• 第一章 绪论
• 1.1 研究背景
• 1.1.1 软件恶意代码检测技术发展迅速
• 1.1.2 硬件木马给信息安全带来新的威胁
• 1.1.3 硬件木马相关研究正在全面展开
• 1.2 目的和意义
• 1.3 本文主要工作和贡献
• 1.4 论文结构安排
• 第二章 相关基础理论研究
• 2.1 硬件木马基础研究
• 2.1.1 硬件木马定义与特性
• 2.1.2 硬件木马分类研究
• 2.2 硬件木马检测和防护技术相关研究
• 2.2.1 硬件木马防护技术
• 2.2.2 破坏性硬件木马检测技术
• 2.2.3 功能测试技术
• 2.2.4 可测性设计技术
• 2.2.5 基于旁路信号分析的硬件木马检测技术
• 2.2.6 基于形式化验证的硬件木马检测技术
• 2.3 硬件故障诊断相关研究
• 2.4 固件代码分析相关研究
• 2.5 小结
• 第三章 指令诱发型硬件木马模型研究
• 3.1 引言
• 3.2 硬件木马模型相关研究与分析
• 3.3 基于 Thimbleby 方法的硬件木马模型研究
• 3.3.1 Thimbleby 木马模型
• 3.3.2 T-HTH 模型
• 3.4 指令诱发型硬件木马模型研究
• 3.4.1 指令诱发型硬件木马特性分析
• 3.4.2 指令诱发型硬件木马模型
• 3.5 指令诱发型硬件木马实例分析
• 3.6 小结
• 第四章 ITHTH 检测技术研究
• 4.1 引言
• 4.2 模型检验相关研究
• 4.2.1 模型检验基本理论
• 4.2.2 系统模型
• 4.2.3 时态逻辑概述
• 4.2.4 模型检验工具
• 4.3 基于指令序列覆盖的 ITHTH 检测思想与算法
• 4.3.1 基于指令序列覆盖的 ITHTH 检测思想
• 4.3.2 基于指令序列覆盖的 ITHTH 检测算法
• 4.4 基于模型检验的 ITHTH 检测技术
• 4.4.1 固件代码特性分析
• 4.4.2 基于模型检验的 ITHTH 检测技术的可行性分析
• 4.4.3 基于模型检验的 ITHTH 检测过程
• 4.5 迁移系统生成算法研究
• 4.5.1 Kripke 结构的生成
• 4.5.2 迁移系统生成算法
• 4.5.3 迁移系统生成过程中相关问题的解决
• 4.6 实验与分析
• 4.6.1 检测对象概述
• 4.6.2 检测系统描述
• 4.6.3 检测结果与分析
• 4.7 小结
• 第五章 基于抽象解释的二进制代码变量区间分析
• 5.1 引言
• 5.2 相关研究
• 5.2.1 区间分析相关研究
• 5.2.2 抽象解释相关理论
• 5.3 固件二进制代码变量特点分析
• 5.4 二进制代码变量区间抽象域
• 5.4.1 字级数据区间抽象域
• 5.4.2 位级数据区间抽象域
• 5.5 二进制代码变量区间抽象域运算
• 5.5.1 字级数据区间抽象域运算
• 5.5.2 位级数据区间抽象域运算
• 5.6 二进制代码变量区间抽象域转换算法
• 5.6.1 字级数据区间抽象域转化为位级数据区间抽象域
• 5.6.2 位级数据区间抽象域转化为字级数据区间抽象域
• 5.7 实验测试与分析
• 5.7.1 实验方法
• 5.7.2 运算效率测试
• 5.7.3 运算精度测试
• 5.8 小结
• 第六章 基于敏感位置识别的状态缩减技术研究
• 6.1 引言
• 6.2 相关研究
• 6.3 敏感位置识别技术
• 6.3.1 敏感位置定义
• 6.3.2 敏感位置识别方法
• 6.4 子过程摘要信息的获取
• 6.4.1 固件代码结构分析
• 6.4.2 子过程摘要信息的定义
• 6.5 敏感位置识别算法研究
• 6.5.1 基于数据流切片的敏感位置识别方法
• 6.5.2 结合子过程摘要信息的敏感位置识别算法
• 6.6 实验测试与分析
• 6.6.1 状态数量优化效果测试
• 6.6.2 时间优化效果测试
• 6.6.3 时间组成情况测试
• 6.7 小结
• 第七章 结束语
• 7.1 总结
• 7.2 下一步的研究展望
• 致谢
• 参考文献
• 作者简历