BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Not-quite-so-broken TLS: lessons in re-engineering a security prot
 ocol specification and implementation - David Kaloper Mersinjak
DTSTART:20150311T130000Z
DTEND:20150311T140000Z
UID:TALK53619@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:\nTransport Layer Security (TLS) implementations have a histor
 y of security flaws.  The immediate causes of these are often programming 
 errors\, e.g.~in memory management\, but the root causes are more fundamen
 tal: the challenges of interpreting the ambiguous prose specification\, th
 e complexities inherent in large APIs and code bases\, inherently unsafe p
 rogramming choices\, and the impossibility of directly testing conformance
  between implementations and the specification.\n\nWe present Not-quite-so
 -broken TLS\, the result of our re-engineered approach to security protoco
 l specification and implementation that addresses these root causes.  The 
 same code serves dual roles: it is both a specification of TLS\, executabl
 e as a test oracle to check conformance of traces from arbitrary implement
 ations\, and a usable implementation of TLS\; a modular and declarative pr
 ogramming style provides clean separation between its components.  Many se
 curity flaws are thus excluded by construction.\n\nNot-quite-so-broken TLS
  can be used in standalone applications\, which we demonstrate with a mess
 aging client\, and can also be compiled into a Xen unikernel (a specialise
 d virtual machine image) with a TCB that is 4\\% of a standalone system ru
 nning a standard Linux/OpenSSL stack\, with all network traffic being hand
 led in a memory-safe language\; this supports applications including HTTPS
 \, IMAP\, Git\, and Websocket clients and servers.
LOCATION:FW26
END:VEVENT
END:VCALENDAR