Improving the Coq proof automation tactics of the Verified Software Toolchain, based on a case study on verifying a C implementation of the AES encryption algorithm

Abstract:

We present a (almost complete) machine-checked proof of functional correctness of a
C implementation of the AES encryption algorithm. The proof is written in Coq,
using the Veried Software Toolchain (VST), which connects to the CompCert veried
C compiler. Since both of these come with a machine-checked correctness proof, we
obtain an end-to-end proof linking the high-level specication of AES to the assembly
code produced by CompCert.
Moreover, we report on the challenges encountered with VST's proof automation
library, and identify and implement the improvements needed to write the AES proof,
such as a generalization of the proof automation for memory loads and stores allowing
accesses to nested elds inside arrays and/or structs whose access path is not explicitly
written in the load or store statement, a more careful invocation of Coq's term sim-
plication preventing unfeasibly slow proof script running times, and various usability
improvements.