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