A Messy State of the Union: Taming the Composite State Machines of TLS
Top Cited Papers
- 1 May 2015
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10816011,p. 535-552
- https://doi.org/10.1109/sp.2015.39
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
This publication has 14 references indexed in Scilit:
- Multi-Ciphersuite Security of the Secure Shell (SSH) ProtocolPublished by Association for Computing Machinery (ACM) ,2014
- Guiding a general-purpose C verifier to prove cryptographic protocolsJournal of Computer Security, 2014
- Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLSPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2014
- Verified Cryptographic Implementations for TLSACM Transactions on Information and System Security, 2012
- Certified Lies: Detecting and Defeating Government Interception Attacks against SSL (Short Paper)Published by Springer Nature ,2012
- JavaSPIInternational Journal of Secure Software Engineering, 2011
- Finding Error Handling Bugs in OpenSSL Using CoccinellePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2010
- ASPIER: An Automated Framework for Verifying Security Protocol ImplementationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2009
- Security Analysis of Crypto-based Java Programs using Automated Theorem ProversPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- Cryptographic Protocol Analysis on Real C CodePublished by Springer Nature ,2005