ACM通信
研究突出了
技术视角:编译器的故事
20世纪70年代初，Floyd、Dijkstra和Hoare等先驱认为，项目应该被正式指定，并被证明是正确的。但在过去的40年里，计算机科学界的大多数人都认为这是一个不切实际的目标。也许最重要的原因是简单的经济因素:在整个20世纪80年代和90年代，该行业往往对上市时间等因素更感兴趣，而不是涉及正确性的问题。
但在过去的几年里，环境发生了巨大的变化:在嵌入式系统等发展最快的领域，安全性和可靠性已经成为关键问题，而在这些领域，生命可能受到威胁。即使在非关键域，开发人员也必须担心bug，包括缓冲区溢出和可能导致安全漏洞的竞态条件。研究人员已经开发了各种工具，包括强静态类型检查器、软件模型检查器和抽象解释器，所有这些工具都可以(并且正在)用于帮助强制执行一系列安全属性。因此，形式化方法在今天被广泛使用，尽管在工具中有所隐藏。
但是，这些工具通常在源代码级(或者，最多是VM字节码级)而不是在机器码级进行操作。为了扩展，他们必须假设编译器如何将源代码细化为机器代码。例如，尽管C语言规范没有指定函数参数的求值顺序，但大多数分析工具假定编译器将使用从左到右的策略，因为分析所有可能的求值策略将花费太多时间。这种假设的不匹配，或者编译器本身的错误，很容易使分析工具变得无用。
在接下来的文章中，Xavier Leroy通过描述他使用Coq证明开发系统构建并验证的编译器来解决这些问题。尽管Leroy不是第一个构建经过验证的转换器的人，但他的编译器之所以引人注目和令人兴奋，主要有三个原因:第一，它将一种有用的源语言(C的一个重要子集)映射到PowerPC程序集，使其可直接用于一系列嵌入式应用程序。其次，他的编译器包括大量的分析和优化，如活性分析和图形着色寄存器分配，这使得生成的代码具有竞争力gcc 0．第三，对正确性的证明进行机械检查，以获得我们希望达到的最高水平的保证。简而言之，开发人员可以确信，尽管进行了优化，Leroy编译器的输出将与源代码输入的行为相同。
除了构建一个完全验证的、优化的编译器之外，这项工作还有许多隐藏的贡献:编译器以模块化、流水线的方式构建，作为一系列指定良好的中间语言之间的翻译，使得为其他项目添加新的优化或重用组件成为可能。例如，c子集的规范可以被重用以构建新的经过验证的工具，例如源代码级别的分析。
编译器还演示了翻译验证而不是完全的验证。使用转换验证，我们可以使用未经验证的组件来计算某些东西(例如，将变量赋值给寄存器)，只需要检查输出是否有效(没有干扰变量被赋值给同一个寄存器)。只有检查器必须被验证以确保可靠性，这通常比验证完整的分析和转换要容易得多。翻译验证是一种可以大大减少构建验证系统负担的工程技术。
本文还展示了在验证对于生产编译器或任何其他设置成为常规可行之前，我们必须走多远。最重要的是随着代码的发展构建和维护证明的成本。Leroy的正确性证明大约是编译器本身的5到6倍，这使得在不破坏证明的情况下显著更改代码非常困难。然而，证明主要是手工构造的，而且在大多数情况下，没有利用半自动化的决策过程或证明搜索，这是一个在过去十年中取得了巨大进展的研究领域。事实上，跟随Leroy的其他研究人员的工作表明，我们可以潜在地将证明的大小减少一个数量级。
也许我们面临的最大挑战是规范。编译器对“正确性”有一个相当清晰的概念(输出代码的行为应该与输入代码相同)，但大多数软件系统都没有。例如，操作系统或Web浏览器的正确性意味着什么?最好的情况是，我们可以希望将这些系统应该遵守的一些安全和安全属性形式化，并且随着我们对故障和攻击的理解的提高，我们愿意适应这些属性。反过来，这要求验证体系结构允许对规范进行几乎与代码一样频繁的修改和调整。幸运的是，经过验证的编译器使使用高级语言进行这种适应成为可能，而无需牺牲对生成的机器代码的保证。
因此，我认为我们正处于安全和安全性关键的软件系统的新工程范式的边缘，我们依靠正式的、机器检查的验证进行认证，而不是人工审计。Leroy的编译器是朝着这个目标迈出的令人印象深刻的一步。
©2009 acm 0001-0782/09/0700 $10.00
允许为个人或课堂使用本作品的全部或部分制作数字或硬拷贝，但不得为盈利或商业利益而复制或分发，且副本在首页上附有本通知和完整的引用。以其他方式复制、重新发布、在服务器上发布或重新分发到列表，需要事先获得特定的许可和/或付费。
数字图书馆是由计算机协会出版的。版权所有©2009 ACM, Inc.
没有发现记录