Date: Thu, 14 Jul 2011 11:26:00 +0200 From: Mateusz Kocielski <shm@freebsd.org> To: soc-status@freebsd.org Subject: Testing temporal properties with Temporally Enhanced Security Logic Assertions - week 7/mid-term Message-ID: <CAJTcWchYcXtT056Eesx0Ay4ZrW=9DSx1C5bw6c1=Av76=cN_3A@mail.gmail.com>
next in thread | raw e-mail | index | archive | help
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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?CAJTcWchYcXtT056Eesx0Ay4ZrW=9DSx1C5bw6c1=Av76=cN_3A>