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

点击翻译按钮获取中文摘要

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.