Welcome to the resource topic for 2023/1861
Title:
Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking
Authors: Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
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.
ePrint: https://eprint.iacr.org/2023/1861
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 .