Testing temporal properties with Temporally Enhanced Security Logic Assertions (TESLA)
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.
Schedule
week |
plan |
status |
week 1, May 23 - May 29 |
writing tests for the tesla instrumenter, writing TESLA assertions, extending TESLA framework, writing weekly report |
|
week 2, May 30 - June 5 |
Fixing bugs, reading sources, VM research |
|
week 3, June 6 - June 12 |
Fixing bugs, writing basic examples , llvm/clang research, |
|
week 4, June 13 - June 19 |
writing TESLA assertions , extending TESLA framework, writing fuzzers, bug fixing |
|
week 5, June 20 - June 26 |
writing TESLA assertions , extending TESLA framework , writing test cases , writing fuzzers , testing , bug fixing |
|
week 6, June 27 - July 3 |
writing TESLA assertions , extending TESLA framework , writing test cases , writing fuzzers , testing , writing test reports draft , bug fixing |
|
week 7, July 4 - July 10 |
writing TESLA assertions , extending TESLA framework , writing test cases , writing fuzzers , testing , mid-term report |
|
week 8, July 11 - July 17 |
stress2 tests , writing TESLA assertions , extending TESLA framework , testing , bug fixing |
|
week 9, July 18 - July 24 |
stress2 tests , writing TESLA assertions , extending TESLA framework , testing , bug fixing |
|
week 10, July 25 - July 31 |
writing test reports , writing final report (article) |
|
week 11, August 1 - August 7 |
writing TESLA assertions , extending TESLA framework , test reports release , writing final report (article) |
|
week 12, August 7 - August 15 |
extending TESLA framework , doing clean-ups , testing test cases database , final report release (article) |
|
Milestones
- Syscall tests
- Network stacks tests
- MAC framework tests
- Capsiucm framework tests
- Final test report
- Final report
Respository
SVN repository is available at https://socsvn.freebsd.org/socsvn/soc2011/ you can get it by svn co https://socsvn.freebsd.org/socsvn/soc2011/shm/ or browse it at https://socsvn.freebsd.org/socsvn/soc2011/shm/
Public GIT Tesla repository is available at https://github.com/CTSRD-TESLA/
Tutorial
References
Contact
MateuszKocielski - student
RobertWatson - mentor