Paper 2023/1861 Original: eprint.iacr.org/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.
- History
- 2023-12-04: last updated
- 2023-12-04: published
- Short URL
- https://ia.cr/2023/1861
- License
- https://creativecommons.org/licenses/by/4.0/
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},
url = {https://eprint.iacr.org/2023/1861}
}