Not-quite-so-broken TLS 1.3 mechanised conformance checking

Add to your list(s) Download to your calendar using vCal

• Hannes Mehnert
• Wednesday 10 February 2016, 13:00-14:00
• FW11.

If you have a question about this talk, please contact Peter Sewell.

[While I expect participants at TRON to know TLS 1 .3, I’d preface the REMS talk with 5-10 minutes brief intro to TLS 1 .3, followed by the 25 minute TRON talk]

abstract: TLS 1 .3 is currently being standardised. We’ll start with a brief outline of the changes between TLS 1 .2 and 1.3, and their motivation. Afterwards we’ll describe our contribution, mechanised TLS 1 .3 conformance checking.

This is a practice talk for TRON (https://www.internetsociety.org/events/ndss-symposium-2016/tron-workshop-programme). This is joint work with David Kaloper.

We present a set of tools to aid TLS 1 .3 implementors, all derived from a single TLS implementation/model. These include an automated offline TLS protocol conformance checker, a test oracle validating recorded sessions, a tool replicating recorded sessions with other implementations, and an interactive online handshake visualisation.

The conformance checker repeatedly runs a user-provided TLS implementation, attempting to establish TLS sessions with it; the checker explores the TLS parameter space to determine feature coverage of the provided implementation. The test oracle takes a recorded session between two endpoints and decides whether the session was conformant with the specification. The replication utility re-runs one side of a recorded session against another TLS implementation, and observes its behaviour. The online visualisation accepts connections from clients and presents the TLS session as an interactive sequence diagram.

All of these tools are based on our clean-slate nqsb-TLS implementation/model. It already supports TLS 1 .0-1.2, and interoperates with a broad range of other TLS implementations. We are currently extending nqsb-TLS with TLS 1 .3 support, and tracking the progress of the TLS 1 .3 draft, adapting our implementation/model accordingly.

We invite the community to use our tools while implementing the TLS 1 .3 RFC , and provide feedback on deviations in the interpretation thereof. This process enables the community to converge to a single, mechanically checkable TLS 1 .3 model, as implemented by nqsb-TLS.

This talk is part of the REMS lunch series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW11
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.