The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography

Explore a groundbreaking conference talk on foundational end-to-end verification of high-speed cryptography presented at CPP 2024. Delve into the unified framework developed by researchers to address the gap in formal verification of efficient cryptographic implementations. Learn how they connect three existing tools - Hacspec, Jasmin, and SSProve - using the Coq proof assistant. Discover the novel translations between these tools and their formal correctness proofs. Examine a case study demonstrating the framework's effectiveness through a foundational end-to-end Coq proof of an efficient AES implementation using hardware acceleration. Gain insights into the future of high-assurance cryptography and its potential impact on secure systems development.