Collaborative Research: Expeditions in Computing: The Science of Deep Specification

合作研究：计算探索：深度规范的科学

• 批准号: 1521584
• 负责人: Adam Chlipala
• 金额: $ 114.83万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-12-15 至 2020-11-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1521584&HistoricalAwards=false
• 关键词: Collaborative; Research; Expeditions; Computing; Science

In our interconnected world, software bugs and security vulnerabilities pose enormous costs and risks. The Deep Specification ("DeepSpec", deepspec.org) project addresses this problem by showing how to build software that does what it is supposed to do, no less and (just as important) no more: No unintended backdoors that allow hackers in, no bugs that crash your app, your computer, or your car. "What the software is supposed to do" is called its specification. The DeepSpec project will develop new science, technology, and tools--for specifying what programs should do, for building programs that conform to those specifications, and for verifying that programs do behave exactly as intended. The key enabling technology for this effort is modern interactive proof assistants, which support rigorous mathematical proofs about complex software artifacts. Project activities will focus on core software-systems infrastructure such as operating systems, programming-language compilers, and computer chips, with applications such as elections and voting systems, cars, and smartphones.Better-specified and better-behaved software will benefit us all. Many high-profile security breaches and low-profile intrusions use software bugs as their entry points. Building on decades of previous work, DeepSpec will advance methods for specifying and verifying software so they can be used by the software industry. The project will include workshops and summer schools to bring in industrial collaborators for technology transfer. But the broader use of specifications in engineering also requires software engineers trained in specification and verification--so DeepSpec has a major component in education: the development of introductory and intermediate curriculum in how to think logically about specifications, how to use specifications in building systems-software components, or how to connect to such components. The education component includes textbook and on-line course material to be developed at Princeton, Penn, MIT, and Yale, and to be available for use by students and instructors worldwide. There will also be a summer school to train the teachers who can bring this science to colleges nationwide.Abstraction and modularity underlie all successful hardware and software systems: We build complex artifacts by decomposing them into parts that can be understood separately. Modular decomposition depends crucially on the artful choice of interfaces between pieces. As these interfaces become more expressive, we think of them as specifications of components or layers. Rich specifications based on formal logic are little used in industry today, but a practical platform for working with them will significantly reduce the costs of system implementation and evolution by identifying vulnerabilities, helping programmers understand the behavior of new components, facilitating rigorous change-impact analysis, and supporting maintainable machine-checked verifications that components are correct and fit together correctly. This Expedition focuses on a particularly rich class of specifications, "deep specifications." These impose strong functional correctness requirements on individual components such that they connect together with rigorous composition theorems. The Expedition's goal is to focus the efforts of the programming languages and formal methods communities on developing and using deep specifications in the large. Working in a formal proof management system, the project will concentrate particularly on connecting infrastructure components together at specification interfaces: compilers, operating systems, program analysis tools, and processor architectures.

在我们互联互通的世界里，软件漏洞和安全漏洞带来了巨大的成本和风险。深度规范(DeepSpec，Deepspec.org)项目解决了这个问题，它展示了如何构建软件来完成它应该做的事情，同样重要的是：没有让黑客进入的意外后门，没有使你的应用程序、电脑或汽车崩溃的错误。“软件应该做什么”被称为它的规范。DeepSpec项目将开发新的科学、技术和工具--用于指定程序应该做什么，用于构建符合这些规范的程序，以及用于验证程序是否完全按照预期运行。实现这一努力的关键技术是现代交互式证明助手，它支持关于复杂软件构件的严格数学证明。项目活动将集中在核心软件系统基础设施上，如操作系统、编程语言编译器和计算机芯片，以及选举和投票系统、汽车和智能手机等应用程序。更具体、更好的软件将使我们所有人受益。许多高调的安全漏洞和低调的入侵都使用软件漏洞作为切入点。在过去几十年工作的基础上，DeepSpec将改进指定和验证软件的方法，以便软件行业可以使用这些方法。该项目将包括讲习班和暑期学校，以引入行业合作者进行技术转让。但在工程中更广泛地使用规范也需要经过规范和验证培训的软件工程师--因此DeepSpec在教育中有一个主要组成部分：开发入门和中级课程，介绍如何从逻辑上思考规范，如何在构建系统中使用规范-软件组件，或者如何连接到这些组件。教育部分包括将在普林斯顿大学、宾夕法尼亚大学、麻省理工学院和耶鲁大学开发的教科书和在线课程材料，并可供世界各地的学生和教师使用。还将有一个暑期班来培训能够将这门科学带到全国大学的教师。抽象性和模块化是所有成功的硬件和软件系统的基础：我们通过将它们分解成可以单独理解的部分来构建复杂的人工制品。模块化分解在很大程度上取决于组件之间接口的巧妙选择。随着这些接口变得更具表现力，我们将其视为组件或层的规范。基于形式逻辑的丰富规范在今天的工业中很少使用，但使用它们的实用平台将通过识别漏洞、帮助程序员了解新组件的行为、促进严格的更改影响分析以及支持可维护的机器检查组件正确和正确组装的验证，显著降低系统实施和发展的成本。这次考察的重点是一类特别丰富的规范，即“深度规范”。这些对单个组件施加了强大的功能正确性要求，使得它们与严格的组合定理联系在一起。探险队的目标是集中编程语言和形式化方法社区的努力，在大范围内开发和使用深度规范。在一个正式的验证管理系统中工作，该项目将特别专注于在规范接口将基础设施组件连接在一起：编译器、操作系统、程序分析工具和处理器体系结构。

项目成果

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code

性能关键型应用程序的关系编译：将功能模型转换为低级代码的可扩展证明生成

• DOI: 10.1145/3519939.3523706
• 发表时间: 2022
• 期刊: PLDI 2022
• 作者: Pit-Claudel, Clément;Philipoom, Jade;Jamner, Dustin;Erbsen, Andres;Chlipala, Adam
• 通讯作者: Chlipala, Adam