shmsoc2011qgtt

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
shmsoc2011qgtt [2011/06/26 11:02] – MateuszKocielskishmsoc2011qgtt [2017/09/18 14:03] (current) – Use local wiki LinkNames (remove absolute wiki urls) KubilayKocak
Line 1: Line 1:
 ====== Quick Guide to TESLA ====== ====== 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 running code.+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 [[ShmSoc2011|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? ===== ===== 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 ===== ===== 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:
 +
 +<code>
 +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
 +</code>
 +
 +Fair description of the LTL logic could be found at [[http://en.wikipedia.org/wiki/Linear_temporal_logic|wiki]], it's recommended to get familiar with this material before going further, espiecially if you haven't heard about temporal logic before.
  
 ===== Building ===== ===== 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 ==== ==== Pre-requirements ====
  
-TESLA relies on some 3rd party software (which you can install from the ports or package system), notable requirements are:+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) +  * environment able to build llvm/clang (CMake, Python, ...) 
-  * OCaml +  * OCaml (ports/lang/ocaml) to build CFA compiler 
-  * svn (in order to get sources)+  * svn (best way to get sources) 
 + 
 +==== Getting sources ==== 
 + 
 +In order to get all sources (llvm/clang, CFA, TESLA) run command: 
 + 
 +<code> 
 +> svn co https://socsvn.freebsd.org/socsvn/soc2011/shm/ 
 +</code> 
 + 
 +You can also browse sources at https://socsvn.freebsd.org/socsvn/soc2011/shm/ .
  
 ==== clang/llvm ==== ==== 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.
 +
 +<code>
 +$ ./build_clang.sh
 +</code>
 +
 +You could get now a cup of [[http://en.wikipedia.org/wiki/Dale_Cooper|good coffe]], building this software could take few hours.
  
 ==== CFA - TEAL compiler ==== ==== CFA - TEAL compiler ====
 +
 +CFA sources are placed in cfa/ directory, building it is easy as:
 +
 +<code>
 +> 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
 +</code>
 +
 +%%=%%== libtesla ==
 +
 +libtesla sources are located in the TESLA/libtesla/ directory. library can be built using makefile.
  
 ===== Using TESLA ===== ===== Using TESLA =====
-==== Tesla assertions ====+
 ==== TEAL ==== ==== TEAL ====
  
-===== Example =====+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:
  
-===== Using TESLA with FreeBSD kernel =====+<code> 
 +automaton example() 
 +{ 
 +  void main(struct test *x) 
 +  { 
 +    x->y = z; 
 +    abc(); 
 +  } 
 +} 
 +</code> 
 + 
 +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. 
 + 
 +<code> 
 +dhcp.spl tcp_connect.spl tcpc.spl 
 +</code> 
 + 
 +==== 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: 
 + 
 +<code> 
 +       +------+ 
 +       |      | 
 +       +---> P2---+   +---> P4 ---+ 
 +P1 ----+          +---+           +--> P6 
 +       +---> P3---+   +---> P5 ---+ 
 +       |      | 
 +       +------+ 
 +</code> 
 + 
 +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: 
 + 
 +<code> 
 +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; 
 +  } 
 +} 
 +</code> 
 + 
 +If you're looking for more complex example, then few are available in the [[https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/assertions/tcp/tcpc-alt.spl|CFA directory]]. 
 +From TEAL, we need to generate validation automata: 
 + 
 +<code> 
 +> 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 
 +</code> 
 + 
 +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: 
 + 
 +<code> 
 +*.c + *.spec --[clang, instrumentation]--> instrumented code --+--> code guarded by TESLA 
 +                          *.spl --[cfa]--> automata          --/ 
 +</code> 
 + 
 +For now, automata has been generated. To instrument code, following spec file is used: 
 + 
 +<code> 
 +field_assign,struct test,state 
 +</code> 
 + 
 +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: 
 + 
 +<code> 
 +> 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; 
 + 
 +... 
 +</code> 
 + 
 +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: 
 + 
 +<code> 
 +t->state = atoi(x[i]); 
 +</code> 
 + 
 +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: 
 + 
 +<code> 
 +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); 
 +} 
 +</code> 
 + 
 +tesla_* functions are well documented in [[https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/libtesla/|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: 
 + 
 +<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 
 +</code> 
 + 
 +As mentioned before P1,P2,P2,P3,P4,P6 is valid sequence: 
 + 
 +<code> 
 +$ ./example2 1 2 2 3 4 6 
 +-> 1 
 +-> 2 
 +-> 2 
 +-> 3 
 +-> 4 
 +-> 6 
 +Processed 6 states 
 +</code> 
 + 
 +While P1,P2,P4,P2 is invalid and should be recognized by state machine as a protocol violation: 
 + 
 +<code> 
 +$ ./example2 1 2 4 2 
 +-> 1 
 +-> 2 
 +-> 4 
 +-> 2 
 +example2: tesla_assert failed: TEAL automata example: this is just a simple example 
 +</code> 
 + 
 +Source code for this example is located at https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/examples/example2/
  
 ===== Further reading ===== ===== Further reading =====
 +
 +  * https://socsvn.freebsd.org/socsvn/soc2011/shm/ - SVN repository, header files of libtesla are well commented: https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/tesla/
 +  * [[BuildingFreeBSDWithClang|Building FreeBSD (world) using llvm/clang toolkit]]
 +  * [[ShmSoc2011|GSoC 2011 TESLA]] - Testing temporal properties with Temporally Enhanced Security Logic Assertions (TESLA)
 +  * http://www.tcs.hut.fi/Studies/T-79.231/2003/slides5.pdf - Notes on Temporal logic
  
  • shmsoc2011qgtt.1309086120.txt.gz
  • Last modified: 2011/06/26 11:02
  • by MateuszKocielski