Verifying ECC Implementations

Last Thursday, the University of Bristol posted a press release and paper describing a way to exploit a bug in version 0.9.8g of OpenSSL and extract the value of a private key. The bug was known, and has been fixed in recent versions of OpenSSL (0.9.8g was released in 2007, and 0.9.8h fixed the bug in 2008), but an exploit was not previously known, and version 0.9.8g is still in production use.

The bug was in the modular reduction algorithm, used in the implementation of Elliptic Curve Cryptography (ECC), particularly the Elliptic Curve Diffie-Helman (ECDH) and Elliptic Curve Digital Signature Algorithm (ECDSA) code. These algorithms can be used to agree on shared encryption keys to implement the Secure Sockets Layer (SSL) used to encrypt HTTP transactions. An attacker who could discover the agreed-upon encryption key could therefore eavesdrop on secure web transactions.

The authors of the Bristol paper use the bug and associated exploit as an argument for the formal verification of key security components such as OpenSSL. Galois has long been a strong advocate for this position, and much of our formal methods work has been directed at establishing information assurance properties of security-critical software. As we describe below, our work recently used formal methods to prove the equivalence of a Java ECDSA implementation and a reference specification, discovering in the process that our Java implementation shared a very similar bug.

During 2011 we developed a high-speed Java implementation of ECDSA with the intent of formally proving its equivalence to a reference specification written in Cryptol, the domain-specific language we have developed for the high-level description of cryptographic algorithms. As a validation step, we confirmed the implementation generated the correct hashes for NIST test vectors, and subjected the implementation to one hundred thousand randomly-generated test vectors to ensure the property that the signature verification algorithm always succeeded on messages properly signed by the signature algorithm.

In January 2012, we completed the verification of our Java ECDSA implementation (with respect to our Cryptol specification) and in the process discovered a bug in our own implementation of the same modular reduction algorithm that led to the vulnerability in OpenSSL. Our verification process used a symbolic simulation tool for Java that we built during 2010 and 2011, and was able to discover a bug that had evaded our validation strategy based on testing.

To obtain empirical evidence of the difficulty of testing algorithms such as ECDSA, we ran the buggy implementation through millions of test vectors to determine how long it would take to discover the bug through manual testing alone. For the bug in our ECDSA implementation, we were able to reproduce the bug after running 600 thousand sign/verify test vectors, which amounted to more than 8 billion field reductions. The OpenSSL bug is even more rare, and should cause incorrect results for less than one out of every 229 test vectors. Despite the rarity of the bug, the OpenSSL bug was exploitable through an adaptive attack against the SSL server.

Our formal verification results show that our Java ECDSA implementation corresponds to the specification for all 21152 legal inputs to ECDSA signing, and 21920 legal inputs to ECDSA signature verification. Although the possibility still remains that the specification is incorrect, or the implementation is vulnerable to side channel attacks, the OpenSSL ECDSA bug shows that security can be compromised even if the bug only affects a very small fraction of the overall input space. There simply is no alternative to formal verification for comprehensive coverage of input spaces this large.