Lennart Beringer在已验证的软件工具链上

卢克·穆罕沃斯：你贡献的一个项目是已验证软件工具链。您如何总结到目前为止已经取得的成就吗？您希望在明年或两个项目上实现什么？

Lengart Beringer.：已验证的软件工具链是C编程语言的验证工具集合，在COQ验证助手中实现和正式验证，与正式验证的连接Compcert编译器由Xavier Leroy在法国inria开发。

VST的核心是一个适用于验证部分正确性和程序安全性的HOARE风格的程序逻辑，即，由于例如，缺乏异常的程序终止，例如，例如，试图取消引用悬挂指针。程序规范写入了同时分离逻辑的高度富有效应的变体，支持更高阶推理，非法性量化和制定所需的其他概念，例如，例如Posix样式多线程中锁的资源不变。

除了核心程序逻辑外，VST还包含对校对自动化的支持，以及一种验证的声音分析，其两个组件 - 一个符号执行引擎和分离逻辑的小型脚踏片段的诱因检查器 - 可以要么代码提取，要么产生独立的工具，或集成到CoQ或基于OCAML的分析中，包括Smallfoot本身。证明自动化组件由各种COQ策略，辅助LEMMAS和规范抽象组成，可捕获混凝土应用程序中的典型证明模式。这里的特殊重点是对分层组织的断言格式的想法，隐藏来自用户的底层逻辑的大部分复杂性。我们目前的研究的一个重要目标是发现各种编程和规范样式的额外这种推理金宝博娱乐模式，以及利用这种结构，以进一步增强自动化和性能。关于VST的应用，我们认为除了高保证软件的典型领域，正式标准或图书馆的具体开源实现为评估VST的进一步增强提供了优异的案例研究。与此同时，这些库的机器可检测的证明（甚至只是精确规格）可以促进公共信任水平，即日常用户在这些图书馆上。

Andrew Appel最近的书籍中描述了VST的许多设计决策和实施细节，用于认证编译器的程序逻辑（2014杯），源代码公开可用这里。

我们工作的另一个方面涉及Compercer本身。在这里，我们与Leroy和其他人合作，以发展Compert的规范和证明，以涵盖线程之间的共享内存交互，以及链接的正式模型。实际上，编译器正确性的模块化概念应该尊重与操作系统的通信，包括库中的单独编译的程序模块致命地依赖于交换指针到缓冲区或其他共享数据结构。相反，Compcert的编译器正确性的概念采用了整个程序的编译视图。但是，与典型编译器优化的要求，它远非易于协调指针共享，因为这些定期更改内存布局并消除或重新定位现有指针。此外，编译器管理的内存位置，例如返回地址和溢出位置必须保持未修改，甚至是那些具有合法访问其他堆叠保存数据的外部分支机构。

卢基：您如何描述VST的潜在动机？如果VST继续资助并以良好的步伐进行资金和工作，世界将如何为各种程序员（和其他演员）不同的程序员（和其他演员）如何不同？

Lennart.：指定软件的预期行为，并验证具体实施满足这些规范，是几十年的活跃研究区域。金宝博娱乐但多年来，程序逻辑的有效性有限，其中一个原因是缺乏对模块化推理的支持，特别是关于在内存中布局的指针共享和数据结构。大约十年前，分离逻辑作为一个有希望的技术来解决这种缺点，允许规范和不变性地捕捉堆和其他共享资源的优雅捕获。

与此同时，互动证明助理（以及底层硬件的计算能力）已经充分成熟，以便可以有效地实现程序逻辑，并且可以配备机器可检测的声音证明。事实上，通过开发Compcert，Leroy表明，互动定理证明是现实世界语言的尺度，并且可以应对工业强度优化编译器中固有的复杂性。

VST项目结合了这两个线程，同时探索了当前自动化和规范边界如何进一步推动。

