Paper 2022/1116
Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE
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.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- Formal Verification CoQCryptoLine
- Contact author(s)
-
mhtsai208 @ gmail com
yufu @ gatech edu
xshi0811 @ gmail com
jiaxiang0924 @ gmail com
bywang @ iis sinica edu tw
byyang @ iis sinica edu tw - History
- 2022-08-29: approved
- 2022-08-29: received
- See all versions
- Short URL
- https://ia.cr/2022/1116
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2022/1116, author = {Ming-Hsien Tsai and Yu-Fu Fu and Xiaomu Shi and Jiaxiang Liu and Bow-Yaw Wang and Bo-Yin Yang}, title = {Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE}, howpublished = {Cryptology ePrint Archive, Paper 2022/1116}, year = {2022}, note = {\url{https://eprint.iacr.org/2022/1116}}, url = {https://eprint.iacr.org/2022/1116} }