DeepSEA: A Language for Certified System Software
Last modified: Sat Sep 7 21:05:56 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, Volume 3, 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