Verifiable C: Proving Functional Correctness of C Programs in Coq, e.g. SHA-256 and HMAC

Presented as part of the 2015 HCSS conference.

Abstract:

Verifiable C is a program logic for C--a higher-order impredicative concurrent separation logic. As part of the Verified Software Toolchain, it comes with automated+interactive tactical proof tools for applying the logic to C programs. Verifiable C is proved sound w.r.t. the operational semantics of C; this proof connects to Leroy et al.'s correctness proof for the CompCert optimizing C compiler. All these proofs (including user proofs) are machine-checked in the Coq proof assistant. Composed together inside Coq, they guarantee that the functional-correctness properties you prove about the source program, are obeyed by the assembly-language (compiled) program.

Verifiable C is generally applicable to C programs; we demonstrate it on SHA-256 and HMAC lightly adapted from the OpenSSL implementations. We prove SHA and HMAC correct with respect to the FIPS 180 and FIPS 198 standards (respectively), and connect to Coq proofs of the high-level cryptographic properties of HMAC.

I'll use these examples to show the architecture of a functional-correctness specification: (1) pure functional spec, (2) proving user-relevant properties of functional specs, (3) API spec, which relates functional spec to the Application Programmer Interface of a C program, (4) proof that a program satisfies the API spec. HMAC's user-relevant property is that it implements a PRF (pseudorandom function), subject to certain standard (and fully formalized) assumptions about SHA-2.

Biography:

Andrew W. Appel is Eugene Higgins Professor and Chairman of the Department of Computer Science at Princeton University. He is a member of Princeton's Center for Information Technology Policy. His research is in software verification, computer security, programming languages and compilers, and technology policy. He received his A.B. summa cum laude in physics from Princeton in 1981, and his PhD in computer science from Carnegie Mellon University in 1985. He has been Editor in Chief of ACM Transactions on Programming Languages and Systems and is a Fellow of the ACM (Association for Computing Machinery). He has worked on fast N-body algorithms (1980s), Standard ML of New Jersey (1990s), Foundational Proof-Carrying Code (2000s), and the Verified Software Toolchain (2010s).