Sciweavers

Share
ACL2
2006
ACM

A verifying core for a cryptographic language compiler

9 years 4 months ago
A verifying core for a cryptographic language compiler
A verifying compiler is one that emits both object code and a proof of correspondence between object and source code.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 ...
Lee Pike, Mark Shields, John Matthews
Added 13 Jun 2010
Updated 13 Jun 2010
Type Conference
Year 2006
Where ACL2
Authors Lee Pike, Mark Shields, John Matthews
Comments (0)
books