A Verifying Core for a Cryptographic Language Compiler
Lee Pike, Mark Shields, and John Matthews.

---

A verifying compiler is one that emits both object code and a proof of correspondence between object and source code[Footnote 1]. We report the use of ACL2 in building a verifying compiler for Cryptol, a stream-based language for encryption algorithm specification that targets Rockwell Collins' AAMP7 microprocessor (and is designed to compile efficiently to hardware, too). This paper reports on our success in verifying the "core" transformations of the compiler -- those transformations over the sub-language of Cryptol that begin after "higher-order" aspects of the language are compiled away, and finish just before hardware or software specific transformations are exercised. The core transformations are responsible for aggressive optimizations. We have written an ACL2 macro that automatically generates both the correspondence theorems and their proofs. The compiler also supplies measure functions that ACL2 uses to automatically prove termination of Cryptol programs, including programs with mutually-recursive cliques of streams. Our verifying compiler has proved the correctness of its core transformations for multiple algorithms, including TEA, RC6, and AES. Finally, we describe an ACL2 book of primitive operations for the general specification and verification of encryption algorithms.

Footnote 1
Our use of the term "verifying compiler" differs from Tony Hoare's use of it in describing his "Grand Challenge" [10]. However, the fundamental goal of increased software assurance via proof is shared by a verifying compiler (in our sense) and the Grand Challenge. Henceforth in this paper, "verifying compiler" should be understood in our sense only.