DeepSEA: A Language for Certified System Software
Last modified: Fri Sep 27 22:01:22 2019 GMT.
AbstractWriting certifiably correct system software is still very labor-intensive, and current programming languages are not well suited for the task. Proof assistants work best on programs written in a high-level functional style, while operating systems need low-level control over the hardware. We present DeepSEA, a language which provides support for layered specification and abstraction refinement, effect encapsulation and composition, and full equational reasoning. A single DeepSEA program is automatically compiled into a certified ``layer'' consisting of a C program (which is then compiled into assembly by CompCert), a low-level functional Coq specification, and a formal (Coq) proof that the C program satisfies the specification. Multiple layers can be composed and interleaved with manual proofs to ascribe a high-level specification to a program by stepwise refinement. We evaluate the language by using it to reimplement two existing verified programs: a SHA-256 hash function and an OS kernel page table manager. This new style of programming language design can directly support the development of correct-by-construction system software.
PublishedIn Proc. 2019 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'19), Athens, Greece, October 2019. Published as Proceedings of the ACM on Programming Languages (PACMPL), Volume 3, Number OOPSLA, Article 136 (October 2019), 27 pages.
Copyright © 1996-2019 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science