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

6 files changed, 71 insertions, 0 deletions

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 <bsd.port.mk>
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