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

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

doi:10.1109/SP.2015.39

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

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	2015 IEEE Symposium on Security and Privacy
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	535-552
Number of pages	18
ISBN (Electronic)	978-1-4673-6949-7
DOIs	https://doi.org/10.1109/SP.2015.39
Publication status	Published - 20 Jul 2015
Event	2015 IEEE Symposium on Security and Privacy - The Fairmont, San Jose, CA, United States Duration: 18 May 2015 → 20 May 2015 https://www.ieee-security.org/TC/SP2015/

Publication series

Name
Publisher	IEEE
ISSN (Print)	1081-6011
ISSN (Electronic)	2375-1207

Conference

Conference	2015 IEEE Symposium on Security and Privacy
Country/Territory	United States
City	San Jose, CA
Period	18/05/15 → 20/05/15
Internet address	https://www.ieee-security.org/TC/SP2015/

Keywords

cryptographic protocols
formal verification
TLS protocol
authentication modes
composite TLS state machine
key exchange methods
message sequence
open-source TLS
security vulnerabilities
transport layer security protocol
Authentication
Computer bugs
Cryptography
Libraries
Protocols
Servers
Transport Layer Security
formal methods
man-in-the-middle attacks
software verification

Access to Document

10.1109/SP.2015.39Licence: All Rights Reserved

S&P-messy-state-of-the-unionAccepted author manuscript, 576 KB

https://ieeexplore.ieee.org/document/7163046/Licence: All Rights Reserved

Markulf Kohlweiss
- markulf.kohlweissed.acuk
- School of Informatics - Senior Lecturer in Security and Privacy
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active , Academic: Research Active (Teaching)

Cite this

@inproceedings{026cb1f7a590435f86a1b1c8c2b42d36,

title = "A Messy State of the Union: Taming the Composite State Machines of TLS",

abstract = "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.",

keywords = "cryptographic protocols, formal verification, TLS protocol, authentication modes, composite TLS state machine, key exchange methods, message sequence, open-source TLS, security vulnerabilities, transport layer security protocol, Authentication, Computer bugs, Cryptography, Libraries, Protocols, Servers, Transport Layer Security, formal methods, man-in-the-middle attacks, software verification",

author = "Benjamin Beurdouche and Karthikeyan Bhargavan and Antoine Delignat-Lavaud and C{\'e}dric Fournet and Markulf Kohlweiss and Alfredo Pironti and Pierre-Yves Strub and Zinzindohoue, {Jean Karim}",

year = "2015",

month = jul,

day = "20",

doi = "10.1109/SP.2015.39",

language = "English",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

pages = "535--552",

booktitle = "2015 IEEE Symposium on Security and Privacy",

address = "United States",

note = "2015 IEEE Symposium on Security and Privacy ; Conference date: 18-05-2015 Through 20-05-2015",

url = "https://www.ieee-security.org/TC/SP2015/",

}

Beurdouche, B, Bhargavan, K, Delignat-Lavaud, A, Fournet, C, Kohlweiss, M, Pironti, A, Strub, P-Y & Zinzindohoue, JK 2015, A Messy State of the Union: Taming the Composite State Machines of TLS. in 2015 IEEE Symposium on Security and Privacy. Institute of Electrical and Electronics Engineers (IEEE), pp. 535-552, 2015 IEEE Symposium on Security and Privacy, San Jose, CA, United States, 18/05/15. https://doi.org/10.1109/SP.2015.39

TY - GEN

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

AU - Beurdouche, Benjamin

AU - Bhargavan, Karthikeyan

AU - Delignat-Lavaud, Antoine

AU - Fournet, Cédric

AU - Kohlweiss, Markulf

AU - Pironti, Alfredo

AU - Strub, Pierre-Yves

AU - Zinzindohoue, Jean Karim

PY - 2015/7/20

Y1 - 2015/7/20

N2 - 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.

AB - 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.

KW - cryptographic protocols

KW - formal verification

KW - TLS protocol

KW - authentication modes

KW - composite TLS state machine

KW - key exchange methods

KW - message sequence

KW - open-source TLS

KW - security vulnerabilities

KW - transport layer security protocol

KW - Authentication

KW - Computer bugs

KW - Cryptography

KW - Libraries

KW - Protocols

KW - Servers

KW - Transport Layer Security

KW - formal methods

KW - man-in-the-middle attacks

KW - software verification

U2 - 10.1109/SP.2015.39

DO - 10.1109/SP.2015.39

M3 - Conference contribution

SP - 535

EP - 552

BT - 2015 IEEE Symposium on Security and Privacy

PB - Institute of Electrical and Electronics Engineers (IEEE)

T2 - 2015 IEEE Symposium on Security and Privacy

Y2 - 18 May 2015 through 20 May 2015

ER -

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Profiles

Markulf Kohlweiss

Cite this