Certified Verification for Algebraic Abstraction
Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo‐Yin Yang · Lecture notes in computer science · 2023
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.