2009 Poster Sessions : 'Automatic Formal Verification of Block Cipher Implementations'

Student Name : Eric Smith
Advisor : David Dill
Research Areas: Computer Systems
We have developed an automatic method for verifying implementations of block ciphers and similar cryptographic algorithms. The method can compare two implementations or compare an implementation to a formal, mathematical specification. In either case it proves that the computations being compared are bit-for-bit equivalent. The method has two steps. First the computations are represented as directed acyclic graphs (DAGs), and then the two DAGs are proved equivalent using a phased approach which is optimized for verifying block ciphers and uses a careful choice of both word-level and bit-level simplifications. The approach also relies on STP, a SAT-based decision procedure for bit-vectors and arrays. Our method has been applied to verify real, widely-used Java code from Sun and the open source Bouncy Castle project. In particular, it has been used to verify implementations of the block ciphers AES, DES, Blowfish, RC2, RC6, and Skipjack, as well as applications of the cryptographic hash functions SHA-1 and MD5 on fixed-length messages.

Eric Smith is a Ph.D. student in Computer Science at Stanford University, advised by David Dill. His research interests focus on formal verification, including combinational and sequential equivalence checking, decision procedures, theorem proving, verification of Java code, and reasoning about heap-manipulating programs. Before coming to Stanford, he received concurrent bachelor's degrees in Computer Science and Plan II Honors from the University of Texas at Austin and then spent a year working on processor verification at Advanced Micro Devices.