V5 Verifiable C

References:

Overview

Verifiable C is a a language. The language is a subset of CompCert C light; it is a dialect of C in which side-effects and loads have been factored out of expressions.

Verifiable C is a program logic. The program logic is a higher-order separation logic, a kind of Hoare logic with better support for reasoning about pointer data structures, function pointers, and data abstraction.

Verifiable C is for reasoning about functional correctness of C programs.

Verifiable C is foundationally sound. That is, it is proved that, “Whatever observable property about a C program you prove using the Verifiable C program logic, that property will acutually hold on the assembly-language program that comes out of the C compiler”.

  • The program logic is proved sound with respect to the semantics of CompCert C, by a team of researchers primarily at Princeton University;
  • The C compiler is proved correct with respect to those same semantics, by a team of researchers primarily at INRIA.
  • This chain of proofs from top to bottom, connected in Coq at specification interfaces, is part of the Verified Software Toolchain.

Workflow

  1. Write a C program, say F.c
  2. Run clightgen -normalize F.c to translate it into a Coq file F.v
  3. Write a verification of F.v in a file such as verif_F.v. That latter file must import both F.v and the VST Floyd program verification system, VST.floyd.proofauto.

clignten tool: from CompCert, translates C into CompCert Clight language.

Load Paths. CoqIDE or Proof General will need their load paths properly initialized. Running make in vst creates a file _CoqProject file with the right load paths for proof development of the VST itself (or of its progs/examples).

coqide progs/verif_reverse.v &

In normal use(not using the examples in VST/progs/), your own files (F.c, F.v, verif_F.v) will not be inside the VST directory. You will need to use _CoqProject-export file to tell Coq to access the VST components:

cd my-own-directory
cp my/path/to/VST/_CoqProject-export _CoqProject
coqide myfile.v &

Restrictions to C

  • No casting between integers and pointers.
  • No goto statements.
  • No bitfields in structs.
  • No struct-copying assignments, struct parameters, or struct returns.
  • Only structured switch statements (No Duff’s device).
  • No varargs functions, except limited undocumented support for calling printf and fprintf.

CompCert Clight language (and clightgen tool) does support some of the above language features (such as goto, bitfields, struct-copying), but programs with those features cannot be proved in Verifiable C.

More

Created Apr 29, 2021 // Last Updated Nov 25, 2022

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?