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

Benjamin Beurdouche 1 Karthikeyan Bhargavan 1 Antoine Delignat-Lavaud 1 Cédric Fournet 2 Markulf Kohlweiss 2 Alfredo Pironti 1 Pierre-Yves Strub 3 Jean Karim Zinzindohoue 1
1 PROSECCO - Programming securely with cryptography
Inria de Paris
2 Microsoft - Microsoft Research [Cambridge]
3 Institute IMDEA Software [Madrid]
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 ciphersuites. Our attacks expose the need for the formal verifica- tion of core components in cryptographic protocol libraries; our implementation demonstrates that such mechanized proofs are within reach, even for mainstream TLS implementations.
Type de document :
Communication dans un congrès
IEEE Symposium on Security & Privacy 2015, May 2015, San Jose, United States. IEEE, 2015
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01114250
Contributeur : Bruno Blanchet <>
Soumis le : lundi 4 avril 2016 - 18:23:12
Dernière modification le : jeudi 26 avril 2018 - 10:28:11
Document(s) archivé(s) le : lundi 14 novembre 2016 - 16:06:46

Fichier

messy-state-of-the-union-oakla...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01114250, version 1

Collections

INRIA | INRIA-ROCQ

Citation

Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, et al.. A Messy State of the Union: Taming the Composite State Machines of TLS. IEEE Symposium on Security & Privacy 2015, May 2015, San Jose, United States. IEEE, 2015. 〈hal-01114250〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

228

Téléchargements de fichiers

932

Contact


archive-ouverte@inria.fr