Talk by Anil Madhavapeddy, University of Cambridge (hosted by Andy Warfield)

Title: TESLA: Temporally Enhanced System Level Assertions

Abstract:

Experienced programmers of complex software systems document and test invariants through extensive use of software assertions. Unfortunately, C language assertions are only able to test invariants that can be evaluated at the instant assert is invoked. Checking more complex temporal properties requires programmers to manually instrument code and data structures. This makes checking safety properties (e.g., correct memory allocation protocols, check-before-use, conformance to the TCP state machine, and wall clock timeliness goals) verbose, time-consuming, and error-prone. TESLA significantly improves on existing approaches by enhancing the C language and runtime to support temporal assertions. These are able to reference past and future events, and also to attach automata to data structures (such as the kernel TCP state machine). I will describe our prototype implementation that uses an LLVM/clang plugin to automatically insert runtime instrumentation, and how the runtime works in both an OS kernel (FreeBSD) and userspace applications (e.g. OpenSSH, Tor).

Bio:

Dr Anil Madhavapeddy is a Senior Research Fellow at Wolfson College Cambridge based in the Systems Research Group. Dr. Madhavapeddy was on the original team at Cambridge that developed the Xen hypervisor, and subsequently served as the senior architect and product director for XenSource/Citrix before returning to academia. Prior to obtaining his PhD in 2006 from the University of Cambridge, he had a diverse background in industry at Network Appliance, NASA, and Internet Vision. In addition to professional and academic activities, Dr. Madhavapeddy is an active member of the open source development community with the OpenBSD operating system, a member of the steering committee for Commercial Uses of Functional Programming, and on the boards of startup companies such as Ashima Arts.