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

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

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.