TESLA
Demos
demos/smoketest
The 'demos/smoketest' directory contains an example of how TESLA assertions can be written in C code. If you run it as-is:
$ cd demos/smoketest
$ ./run.demo # without TESLA
TESLA demo application; version 7329b3b
Calling the 'example_syscall' function...
'example_syscall' returned 0
$ ./run.demo -D TESLA # with TESLA
TESLA demo application; version 7329b3b
Calling the 'example_syscall' function...
[CALE] example_syscall 0x7fff4fcaf5b8 0 0
[CALE] hold 0x10ff58300
[FSET] struct.object.refcount 0x10ff58300 1 0x10ff58300
[RETE] hold 0x10ff58300
[RETE] get_object 0 0x7fff4fcaf548 0
[RETR] DES_set_key 0x7fff4fcaf568 0x7fff4fcaf4c0 0
[CALE] security_check 0x7fff4fcaf5b8 0x10ff58300 0
[RETE] security_check 0x7fff4fcaf5b8 0x10ff58300 0 0
[RETE] some_helper 0 0
[CALE] void_helper 0x10ff58300
[NOW] automaton 4 267748096 0
[NOW] automaton 5
[NOW] automaton 6 267748096
[NOW] automaton 7 267748096
[NOW] automaton 8 267748096
[NOW] automaton 9 267748096
[NOW] automaton 10 267748096 0
[NOW] automaton 11 267748096 0
[NOW] automaton 3 1338701160 1338700992
[RETE] log_audit_record 0x10ff58300 0 0
[CALE] release 0x10ff58300
[FSET] struct.object.refcount 0x10ff58300 0 0x10ff58300
[RETE] release 0x10ff58300
[RETE] example_syscall 0x7fff4fcaf5b8 0 0 0
This just shows that the 'demo' application runs normally. If, however, you comment out line 96 of example.c (which calls the security_check() function):
--- a/demos/smoketest/example.c
+++ b/demos/smoketest/example.c
@@ -93,7 +93,7 @@ example_syscall(struct credential *cred, int index, int op)
crypto_setup(&des_key, &key_schedule);
- if ((error = security_check(cred, o, op))) return error;
+// if ((error = security_check(cred, o, op))) return error;
some_helper(op);
void_helper(o);
perform_operation(op, o);
... you should see an error when you run the 'demo' application:
$ ./run.demo -D TESLA
TESLA demo application; version 7329b3b (dirty)
Calling the 'example_syscall' function...
[...]
[NOW] automaton 4 117814016 0
TESLA failure:
In automaton 'example.c:45#0':
automaton 4 {
state 0 (X,X): --(example_syscall(X,X,X): Entry <<init>>)-->(1)
state 1 (X,X): --(security_check(X,o,op) == 0: o op)-->(2) --(example_syscall(X,X,X) == X)-->(3)
state 2 (o,op): --(security_check(X,o,op) == 0: op)-->(2) --(example_syscall(X,X,X) == X)-->(3) --(NOW)-->(4)
state 3 (o,op):
state 4 (o,op): --(example_syscall(X,X,X) == X <<cleanup>>)-->(3)
}
smoketest: No instance matched key '0x3 [ 10705b300 0 X X ]' for transition(s) [ (2:0x3 -> 4:0x3) ]
This shows that, when we reach the assertion site for automaton 4, we detect that a transition (the security_check event) was missed.