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 在教育中具有重要组成部分：开发入门和中级课程，指导如何逻辑地思考规范，如何在构建系统中使用规范-软件组件，或如何连接到此类组件。教育部分包括普林斯顿大学、宾夕法尼亚大学、麻省理工学院和耶鲁大学开发的教科书和在线课程材料，可供全世界的学生和教师使用。还将举办一所暑期学校，培训能够将这门科学带到全国大学的教师。抽象和模块化是所有成功的硬件和软件系统的基础：我们通过将复杂的工件分解为可以单独理解的部分来构建它们。模块化分解很大程度上取决于各部分之间接口的巧妙选择。随着这些接口变得更具表现力，我们将它们视为组件或层的规范。基于形式逻辑的丰富规范在当今的行业中很少使用，但是使用它们的实用平台将通过识别漏洞、帮助程序员理解新组件的行为、促进严格的变更影响分析来显着降低系统实施和演进的成本，并支持可维护的机器检查验证，以确保组件正确且正确装配在一起。本次探索重点关注一类特别丰富的规范，即“深度规范”。这些对各个组件提出了强烈的功能正确性要求，以便它们通过严格的组合定理连接在一起。 Expedition 的目标是将编程语言和形式方法社区的努力集中在大规模开发和使用深层规范上。该项目在正式的证明管理系统中工作，将特别专注于在规范接口上将基础设施组件连接在一起：编译器、操作系统、程序分析工具和处理器架构。