A messy state of the union: taming the composite state machines of TLS - Archive ouverte HAL Access content directly
Journal Articles Communications of the ACM Year : 2017

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

(1) , (1) , (1) , (2) , (2) , (3) , (4) , (1)
1
2
3
4

Abstract

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 challenge for TLS implementations is to define a composite state machine that correctly handles these combinations. If the state machine is too restrictive, the implementation may fail to interoperate with others; if it is too liberal, it may allow unexpected message sequences that break the security of the protocol. We systematically test popular TLS implementations and find unexpected transitions in many of their state machines that have stayed hidden for years. We show how some of these flaws lead to critical security vulnerabilities, such as FREAK. While testing can help find such bugs, formal verification can prevent them entirely. To this end, we implement and formally verify a new composite state machine for OpenSSL, a popular TLS library.
Not file

Dates and versions

hal-01673714 , version 1 (31-12-2017)

Identifiers

Cite

Karthikeyan Bhargavan, Benjamin Beurdouche, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, et al.. A messy state of the union: taming the composite state machines of TLS. Communications of the ACM, 2017, 60 (2), pp.99 - 107. ⟨10.1145/3023357⟩. ⟨hal-01673714⟩

Collections

INRIA INRIA2
161 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More