Quick Guide to TESLA

This is a quick write-up on what is TESLA and how to use it in order to verify temporal properties of a running code. Guide is a part of a GSoC 2011 project - Testing temporal properties with Temporally Enhanced Security Logic Assertions (TESLA), more information on project is available at GSoC project page.

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.

TESLA assertions are subset of LTL logic, which is temporal logic expressive enough to check if something happend or will happen in the future. This makes LTL perfect to check properties of the code, imagine that you can check if code checked if user has access to the object before using it by writing simple assertion in LTL language. To get more real life example consider network stack state machine i.e. 802.11 state machine, by using LTL it's possible to ensure that all transitions between states are done upon a fixed protocol by using statements like following one:

if current_state == IEEE80211_S_ASSOC, then 
      previous_state == IEEE80211_S_AUTH and authentication was
      successful
    or
      previous_state == IEEE80211_S_RUN and DisAssoc frame is received

Fair description of the LTL logic could be found at wiki, it's strongly recommended to get familiar with it before going further, espiecially if you haven't heard about temporal logic before.

TESLA framework is contains following parts:

• llvm/clang - scans C code and instrument is
• CFA - automata compiler, TEAL automatas are used behind LTL expressions
• libtesla - responsible for handling TESLA events, multiplexing/demultiplexing them to TEAL automatas

TESLA relies on some 3rd party software (all required software is open-source and could be installed from the ports or package system), notable requirements are:

• environment able to build llvm/clang (CMake, Python, …)
• OCaml (ports/lang/ocaml) to build CFA compiler
• svn (recommended way to get sources)

It's recommended to get them installed before

In order to get all sources (llvm/clang, CFA, TESLA) run command:

> svn co https://socsvn.freebsd.org/socsvn/soc2011/shm/

You can also browse sources at https://socsvn.freebsd.org/socsvn/soc2011/shm/ .

Use build_clang.sh script, which is in the TESLA directory to build llvm/clang. Script will download all needed sources or eventually sync them with repository if any updates are available.

$ ./build_clang.sh

You could get now a cup of damn good coffe, building this software could take even few hours.

CFA sources are placed in cfa/ directory, building it is also as easy as:

> gmake
...
> ./splc --help
Usage: splc <options> input-file
  -O Optimisation level [0|1]
  -q Quiet mode
  -v Verbose mode
  -hdir HTML Template Directory [.]
  -d Debug mode [false]
  -t Output mode [tesla|ocaml|dot|promela]
  -s Filename for statecalls output (backend specific)
  -o Output file basename (without extension)
  -help  Display this list of options
  --help  Display this list of options

Directory contains also a few examples of TEAL automata, it's worth to at least review them.

dhcp.spl        tcp_connect.spl tcpc.spl

TEAL language:

• automaton
• either {} or
• multiple
• exit

Consider protocol where states could be described by schema:

       +------+
       |      |
       +---> P2---+   +---> P4 ---+
P1 ----+          +---+           +--> P6
       +---> P3---+   +---> P5 ---+
       |      |
       +------+

I.e. P1, P2, P2, P3, P4, P6 is a valid sequence of protocol states, P1, P2, P4, P2 is invalid sequence, because state P2 cannot be folloed by state P4. Goal is to use TESLA to ensure in dynamic environment that protocol is not violated.

First we nned to write an TEAL specification for the protocol, it's pretty easy to express protocol states:

automaton simple_protocol() {
  void main(struct test *t) {
    t->state = P1;
    multiple {
      either {
        t->state = P2;
      } or {
        t->state = P3;
      }
    }
    either {
      t->state = P4;
    } or {
      t->state = P5;
    }
    t->state = P6;
    exit;
  }
}

More complex example is available in CFA directory.

• http://wiki.freebsd.org/BuildingFreeBSDWithClang - builing world using llvm/clang
• GSoC 2011 TESLA - Testing temporal properties with Temporally Enhanced Security Logic Assertions (TESLA)