可信编译器
基本介绍：
可信编译具有两方面含义:一是编译器自身是可信的。即必须保证整个编译操作的可信性, 保证编译器在编译过程中不会给编译处理对象带来任何安全性问题, 防止恶意攻击者通过修改编译器, 在编译过程中对代码的原始语义进行篡改, 影响程序代码本身的可信性。编译器本身是一个可执行程序, 同样会遭受到攻击, 造成编译器自身的不可信。二是编译所得可执行程序代码是可信的。可信编译器除实现传统的编译功能外,还需对其编译对象的安全性进行检测加强、可信性进行验证, 确保系统安全、可靠运行。
1. 主要构造途径
1.1 通过测试和过程管理实现编译器的可信性
为了保证编译器实现的正确性，普遍的做法是采用大量的测试用例对编译器进行测试。例如，GCC[1]的torture测试集包含几千个C源程序用例，商用的Plum Hall Standard Validation Suite for C[2]有几万个用例，Lustre V6[3]的开源软件包中含几百个源程序用例，等等。还有一些 Bug-Ghunting工具，例如 Csmith[4]，它可以产生更多或更独特的源程序用例，从而扩大覆盖范围，发现更多的编译器缺陷。
尽管如此，采用测试的手段仍是不完善的，如果测试用例的覆盖范围不够广泛，则可能会遗漏编译器中的错误。即便是通过测试发现了错误并且做了修改，也无法保证编译器自身的正确性。实际上，仅编译器自动测试工具Csmith(截至2011年2月)以及EMI/SPE(截至2017年10月)就发现了GCC和LLVM的近1700个编译错误。
Scade[5]工具的代码生成器KCG经过了严格的V&V过程，符合民航电子系统的国际标准DO-178B/C，并且在空客公司的多款客机如A340和A380中成功应用。然而DO-178B/C主要是以过程质量控制为主的标准，不足以说明Scade的编译器不存在“误编译”。KCG并没有通过形式化的方法加以严格验证，虽然DO-178C中包含了一些非强制的形式化相关条款，但经调研，业界的用户仍会不时发现Scade KCG的某些翻译漏洞
1.2 验证翻译过程
为增加编译器的安全和可信程度，仅通过测试和严格的过程管理都是不够的。对编译器进行正确性验证，是解决问题的根本途径。最严格的验证手段莫过于采用形式化方法。工业界也早已意识到形式化软件开发的潜力，在一些安全攸关领域的安全级软件开发标准中也逐步新增了与形式化方法相关的目标或者相应的补充说明。CC(CommonCriteria)安全评估标准[6]中将可信性分为7个级别(EAL1到EAL7)，可信性级别越高，其采用形式化规范和验证的程度就越高。航空无线电委员会(RTCA)近期也已推出民航电子系统的国际标准DO-178C，其在DO-178B的基础上增加了对形式化规范和验证的要求[7]，如DO-178C和DO-333等补充说明。
近年来，有关编译器形式化验证的研究工作取得了长足的进步，达到了实用化水平，为未来制定新的工业标准奠定了强有力的基础。CompCert[8]编译器是经过形式化验证的可信编译器的杰出代表。该编译器将C的一个重要子集Clight翻译为PowerPC汇编代码(后来也支持IA32和ARM后端，目前已扩展至可支持64位处理器以及开源的RISC V体系结构)，其编译过程划分为多个阶段，前端解析过程之后每个阶段的翻译正确性都借助辅助工具 Coq进行了证明，且这些证明可由独立的证明检查器检查。这是迄今最强的形式化验证手段，达到了人们所能期望的最高可信程度[9]。由于其目标是对主体翻译过程本身进行验证(如图一所示)，因此称此类可信编译器为经过验证的编译器。Yang等[4]关于Csmith的研究工作表明：CompCert在正确性方面的表现明显优于常用的开源或商用C编译器。因CompCert编译器具有的杰出成就，其代表性论文[10]的作者Leroy获得了2016年度的“十年前最有影响 POPL论文奖”（Most Influential POPL Paper Award）。
图
一
经
过
验
证
的
编
译
器
(
以
C
o
m
p
C
e
r
t
为
例
)
图一 经过验证的编译器(以 CompCert为例)
图一经过验证的编译器(以CompCert为例)
1.3 采用翻译确认技术实现可信编译器
翻译确认的方法不是直接验证翻译程序，而是用统一的语义框架为翻译过程的源和目标代码建模，两个模型之间定义一种特定的语义等价关系/模拟等价关系，设计一种可自动证明二者等价性的确认程序(返回成功与否，成功时或给出证明脚本，不成功时或给出反例)。根据不同的语义模型，确认程序可以通过自动求解或证明、符号计算、模型检查、静态分析等方式来实现模型间的等价性确认。
图二 翻译确认（针对某个主体翻译阶段）
图三 翻译确认(针对某个中间表示上的优化)
早期，Necula和Lee提出了PCC(proof carrying code)机制，并带动了关于确认式编译器 (certifying compiler)的研究[12]。可以认为Pnueli的翻译确认是比PCC更通用的机制。PCC机制主要被用来对编译结果进行安全性检查，而不是对编译器进行验证。
对于翻译确认来说，如果翻译前后的语义保持性的确认过程比较容易构造，或者说源语言与目标语言的语义模拟等价性关系比较容易定义，则证明也会相对容易，那么验证该等价关系是一个不错的选择[8]。因为该方法最大的优点就是可以不放弃现有的编译框架，其可扩展性较好。一些大型编译器也有类似的工作[13]。但是当源语言与目标语言差异较大(类似于将同步数据流语言翻译成串行语言)时，两种语言的语义等价性关系是很难定义的，其证明过程也会更加困难。
相比较而言，当源语言和目标语言的语义定义达到认可的程度时，对翻译过程进行验证是一种彻底的做法，原理上可以保证源程序的一般性质都可以保持到目标程序上。而翻译确认的做法往往只是关注部分性质的保持性(当然，也可以逐步逼近一般性质)，因而有可能会存在“虚假预警”(false alarms)。因此，直接验证翻译过程与翻译确认两种方案各有利弊。目前看来，针对一个完整的编译过程，根据各个翻译的特点，将这两种方案混合使用是一种十分有益的做法。比如，一些针对优化算法的翻译确认工作可以很好地融合到CompCert编译器中。
正确性验证
2.主要方式
2.1 多遍交叉编译Diverse Double-Compiling
采用全自动方案保证编译器源代码和二进制代码是对应的，不能确保编译器本身没有漏洞.
2.2 借助微型可信编译器进行验证
先构造一个可证明的微型编译器, 不涉及复杂的优化操作, 只实现最基本的编译转换操作, 使用形式化验证的方法对其可信性进行证明, 并由操作系统提供的安全管理机制对其可信性进行保障。然后, 借助“可证明微型内核编译器”对较为复杂的可信编译器中传统编译模块的可信性进行对比认证, 检查其编译操作是否正确、安全。可信编译器的基本框架如图1所示：
内容详见：可信编译器关键技术研究
标签：可信性,翻译,验证,简介,可信,编译,编译器 来源： https://blog.csdn.net/xsx_6361/article/details/117519601
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。