Welcome to the resource topic for 2022/1116
Title:
Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE
Authors: Ming-Hsien Tsai, Yu-Fu Fu, Xiaomu Shi, Jiaxiang Liu, Bow-Yaw Wang, Bo-Yin Yang
Abstract:COQCRYPTOLINE is an automatic certified verification tool for cryptographic programs. It is built on OCAML programs extracted from algorithms fully certified in COQ with SS- REFLECT. Similar to other automatic tools, COQCRYPTO- LINE calls external decision procedures during verification. To ensure correctness, all answers from external decision procedures are validated by certified certificate checkers in COQCRYPTOLINE. We evaluate COQCRYPTOLINE on cryp- tographic programs from BITCOIN, BORINGSSL, NSS, and OPENSSL. The first certified verification of the reference implementation for number theoretic transform in the post- quantum key exchange mechanism KYBER is also reported.
ePrint: https://eprint.iacr.org/2022/1116
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .