Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language

by Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel

Software Verification - 12th International Conference, VSTTE 2020

 Paper  Pre-print  Artifact

Hand-optimized assembly language code is often difficult to formally verify. This paper combines Hoare logic with verified code transformations to make it easier to verify such code. This approach greatly simplifies existing proofs of highly optimized OpenSSL-based AES-GCM cryptographic code. Furthermore, applying various verified transformations to the AES-GCM code enables additional platform-specific performance improvements.