可信编译理论与实现方法研究

编译器作为重要系统软件之一，其可信性对于整个计算机系统而言具有非常关键的意义，如果编译器不可信，则难以保证系统所运行软件的可信性。近年来，国外研究者就安全编译器、验证编译器、代码形式化证明等方面展开了广泛的研究，国内这方面的相关研究虽已起步，但略有滞后。本项目拟对可信编译理论及实现方法进行研究，研究内容主要包括两个方面：1）编译器本身的可信性研究，即如何防止编译器对程序代码进行恶意篡改，保证编译器编译过程的正确性、安全性和可靠性；2）编译所生成代码的可信性研究，即如何在编译的同时对所生成代码的安全性进行最大程度的加强、主要可信属性进行形式化验证，且对编译后生成的可执行代码进行安全性保护。通过可信编译器我们能够尽可能地保证系统最终运行程序的可信性，大幅度地增强系统运行的安全性和可靠性。因此，可信编译研究不仅具有重要的理论意义，而且具有明显的应用价值。