Paper 2023/1861
Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking
Abstract
Given a fixed-size block, cryptographic block functions gen- erate outputs by a sequence of bitwise operations. Block functions are widely used in the design of hash functions and stream ciphers. Their correct implementations hence are crucial to computer security. We pro- pose a method that leverages logic equivalence checking to verify assem- bly implementations of cryptographic block functions. Logic equivalence checking is a well-established technique from hardware verification. Using our proposed method, we verify two dozen assembly implementations of ChaCha20, SHA-256, and SHA-3 block functions from OpenSSL and XKCP automatically. We also compare the performance of our technique with the conventional SMT-based technique in experiments.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- hash functionsstream cipherscryptographic programslogical equivalence checkingformal verification
- Contact author(s)
-
alxlai @ csie ntu edu tw
jiaxiang0924 @ gmail com
xshi0811 @ gmail com
mht208 @ gmail com
bywang @ iis sinica edu tw
byyang @ iis sinica edu tw - History
- 2023-12-06: approved
- 2023-12-04: received
- See all versions
- Short URL
- https://ia.cr/2023/1861
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2023/1861,
author = {Li-Chang Lai and Jiaxiang Liu and Xiaomu Shi and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang},
title = {Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking},
howpublished = {Cryptology ePrint Archive, Paper 2023/1861},
year = {2023},
note = {\url{https://eprint.iacr.org/2023/1861}},
url = {https://eprint.iacr.org/2023/1861}
}
