GCC编译器安全验证方法研究

论文摘要

编译器作为计算机软件中最为基础的软件之一,与操作系统、数据库系统一起被列为构成计算机系统软件的关键性的基础设施。而编译器作为任何软件的产生器,它的安全性、可靠性和稳定性更是至关重要。特别是在那些对软件的可靠性要求十分高的特殊环境里面,我们必须保证编译器编译出来的代码是对程序源代码的正确、真实的反应,保证编译器在编译过程中逻辑上的正确性以及行为上的透明性。本文首先研究了目前国内外对于软件验证,特别是编译器验证领域的一些工作进展。主要包括形式化的验证方法、模型校验、目标文件结构比较等等方法,分析并讨论了这些方法在理论上的优缺点以及它们在实践应用中的效果。本文对于编译器的安全性的关注点在于:验证编译器是否在编译阶段在输出目标代码中插入恶意的代码或者后门程序。之后本文提出了两种可行的编译器验证方案:编译器代码分析及对比验证以及目标码逻辑结构对比验证。在第一个方案中,我们以GCC编译器为例,试图将GCC编译器源代码中的所有函数分成两类:对于那些会在函数内部改变它的输入数据的函数,影响编译器最终输出结果的,我们将它们归类为第一类;对于那些在函数内部不会改变输入数据的函数,不影响编译器最终输出结果的,我们将它们归类为第二类。对于第二类函数,我们在函数的入口处将所有输入数据保存,然后在函数返回时将所有输入数据与之前保存的数据进行对比,如果对比成功,则证明该函数的确没有改变编译器的最终输出结果;对于第一类函数,我们将人工地检查这些函数的代码并且由一组独立的小组将这些函数根据描述重新实现,然后对比原先这些函数的运行结果以及独立实现的函数运行结果,如果结果一致,则表示该函数安全。第二个方案中,本文采用了一种对比编译器的输出目标文件与源文件的控制流逻辑结构的方案。在这个方案中,我们采用GCC编译器编译一份源代码,然后提取源代码和编译以后目标码的控制流图的结构,使用同构图算法对这两个控制流图进行比较,如果这两份控制流图的逻辑对比一致,那么可以证明该编译器在编译过程中没有插入恶意代码,即证明这目标编译器在行为上安全的。最终,本文提出将这两种方案相互结合的综合的编译器安全验证方法,使得一方面能够大大减轻编译器验证的工作量,另一方面又能够保证验证的完整性。本文所提出的方法和结论可以进一步地推广到其他的编译器和硬件平台的验证工作中去,它们应该有着更广泛的应用前景。

论文目录

• 摘要
• Abstract
• 第1章 绪论
• 1.1 研究背景
• 1.1.1 可信软件与软件验证
• 1.1.2 静态分析与形式化方法
• 1.1.3 动态分析与软件测试
• 1.2 研究内容
• 1.3 研究目标
• 1.4 本文结构组织
• 1.5 本章小结
• 第2章 编译器验证研究综述
• 2.1 编译器安全验证
• 2.2 编译优化验证
• 2.3 编译结果运行时保证
• 2.4 本章小结
• 第3章 编译器代码分析及保障对比验证
• 3.1 引言
• 3.2 总体方案描述
• 3.2.1 基本思路
• 3.2.2 实施步骤
• 3.2.3 参与人员角色与约束
• 3.2.4 其他注意事项
• 3.3 实施实例
• 3.3.1 循环代码外提优化的安全性验证
• 3.4 工作量估计
• 3.5 本章小结
• 第4章 控制流逻辑结构对比验证
• 4.1 引言
• 4.2 控制流图
• 4.2.1 控制流图结构
• 4.2.2 同构图问题
• 4.3 C语言源代码控制流图生产
• 4.3.1 Lex& Yacc
• 4.3.2 条件判断语句
• 4.3.3 循环语句
• 4.3.4 函数调用
• 4.4 目标码控制流图生产
• 4.5 控制流图简化与图同构
• 4.5.1 控制流图简化
• 4.5.2 控制流图同构
• 4.6 实验评估测试
• 4.6.1 控制流图实验用例
• 4.6.2 恶意代码嵌入
• 4.6.3 恶意代码嵌入实验
• 4.6.4 真实程序测试用例
• 4.7 本章小结
• 第5章 总结与展望
• 5.1 本文完成的主要研究工作
• 5.2 本文的主要贡献以及创新点
• 5.3 进一步的研究工作
• 附录
• C语言词法规则
• C语言语法规则
• 参考文献
• 致谢