Formal Functional Correctness of libsecp256k1's Modular Inverse
summary
Completes a computer-verified proof that one libsecp256k1 modular-inverse implementation actually computes inverses and terminates, formalizing the safe GCD termination argument (convex-hull proof rechecked from Python/Haskell reimplementations) and proving the C implementation correct with Coq with Verifiable C / VST tied to CompCert semantics; the verified C routine corresponds to code merged into libsecp256k1 (included in Bitcoin), while noting the proof covers functional correctness but not constant-timeness or C++ features.
AI-written summary · about
chapters (9)
- 0:00Formal correctness journey
- 1:13Humans writing correct software
- 5:28Proof theory to formalized math
- 8:25Modular inverse algorithms history
- 11:57Safe GCD algorithm correctness
- 16:15Termination proofs to code
- 18:24Implementation correctness with separation logic
- 23:38Verifying C code in libsecp256k1
- 25:24Adopt formal verification tools
related talks
20mFoundational Integration Verification of a Cryptographic Server
26mA Core Calculus for Equational Proofs of Cryptographic Protocols
01h 09mCrypto + ML 1
01h 09mProofs - Practice 1
22mComputational-Bounded Robust Compilation and Universally Composable Security
57mEssentially Optimal Interactive Certificates in Linear Algebra
44mModular Approach to Cloud Security
01h 16mMultilinear Maps Over the Integers: From Design to Security