VST的主要工具链将很可能是C程序员对诸如Crypto库等中型软件的实现者的兴趣，或者使用代码综合技术的开发人员 - 而不是验证正确性individually generated programs — one could envision verified synthesis tools that target the VST’s Clight program logic. Functional programmers may benefit by having a precise way to formally relate their high-level code written in Ocaml or Haskell to potentially more efficient code written in C, using Coq’s code extraction feature to mediate between these two worlds. By combining code extraction and compilation, it may even become possible to verify hybrid software systems in which some components are written in C and others in a functional language.

另一组潜在用户是系统设计人员的潜在用户：VST规范使单个组件能够使用C头文件或Java接金宝博官方口可以实现比可能的更丰富的接口。由于接口变得更加强大，因此，真正的组件化软件开发成为可能，如果遵守规范足以保证代替各个组件对全球系统性质的影响。金宝博官方

对于标准系统堆栈（OS，网络协议，......）的典型组件，这种形式定义的接口金宝博官方实际上是他们自己的权利，因为撰写OS，编译器和架构的不同组件之间的合同，难以理解地难以理解。除系统开发人员和研究人员外，第金宝博官方三个客户还可能是教育工作者，规范为其提供指导金宝博娱乐，用于将其材料分成自我融入的，但相互依存的教学单位，以及解释相互合同和假设。

卢基：一些其他项目似乎旨在瞄准类似的目标，而是如此。对于其他语言或通过其他方法？

Lennart.：我不知道其他尝试为主流语言开发类似的表现力程序逻辑，验证其在校正助手中的声音，将其与经过验证的优化编译器链接，并用足够的证明自动化将其装备以启用非竞争程序的验证。

但是，许多研究组地址解决了这金宝博娱乐些功能的各种子集。

过去十年的Micro金宝博娱乐soft Research开发了令人印象深刻的验证工具集合（vcc.那布吉/达菲尼，......）主要针对C＃，但包含也适用于其他编程语言的组件或中间验证平台。这些具有优异的防范自动化，并与现代SAT / SMT求解器，软件模型检查器和其他代码分析和检测工具紧密集成，但没有通过机器可检测的声音证明正式备份。与此同时，MSR中的几个组已经使用证明助手来验证编译器，开发机器代码的正式模型，并验证与VST大致相当的程序逻辑。如果这些互补的研究努力最终集成，它几乎不会令人惊讶，以产生C＃的端到端机器可搏斗的工具链。金宝博娱乐

Chlipala基岩框架通过提供机器检查的代码和规范模式来支持验证的汇编代码，使能偏离C的Calling惯例的代码片段之间的交互。此外，本集团的开创性证明工程技术开采了CoQ的策略语言和类型理论的高级功能，包括我们现在在VST中申请的一些方法。我们还从Jesper Bengtson的想法纳入了想法收费！项目，为Java提供CoQ验证的分离逻辑。

关于编译器验证，初学者Leroy及其合作者正在扩展Compcert.为了全面支持C99和C11，同时验证进一步的优化阶段，最近 - 添加了验证的解析器。

omenn's瓦姆项目开发了用于LLVM中间代表中表达的程序的机械化推理支持，表明Compcert的验证原则也适用于编译器基础架构，这些基础设施不是在牢记正式验证的情况下，以及基于静态单分配（SSA）的编译。

与编译器验证密切相关是翻译验证的方法 - 事实上，Compcert的寄存器分配器也被证明在这种情况下。最近对机械化翻译验证的贡献包括Sorin Lerner集团在圣地亚哥的集团，在哈佛大学Greg Morrisett的集团。

实际验证，但正式精确，机械化规范的现实世界的硬件和软件系统的发展是一个继续增长的领域，最近的示例包括Web服务器，浏览器，数据库，操作系统和虚拟机管理程序，轻松的内存模型，金宝博官方和处理器架构。特别值得注意的是Darpa的项目碰撞节目，以及REMS.彼得塞威尔在剑桥（英国）领导的努力。

我可能没有提到一些项目，但我希望我提到的那些项目给你一个粗略的发展图片。

卢克：谢谢，Lennart！