Testing temporal properties with Temporally Enhanced Security Logic Assertions - week 7/mid-term

[Mateusz Kocielski]

Hello!

1. What is this all about?

  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.

  Project homepage could be found at [1]. Page includes quick guide to TESLA,
which is a write-up on using existing bits. Repository is available at [2]
https://socsvn.freebsd.org/socsvn/soc2011/shm/ - here are mostly things that
works or are interesting enough to be there, except that there exists small
garbage [3] with random bits which I've written  so far (do not dive there,
unless you really know what you're doing).


2. What was done

 * tesla instrumenter test cases - this a simple script (previously it was
   based on the ATF testing framework, but I've decided to rewrite it since
   we check if two ASTs equal. Moreover ATF is not present in FreeBSD base
   system) which performs unit tests on tesla instrumenter. My work was
   mainly in that part focused on writing tests, deciding if instrumenter
   behaves as expected, then eventually I was fixing bugs. Now it's used in
   the project as a regression suite.

 * fixing bugs - I've spent lots of time on looking for bugs and fixing them.
   Some instrumenter bugs (like double rhs evaluation or problem with
   CompndStmts) took me few days (in extreme case almost a week ;)). This part
   was quite challenging since I'm not very familiar with llvm/clang internals,
   so introduction costed me another few days. Instrumenter is modyfing AST
   in place which is clearly not dedicated for doing such things. Lack of
   defensive checks implies that in case of any mistake it takes lot of
   resources to figure out what's wrong.

 * examples, worth seeing are at least two of them: ping - which checks if ping
   mainloop behaves as expected (this example is based on function events and
   checks if functions are invoked in right order) and example2 which validates
   if session is not violating the protocol (which is described in write-up).
   More examples could be found at assertions/ and [3].

 * small write-up on TESLA, this is a small article on starting using
TESLA. It covers
   background behind tesla, installation process, small introduction to TEAL and
   instrumenter, some examples.

 * I've started writing fuzzers skeletons, I want to complete syscall fuzzer
   (better than simple algorithms used in stress2 suite [4]) and network
   fuzzers (802.11, etc...) to more efficent testing (keep in mind that
   tesla is working on running code)

3. What's missing (what I've started and not finished)

 * I've broken MAC tests last week (I'm still trying to figure out what's
   wrong), hopefully I'll release this bits next week. Adding TESLA to
   kernel is pretty straight-forward task, if you're interested how to do
   that then drop me an e-mail I'll write few words about that in quick
   guide to TESLA. My intention was to clone (less or more) mac_test
   functionality (but for now I get constant panics).

 * I've been working on more granular scheme for GLOBAL_STATE, for now
   it uses global lock for all instances, which obviously is not perfect
   solution. My implementation is based on previous ideas on that which
   involves hashing tables (for now it uses simple modulo sum of all keys).
   Limit passed to libtesla is also rounded to nearest prime by brute-force
   algorithm, I haven't decided yet how to speed it up, but probably some
   candidate ideas involves probability tests (i.e. Miller-Rabin method
   involving fixed witnesses, which seems to be good enough for
   kernel-space).

4. Future plans

 * Finish missing bits - locking scheme/mac tests
 * Handling assignments in sub-expressions by instrumenter.
 * Doing some clean-ups in instrumenter (i.e. resolve Stmts to
   CompoundStmts in more elegant way)
 * 802.11 tests (fuzzing + assertions)
 * syscall tests (fuzzing + assertions)
 * libtesla clean-ups (locking scheme etc.)

 In the second period I'd like to focus more on testing the FreeBSD project,
 if you've got any ideas what's worth testing (additionally) then feel free to
 drop me an e-mail.

5. post GSoC era

 * It's not known if Capsicum bits will be included in FreeBSD during the
   GSoC coding phrase, if not then it'll be tested after GSoC.
 * CFA compiler is written in OCaml, FreeBSD hasn't got any OCaml interpreter
   in base which is an integration stopper. This task doesn't fit well into
   coding phrase (TEAL and CFA is still under developement, OCaml is much easier
   to modify or write quick prototype than C), but could be considered as a good
   goal after GSoC.
 * Usually network clients/daemons have got some procotol state behind
connection,
   TESLA is a perfect tool to find protocol violations, FreeBSD base system
   includes few clients which could be considered as a good condidate to verify
   them.

 As usually, in case of any questions please catch me on IRC (I'm shm
at freenode). :)

References:

 [1] http://wiki.freebsd.org/action/login/ShmSoc2011
 [2] https://socsvn.freebsd.org/socsvn/soc2011/shm/
 [3] https://shm.hard-core.pl/soc-garbage/
 [4] http://people.freebsd.org/~pho/stress/index.html

Regards,
Mateusz