From owner-svn-ports-head@FreeBSD.ORG Fri Apr 25 22:21:15 2014 Return-Path: Delivered-To: svn-ports-head@freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [8.8.178.115]) (using TLSv1 with cipher ADH-AES256-SHA (256/256 bits)) (No client certificate requested) by hub.freebsd.org (Postfix) with ESMTPS id 3383CAE3; Fri, 25 Apr 2014 22:21:15 +0000 (UTC) Received: from svn.freebsd.org (svn.freebsd.org [IPv6:2001:1900:2254:2068::e6a:0]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 141451043; Fri, 25 Apr 2014 22:21:15 +0000 (UTC) Received: from svn.freebsd.org ([127.0.1.70]) by svn.freebsd.org (8.14.8/8.14.8) with ESMTP id s3PMLEWR073403; Fri, 25 Apr 2014 22:21:14 GMT (envelope-from brooks@svn.freebsd.org) Received: (from brooks@localhost) by svn.freebsd.org (8.14.8/8.14.8/Submit) id s3PMLDdv073397; Fri, 25 Apr 2014 22:21:13 GMT (envelope-from brooks@svn.freebsd.org) Message-Id: <201404252221.s3PMLDdv073397@svn.freebsd.org> From: Brooks Davis Date: Fri, 25 Apr 2014 22:21:13 +0000 (UTC) To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r352156 - in head/devel: . tesla tesla/files X-SVN-Group: ports-head MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-BeenThere: svn-ports-head@freebsd.org X-Mailman-Version: 2.1.17 Precedence: list List-Id: SVN commit messages for the ports tree for head List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 25 Apr 2014 22:21:15 -0000 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@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 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