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

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

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.