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

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

• 批准号: 1521523
• 负责人: Zhong Shao
• 金额: $ 204.64万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-12-15 至 2021-11-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1521523&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.

在我们相互联系的世界中，软件错误和安全漏洞构成了巨大的成本和风险。 Deep Specification（“ DeepSpec”，DeepSpec.org）项目通过展示如何构建可以执行该操作的软件来解决此问题，而同样重要，并且（同样重要）不再：不再允许黑客入侵的后门，没有崩溃的应用程序，您的应用程序，计算机或您的汽车。 “该软件应该做的事情”称为其规范。 DeepSpec项目将开发新的科学，技术和工具 - 指定程序应采取的措施，用于构建符合这些规格的程序，并验证程序的行为确实按预期的方式行为。 这项工作的关键使技术是现代交互式证明助手，该辅助助理支持有关复杂软件工件的严格数学证明。 项目活动将重点放在核心软件系统基础架构上，例如操作系统，编程语言编译器和计算机芯片，以及诸如选举和投票系统，汽车和智能手机之类的应用程序。预定且行为更好的软件将使我们所有人受益。 许多备受瞩目的安全漏洞和低调的入侵都使用软件错误作为其入口点。 在几十年以前的工作的基础上，DeepSpec将推进指定和验证软件的方法，以便软件行业可以使用它们。 该项目将包括研讨会和暑期学校，以吸引工业合作者进行技术转移。 但是，在工程中，更广泛的规格使用还需要接受规范和验证培训的软件工程师 - 如此DeepSpec在教育方面具有主要组成部分：介绍性和中级课程的开发，如何在逻辑上进行逻辑思考，如何在规范上进行思考，如何在构建系统软件组件中使用规格，或如何连接到此类组件。 教育组成部分包括在普林斯顿，宾夕法尼亚州，麻省理工学院和耶鲁大学开发的教科书和在线课程材料，以及全球学生和讲师使用。 还将有一所暑期学校来培训可以将这项科学带入全国大学的老师。Abstraction和Modularity是所有成功的硬件和软件系统的基础：我们通过将它们分解为可以单独理解的部分来建立复杂的文物。模块化分解至关重要地取决于零件之间的界面的精心选择。随着这些接口变得更加表现力，我们将它们视为组件或层的规格。基于正式逻辑的丰富规格在当今的行业中很少使用，但是与它们合作的实用平台将通过识别漏洞来大大降低系统实施和演变的成本，从而帮助程序员了解新组件的行为，从而促进了可维护的机器 - 检查组件正确和拟合组件的可维护的机器验证和正确拟合。 这次探险专注于特别丰富的规格“深度规格”。这些对单个组件施加了强大的功能正确性要求，以便它们与严格的组成定理相连。探险的目标是将编程语言和正式方法社区的努力集中在整个大型规范上。 在正式的证明管理系统中，该项目将特别集中于在规范接口上将基础架构组件连接在一起：编译器，操作系统，程序分析工具和处理器架构。

项目成果

Blinder: Partition-Oblivious Hierarchical Scheduling

Blinder：忽略分区的分层调度

• 发表时间: 2021
• 期刊: Proceedings of the 30th USENIX Security Symposium (USENIX Security 2021
• 作者: Yoon, Man-Ki;Liu, Mengqi;Chen, Hao;Kim, Jung-Eun;Shao, Zhong
• 通讯作者: Shao, Zhong

CompCertELF: verified separate compilation of C programs into ELF object files

• DOI: 10.1145/3428265
• 发表时间: 2020-11
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Yuting Wang;Xiangzhe Xu;Pierre Wilke;Zhong Shao

Verified compilation of C programs with a nominal memory model

• DOI: 10.1145/3498686
• 发表时间: 2022-01
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Yuting Wang;Ling Zhang;Zhong Shao;Jérémie Koenig

ADLP: Accountable Data Logging Protocol for Publish-Subscribe Communication Systems

• DOI: 10.1109/icdcs.2019.00117
• 发表时间: 2019-07
• 期刊: 2019 IEEE 39th International Conference on Distributed Computing Systems (ICDCS)
• 作者: Man-Ki Yoon;Zhong Shao

Refinement-Based Game Semantics and Certified Abstraction Layers

基于细化的游戏语义和经过认证的抽象层

• 发表时间: 2020
• 期刊: Proc. 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'20
• 作者: Koenig, Jeremie;Shao, Zhong
• 通讯作者: Shao, Zhong