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:20150324T131500Z
DTEND:20150324T134500Z
UID:TALK58448@talks.cam.ac.uk
CONTACT:Heidi Howard
DESCRIPTION:Transport Layer Security (TLS) implementations have a history 
 of security flaws.  The immediate causes of these are often programming er
 rors\, e.g.~in memory management\, but the root causes are more fundamenta
 l: the challenges of interpreting the ambiguous prose specification\, the 
 complexities inherent in large APIs and code bases\, inherently unsafe pro
 gramming choices\, and the impossibility of directly testing conformance b
 etween implementations and the specification.\n\nWe present Not-quite-so-b
 roken TLS\, the result of our re-engineered approach to security protocol 
 specification and implementation that addresses these root causes.  The sa
 me code serves dual roles: it is both a specification of TLS\, executable 
 as a test oracle to check conformance of traces from arbitrary implementat
 ions\, and a usable implementation of TLS\; a modular and declarative prog
 ramming style provides clean separation between its components.  Many secu
 rity flaws are thus excluded by construction.\n\nNot-quite-so-broken TLS c
 an be used in standalone applications\, which we demonstrate with a messag
 ing client\, and can also be compiled into a Xen unikernel (a specialised 
 virtual machine image) with a TCB that is 4\\% of a standalone system runn
 ing a standard Linux/OpenSSL stack\, with all network traffic being handle
 d in a memory-safe language\; this supports applications including HTTPS\,
  IMAP\, Git\, and Websocket clients and servers.
LOCATION:Computer Laboratory\, William Gates Building\, Room FW11
END:VEVENT
END:VCALENDAR