Lennart贝灵哲酒庄他是普林斯顿大学的副研究学者，在亚博体育官网那里他使用交互式证明助手来开发可证明正确的编译器、程序分析和其他软件验证工具。此前，他曾在路德维希-马克西米利安-慕尼亚博体育官网黑大学和爱丁堡大学担任研究职务，在那里他为移动代码架构开发了携带证明代码技术，专注于资源消耗和信息流安全的特性。他获得了爱丁堡大学的博士学位，主要研究基于语言的理想异步处理器架构分析。2012年，他担任第三届交互式定理证明国际会议(ITP)的联合主席。
路加福音Muehlhauser:你参与的一个项目是验证软件工具链．你如何总结到目前为止所取得的成就?你希望在接下来的一两年里在这个项目上取得什么成就?
Lennart贝灵哲酒庄验证软件工具链是C编程语言的验证工具集合，在Coq证明助手中实现并正式验证，并连接到正式验证CompCert编译器由法国INRIA的Xavier Leroy开发。
VST的核心是一个霍尔式的程序逻辑，适合于验证部分正确性属性和程序安全性，也就是说，不存在由于试图解引用悬空指针而导致的异常程序终止。程序规范是用并发分离逻辑的一种高度表达的变体编写的，这种变体支持高阶推理、非断言量化和其他必要的概念，例如posix风格的多线程中锁的资源不变量。
除了核心程序逻辑之外，VST还包含了对证明自动化的支持，以及一个可验证的形状分析实现，其中的两个组件——一个符号执行引擎和一个用于分离逻辑的small脚片段的推理检查器可以提取代码以生成独立的工具，也可以集成到基于Coq或ocaml的分析中，包括Smallfoot本身。证明自动化组件由各种Coq策略、辅助引理和规范抽象组成，它们捕获具体应用程序中的典型证明模式。这里特别强调的是断言格式分层组织的思想，它向用户隐藏了底层逻辑的大部分复杂性。我们当前研究的一个重要目标是发现用于各种编程和规范风格的额外的这种亚博体育官网推理模式，以及利用这种结构来进一步提高自动化和性能。关于VST的应用，我们相信，除了典型的高保证软件领域外，正式标准或库的具体开源实现为评估VST的进一步增强提供了优秀的案例研究。与此同时，这些库的机器检查证明(甚至只是精确的规范)可以提高日常用户对这些库的公共信任水平。
Andrew Appel的新书中描述了VST的许多设计决策和实现细节，认证编译器的程序逻辑(CUP 2014)，而源代码是公开的在这里．
我们工作的另一个方面涉及CompCert本身。在这里，我们正在与Leroy和其他人合作，发展CompCert的规范和证明，以涵盖线程之间的共享内存交互，以及正式的链接模型。实际上，编译器正确性的模块化概念应该尊重与操作系统、库或C语言中单独编译的程序模块的通信关键依赖于交换指向缓冲区或其他共享数据结构的指针。相反，CompCert的编译器正确性概念采用了整个程序的编译视图。然而，要使指针共享与典型的编译器优化需求相一致远非易事，因为这些优化通常会改变内存布局，消除或重新定位现有的指针。此外，编译器管理的内存位置，如返回地址和溢出位置，必须保持不修改，即使是那些外部调用者，有合法的访问其他堆栈保存的数据。
路加福音:你如何描述VST的潜在动机?如果VST继续得到资助并以良好的速度开发，那么10年后对于各种程序员(和其他参与者)来说，世界将会有什么不同?
Lennart:指定软件的预期行为，并验证具体的实现满足这些规范，这是几十年来一个活跃的研究领域。亚博体育官网但是多年来，程序逻辑的有效性是有限的，其中一个原因是缺乏对模块化推理的支持，特别是在指针共享和在内存中布置的数据结构方面。大约十年前，通过允许规范和不变量优雅地捕获堆和其他共享资源的属性，分离逻辑成为解决这一缺点的一种有前途的技术。
同时，交互式证明助手(以及底层硬件的计算能力)已经足够成熟，可以有效实现程序逻辑，并具备机器可校验的稳健性证明。事实上，通过开发CompCert, Leroy证明了交互式定理可以适用于真实世界的语言，并且可以处理工业级优化编译器固有的复杂性。
VST项目结合了这两个线程，同时探索如何进一步推动当前的自动化和规范边界。
VST的主要工具链很可能会对编写高安全性软件的C程序员、加密库等中等规模软件的实实者或使用代码合成技术的开发人员感兴趣，而不是对单独生成的程序进行正确性验证我们可以设想出针对VST的Clight程序逻辑的经过验证的合成工具。函数式程序员可以通过一种精确的方式，正式地将他们用Ocaml或Haskell编写的高级代码与用C编写的更高效的代码联系起来，使用Coq的代码提取特性在这两个世界之间进行中介，从而受益。通过将代码提取和编译相结合，甚至有可能验证混合软件系统，其中一些组件是用C编写的，而另一些是用函数语言编写的。亚博体育苹果app官方下载
另一组潜在用户是系统设计人员:VST规范允许使用比使用C头文件或Java接口更丰富的接口亚博体育苹果app官方下载来描述单个组件。随着接口变得更加健壮，真正的面向组件的软件开发成为可能，在这种情况下，遵守规范足以保证替换单个组件不会对全局系统属性产生负面影响。亚博体育苹果app官方下载
对于标准系统栈的典型组件(操作系统、网络协议……)，这种正式定义的接口实际上有亚博体育苹果app官方下载其自身的利益，因为操作系统、编译器和体系结构的不同组件之间的契约是出了名的难以理解。除了系统开发人员和研究人员之外亚博体育苹果app官方下载，第三个客户可能是教育者，对他们来说，规范提亚博体育官网供了指导，可以将他们的材料划分为独立的、但相互依赖的教学单元，并解释相互的契约和假设。
路加福音:还有哪些其他的项目看起来也有类似的目标，但却针对其他语言或通过其他方法?
Lennart:我不知道有其他的尝试为主流语言开发一个类似的表达程序逻辑，在证明助手中验证它的可靠性，将它与经过验证的优化编译器链接，并配备足够的证明自动化来实现对重要程序的验证。
然而，许多研究小组处理这些特亚博体育官网性的不同子集。
微软研究院过去十年开亚博体育官网发了一系列令人印象深刻的验证工具(VCC，不羁/Dafny它主要针对c#，但也包含了同样适用于其他编程语言的组件或中间验证平台。它们具有优秀的证明自动化，并与现代SAT/SMT求解器、软件模型检查器和其他代码分析和检查工具紧密集成，但没有得到机器可检查的可靠性证明的正式支持。与此同时，MSR中的几个小组已经使用了证明助手来验证编译器，开发机器码的正式模型，并验证程序逻辑，这些逻辑大致可以与VST相媲美。如果这些互补的研究成果最终被集成到c#的端到端机器检查工具链中，这并不令人惊讶。亚博体育官网
Chlipala的基础框架通过提供机器检查的代码和规范模式，可以合成经过验证的汇编代码，使代码片段之间的交互偏离了C的调用约定。此外，该团队还开创了利用Coq战术语言和类型理论的高级特性的证明工程技术，包括我们现在在VST中应用的一些方法。我们还吸收了Jesper Bengtson的想法负责!项目，它为Java提供了一个coq验证的分离逻辑。
关于编译器验证，Xavier Leroy和他在INRIA的合作者正在扩展CompCert完全支持C99和C11，同时验证进一步的优化阶段，最近还添加了一个经过验证的解析器。
宾夕法尼亚大学的牛皮纸项目为LLVM中间表示形式的程序开发了机械化推理支持，证明了CompCert的验证原则也适用于没有考虑形式验证的编译基础设施，特别是基于静态单赋值(SSA)的编译。
与编译器验证紧密相关的是翻译验证方法——实际上，CompCert的寄存器分配器也是用这种方式验证的。最近，圣地亚哥的索林·勒纳(Sorin Lerner)团队和哈佛大学的格雷格·莫里塞特(Greg Morrisett)团队对机械化翻译验证做出了贡献。
实际验证的、正式的、机械化的真实硬软件系统规范的开发是一个持续增长的领域，最近的例子包括web服务器、浏览器、数据库、操作系统和虚拟机监控程序、宽松的内存模型和处理器架构。亚博体育苹果app官方下载特别值得注意的是DARPA的项目崩溃项目，以及雷姆由英国剑桥大学的彼得·休厄尔领导的这项研究。
我可能没有提到许多项目，但我希望我所提到的项目能够让您大致了解当前的开发情况。
卢克:谢谢,Lennart !
你喜欢这篇文章吗?你可以享受我们的另一个对话的帖子,包括:
