ciphersuite, and that this sequence cannot be confused with
that of another ciphersuite. The second step is to prove that it
is safe to share the long-term signing keys used in our ciphersuite with other, unverified ciphersuites. This property is problematic for current versions of TLS, but is expected to hold for
TLS 1. 3. 14 The third step is to show that the session secrets of
our verified ciphersuite are cryptographically independent
from any other ciphersuite. This property should hold for connections that use TLS 1. 3, and also for those that use the TLS
extended master secret extension. 4
In summary, by verifying its state machine, we have taken a
first step toward an OpenSSL security theorem, but many problems remain before we can verify mainstream libraries that
include legacy code, insecure ciphersuites, and obsolete protocol versions. Partly as a result of our work, the state machine in
next major version OpenSSL 1. 1.0 was rewritten from scratch,
with the goal of making it simpler, stricter, and easier to validate.
We hope that with similar efforts in the rest of the codebase, all of
OpenSSL will one day become amenable to formal verification.
5. RELATED WORK
5. 1. TLS attacks
The reader is advised to refer to Soghoian and Stamm24 for a
broad survey of previous attacks on TLS and its implementations; here, we discuss here only closely related work.
Wagner and Schneier28 describe various attacks against
SSL 3.0, and their analysis has proved prescient for many
attacks on TLS, including the state machine flaws discussed
in this paper. For instance, they present an early cross-cipher-suite attack (predating23) that rely on confusing ephemeral
RSA handshakes with ephemeral Diffie–Hellman. They also
anticipate some of our message skipping attacks by pointing
out that, in MAC-only ciphersuites, the attacker can bypass
authentication by skipping CCS messages.
In parallel with our work, de Ruiter and Poll12 apply
machine learning techniques to reverse engineer the state
machines of several TLS libraries and discover flaws like
the ones described in this paper. Their technique is able to
reconstruct abstract state machines even for closed-source
libraries, whereas our method focuses on testing conformance to the standard and uncovering concrete exploits.
Jager et al. 17 identify a class of backwards compatibility
attacks on protocol implementations that support both
strong and weak algorithms, showing for instance how a
side-channel attack on RSA decryption in TLS servers can be
exploited to mount a cross-protocol attack on server signatures. 18 FREAK, our downgrade attack on export RSA ciphersuites, can also be seen as a backwards compatibility attack.
Inspired by FREAK, Logjam1 is a downgrade attack that
exploits a protocol-level ambiguity between the DHE and
export DHE ciphersuites. Whereas FREAK relied on a state
machine flaw, Logjam relies on the widespread acceptance
of weak Diffie–Hellman groups in TLS clients.
Another class of TLS vulnerabilities stems from the
incorrect composition of TLS sub-protocols for renegotiation, 26 alerts, 6 and resumption. 8 These flaws may be partly
blamed on the state machine being underspecified in the
standard—the last two were discovered while designing and
verifying the state machine of mi TLS.
far is allowed by the state machine. We then specify that this
predicate must be maintained as an invariant by our ssl3_
To mechanically verify that our state machine implementation complies with its isValidState specification, we use
the C verification tool Frama-C. 11 We annotate our code with
logical assertions and requirements in Frama-C’s specification language, called ACSL, including 460 lines of first-order
logic to define isValidState. To verify our state machine code,
we ran Frama-C to generates proof obligations for multiple
SMT solvers. We used Alt-Ergo to discharge some obligations and Z3 for others, for a total verification time of 30 min.
Technically, verification also involves memory invariants, to
ensure that our code maintains separation between its private state and the rest of OpenSSL, and 900 lines of lemmas
to facilitate the proof. (We formally assume that the rest of
OpenSSL does not interfere with our code; verifying their full
codebase is well beyond the scope of this work.)
4. 4. Discussion
Predicates such as isValidState are logical encodings of our
state machines. They are inspired by the simpler log predicates used in the cryptographic verification of miTLS. 6 The
properties they capture depend only on the TLS specification; they omit any implementation details, and are even
independent of their programming languages.
Although our logical specification is almost as long as the
code we verified, we found verification useful in several ways.
First, in addition to our state invariant, we prove memory
safety for our code, a mundane but important goal for C programs. Second, our predicates provide an independent specification of the state machine, and verifying that they agree with
the code helped us find bugs, especially regressions due to the
addition of new features to the machine. Third, our logical
formulation of the state machine allows us to prove theorems
about its precision. For example, we used the Coq proof assistant to formally establish that the message sequence stored in
STATE is unambiguous, that is, if the sequences in two valid
state are the same, then the rest of the states must be the same
as well. This property is a key lemma for proving the security of
TLS, inasmuch as the message transcripts (not the states they
encode) are authenticated at the end of the handshake.
Still, our verification result is far from a mi TLS-style security
theorem for OpenSSL. We proved that our state machine for
OpenSSL is functionally correct, but we did not, for example,
verify the cryptographic constructions or the full message processing code. We could attempt to extend our results to a larger
fragment of OpenSSL that implements all important protocol
features; verifying all this code may be feasible but remains a
An intermediate goal may be to verify the code in OpenSSL
for a single strong ciphersuite, such as TLS_ECDHE_ECDSA_
WITH_AES_128_GCM_SHA256. We would then need to prove
that, no matter which other ciphersuites are supported, if the
client and server choose this ciphersuite, then the resulting
connection is secure. To achieve even this limited security
theorem, we must overcome several challenges. The first step,
which we have already accomplished, is to prove that the state
machine correctly implements the message sequence for this