In this talk, I will present an approach to ease the verification of file-system
code using a domain-specific language, currently called CoGent, supported by
a self-certifying compiler that produces C code, a high-level specification, and
translation correctness proofs.
CoGent is a restricted, polymorphic, higher-order, and purely functional
language with linear types and without the need for a trusted runtime or
garbage collector. It compiles to efficient C code that is designed to
interoperate with existing C functions.
For a well-typed CoGent program, the compiler produces C code, a
high-level shallow embedding of its semantics in Isabelle/HOL, and a
proof that the C code correctly implements this embedding. The aim is
for proof engineers to reason about the full semantics of real-world
systems code productively and equationally, while retaining the
interoperability and leanness of C.
I will give a high-level overview of the formal verification stages of the
compiler, which include automated formal refinement calculi, a switch
from imperative update semantics to functional value semantics formally
justified by the linear type system, and a number of standard compiler phases
such as type checking and monomorphisation. The compiler certificate is a
series of language-level meta proofs and per-program translation validation
phases, combined into one coherent top-level theorem in Isabelle/HOL.