BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:TESLA: Temporally-enhanced security logic assertions - Jonathan An
 derson\, University of Cambridge
DTSTART:20131126T161500Z
DTEND:20131126T171500Z
UID:TALK48812@talks.cam.ac.uk
CONTACT:Laurent Simon
DESCRIPTION:*Abstract:*\nThe security of complex software such as operatin
 g system kernels\ndepends on properties that we (currently) cannot prove c
 orrect. We can\nvalidate some of these properties with assertions and test
 ing\, but\ntemporal properties such as access control and locking protocol
 s are\nbeyond the reach of contemporary tools. TESLA is a compiler-based t
 ool\nthat helps programmers describe and understand the temporal behaviour
 \nof low-level systems code. Using temporal assertions (inspired by\nlinea
 r temporal logic)\, developers can specify security properties and\nvalida
 te them at run-time. We have used TESLA to validate OpenSSL API\nuse\, fin
 d security-related bugs in the FreeBSD kernel and to explore\ncomplex rend
 ering bugs that were impervious to existing debugging\ntools.\n\n*Bio:*\nJ
 onathan Anderson is a postdoctoral researcher in the security group\nhere 
 at the CL. He works on tools that support application and OS\nsecurity as 
 part of the CTSRD project. His PhD work (also at\nCambridge) explored the 
 intersection of privacy and operating systems\nconcepts in the context of 
 online social network.\n\n
LOCATION:Lecture Theatre 2\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR