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

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

12th Conference on Verified Software: Theories, Tools, and Experiments (VSTTE) |

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