Testing temporal properties with Temporally Enhanced Security Logic Assertions - week 1

[Mateusz Kocielski]

Hello,

  My project is Testing temporal properties with Temporally Enhanced
Security Logic Assertions (TESLA). Its wikipage is available at [1].
You can find there more information on project as well as schedule and
links to repository.

  What was done this week:

  - writing test cases for the TeslaInsrumenter
  - setting up testing environment (on kvm)
  - writing basic examples of using TESLA (userland)

  My plans for the next week:

  - move testing environment to virtualbox
  - polish up test suite for the TeslaInstrumenter (discuss it with TI
    developers)
  - write some basic tesla assertions for the kernel and test it
  - read MAC framework code
  - write schedule for MAC framework testing
  - (hopefully) start MAC testing (e.g. replace mac_test module with
    tesla automata)

  Please contact me in case of any questions. Usually best way of
communication with me is IRC, I'm shm at freenode.

  [1] - http://wiki.freebsd.org/ShmSoc2011

Regards,
Mateusz Kocielski