Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises
Explore a groundbreaking approach to implementing cryptographic arithmetic in this 18-minute IEEE conference talk. Discover how to create short, high-level code with machine-checked proofs of functional correctness, and learn how simple partial evaluation can transform it into the fastest-known C code. Examine the development of an elliptic-curve library that achieves competitive performance across 80 prime fields and multiple CPU architectures. Gain insights into the first verified high-performance implementation of P-256, the most widely used elliptic curve. Follow the journey of how these implementations were integrated into BoringSSL, replacing existing specialized code for major deployments in Chrome, Android, and CloudFlare. Delve into topics such as compile-time representation, call-by-value evaluation, specialized versions, known weights, and the technical deliverables that made this innovation possible.