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.