Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking
摘要
Given a fixed-size block, cryptographic block functions generate 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 propose a method that leverages logic equivalence checking from hardware verification to verify assembly implementations of cryptographic block functions. Using our technique, we verify more than 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 SMT-based techniques in experiments.