可信编译理论及其核心实现技术:研究综述

• 作者: 何炎祥 刘健博 刘陶 吴伟 李清安 石谦 胡明昊 陈勇
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 可信编译器 编译正确性 编译器验证 可信软件
• 年，卷（期）: 2011,（1）
• 页码范围: 1-22
• 分类号: TP314
• 字数: 21684字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.2011.01.001

摘要

编译器是重要的系统软件之一,高级语言编写的软件都必须经过编译器的编译才能成为可执行程序.编译器的可信性对于整个计算机系统而言具有非常关键的意义,如果编译器不可信,则很难保证系统所运行软件的可信性.可信编译是指编译器在保证编译正确的同时提供相应的机制保证编译对象的可信性,对可信编译理论和技术的研究具有重要理论意义和实用前景.阐述了可信编译器的概念,介绍了编译过程正确性的形式化定义,对可信编译的主要研究内容进行了概括.在全面分析可信编译研究现状的基础上,从编译器自身可信性和确保编译对象可信性两个方面,对可信编译器设计和实现的相关理论和方法进行了分类和总结.最后,讨论了可信编译有待解决的问题和未来的研究方向.