svn commit: r352156 - in head/devel: . tesla tesla/files

[Brooks Davis]

Author: brooks
Date: Fri Apr 25 22:21:13 2014
New Revision: 352156
URL: http://svnweb.freebsd.org/changeset/ports/352156
QAT: https://qat.redports.org/buildarchive/r352156/

Log:
  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

Added:
  head/devel/tesla/
  head/devel/tesla/Makefile   (contents, props changed)
  head/devel/tesla/distinfo   (contents, props changed)
  head/devel/tesla/files/
  head/devel/tesla/files/patch-doc__CMakeLists.txt   (contents, props changed)
  head/devel/tesla/pkg-descr   (contents, props changed)
  head/devel/tesla/pkg-plist   (contents, props changed)
Modified:
  head/devel/Makefile

Modified: head/devel/Makefile
==============================================================================
--- head/devel/Makefile	Fri Apr 25 22:05:35 2014	(r352155)
+++ head/devel/Makefile	Fri Apr 25 22:21:13 2014	(r352156)
@@ -4542,6 +4542,7 @@
     SUBDIR += tclxml
     SUBDIR += tdl
     SUBDIR += terminality
+    SUBDIR += tesla
     SUBDIR += tevent
     SUBDIR += tex-kpathsea
     SUBDIR += tex-web2c

Added: head/devel/tesla/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/devel/tesla/Makefile	Fri Apr 25 22:21:13 2014	(r352156)
@@ -0,0 +1,31 @@
+# $FreeBSD$
+
+PORTNAME=	tesla
+DISTVERSION=	0.0.20140425
+CATEGORIES=	devel lang
+
+MAINTAINER=	brooks at 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>

Added: head/devel/tesla/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/devel/tesla/distinfo	Fri Apr 25 22:21:13 2014	(r352156)
@@ -0,0 +1,2 @@
+SHA256 (tesla-0.0.20140425.tar.gz) = 325827f1b3df0da4b80486b35fbd0f99fce841f7da4d3e3f3bd48da21e900125
+SIZE (tesla-0.0.20140425.tar.gz) = 782021

Added: head/devel/tesla/files/patch-doc__CMakeLists.txt
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/devel/tesla/files/patch-doc__CMakeLists.txt	Fri Apr 25 22:21:13 2014	(r352156)
@@ -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)
+ 
+ 
+ #

Added: head/devel/tesla/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/devel/tesla/pkg-descr	Fri Apr 25 22:21:13 2014	(r352156)
@@ -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/

Added: head/devel/tesla/pkg-plist
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/devel/tesla/pkg-plist	Fri Apr 25 22:21:13 2014	(r352156)
@@ -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