SHF: Medium: DeepSEA: A Language for Programming and Synthesizing Certified Software

SHF：媒介：DeepSEA：一种用于编程和综合认证软件的语言

• 批准号: 1763399
• 负责人: Zhong Shao
• 金额: $ 80万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-06-01 至 2024-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1763399&HistoricalAwards=false
• 关键词: SHF; Medium; DeepSEA; Language; Programming

Building certifiably reliable and secure software is one of the grand challenges facing today's computing community. Despite the extensive progress in programming languages in the past few decades, today's mainstream operating systems and hypervisors are still written in C-like low-level languages. There seems to be an inherent conflict between high-level formal reasoning and low-level systems programming: the former relies on a rich theory at a high abstraction level while the latter must manipulate and manage low-level effects and hardware resources. The chief novelties of this project are (1) to design and implement a new language (named DeepSEA) that can be used to tackle this inherent conflict and directly program and synthesize certified software, and (2) to develop a DeepSEA toolchain and apply it to build certified OS kernels and Ethereum-style smart contracts. The project's impacts are demonstrated in multiple ways. The technology for building certified software will have a profound impact on the software industry and the society in general; it will dramatically improve the reliability and security of many key components in the world's critical infrastructure. The project would catalyze a change in the way computing science is taught at U.S. universities, by pushing new courses on formal methods into the existing curriculum; it would broaden the participation of underrepresented groups and give U.S. students a unique combination of technical training and international experience in this cutting-edge field.Certified programming is a unique challenge for language design: both operating systems and smart contracts are inherently low-level and effectful, while software verification requires high-level abstractions and pure functions. Recent projects on OS kernel verification required writing (manually) the actual kernel in a C-like language and a formal specification of the kernel in a proof-assistant language; a large part of the verification effort is then spent on showing that the implementation indeed satisfies the specification. DeepSEA bridges this chasm automatically---from a single input program, one can derive the relation between abstract data types and bytes, and between functional specification and concrete implementation. Instead of having to choose between high- and low-level languages, DeepSEA can have the best of both. The DeepSEA language provides native support for layered specification and abstraction refinement, full equational reasoning, a functional model of effects (including concurrency), and effect encapsulation and composition: consequently it directly supports certified programming at multiple abstraction levels. Using DeepSEA, a programmer need only to write the formal specification of a desirable system; then the DeepSEA compiler will automatically compile the DeepSEA program into a certified artifact consisting of a C program (which is then compiled into assembly by the verified C compiler, CompCert), a Coq specification, and a formal (Coq) proof that the C program satisfies the specification. The project opens up a new space of language designs that can directly support the development of correct-by-construction system software.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

确认可靠且安全的软件是当今计算社区面临的巨大挑战之一。尽管在过去几十年中，编程语言取得了广泛的进展，但当今的主流操作系统和虚拟机程序仍然以类似C的低级语言编写。 高级形式推理和低级系统编程之间似乎存在固有的冲突：前者依靠高抽象水平的丰富理论，而后者必须操纵和管理低级效果和硬件资源。 该项目的主要新颖性是（1）设计和实施一种新语言（命名为DeepSea），该语言可用于解决这一固有的冲突，并直接编程和合成认证的软件，以及（2）开发DeepSea工具链，并将其应用于建立认证的OS内核和以太坊风格的智能合约。该项目的影响通过多种方式证明。建立认证软件的技术将对软件行业和整个社会产生深远的影响；它将大大提高世界关键基础架构中许多关键组成部分的可靠性和安全性。该项目将通过将正式方法的新课程推入现有课程来促进美国大学教授计算科学的变化。它将扩大代表性不足的群体的参与，并为美国学生提供技术培训和国际经验的独特组合。确定的编程是语言设计的独特挑战：操作系统和智能合约固有的低级且有效，而软件验证则需要高级抽象和纯粹的功能。 有关OS内核验证的最新项目需要（手动）以C型语言的实际内核和以证明辅助语言对内核进行正式规范；然后将大部分验证工作用于表明该实施确实满足了规格。 DeepSea从单个输入程序中自动桥接此鸿沟，可以得出抽象数据类型和字节之间以及功能规范和具体实现之间的关系。 Deepsea不必在高级语言和低级语言之间进行选择，而是两者兼而有之。 DeepSea语言为分层规范和抽象细化，完整的方程推理，效果的功能模型（包括并发）以及效果封装和组成提供了本地支持：因此，它直接在多个抽象水平上直接支持认证的编程。 使用DeepSea，程序员只需要编写理想系统的正式规范即可。然后，DeepSea编译器将自动将DeepSea程序编译为由C程序组成的认证人工制品（然后由经过验证的C编译器，COMPCERT），COQ规范和正式（COQ）证明C计划满足规范。该项目开辟了一个新的语言设计空间，可以直接支持正确的构造系统软件的开发。该奖项反映了NSF的法定任务，并且使用基金会的知识分子优点和更广泛的审查标准，被认为值得通过评估来获得支持。

项目成果

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