Testing temporal properties with Temporally Enhanced Security Logic Assertions (TESLA)

This is an old revision of the document!

Abstract

TESLA is a framework for testing temporal properties of a software written in the C language. Standard assertions i.e. assert(3) are able to test simple expressions which refer only to an actual state of a program, testing temporal properties in this case (e.g. conformance with the protocols, condition checks before usage etc.) is complex, requires additional code and data structures, thus it could be a source of unnecessary complexity and bugs. TESLA introduces assertions which test temporal expressions, it means that it's able to refer to the future and to the past, which is a great help when a goal is to verify some property which refers to the time, i.e. check if access control checks were done.

FreeBSD can benefit from TESLA assertions in many ways, kernel is complex piece of code which contains a lot of places where some temporal conditions MUST be satisfied in order to provide security or consistency. Project goal is to use TESLA assertions to test sensitive parts of the FreeBSD code like MAC framework, Capsicum, network stacks (802.11 stack etc.), to make sure that they meet desired temporal properties.

This project seems to be reasonable step in order to make FreeBSD more robust and secure platform. As a result of the project we expect to deliver code with TESLA assertions, set of the test cases, fuzzers (probably integrated with the stress2 framework), testing report and patches for the fixed bugs. TESLA is still under development, thus part of the project will be helping to make it ready for inclusion into the FreeBSD, some parts of the project are not ready to be in the base systems (e.g. they're not written in C), some parts might be extended to fit better into the FreeBSD world.

TBD