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 challenge for TLS implementations is to define...
| Published in: | Communications of the ACM Vol. 60; no. 2; pp. 99 - 108 |
|---|---|
| Main Authors: | , , , , , , , |
| Format: | Article |
| Published: |
Association for Computing Machinery
Feb2017
|
| Subjects: | |
| Online Access: | View this record in EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=121046536&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 121046536 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Feb2017 vid: 60 iid: 2 pid: 68 pub: Association for Computing Machinery artinfo: ui: 121046536 10.1145/3023357 ppf: 99 ppct: 9 formats: tig: atl: A Messy State of the Union: Taming the Composite State Machines of TLS. aug: au: Beurdouche, Benjamin Bhargavan, Karthikeyan Delignat-Lavaud, Antoine Fournet, Cédric Kohlweiss, Markulf Pironti, Alfredo Strub, Pierre-Yves Zinzindohoue, Jean Karim affil: INRIA. Microsoft Research. IOActive. IMDEA Software Institute. INRIA & Ecole des Ponts, ParisTech. su: Computer network protocols Finite state machines Client/server computing Computer security OpenSSL (Computer software) sug: subj: Computer network protocols Finite state machines Client/server computing Computer security OpenSSL (Computer software) ab: 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. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2017 holdings: @attributes: islocal: N |
|---|