Temporally Enhanced Security Logic Assertions (TESLA)
TESLA builds on our experiences developing the TrustedBSD MAC Framework
and Capsicum: our most critical security properties are frequently safety
(temporal) properties rather than static invariants.
Current tools for testing temporal properties are largely static, and unable
to work effectively on extremely large C-language software bases, such as
multi-million lines-of-code operating system kernels and web browsers.
TESLA borrows ideas from model checking, applying them in a dynamic context
using compiler-assisted instrumentation to continuously validate temporal
security assertions during software execution.
We have implemented a prototype of TESLA based on clang/LLVM AST transforms,
which is able to test both explicit automata against C implementations (such
as protocol state machines in the kernel and OpenSSL) and inline assertions
checking for missing access control checks in OS logic.
Building TESLA
For the moment, TESLA requires a bit of effort to build: it has a very
heavyweight dependency (recent LLVM/Clang). The steps required to build are:
- acquire prerequisites
- build (a very recent version of) LLVM
- build TESLA
- exercise TESLA
Prerequisites
Here is a table of dependencies and the names of their ports/packages on various platforms:
Build a recent LLVM/Clang
You need to download and build a very recent version of LLVM/Clang from source
unless you're using FreeBSD, which has a very recent version available from
ports (see prerequisites, above).
$ cd somewhere/to/stash/1GB/of/LLVM
$ svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm
[...]
U llvm
Checked out revision 175226.
$ cd llvm/tools
$ svn co http://llvm.org/svn/llvm-project/cfe/trunk clang
[...]
A clang/LICENSE.TXT
U clang
Checked out revision 175226.
$ cd ../..
$ mkdir build
$ cd build
$ cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ../llvm
-- The C compiler identification is [...]
-- Check for working C compiler using: Ninja
-- Check for working C compiler using: Ninja -- works
[...]
-- Generating done
-- Build files have been written to: /home/jonathan/LLVM/build
$ cmake -D CMAKE_BUILD_TYPE=Release . # if you feel adventurous
$ ninja
[1932/1932] Linking CXX executable bin/c-index-test
Build TESLA
Once you have LLVM, make sure that it's at the front of your PATH:
$ export PATH=/path/to/LLVM/build/bin:$PATH
$ llvm-config --libdir # test that llvm-config works
Next, we download and configure TESLA:
$ git clone https://github.com/CTSRD-TESLA/TESLA.git tesla
Cloning into 'TESLA'...
remote: Counting objects: 3138, done.
[...]
$ cd tesla
$ mkdir build
$ cd build
$ cmake -G Ninja -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ ..
-- The C compiler identification is Clang 3.3.0
-- Check for working C compiler using: Ninja
-- Check for working C compiler using: Ninja -- works
-- Detecting C compiler ABI info
[...]
-- Found PROTOBUF: /usr/local/lib/libprotobuf.so
-- Configuring done
-- Generating done
-- Build files have been written to: /home/jonathan/TESLA/build
$ ccmake . # nice UI for further configuration, or else:
$ cmake -D USE_LIBCXX=false . # if you have libc++ but didn't link LLVM against it
$ cmake -D CMAKE_MODULE_PATH=/<LLVM prefix>/share/llvm/cmake . # if CMake can't find LLVM-Config or AddLLVM
$ cmake -D CMAKE_C_FLAGS=-fcolor-diagnostics . # optional but nice
$ cmake -D CMAKE_CXX_FLAGS=-fcolor-diagnostics . # optional but nice
Then we can build and test it:
$ ninja
[49/49] Testing TESLA
After that, you'll want to be able to actually run TESLA.
You can either set some environment variables:
$ export TESLA_BUILD_DIR=/path/to/TESLA/build
$ export TESLA_SOURCE_DIR=/path/to/TESLA
$ export PATH=$TESLA_SOURCE_DIR/scripts:$PATH
or else you can install the tools somewhere on your PATH:
$ cd build
$ cmake -D CMAKE_INSTALL_PREFIX=/some/sensible/path . # or else things go in /usr/local
$ ninja install
[1/1] Install the project...
-- Install configuration: "Debug"
-- Up-to-date: /some/sensible/path/lib/libtesla.so
-- Installing: /some/sensible/path/bin/tesla-analyse
-- Installing: /some/sensible/path/bin/tesla-instrument
-- Installing: /some/sensible/path/bin/tesla-graph
-- Installing: /some/sensible/path/bin/llvm-triple
-- Installing: /some/sensible/path/bin/tesla-read
-- Installing: /some/sensible/path/bin/tesla
$ export PATH=/some/sensible/path
Having either set variables or installed TESLA, you should now be able
to run TESLA commands:
$ tesla graph -help
USAGE: tesla-graph [options] <input file>
OPTIONS:
automata determinism:
-u - unlinked NFA
-l - linked NFA
-d - DFA
-help - Display available options (-help-hidden for more)
-o=<string> - <output file>
-version - Display the version of this program
Exercise TESLA
The 'strawman' directory contains an example of how TESLA assertions can be written in C code. If you run it as-is:
$ cd strawman
$ export LD_LIBRARY_PATH=../build/libtesla/src # or 'ninja install' in ../build
$ make && ./demo
TESLA demo application; version 3454895 (dirty)
Calling the 'example_syscall' function...
[CALR] example_syscall 0x7fff5b7ab7a8 0 0
[CALE] example_syscall 0x7fff5b7ab7a8 0 0
[RETE] security_check 0x7fff5b7ab7a8 0x104456020 0 0
[RETR] security_check 0x7fff5b7ab7a8 0x104456020 0 0
[RETE] some_helper 0 0
[RETR] some_helper 0 0
[CALR] void_helper 0x104456020
[CALE] void_helper 0x104456020
[RETE] void_helper 0x104456020
[RETR] void_helper 0x104456020
[NOW] automaton 0 71655456 0
[RETE] example_syscall 0x7fff5b7ab7a8 0 0 0
[RETR] example_syscall 0x7fff5b7ab7a8 0 0 0
'example_syscall' returned 0
This just shows that the 'demo' application runs normally.
If, however, you comment out line 78 of example.c (which calls the security_check() function):
--- a/strawman/example.c
+++ b/strawman/example.c
@@ -75,7 +75,7 @@ example_syscall(struct credential *cred, int index, int op)
int error;
struct object *o = objects + index;
- 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:
$ make && ./demo
TESLA demo application; version 3454895 (dirty)
Calling the 'example_syscall' function...
[...]
[NOW] automaton 0 245383200 0
demo: tesla_assert_failed: unable to move 'example.c:42#0' 2->3: current state is 1
This shows that, when we reach the assertion site for automaton 0, we detect that a transition (the security_check event) was missed!
