TESLA

Temporally Enhanced Security Logic Assertions (TESLA)

TESLA builds on our experiences developing the TrustedBSD MAC Framework and Capsicum: our most critical security properties are frequently safety (temporal) properties rather than static invariants. Current tools for testing temporal properties are largely static, and unable to work effectively on extremely large C-language software bases, such as multi-million lines-of-code operating system kernels and web browsers. TESLA borrows ideas from model checking, applying them in a dynamic context using compiler-assisted instrumentation to continuously validate temporal security assertions during software execution. We have implemented a prototype of TESLA based on clang/LLVM AST transforms, which is able to test both explicit automata against C implementations (such as protocol state machines in the kernel and OpenSSL) and inline assertions checking for missing access control checks in OS logic.

Further work on TESLA will take place in the context of the CADETS, a successor DARPA-sponsored project investigating program analysis and transformation in support of distributed security tracing.

Papers and slides

• Jonathan Anderson, Robert N. M. Watson, David Chisnall, Khilan Gudka, Brooks Davis, and Ilias Marinos. TESLA: Temporally Enhanced System Logic Assertions, Proceedings of The 2014 European Conference on Computer Systems (EuroSys 2014), April 14–16 2014, Amsterdam, The Netherlands.