Verified Transformations and Hoare Logic - Beautiful Proofs for Ugly Assembly Language.

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.