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 the GSoC 2011 project - Testing temporal properties with Temporally Enhanced Security Logic Assertions (TESLA). More information on the project is available at GSoC project page. Before you start, please beware that TESLA is under developement, some parts could be broken, some parts could be undocumented, finally something could not working yet as expected, all bugs reports are more than welcome!

What is the TESLA?

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.

Temporal Logic

TESLA assertions are subset of the 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 validate 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 recommended to get familiar with this material before going further, espiecially if you haven't heard about temporal logic before.

Building

TESLA framework 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

Pre-requirements

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 (best way to get sources)

Getting sources

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/ .

clang/llvm

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 good coffe, building this software could take few hours.

CFA - TEAL compiler

CFA sources are placed in cfa/ directory, building it is 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

=== libtesla ==

libtesla sources are located in the TESLA/libtesla/ directory. library can be built using makefile.

Using TESLA

TEAL

TEAL language is used to describe sequences of events which are used to verify assertions in the code. It's syntax is strongly based on C language. TEAL starts events from main function:

automaton example()
{
  void main(struct test *x)
  {
    x->y = z;
    abc();
  }
}

Automata above describes event of assigning z to field y of x structure followed by abc invocation. Other functions could be declared inside automaton block and could be called from main as well as other functions. Following keywords could be used to build valid sequences of events:
either { X } or { Y } - X or Y sequences are valid
multiple { X } - multiple sequence X is valid
optional { X } - sequence X is optional

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

dhcp.spl tcp_connect.spl tcpc.spl

Instrumenter

Tesla instrumenter is a clang/llvm plugin used to analyze C code, it looks for tesla assertions and generate teal code, then instrument code basing on *.spec file which includes two types of declarations:

function,function_name - means that instrumetner should handle function call/return
field_assign,struct type,field - means that instrumenter should handle assignments to field of struct type.

Script kernel/tesla-clang can be used to invoke plugin.

Simple example

Consider protocol where states could be described by following 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.

TEAL automata

First we need 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;
  }
}

If you're looking for more complex example, then few are available in the CFA directory. From TEAL, we need to generate validation automata:

> splc -t tesla -s example2 example2.spl
Input files: example2.spl
Processing example2.spl
Compiling function main (public) ... 
  19 states
Optimising CFA... 
  12 states eliminated
Input files: example2.spl
Output files: example2

CFA compiler creates two files:
example2_automata.c - contains automata generated from TEAL specification, this automata is feed by libtesla.
example2_defs.h - contains definitions of automata events and prototypes of state machine init/destroy functions.

Connecting automata with the code

To get code guarded by TESLA it's needed to apply following steps:

   *.c + *.spec --[clang, instrumentation]--> instrumented code --+--> code guarded by TESLA
                             *.spl --[cfa]--> automata          --/

For now, automata has been generated. To instrument code, following spec file is used:

field_assign,struct test,state

This declaration means, that compiler will instrument places where some expression is assigned to field state of struct test type. Let's check if TESLA instrumenter meets our expectations:

> kernel/tesla-clang-print-ast example2.c instrumentation.spec
...
        int __tesla_tmp_assign;
        __tesla_tmp_assign = atoi(x[i]);
        __tesla_event_field_assign_struct_test_state(t, __tesla_tmp_assign);
        t->state = __tesla_tmp_assign;

...

https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/examples/example2/example2.c is used as an example. We can see that code above replaced code:

        t->state = atoi(x[i]);

tesla_event_field_assign_struct_test_state is a function which connects instrumented code with the state machine (in the future needed glue will be generated automatically). Most cases of your potential usage will be copy & pasted from https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/examples/example2/example2_assert.c . For our purposes simple handler looks as follows:

void
__tesla_event_field_assign_struct_test_state(struct test *t, u_int state)
{
    struct tesla_instance *tip;
    int alloc;
    int event;
    printf("-> %d\n", state);
    assert(tesla_instance_get1(example_state, (register_t)t, &tip, &alloc) ==
      0);

    if (alloc == 1)
        example2_automata_init(tip);

    switch(state)
    {
      case P1:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P1;
        break;
      case P2:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P2;
        break;
      case P3:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P3;
        break;
      case P4:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P4;
        break;
      case P5:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P5;
        break;
      case P6:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P6;
        break;
      default:
        printf("UNKNOWN STATE\n");
        tesla_assert_fail(example_state, tip);
    }

    if(example2_automata_prod(tip, event))
        tesla_assert_fail(example_state, tip);

    tesla_instance_put(example_state, tip);
}

tesla_* functions are well documented in libtesla], please take a look there to get more background on procedure above. Usually you'll need to define own mapping between field values and state machine events. The last thing we need to test our example is state machine initalization it can be achieved by invoking example2_init function in the code. We've got all needed pieces to test our code:

$ gmake
../../kernel/tesla-clang -c -Wall -g -I../.. -I. -O0 -o example2_automata.o example2_automata.c
../../kernel/tesla-clang -c -Wall -g -I../.. -I. -O0 -o example2_assert.o example2_assert.c
../../kernel/tesla-clang -Wall -g -I../.. -I. -O0   -c -o example2.o example2.c
example2.c:31:9: warning: Adding TESLA instrumentation
        t->state = atoi(x[i]);
        ^~~~~~~~~~~~~~~~~~~~~
1 warning generated.
../../kernel/tesla-clang -o example2 example2_automata.o example2_assert.o example2.o ../../libtesla/tesla_state.o ../../libtesla/tesla_state_global.o ../../libtesla/tesla_state_perthread.o ../../libtesla/tesla_util.o

As mentioned before P1,P2,P2,P3,P4,P6 is valid sequence:

$ ./example2 1 2 2 3 4 6
-> 1
-> 2
-> 2
-> 3
-> 4
-> 6
Processed 6 states

While P1,P2,P4,P2 is invalid and should be recognized by state machine as a protocol violation:

$ ./example2 1 2 4 2
-> 1
-> 2
-> 4
-> 2
example2: tesla_assert failed: TEAL automata example: this is just a simple example

Source code for this example is located at https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/examples/example2/