程序安全性已成为现代软件开发中必须重视的关键问题。在软件开发流程中，从设计到编码到编译为最终的可执行代码，任何一个阶段的安全隐患都可能导致最终软件的安全性问题。因此，对软件开发流程的各个阶段进行安全性测试是保证软件质量的一个必要部分。在软件开发过程中，编译器负责从软件源代码到目标代码的变换这一重要阶段，因此编译过程的正确性和安全性对软件的安全性有着非常大的影响。目前，针对软硬件系统的形式化验证技术发展迅速，相关工具的工具也逐步成熟，这些进步使得对编译器这类复杂的软件进行验证成为可能。由于编译验证在安全软件开发中的重要意义，它已经成为当前研究的一个热点。本论文以编译过程验证为主要研究方向，针对编译验证的核心问题，对编译器安全性的验证方法进行了探索研究，其中包括对程序属性的描述与分析方法的研究，以及对基本的编译验证方案的探索。文中提出了一种基于程序分析的编译验证框架，该框架基于对编译过程中个阶段的编译中间表示形式的分析验证编译过程是否保证了特定的安全特性。文中研究了对源语言程序和中间代码的安全属性分析方法，提出了一种新颖的算法，并将利用其对重要的软件安全属性进行分析。另外，文中还提出了一种新颖有效的二进制代码的分析方案，将对高级语言程序的属性检查方法扩展到了可执行程序的领域，因此使得能够采用统一的分析方法完成程序在编译各个阶段的各种形式的安全属性验证，从而为本文提出的编译验证框架提供了有效的安全属性分析手段。本文主要研究内容包括：(1)在深入分析编译验证的根本问题和研究方法的基础上，提出了一种基于程序分析的编译验证框架。在该验证框架中，编译验证与分析作为一个独立的大模块集成到一个已有编译器实现中，通过对编译各个阶段中的程序形式的安全属性检查，验证编译器实现的正确性与安全性。(2)针对基于程序分析的编译验证框架的基本需求，在深入分析程序基本属性的形式化描述方法的基础上，研究了内存安全属性与信息流安全属性这两种重要的安全属性的描述方法，提出了基于类型精化方法的内存安全性的统一表示方法。类型精化是基于对已有类型进行扩展的一种方法，这种方法对于描述程序的安全属性有着重要的意义。另外，还将类型扩展技术应用在信息流安全属性描述方面，并以SSA中间语言作为载体进行了信息流安全属性描述的一个实例研究。(3)在分析了编译器的典型实现技术的基础上，提出了对编译几个主要阶段的正确性验证方法。在分析了parse(从具体语法到抽象语法的语法解析技术)与unparse(从抽象语法到具体语法，将抽象语法树线性化)之间的关系，提出基于parse-unparse的编译前端验证方案。基于对代码实现算法的分析与研究，提出了基于对树重写条件检查的正确性验证方案，对树模式匹配的条件进行检验，从而验证代码生成算法的正确性。基于对编译优化算法实现的深入分析，提出了一种能够有效地表示程序中的数据流属性以及控制流属性的扩展属性文法，并基于此提出了基于属性文法计算程序属性并生成程序的抽象模型，进而利用模型检测工具检验编译优化正确性的验证方案。(4)在深入研究了程序分析方法之后，提出了基于类型分析与模型检测方法相结合的混合式分析方法TCMC(Type Checking and Model Checking)，并将其应用于程序的内存安全属性以及信息流安全性分析。其中特别针对内存泄漏的静态分析方法，说明了TCMC算法的应用，及其相对于类型分析方法的优势。(5)在深入分析底层代码的验证问题及其研究方法的基础上，提出了一种新的目标机器代码分析方法。该方法基于反编译技术恢复程序中的控制流，并基于恢复的控制流图对程序进行数据流分析和类型分析，也可以将控制流图转换到SSA形式，进而利用TCMC算法进行程序安全属性的分析。综上，本论文做出的主要贡献如下：(1)提出一个基于程序分析的编译验证框架。该框架建立在一个具有良好模块化结构的编译器实现之上，各个主要验证模块作为对编译器的扩展很方便地集成到编译器的编译过程中。该框架利用SSA形式作为统一的编译中间表示形式，便于程序属性分析，也便于向框架中添加自定义的分析模块。(2)提出基于类型精化的内存安全性统一表示，同时提出了在SSA中间表示形式上基于类型扩展进行信息流安全编码的方法。这部分程序属性描述方法的研究为验证框架中的属性检测方法研究打下了基础。(3)提出了类型分析与模型检测方法相结合的TCMC算法，并将其应用于程序安全属性的分析过程中。该算法避免了类型分析算法对控制流不敏感的不足，利用模型检测算法对类型分析的结果进行分析，提高了分析的精度，同时也避免了单纯使用模型检测算法进行分析可能造成的较大时间开销。(4)提出了基于反编译技术对汇编码和二进制程序进行分析的方法。该方法不需要编译器提供额外的调试符号信息，能够直接从二进制代码中恢复其控制流与数据流结构。这种方法的提出为底层代码安全属性提供了有效的方法，与基于源语言、中间语言的属性分析一起，为基于程序分析的编译验证框架提供了一整套有效的分析工具。