Cryptographically verified implementation of TLS 1.2

Duration: 1 hour 3 mins 48 secs

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/1247182/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	Fournet, C (Microsoft Research) Friday 13 April 2012, 13:30-14:30


Created:	2012-04-23 17:25
Collection:	Semantics and Syntax: A Legacy of Alan Turing
Publisher:	Isaac Newton Institute
Copyright:	Fournet, C
Language:	eng (English)


Abstract:	Joint work with Karthik Bhargavan, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. We develop a reference implementation of the TLS 1.2 Internet Standard. Our code fully supports binary wire formats, multiple ciphersuites, sessions and connections with re-handshakes and resumptions, alerts, message fragmentation, ... as prescribed by the standard; it interoperates with other implementations, notably existing web browsers and servers. At the same time, our code is carefully structured to enable its automated, modular verification, from its main API down to computational security assumptions on its underlying cryptographic algorithms. In the talk, I will review our modular cryptographic verification method, which is based on F7, a refinement type checker coupled with an SMT-solver, with a theory formalized in Coq. Using F7, we verify constructions and protocols coded in F# by typing them against new cryptographic interfaces that capture their authenticity and secrecy properties. We relate their ideal functionalities and concrete implementations, using game-based program transformations behind typed interfaces, so that we can easily compose them. I will also outline our TLS implementations, coded in F# and specified in F7. I will present its main typed interfaces, which can be read as specifications of "giant" ideal functionalities for its main components, such as authenticated encryption for the record layer and key establishment for the handshake. I will finally describe our main security results, as well as some new attacks we found in the process.

Abstract:

Joint work with Karthik Bhargavan, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub.

We develop a reference implementation of the TLS 1.2 Internet Standard. Our code fully supports binary wire formats, multiple ciphersuites, sessions and connections with re-handshakes and resumptions, alerts, message fragmentation, ... as prescribed by the standard; it interoperates with other implementations, notably existing web browsers and servers. At the same time, our code is carefully structured to enable its automated, modular verification, from its main API down to computational security assumptions on its underlying cryptographic algorithms.

In the talk, I will review our modular cryptographic verification method, which is based on F7, a refinement type checker coupled with an SMT-solver, with a theory formalized in Coq. Using F7, we verify constructions and protocols coded in F# by typing them against new cryptographic interfaces that capture their authenticity and secrecy properties. We relate their ideal functionalities and concrete implementations, using game-based program transformations behind typed interfaces, so that we can easily compose them.

I will also outline our TLS implementations, coded in F# and specified in F7. I will present its main typed interfaces, which can be read as specifications of "giant" ideal functionalities for its main components, such as authenticated encryption for the record layer and key establishment for the handshake. I will finally describe our main security results, as well as some new attacks we found in the process.

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video	640x360	1.84 Mbits/sec	885.21 MB	View	Download
WebM	640x360	976.31 kbits/sec	450.50 MB	View	Download
Flash Video	484x272	568.58 kbits/sec	265.69 MB	View	Download
iPod Video	480x270	506.16 kbits/sec	236.52 MB	View	Download
MP3	44100 Hz	125.03 kbits/sec	58.29 MB	Listen	Download
Auto *	(Allows browser to choose a format it supports)