|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
TESLA: Temporally-enhanced security logic assertions
If you have a question about this talk, please contact Laurent Simon.
Abstract: The security of complex software such as operating system kernels depends on properties that we (currently) cannot prove correct. We can validate some of these properties with assertions and testing, but temporal properties such as access control and locking protocols are beyond the reach of contemporary tools. TESLA is a compiler-based tool that helps programmers describe and understand the temporal behaviour of low-level systems code. Using temporal assertions (inspired by linear temporal logic), developers can specify security properties and validate them at run-time. We have used TESLA to validate OpenSSL API use, find security-related bugs in the FreeBSD kernel and to explore complex rendering bugs that were impervious to existing debugging tools.
Bio: Jonathan Anderson is a postdoctoral researcher in the security group here at the CL. He works on tools that support application and OS security as part of the CTSRD project. His PhD work (also at Cambridge) explored the intersection of privacy and operating systems concepts in the context of online social network.
This talk is part of the Computer Laboratory Security Seminar series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsCambridge Alumni Energy Society ME Seminar RSC Organic Division South Eastern Regional Meeting
Other talksRehabilitating and Maintaining Golden-Cheeked Gibbons (Nomascus gabriellae) and Pygmy Loris (Nycticebus pygmaeus) Confiscated from the Illegal Wildlife Trade in South Vietnam Greek-Turkish language contacts in the Ottoman Empire: ways of verbal integration Evolution of turbulence and buoyancy under strong rotation - the role of inertial waves in structure formation The characteristic polynomial of a random unitary matrix and Gaussian multiplicative chaos. MULTIMODAL VIDEO ANALYSIS: Is Play a form of learning? Research at TU Dortmund in Supply Net Order Management