Access Restriction

Author Kohlweiss, Markulf ♦ Strub, Pierre-Yves ♦ Beurdouche, Benjamin ♦ Delignat-Lavaud, Antoine ♦ Fournet, Cédric ♦ Bhargavan, Karthikeyan ♦ Pironti, Alfredo ♦ Zinzindohoue, Jean Karim
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
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.
Description Affiliation: INRIA (Beurdouche, Benjamin; Bhargavan, Karthikeyan) || INRIA & Ecole des Ponts, ParisTech (Zinzindohoue, Jean Karim) || Microsoft Research (Delignat-Lavaud, Antoine; Fournet, Cédric; Kohlweiss, Markulf) || IMDEA Software Institute (Strub, Pierre-Yves) || IOActive (Pironti, Alfredo)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 60
Issue Number 2
Page Count 9
Starting Page 99
Ending Page 107

Open content in new tab

   Open content in new tab
Source: ACM Digital Library