From dfa3ea6fddb05dc7e6fb5b6ded9274f7e3c9feae Mon Sep 17 00:00:00 2001 From: brooks Date: Fri, 25 Apr 2014 22:21:13 +0000 Subject: New port of: 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. Sponsored by: DARPA, AFRL --- devel/Makefile | 1 + devel/tesla/Makefile | 31 +++++++++++++++++++++++++++++ devel/tesla/distinfo | 2 ++ devel/tesla/files/patch-doc__CMakeLists.txt | 11 ++++++++++ devel/tesla/pkg-descr | 15 ++++++++++++++ devel/tesla/pkg-plist | 11 ++++++++++ 6 files changed, 71 insertions(+) create mode 100644 devel/tesla/Makefile create mode 100644 devel/tesla/distinfo create mode 100644 devel/tesla/files/patch-doc__CMakeLists.txt create mode 100644 devel/tesla/pkg-descr create mode 100644 devel/tesla/pkg-plist diff --git a/devel/Makefile b/devel/Makefile index b17534bc5205..d6e30f727def 100644 --- a/devel/Makefile +++ b/devel/Makefile @@ -4542,6 +4542,7 @@ SUBDIR += tclxml SUBDIR += tdl SUBDIR += terminality + SUBDIR += tesla SUBDIR += tevent SUBDIR += tex-kpathsea SUBDIR += tex-web2c diff --git a/devel/tesla/Makefile b/devel/tesla/Makefile new file mode 100644 index 000000000000..4618b314f0f6 --- /dev/null +++ b/devel/tesla/Makefile @@ -0,0 +1,31 @@ +# $FreeBSD$ + +PORTNAME= tesla +DISTVERSION= 0.0.20140425 +CATEGORIES= devel lang + +MAINTAINER= brooks@FreeBSD.org +COMMENT= Temporally Enhanced Security Logic Assertions + +USES= cmake:outsource ninja + +BUILD_DEPENDS= clang33:${PORTSDIR}/lang/clang33 +RUN_DEPENDS= clang33:${PORTSDIR}/lang/clang33 +LIB_DEPENDS= execinfo:${PORTSDIR}/devel/libexecinfo \ + protobuf:${PORTSDIR}/devel/protobuf + +USE_GITHUB= yes +GH_ACCOUNT= CTSRD-TESLA +GH_PROJECT= TESLA +GH_TAGNAME= 3136f0f +GH_COMMIT= 3136f0f + +CC= clang33 +CXX= clang++33 + +CMAKE_ARGS+= -DCMAKE_LLVM_CONFIG=llvm-config33 + +CONFIGURE_WRKSRC= ${WRKSRC}/build +BUILD_WRKSRC= ${WRKSRC}/build + +.include diff --git a/devel/tesla/distinfo b/devel/tesla/distinfo new file mode 100644 index 000000000000..83473c5c51d9 --- /dev/null +++ b/devel/tesla/distinfo @@ -0,0 +1,2 @@ +SHA256 (tesla-0.0.20140425.tar.gz) = 325827f1b3df0da4b80486b35fbd0f99fce841f7da4d3e3f3bd48da21e900125 +SIZE (tesla-0.0.20140425.tar.gz) = 782021 diff --git a/devel/tesla/files/patch-doc__CMakeLists.txt b/devel/tesla/files/patch-doc__CMakeLists.txt new file mode 100644 index 000000000000..442a7666f9f1 --- /dev/null +++ b/devel/tesla/files/patch-doc__CMakeLists.txt @@ -0,0 +1,11 @@ +--- ./doc/CMakeLists.txt.orig 2014-04-15 09:28:42.000000000 +0000 ++++ ./doc/CMakeLists.txt 2014-04-25 22:01:46.147952919 +0000 +@@ -15,7 +15,7 @@ + # + # Static HTML content. + # +-add_subdirectory(html) ++#add_subdirectory(html) + + + # diff --git a/devel/tesla/pkg-descr b/devel/tesla/pkg-descr new file mode 100644 index 000000000000..71c3fcec2ade --- /dev/null +++ b/devel/tesla/pkg-descr @@ -0,0 +1,15 @@ +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. + +WWW: https://www.cl.cam.ac.uk/research/security/ctsrd/tesla/ diff --git a/devel/tesla/pkg-plist b/devel/tesla/pkg-plist new file mode 100644 index 000000000000..eb19188aa143 --- /dev/null +++ b/devel/tesla/pkg-plist @@ -0,0 +1,11 @@ +bin/tesla +bin/tesla-analyse +bin/tesla-cat +bin/tesla-get-triple +bin/tesla-highlight +bin/tesla-instrument +bin/tesla-print +include/libtesla.h +include/tesla-macros.h +include/tesla.h +lib/libtesla.so -- cgit