# PostscriptPostcript and bibliography

- SHA-2 cryptographic hashing [Appel 2015]
- HMAC cryptographic authentication [Beringer 2015]
- HMAC-DRBG cryptographic random number generation [Ye 2017]
- Concurrent messaging system [Mansky 2017]
- Generational copying garbage collector [Wang 2019]
- Bins-based malloc/free system [Appel and Naumann 2020]
- AES encryption, B+Trees, Tries of B+ trees (unpublished master's or undergraduate theses).

## Small examples

VST is distributed with a progs directory of many small C programs that demonstrate different features and methods of Verifiable C. If your VST installation is in the standard place, you can find this as a subdirectory of`coqc -where`/user-contrib/VST

## Modules

The first-draft version of VST's module system -- for verifying multimodule C programs with .c and .h files -- is described in [Beringer 2019]. The newer version, using Verified Software Units, is demonstrated in progs/VSUpile distributed with VST. The description in [Beringer 2019] mostly matches the proofs in progs/VSUpile, but the proofs handle data abstraction using the methods described in the the VSU chapters of this volume.## Input/output

To prove I/O using our Verifiable C logic, we treat the state of the outside world as a resource in the SEP clause, alongside (but separating from) in-memory conjuncts. Proved examples are in progs/io.c, progs/io_mem.c, and their proof files progs/verif_io.v, progs/verif_io_mem.v. Research papers describing these concepts include [Koh 2020] and [Mansky 2020].# Looking around

## Static analyzers

There are many*static analyzers*-- too numerous to list here -- that attempt to check

*safety*of your program: will it crash? Will it access an array out of bounds, or dereference an uninitialized pointer? Static analyzers can be useful in software engineering, but they have two major limitations:

- They don't verify
*functional correctness*-- that is, does your program produce the right answer, or interact with the right behavior? - They are incomplete. For example, proving that a[i] is an in-bounds array access requires proving that 0 ≤ i < N. Sometimes a static analyzer can deduce that from the program flow, but in general it is a functional correctness property that may require sophisticated invariants to prove.

## Functional correctness verifiers -- functional languages

A good way to write proved-correct software is to program in a pure functional program logic, and use higher-order logic to prove correctness. For example:- Write pure functional programs in Coq, prove them correct in Coq, then extract them from Coq to OCaml or Haskell. See Volume 3 of Software Foundations: Verified Functional Algorithms.
- In HOL systems (Higher-order Logic) such as Isabelle/HOL, you can do the same thing: write functional programs, prove them correct, extract, compile.
- You can write Haskell programs, compile with ghc, and import into Coq for verification using hs-to-coq [Spector-Zabusky 2018].
- ACL2 is an older system, that uses a first-order logic. That's less expressive, you don't get polymorphism or quantification, but there have been many successful applications of ACL2 in industry.

## Functional correctness verifiers -- imperative languages

*Software Foundations*. CakeML is a system for proving (and correctly compiling) ML programs in HOL [Kumar 2014].

## Functional correctness verifiers -- C

*low-level imperative language*-- C -- there are several systems:

- Frama-C (https://frama-c.com/)
- VeriFast [Jacobs 2011]
- VST (the subject of this volume).

- In VST, as you have seen, that language is a separation language (PROP/LOCAL/SEP) embedded in Coq, so that the PROP, LOCAL, and SEP clauses can all make use of the full expressive power of the Calculus of Inductive Constructions (CiC). You have seen a simple example of the expressive power of this approach, where we can use ordinary Coq proofs in Hashfun, and directly connect them to separation-logic proofs in Verif_hash.
- Frama-C uses a weaker assertion language, expressed in C syntax. That's a much weaker logic to reason in, and it doesn't directly connect to a general-purpose logic (and proof assistant) like Coq. Also, since Frama-C is not a separation logic, it can be difficult to reason about data structures.
- VeriFast uses a capable Dafny-like logic -- even more capable, since it is separation logic, not just Hoare logic. That means you can reason about data structures. There's no artificial limitation to a C-like syntax in the assertion language. Unfortunately, VeriFast's assertion language is not connected to a general-purpose logic (and proof assistant); that means you can do refinement proofs (this C program implements that functional model), but it's not so easy to reason about properties of your functional models.

## Foundational soundness

- the compiler must not have bugs, and
- the compiler must agree with your verifier on every detail of the semantics of the source language.

# Conclusion

*lingua franca*in which you can express a wide variety of programming paradigms, and Verifiable C is expressive enough to allow to verify them. We wish you success in your future software verification efforts.

(* 2023-03-25 11:30 *)