BSDCan2019 - 1.8

BSDCan 2019
The Technical BSD Conference

Theo Buehler
Day Talks #2 - 18 May - 2019-05-18
Room DMS 1160
Start time 13:30
Duration 01:00
ID 1088
Event type Lecture
Track Hacking
Language used for presentation English

Design and verification of the TLS 1.3 handshake state machine in LibreSSL

The TLS 1.3 handshake is the protocol used for negotiating a TLS 1.3 connection between a client and a server. During the handshake the configuration for the session is agreed upon, ephemeral secrets are exchanged and the server is authenticated. This protocol is encoded in a state machine.

After a general discussion of TLS and in particular a comparison of TLS 1.2 and TLS 1.3, this talk will review the TLS 1.3 handshake state machine and discuss its implementation in LibreSSL. Benefits and drawbacks of both the handshake protocol and LibreSSL's implementation will be discussed. We will also elaborate on the way we verify and guarantee our implementation's correctness using regression testing and other methods.