Verification of Elliptic Curve Cryptography

Presented as part of the 2012 HCSS conference.

Abstract:

Cryptography is essential for ensuring that sensitive information can be securely stored and transmitted without risk of tampering or disclosure to untrusted parties. Although typically only a very small part of an overall system, cryptographic implementations are often highly complex due to a variety of performance optimizations, and may have many edge cases or diffcult to understand implementation tricks.

For public key cryptography in particular, implementations may contain subtle bugs that only affect a very small fraction of the total input space. For example, a bug was recently found in OpenSSL’s implementation of ECC that affects less than 1 in 229 modular reductions2. Exhaustive testing of ECC implementations is infeasible due to the vast state space involved, and the complexity of ECC makes it intractable to verify using existing automated formal verification techniques. How can one have confidence that an ECC implementation is correct?

At Galois, we have found that compositional reasoning is key to solving this problem.

We have developed a compositional verification tool, called SAWScript, that allows individual methods within a cryptographic implementation to be precisely specified and independently verified. Specifications of low-level methods can be used to simplify the verification of more complex methods, and the SAWScript tool has incorporated a variety of automated and manual verification techniques, including SAT, SMT, and rewriting.

To validate the effectiveness of SAWScript, we have successfully implemented and verified a Java-based implementation of ECDSA over the NIST P-384 curve. Our implementation was designed for high performance rather than ease of verification. It is eight times faster than the BouncyCastle Java implementation of ECDSA, and is competitive with OpenSSL’s C implementation. Our correctness proof decomposes the overall verification of ECDSA signing and signature checking into the verification of 50 different methods, and requires approximately 10 minutes to complete on a commodity laptop.

In the talk, I will describe Galois’ tools and verification efforts to date, as well as sketch some more recent developments on the verification of low-level cryptographic implementations written in C.

________________________________

1 Corresponding author: Joe Hendrix, jhendrix@galois.com

2 B. B. Brumley,  M. Barbosa, D. Page, and F. Vercauteren. Practical Realisation and Elimination of an ECC-Related Software Bug Attack. CT-RSA, volume 7178 of LNCS, pages 171186. Springer, 2012.

Biography:

Dr. Joe Hendrix is a researcher working on security and formal methods at Galois, Inc. His work at Galois focuses on development of tools for formal verification and runtime monitoring. He designed the SAWScript verification tools, and authored the implementation at elliptic curve cryptography described in this talk. Prior to joining Galois, he was the main developer of tools for attack surface analysis at Microsoft. Dr. Hendrix received his Ph.D. in Computer Science at the University of Illinois Urbana-Champaign in 2008 for research in new decision procedures for automated reasoning.