A Messy State of the Union: Taming the Composite State Machines of TLS

By Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue. 2015

300 citations recorded by the source corpus.

Implementations of the Transport Layer Security (TLS) protocol must handle a variety of protocol versions and extensions, authentication modes, and key exchange methods. Confusingly, each combination may prescribe a different message sequence between the client and the server. We address the problem of designing a robust composite state machine that correctly multiplexes between these different protocol modes. We systematically test popular open-source TLS implementations for state machine bugs and discover several critical security vulnerabilities that have lain hidden in these libraries for years, and have now finally been patched due to our disclosures. Several of these vulnerabilities, including the recently publicized FREAK flaw, enable a network attacker to break into TLS connections between authenticated clients and servers. We argue that state machine bugs stem from incorrect compositions of individually correct state machines. We present the first verified implementation of a composite TLS state machine in C that can be embedded into OpenSSL and accounts for all its supported cipher suites. Our attacks expose the need for the formal verification of core components in cryptographic protocol libraries, our implementation demonstrates that such mechanized proofs are within reach, even for mainstream TLS implementations.

Subfields: Computer Networks and Communications, Electrical and Electronic Engineering

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computer Networks and Communications

In Electrical and Electronic Engineering

Citations in the corpus

A Search Engine Backed by Internet-Wide Scanning (2015, background): “There have been a large number of research studies over the past several years that have been based on Internet-wide scanning [1,7–11,13,14,18,19,24–29,38], which encouraged us to develop Censys.”
SoK: Security Evaluation of Home-Based IoT Deployments (2019, background): “[59] found flaws in several client and server implementations of TLS/SSL libraries that allow MITM attacks, including the FREAK [57] vulnerability.”
Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice (2015, unknown): “This allows us to compute individual discrete logs in about a minute.”
Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2 (2017, background): “As a result, recent attacks on TLS also affect these mechanisms, examples being [10, 14, 15, 27, 62].”
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif (2016, background): “The first version dates back to 1994, and since then many attacks were discovered, fixed versions were developed, and new attacks are still regularly discovered (Beurdouche et al., 2015; Adrian et al., 2015).”