Article

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

Authors:

Benjamin Beurdouche,

Karthikeyan Bhargavan,

Antoine Delignat-Lavaud,

Jean Karim ZinzindohoueAuthors Info & Claims

SP '15: Proceedings of the 2015 IEEE Symposium on Security and Privacy

Pages 535 - 552

https://doi.org/10.1109/SP.2015.39

Published: 17 May 2015 Publication History

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.

Cited By

View all

Shi QXu XZhang XCalandrino JTroncoso C(2023)Extracting protocol format as state machine via controlled static loop analysisProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620630(7019-7036)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620630
Paterson KScarlata MTruong KCalandrino JTroncoso C(2023)Three lessons from threemaProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620310(1289-1306)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620310
Fischlin MMeng WJensen CCremers CKirda E(2023)Stealth Key Exchange and Confined Access to the Record Protocol Data in TLS 1.3Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623099(2901-2914)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623099
Show More Cited By

Index Terms

Recommendations

A messy state of the union: taming the composite state machines of TLS

The Transport Layer Security (TLS) protocol supports various authentication modes, key exchange methods, and protocol extensions. Confusingly, each combination may prescribe a different message sequence between the client and the server, and thus a key ...
FLEXTLS: a tool for testing TLS implementations
WOOT'15: Proceedings of the 9th USENIX Conference on Offensive Technologies

We present FLEXTLS, a tool for rapidly prototyping and testing implementations of the Transport Layer Security (TLS) protocol. FLEXTLS is built upon MITLS, a verified implementation of TLS, and hence protocol scenarios written in FLEXTLS can benefit ...
RFC 4169: Hypertext Transfer Protocol (HTTP) Digest Authentication Using Authentication and Key Agreement (AKA) Version-2

Reviews

Reviewer: A. Squassabia

By bringing consolidated structure to the panoply of requirements that make up the transport layer security (TLS) standard, this paper allows practitioners to formulate a framework for testing how compliant several of their open-source software (OSS) implementations are. TLS and its precursors have been, for a couple of decades, the lifeblood of secure communication across the Web. Backward compatibility, feature bloat, and many specifications unaware of each other over that lengthy period have together provided a fertile substrate for the culturing of software bugs. This paper contributes a method for framing the assembly of those requirements into a cohesive whole, a mechanism for testing relevant OSS implementations for compliance with that structured assembly, the outcome of such testing (which includes serious vulnerabilities), and an implementation of TLS geared toward correctness rather than performance (therefore arguably not production-ready). The authors have acknowledged limitations as well; for instance, testing is not exhaustive as it disregards many combinations of configuration parameters or content, and vetting, albeit partially automated, depends heavily on manual intervention. The effort is, however, worthwhile. In addition, the methodology can be an inspiration for other software engineering challenges. The mechanisms are focused on the correctness of TLS, but the underlying guidance can be generalized for the verification of certain software artifacts that are otherwise very difficult to test. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SP '15: Proceedings of the 2015 IEEE Symposium on Security and Privacy

May 2015

923 pages

ISBN:9781467369497

Publisher

IEEE Computer Society

United States

Publication History

Published: 17 May 2015

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

61
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Shi QXu XZhang XCalandrino JTroncoso C(2023)Extracting protocol format as state machine via controlled static loop analysisProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620630(7019-7036)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620630
Paterson KScarlata MTruong KCalandrino JTroncoso C(2023)Three lessons from threemaProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620310(1289-1306)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620310
Fischlin MMeng WJensen CCremers CKirda E(2023)Stealth Key Exchange and Confined Access to the Record Protocol Data in TLS 1.3Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623099(2901-2914)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623099
Nie PWan CZhu JLin ZChen YSu Z(2023)Coverage-directed Differential Testing of X.509 Certificate Validation in SSL/TLS ImplementationsACM Transactions on Software Engineering and Methodology10.1145/351041632:1(1-32)Online publication date: 22-Feb-2023
https://dl.acm.org/doi/10.1145/3510416
Bhargavan KCheval VWood CYin HStavrou ACremers CShi E(2022)A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client HelloProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security10.1145/3548606.3559360(365-379)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3548606.3559360
Izhikevich LTeixeira RDurumeric ZKuipers FOrda A(2022)Predicting IPv4 services across all portsProceedings of the ACM SIGCOMM 2022 Conference10.1145/3544216.3544249(503-515)Online publication date: 22-Aug-2022
https://dl.acm.org/doi/10.1145/3544216.3544249
Wan GGong FBarbette TDurumeric ZKuipers FOrda A(2022)RetinaProceedings of the ACM SIGCOMM 2022 Conference10.1145/3544216.3544227(530-544)Online publication date: 22-Aug-2022
https://dl.acm.org/doi/10.1145/3544216.3544227
Zhang HAgarwal YFredrikson MBulusu NAryafar EBalasubramanian ASong J(2022)TEOProceedings of the 20th Annual International Conference on Mobile Systems, Applications and Services10.1145/3498361.3539774(302-315)Online publication date: 27-Jun-2022
https://dl.acm.org/doi/10.1145/3498361.3539774
Hu QAsghar MBrownlee N(2021)A large-scale analysis of HTTPS deploymentsJournal of Computer Security10.3233/JCS-20007029:1(25-50)Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.3233/JCS-200070
Williams RRen TDe Carli LLu LSmith G(2021)Guided Feature Identification and Removal for Resource-constrained FirmwareACM Transactions on Software Engineering and Methodology10.1145/348756831:2(1-25)Online publication date: 24-Dec-2021
https://dl.acm.org/doi/10.1145/3487568
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

Cited By

Index Terms

Recommendations