Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking

Bounded model checking-as well as symbolic equivalence checking-are highly successful techniques in the hardware domain. Recently, bit-vector bounded model checkers like CBMC have been developed that are able to check properties of (mostly low-level) software written in C. However, using these tools to check equivalence of software implementations has rarely been pursued. In this case study we tackle the problem of proving the functional equivalence of two implementations of the AES crypto-algorithm using automatic bounded model checking techniques. Cryptographic algorithms heavily rely on bit-level operations, which makes them particularly suitable for bit-precise tools like CBMC. Other software verification tools based on abstraction refinement or static analysis seem to be less appropriate for such software. We could semi-automatically prove equivalence of the first three rounds of the AES encryption routines. Moreover, by conducting a manually assisted inductive proof, we could show equivalence of the full AES encryption process.