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

构建可证明可靠和安全的软件是当今计算社区面临的重大挑战之一。尽管在过去的几十年里编程语言取得了广泛的进步，但今天的主流操作系统和虚拟机管理程序仍然是用类似C的低级语言编写的。 高级形式推理和低级系统编程之间似乎存在着内在的冲突：前者依赖于高抽象层次上的丰富理论，而后者必须操纵和管理低级效果和硬件资源。 该项目的主要创新之处在于：（1）设计和实现一种新的语言（名为DeepSEA），可用于解决这种内在冲突，并直接编程和合成认证软件;（2）开发DeepSEA工具链，并将其应用于构建认证的操作系统内核和以太坊风格的智能合约。该项目的影响体现在多个方面。构建认证软件的技术将对软件行业和整个社会产生深远的影响;它将大大提高世界关键基础设施中许多关键组件的可靠性和安全性。该项目将促进美国大学计算机科学教学方式的改变，将正式方法的新课程纳入现有课程;它将扩大代表性不足的群体的参与，并为美国学生提供这一前沿领域的技术培训和国际经验的独特组合。认证编程对语言设计来说是一个独特的挑战：操作系统和智能合约本质上都是低层次和有效的，而软件验证需要高层次的抽象和纯功能。 最近的OS内核验证项目需要（手动）编写类似C语言的实际内核和证明辅助语言中的内核正式规范;大部分验证工作都花在显示实现确实满足规范上。 DeepSEA自动弥合了这一鸿沟--从单个输入程序中，可以导出抽象数据类型和字节之间的关系，以及功能规范和具体实现之间的关系。DeepSEA不必在高级语言和低级语言之间进行选择，而是可以两者兼得。 DeepSEA语言为分层规范和抽象细化、完整的等式推理、效果的功能模型（包括并发）以及效果封装和组合提供了原生支持：因此它直接支持多个抽象级别的认证编程。 使用DeepSEA，程序员只需编写所需系统的形式规范;然后DeepSEA编译器将自动将DeepSEA程序编译成由C程序（然后由经过验证的C编译器CompCert编译成汇编），Coq规范和C程序满足规范的形式（Coq）证明组成的认证工件。该项目开辟了一个新的语言设计空间，可以直接支持构建正确的系统软件的开发。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.