Certified Verification for Algebraic Abstraction

Abstract We present a certified algebraic abstraction technique for verifying bit-accurate non-linear integer computations. In algebraic abstraction, programs are lifted to polynomial equations in the abstract domain. Algebraic techniques are employed to analyze abstract polynomial programs; SMT QF_BV solvers are adopted for bit-accurate analysis of soundness conditions. We explain how to verify our abstraction algorithm and certify verification results. Our hybrid technique has verified non-linear computations in various security libraries such as Bitcoin and OpenSSL. We also report the certified verification of Number-Theoretic Transform programs from the post-quantum cryptosystem Kyber.