The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

DeepSEA: A Language for Certified System Software

Last modified: Fri Sep 27 22:01:22 2019 GMT.

Authors

Vilhelm Sjöberg
Yuyang Sang
Shu-Chun Weng
Zhong Shao

Abstract

Writing 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.

Published

In 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.
  • Conference Paper [PDF]

  • Copyright © 1996-2019 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon