socsvn commit: r222562 - in soc2011/shm/TESLA: . assertions
assertions/audit assertions/mac_template assertions/mwc
assertions/ssh assertions/ssh/results assertions/tcp cfa
kernel libtesla strawman...
shm at FreeBSD.org
shm at FreeBSD.org
Sun May 29 20:45:48 UTC 2011
Author: shm
Date: Sun May 29 20:45:45 2011
New Revision: 222562
URL: http://svnweb.FreeBSD.org/socsvn/?view=rev&rev=222562
Log:
* local tesla copy (forked from https://github.com/CTSRD-TESLA/TESLA)
Added:
soc2011/shm/TESLA/
soc2011/shm/TESLA/LICENSE.txt
soc2011/shm/TESLA/README.txt
soc2011/shm/TESLA/assertions/
soc2011/shm/TESLA/assertions/audit/
soc2011/shm/TESLA/assertions/audit/Makefile
soc2011/shm/TESLA/assertions/audit/audit_assertion.c
soc2011/shm/TESLA/assertions/audit/audit_automata.c
soc2011/shm/TESLA/assertions/audit/audit_defs.h
soc2011/shm/TESLA/assertions/audit/instrumentation.spec
soc2011/shm/TESLA/assertions/audit/syscalls.c
soc2011/shm/TESLA/assertions/audit/syscalls.h
soc2011/shm/TESLA/assertions/audit/test.c
soc2011/shm/TESLA/assertions/mac_template/
soc2011/shm/TESLA/assertions/mac_template/Makefile
soc2011/shm/TESLA/assertions/mac_template/generate.sh (contents, props changed)
soc2011/shm/TESLA/assertions/mac_template/instrumentation.spec
soc2011/shm/TESLA/assertions/mac_template/mac_assertion.c.template
soc2011/shm/TESLA/assertions/mac_template/mass_generate.csh
soc2011/shm/TESLA/assertions/mwc/
soc2011/shm/TESLA/assertions/mwc/Makefile
soc2011/shm/TESLA/assertions/mwc/instrumentation.spec
soc2011/shm/TESLA/assertions/mwc/mwc_assertion.c
soc2011/shm/TESLA/assertions/mwc/mwc_automata.c
soc2011/shm/TESLA/assertions/mwc/mwc_defs.h
soc2011/shm/TESLA/assertions/mwc/syscalls.c
soc2011/shm/TESLA/assertions/mwc/syscalls.h
soc2011/shm/TESLA/assertions/mwc/test.c
soc2011/shm/TESLA/assertions/ssh/
soc2011/shm/TESLA/assertions/ssh/Makefile
soc2011/shm/TESLA/assertions/ssh/README.txt
soc2011/shm/TESLA/assertions/ssh/build_openssh.sh (contents, props changed)
soc2011/shm/TESLA/assertions/ssh/instrumentation.spec
soc2011/shm/TESLA/assertions/ssh/openssh-teal.patch
soc2011/shm/TESLA/assertions/ssh/parse.ml
soc2011/shm/TESLA/assertions/ssh/results/
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.1000k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.100k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.150k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.200k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.250k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.300k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.350k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.400k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.450k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.500k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.50k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.550k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.600k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.650k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.700k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.750k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.800k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.850k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.900k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_notesla.950k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.1000k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.100k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.150k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.200k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.250k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.300k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.350k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.400k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.450k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.500k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.50k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.550k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.600k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.650k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.700k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.750k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.800k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.850k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.900k
soc2011/shm/TESLA/assertions/ssh/results/res_clang_tesla.950k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.1000k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.100k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.150k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.200k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.250k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.300k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.350k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.400k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.450k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.500k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.50k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.550k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.600k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.650k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.700k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.750k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.800k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.850k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.900k
soc2011/shm/TESLA/assertions/ssh/results/res_gcc_notesla.950k
soc2011/shm/TESLA/assertions/ssh/run_test.sh (contents, props changed)
soc2011/shm/TESLA/assertions/ssh/ssh.spl
soc2011/shm/TESLA/assertions/ssh/ssh_assertion.c
soc2011/shm/TESLA/assertions/ssh/ssh_channel.spl
soc2011/shm/TESLA/assertions/ssh/ssh_fakeassertion.c
soc2011/shm/TESLA/assertions/ssh/ssh_kex.spl
soc2011/shm/TESLA/assertions/ssh/sshplot.R
soc2011/shm/TESLA/assertions/ssh/sshplot.gp
soc2011/shm/TESLA/assertions/tcp/
soc2011/shm/TESLA/assertions/tcp/Makefile
soc2011/shm/TESLA/assertions/tcp/analysed.results
soc2011/shm/TESLA/assertions/tcp/clang_stub.c
soc2011/shm/TESLA/assertions/tcp/gcc_stub.c
soc2011/shm/TESLA/assertions/tcp/gnuplot.dat
soc2011/shm/TESLA/assertions/tcp/instr.c
soc2011/shm/TESLA/assertions/tcp/instrumentation.spec.in
soc2011/shm/TESLA/assertions/tcp/micro.ps
soc2011/shm/TESLA/assertions/tcp/micro.sh (contents, props changed)
soc2011/shm/TESLA/assertions/tcp/parse.ml
soc2011/shm/TESLA/assertions/tcp/plot.gp
soc2011/shm/TESLA/assertions/tcp/tcpc-alt.spl
soc2011/shm/TESLA/assertions/tcp/tcpc.spec
soc2011/shm/TESLA/assertions/tcp/tcpc.spl
soc2011/shm/TESLA/assertions/tcp/tcpc_assertion.c
soc2011/shm/TESLA/assertions/tcp/tcpc_automata.c
soc2011/shm/TESLA/assertions/tcp/tcpc_defs.h
soc2011/shm/TESLA/assertions/tcp/tcpc_dummy_assertion.c
soc2011/shm/TESLA/assertions/tcp/tcpc_userspace.h
soc2011/shm/TESLA/assertions/tcp/test.c
soc2011/shm/TESLA/build_clang.sh (contents, props changed)
soc2011/shm/TESLA/cfa/
soc2011/shm/TESLA/cfa/Makefile
soc2011/shm/TESLA/cfa/OCamlMakefile
soc2011/shm/TESLA/cfa/README.txt
soc2011/shm/TESLA/cfa/dhcp.spl
soc2011/shm/TESLA/cfa/spl_cfg.ml
soc2011/shm/TESLA/cfa/spl_dot.ml
soc2011/shm/TESLA/cfa/spl_lexer.mll
soc2011/shm/TESLA/cfa/spl_location.ml
soc2011/shm/TESLA/cfa/spl_ocaml.ml
soc2011/shm/TESLA/cfa/spl_optimiser.ml
soc2011/shm/TESLA/cfa/spl_optimiser.mli
soc2011/shm/TESLA/cfa/spl_parser.mli
soc2011/shm/TESLA/cfa/spl_parser.mly
soc2011/shm/TESLA/cfa/spl_promela.ml
soc2011/shm/TESLA/cfa/spl_stdlib.ml
soc2011/shm/TESLA/cfa/spl_stdlib.mli
soc2011/shm/TESLA/cfa/spl_syntaxtree.ml
soc2011/shm/TESLA/cfa/spl_tesla.ml
soc2011/shm/TESLA/cfa/spl_typechecker.ml
soc2011/shm/TESLA/cfa/spl_typechecker.mli
soc2011/shm/TESLA/cfa/spl_utils.ml
soc2011/shm/TESLA/cfa/spl_utils.mli
soc2011/shm/TESLA/cfa/splc.ml
soc2011/shm/TESLA/cfa/tcp_connect.spl
soc2011/shm/TESLA/cfa/tcpc.spl
soc2011/shm/TESLA/kernel/
soc2011/shm/TESLA/kernel/20110315-tesla-src-sys.diff
soc2011/shm/TESLA/kernel/20110316-tesla-src-sys.diff
soc2011/shm/TESLA/kernel/20110318-tesla-src-sys.diff
soc2011/shm/TESLA/kernel/benchmark-clang (contents, props changed)
soc2011/shm/TESLA/kernel/tesla-clang (contents, props changed)
soc2011/shm/TESLA/libtesla/
soc2011/shm/TESLA/libtesla/Makefile
soc2011/shm/TESLA/libtesla/TODO
soc2011/shm/TESLA/libtesla/tesla_internal.h
soc2011/shm/TESLA/libtesla/tesla_registration.c
soc2011/shm/TESLA/libtesla/tesla_state.c
soc2011/shm/TESLA/libtesla/tesla_state_global.c
soc2011/shm/TESLA/libtesla/tesla_state_perthread.c
soc2011/shm/TESLA/libtesla/tesla_util.c
soc2011/shm/TESLA/strawman/
soc2011/shm/TESLA/strawman/Makefile
soc2011/shm/TESLA/strawman/TODO
soc2011/shm/TESLA/strawman/_instrumentation.c
soc2011/shm/TESLA/strawman/caller.c
soc2011/shm/TESLA/strawman/empty.spec
soc2011/shm/TESLA/strawman/evil.h
soc2011/shm/TESLA/strawman/manual.spec
soc2011/shm/TESLA/strawman/syscalls.c
soc2011/shm/TESLA/strawman/syscalls.h
soc2011/shm/TESLA/strawman/types.h
soc2011/shm/TESLA/tesla/
soc2011/shm/TESLA/tesla/tesla.h
soc2011/shm/TESLA/tesla/tesla_registration.h
soc2011/shm/TESLA/tesla/tesla_state.h
soc2011/shm/TESLA/tesla/tesla_util.h
Added: soc2011/shm/TESLA/LICENSE.txt
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/LICENSE.txt Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,33 @@
+Unless specified otherwise, the contents of this directory are distributed
+according to the following terms.
+
+Copyright (c) 2011 Jonathan Anderson
+Copyright (c) 2011 Anil Madhavapeddy
+Copyright (c) 2011 Steven Murdoch
+Copyright (c) 2011 Robert N. M. Watson
+All rights reserved.
+
+This software was developed by SRI International and the University of
+Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
+("CTSRD"), as part of the DARPA CRASH research programme.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
Added: soc2011/shm/TESLA/README.txt
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/README.txt Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,22 @@
+Getting started
+===============
+
+Pre-requisites
+--------------
+Install git, gcc, g++, cmake, make
+
+Build clang and LLVM
+--------------------
+$ ./build_clang.sh
+
+This will check out clang and LLVM if needed. Building will take
+a while (a couple of hours on my laptop).
+
+Build strawman
+--------------
+$ cd strawman
+$ make
+
+Test strawman
+-------------
+$ ./test
\ No newline at end of file
Added: soc2011/shm/TESLA/assertions/audit/Makefile
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/audit/Makefile Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,22 @@
+CC=../../kernel/tesla-clang
+LD=../../kernel/tesla-clang
+CLANGLIB=${HOME}/llvmlib/libTeslaInstrumenter.so
+
+CFLAGS=-Wall -g -I../..
+
+TESLALIBS= \
+ ../../libtesla/tesla_state.o \
+ ../../libtesla/tesla_state_global.o \
+ ../../libtesla/tesla_state_perthread.o \
+ ../../libtesla/tesla_util.o
+
+all: test
+
+test: test.o audit_assertion.o audit_automata.o syscalls.o ${TESLALIBS}
+ ${LD} -o $@ $+ -lpthread
+clean:
+ rm -f test *.o *.bc *.ll *.c-tesla.h
+
+audit_assertion.o: syscalls.c-tesla.h
+syscalls.c-tesla.h: syscalls.o
+syscalls.o: instrumentation.spec
Added: soc2011/shm/TESLA/assertions/audit/audit_assertion.c
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/audit/audit_assertion.c Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,343 @@
+/*-
+ * Copyright (c) 2011 Robert N. M. Watson
+ * All rights reserved.
+ *
+ * This software was developed by SRI International and the University of
+ * Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
+ * ("CTSRD"), as part of the DARPA CRASH research programme.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+ * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+ * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+ * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ *
+ * $Id$
+ */
+
+#include <sys/types.h>
+
+#ifdef _KERNEL
+#include <sys/param.h>
+#include <sys/eventhandler.h>
+#include <sys/kernel.h>
+#include <sys/systm.h>
+#else
+#include <assert.h>
+#include <stdio.h>
+
+#include "syscalls.h"
+#endif
+
+#include <tesla/tesla.h>
+#include <tesla/tesla_registration.h>
+#include <tesla/tesla_state.h>
+#include <tesla/tesla_util.h>
+
+#include "audit_defs.h"
+
+/*
+ * State associated with this assertion in flight.
+ */
+static struct tesla_state *audit_state;
+
+/*
+ * This assertion has two automata: an implied system call automata, and the
+ * explicit autaomata described by audit_automata_states and
+ * audit_automata_rules. For more complex (multi-clause) assertions, there
+ * would be an additional automata for each clause.
+ *
+ * Note: non-zero constants.
+ */
+#define AUDIT_AUTOMATA_SYSCALL 1 /* In a system call. */
+#define AUDIT_AUTOMATA_ASSERTION 2 /* Assertion clause. */
+
+/*
+ * Define the maximum number of instances of the assertion to implement
+ * per-thread. Should be prime, and must be at least 2 so that the system
+ * call automata works.
+ */
+#define AUDIT_LIMIT 3
+
+/*
+ * Strings used when printing assertion failures.
+ */
+#define AUDIT_NAME "audit_submit_check"
+#define AUDIT_DESCRIPTION "VOP_WRITE without eventual audit_submit"
+
+#ifdef _KERNEL
+static eventhandler_tag audit_event_function_prologue_syscallenter_tag;
+static eventhandler_tag audit_event_function_prologue_syscallret_tag;
+#endif
+
+void audit_event_function_prologue_syscallenter(void **tesla_data,
+ struct thread *td, struct syscall_args *sa);
+void audit_event_function_prologue_syscallret(void **tesla_data,
+ struct thread *td, int error, struct syscall_args *sa);
+
+/*
+ * When an assertion is initialised, register state management with the TESLA
+ * state framework. This assertion uses per-thread state, since assertions are
+ * relative to specific threads. Later use of tesla_instance will return
+ * per-thread instances, and synchronisation is avoided.
+ */
+#ifdef _KERNEL
+static
+#endif
+void
+audit_init(int scope)
+{
+ int error;
+
+ error = tesla_state_new(&audit_state, scope, AUDIT_LIMIT, AUDIT_NAME,
+ AUDIT_DESCRIPTION);
+#ifdef _KERNEL
+ if (error)
+ panic("audit_init: tesla_state_new failed due to %s",
+ tesla_strerror(error));
+#else
+ assert(error == 0);
+#endif
+
+ /*
+ * Comment from MWC regarding atomicity also applies here.
+ */
+#ifdef _KERNEL
+ audit_event_function_prologue_syscallenter_tag =
+ EVENTHANDLER_REGISTER(tesla_event_function_prologue_syscallenter,
+ audit_event_function_prologue_syscallenter, NULL,
+ EVENTHANDLER_PRI_ANY);
+ audit_event_function_prologue_syscallret_tag =
+ EVENTHANDLER_REGISTER(tesla_event_function_prologue_syscallret,
+ audit_event_function_prologue_syscallret, NULL,
+ EVENTHANDLER_PRI_ANY);
+#endif
+}
+
+#ifdef _KERNEL
+static void
+audit_sysinit(__unused void *arg)
+{
+
+ audit_init(TESLA_SCOPE_PERTHREAD);
+}
+SYSINIT(audit_init, SI_SUB_TESLA_ASSERTION, SI_ORDER_ANY, audit_sysinit,
+ NULL);
+#endif /* _KERNEL */
+
+/*
+ * When the checker is unloaded, GC its state. Hopefully also un-instruments.
+ */
+#ifdef _KERNEL
+static
+#endif
+void
+audit_destroy(void)
+{
+
+ tesla_state_destroy(audit_state);
+#ifdef _KERNEL
+ EVENTHANDLER_DEREGISTER(tesla_event_function_prologue_syscallenter,
+ audit_event_function_prologue_syscallenter_tag);
+ EVENTHANDLER_DEREGISTER(tesla_event_function_prologue_syscallret,
+ audit_event_function_prologue_syscallret_tag);
+#endif
+}
+
+#ifdef _KERNEL
+static void
+audit_sysuninit(__unused void *arg)
+{
+
+ audit_destroy();
+}
+SYSUNINIT(audit_destroy, SI_SUB_TESLA_ASSERTION, SI_ORDER_ANY,
+ audit_sysuninit, NULL);
+#endif /* _KERNEL */
+
+/*
+ * System call enters: prod implicit system call lifespan state machine.
+ */
+#ifndef _KERNEL
+void
+__tesla_event_function_prologue_syscallenter(void **tesla_data,
+ struct thread *td, struct syscall_args *sa)
+{
+
+ audit_event_function_prologue_syscallenter(tesla_data, td, sa);
+}
+
+void
+__tesla_event_function_return_syscallenter(void **tesla_data, int retval)
+{
+
+}
+#endif
+
+void
+audit_event_function_prologue_syscallenter(void **tesla_data,
+ struct thread *td, struct syscall_args *sa)
+{
+ struct tesla_instance *tip;
+ int error;
+
+ error = tesla_instance_get1(audit_state, AUDIT_AUTOMATA_SYSCALL,
+ &tip, NULL);
+ if (error)
+ return;
+ tip->ti_state[0] = 1; /* In syscall. */
+ tesla_instance_put(audit_state, tip);
+}
+
+/*
+ * Used when iterating over eventually expressions in system call return.
+ */
+static void
+audit_iterator_callback(struct tesla_instance *tip, void *arg)
+{
+ u_int event = *(u_int *)arg;
+
+ if (audit_automata_prod(tip, event))
+ tesla_assert_fail(audit_state, tip);
+}
+
+/*
+ * System call returns: prod implicit system call lifespan state machine,
+ * prod eventually clauses, and flush all assertions.
+ */
+#ifndef _KERNEL
+void
+__tesla_event_function_prologue_syscallret(void **tesla_data,
+ struct thread *td, int error, struct syscall_args *sa)
+{
+
+ audit_event_function_prologue_syscallret(tesla_data, td, error, sa);
+}
+
+void
+__tesla_event_function_return_syscallret(void **tesla_data)
+{
+
+}
+#endif
+
+void
+audit_event_function_prologue_syscallret(void **tesla_data, struct thread *td,
+ int err, struct syscall_args *sa)
+{
+ struct tesla_instance *tip;
+ u_int event;
+ int error;
+
+ error = tesla_instance_get1(audit_state, AUDIT_AUTOMATA_SYSCALL,
+ &tip, NULL);
+ if (error)
+ goto out;
+ if (tip->ti_state[0] == 1)
+ tip->ti_state[0] = 0;
+ tesla_instance_put(audit_state, tip);
+
+ /* Prod each eventually automata. */
+ event = AUDIT_EVENT_TESLA_SYSCALL_RETURN;
+ tesla_instance_foreach1(audit_state, AUDIT_AUTOMATA_ASSERTION,
+ audit_iterator_callback, &event);
+out:
+ tesla_state_flush(audit_state);
+}
+
+/*
+ * Invocation of audit_submit(): prod the state machine.
+ */
+void
+__tesla_event_function_prologue_audit_submit(void **tesla_data)
+{
+ struct tesla_instance *tip;
+ u_int state;
+ int error;
+
+ error = tesla_instance_get1(audit_state, AUDIT_AUTOMATA_SYSCALL,
+ &tip, NULL);
+ if (error)
+ return;
+ state = tip->ti_state[0];
+ tesla_instance_put(audit_state, tip);
+ if (state != 1)
+ return;
+
+ error = tesla_instance_get1(audit_state, AUDIT_AUTOMATA_ASSERTION,
+ &tip, NULL);
+ if (error)
+ return;
+ if (audit_automata_prod(tip, AUDIT_EVENT_AUDIT_SUBMIT))
+ tesla_assert_fail(audit_state, tip);
+ tesla_instance_put(audit_state, tip);
+}
+
+/*
+ * Return from audit_submit(): did we return the correct value?
+ */
+void
+__tesla_event_function_return_audit_submit(void **tesla_data, int retval)
+{
+ /* TODO */
+}
+
+/*
+* The event implied by the assertion; executes at that point in VOP_WRITE.
+*/
+void
+__tesla_event_assertion_helper_which_asserts_0(void)
+{
+ struct tesla_instance *tip;
+ int error, state;
+
+ /*
+ * Check that we are in a system call; if not, we may have incomplete
+ * data.
+ */
+ error = tesla_instance_get1(audit_state, AUDIT_AUTOMATA_SYSCALL,
+ &tip, NULL);
+ if (error)
+ return;
+ state = tip->ti_state[0];
+ tesla_instance_put(audit_state, tip);
+ if (state != 1)
+ return;
+
+ error = tesla_instance_get1(audit_state, AUDIT_AUTOMATA_ASSERTION,
+ &tip, NULL);
+ if (error)
+ return;
+ if (audit_automata_prod(tip, AUDIT_EVENT_ASSERTION))
+ tesla_assert_fail(audit_state, tip);
+ tesla_instance_put(audit_state, tip);
+}
+
+static void
+audit_debug_callback(struct tesla_instance *tip)
+{
+
+ printf("%s: assertion %s failed\n", AUDIT_NAME, AUDIT_DESCRIPTION);
+}
+
+void
+audit_setaction_debug(void)
+{
+
+ tesla_state_setaction(audit_state, audit_debug_callback);
+}
Added: soc2011/shm/TESLA/assertions/audit/audit_automata.c
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/audit/audit_automata.c Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,152 @@
+/*-
+ * Copyright (c) 2011 Robert N. M. Watson
+ * All rights reserved.
+ *
+ * This software was developed by SRI International and the University of
+ * Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
+ * ("CTSRD"), as part of the DARPA CRASH research programme.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+ * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+ * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+ * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ *
+ * $Id$
+ */
+
+#include <sys/types.h>
+
+#ifdef _KERNEL
+#include <sys/param.h>
+#include <sys/systm.h>
+#else
+#include <assert.h>
+#include <stdlib.h>
+#endif
+
+#include <tesla/tesla_state.h>
+#include <tesla/tesla_util.h>
+
+#include "audit_defs.h"
+
+/*
+ * This is a hand-crafted automata implementing the TESLA assertion:
+ *
+ * (assertion in VOP_WRITE) -> eventually(invoked(audit_submit()))
+ *
+ * Many instances of the automata may be in flight at once during a system
+ * call, instantiated by invocations of tesla_assert().
+ *
+ * The automata recognizes !(assertion), so has a "reject" state rather than
+ * an "accept" state. The assertion matches as soon as we hit a reject
+ * state. This is a simple, one-clause previously assertion, so there is
+ * just one automata, no composition required.
+ *
+ * (0) --tesla_assert-> (1) --audit_submit()-> (2) (loop)
+ * \ \
+ * \ tesla_syscall_return() --> (reject (3)) --> (4) (loop)
+ * --*-> (0)
+ *
+ * Note that the assertion will fire once in state 3 and then move onto state
+ * 4, where it lives indefinitely. This ensures that if firing the assertion
+ * is non-fatal, such as when using assertions to trigger DTrace probes, we
+ * fire only once.
+ */
+static struct audit_automata_state {
+ int aas_reject;
+} audit_automata_states[] = {
+ /* 0 */ { 0 }, /* Awaiting tesla_assert() */
+ /* 1 */ { 0 }, /* Awaiting audit_submit() */
+ /* 2 */ { 0 }, /* Termination state */
+ /* 3 */ { 1 }, /* Reject */
+ /* 4 */ { 0 }, /* Loop after reject */
+};
+static int audit_automata_state_count = sizeof(audit_automata_states) /
+ sizeof(audit_automata_states[0]);
+
+static struct audit_automata_rule {
+ u_int aar_fromstate;
+ u_int aar_input;
+ u_int aar_tostate;
+} audit_automata_rules[] = {
+ { 0, AUDIT_EVENT_ASSERTION, 1 }, /* Assertion. */
+ { 0, AUDIT_EVENT_AUDIT_SUBMIT, 0 }, /* Loop in 0. */
+ { 0, AUDIT_EVENT_TESLA_SYSCALL_RETURN, 0 }, /* Loop in 0. */
+ { 1, AUDIT_EVENT_AUDIT_SUBMIT, 2 }, /* Satisfied. */
+ { 1, AUDIT_EVENT_ASSERTION, 1 }, /* Double assertion. */
+ { 1, AUDIT_EVENT_TESLA_SYSCALL_RETURN, 3 }, /* Submit missed! */
+ { 2, AUDIT_EVENT_ASSERTION, 1 }, /* Restart. */
+ { 2, AUDIT_EVENT_AUDIT_SUBMIT, 2 }, /* Double submit. */
+ { 2, AUDIT_EVENT_TESLA_SYSCALL_RETURN, 2 }, /* Loop in 2. */
+ { 3, AUDIT_EVENT_ASSERTION, 1 }, /* Fire, Restart. */
+ { 3, AUDIT_EVENT_AUDIT_SUBMIT, 4 }, /* Loop in 4. */
+ { 3, AUDIT_EVENT_TESLA_SYSCALL_RETURN, 4 }, /* Loop in 4. */
+ { 4, AUDIT_EVENT_ASSERTION, 4 }, /* Loop in 4. */
+ { 4, AUDIT_EVENT_AUDIT_SUBMIT, 4}, /* Loop in 4. */
+ { 4, AUDIT_EVENT_TESLA_SYSCALL_RETURN, 4}, /* Loop in 4. */
+};
+static int audit_automata_rule_count = sizeof(audit_automata_rules) /
+ sizeof(audit_automata_rules[0]);
+
+/*
+ * This automata uses only ti_state[0].
+ */
+#define STATE(tip) ((tip)->ti_state[0])
+
+static __inline struct audit_automata_rule *
+audit_automata_lookup_rule(u_int state, u_int event)
+{
+ u_int i;
+
+ for (i = 0; i < audit_automata_rule_count; i++) {
+ if (audit_automata_rules[i].aar_fromstate == state &&
+ audit_automata_rules[i].aar_input == event)
+ return (&(audit_automata_rules[i]));
+ }
+ return (NULL);
+}
+
+/*
+ * Prod an instance of the AUDIT automata, return (1) if an assertion should
+ * fire, or to let things continue gliding along.
+ */
+int
+audit_automata_prod(struct tesla_instance *tip, u_int event)
+{
+ struct audit_automata_rule *aarp;
+ u_int newstate;
+
+#ifdef _KERNEL
+ KASSERT(STATE(tip) < audit_automata_state_count,
+ ("audit_automata_prod: invalid state %d", STATE(tip)));
+#else
+ assert(STATE(tip) < audit_automata_state_count);
+#endif
+ aarp = audit_automata_lookup_rule(STATE(tip), event);
+#ifdef _KERNEL
+ KASSERT(aarp != NULL,
+ ("audit_automata_prod: event %d not accepted", event));
+#else
+ assert(aarp != NULL);
+#endif
+ STATE(tip) = newstate = aarp->aar_tostate;
+ if (audit_automata_states[newstate].aas_reject)
+ return (1);
+ return (0);
+}
Added: soc2011/shm/TESLA/assertions/audit/audit_defs.h
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/audit/audit_defs.h Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,61 @@
+/*-
+ * Copyright (c) 2011 Robert N. M. Watson
+ * All rights reserved.
+ *
+ * This software was developed by SRI International and the University of
+ * Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
+ * ("CTSRD"), as part of the DARPA CRASH research programme.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+ * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+ * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+ * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ *
+ * $Id$
+ */
+
+#ifndef AUDIT_DEFS_H
+#define AUDIT_DEFS_H
+
+#include <sys/types.h>
+
+/*
+ * Names for events that will trigger AUDIT rules.
+ */
+#define AUDIT_EVENT_ASSERTION 1
+#define AUDIT_EVENT_AUDIT_SUBMIT 2
+#define AUDIT_EVENT_TESLA_SYSCALL_RETURN 3
+
+/*
+ * Prod the AUDIT state machine, return (1) if the assertion has failed.
+ */
+struct tesla_instance;
+int audit_automata_prod(struct tesla_instance *tip, u_int event);
+
+/*
+ * "Public" interfaces to the assertion, to be invoked by load, unload, and
+ * instrumentation handlers.
+ */
+#ifndef _KERNEL
+void audit_init(int scope);
+void audit_destroy(void);
+#endif
+void audit_setaction_debug(void);
+
+#endif /* AUDIT_DEFS_H */
Added: soc2011/shm/TESLA/assertions/audit/instrumentation.spec
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/audit/instrumentation.spec Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,3 @@
+function,audit_submit
+function,syscallenter
+function,syscallret
Added: soc2011/shm/TESLA/assertions/audit/syscalls.c
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/audit/syscalls.c Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,57 @@
+#include <stdarg.h>
+#include <stdlib.h>
+
+#include <tesla/tesla.h>
+
+#include "syscalls.h"
+
+int
+audit_submit()
+{
+ return 0;
+}
+
+void
+helper_which_asserts()
+{
+ TESLA_ASSERT(syscall) {
+ eventually(audit_submit());
+ }
+}
+
+int
+syscallenter(struct thread *td, struct syscall_args *sa)
+{
+
+ return (0);
+}
+
+void
+syscallret(struct thread *td, int error, struct syscall_args *sa)
+{
+
+}
+
+int
+syscall(size_t len, ...)
+{
+ va_list args;
+ va_start(args, len);
+
+ syscallenter(NULL, NULL);
+ for (size_t i = 0; i < len; i++) {
+ int action = va_arg(args, int);
+ switch(action) {
+ case SUBMIT:
+ audit_submit();
+ break;
+
+ case ASSERT:
+ helper_which_asserts();
+ break;
+ }
+ }
+ va_end(args);
+ syscallret(NULL, 0, NULL);
+ return (0);
+}
Added: soc2011/shm/TESLA/assertions/audit/syscalls.h
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/audit/syscalls.h Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,19 @@
+#ifndef SYSCALLS_H
+#define SYSCALLS_H
+
+#include <sys/types.h>
+
+/* actions which can be performed in a syscall */
+#define NOOP 0
+#define SUBMIT 1
+#define ASSERT 2
+
+/* simulate a syscall */
+int syscall(size_t len, ...);
+
+struct thread;
+struct syscall_args;
+int syscallenter(struct thread *td, struct syscall_args *sa);
+void syscallret(struct thread *td, int error, struct syscall_args *sa);
+
+#endif /* SYSCALLS_H */
Added: soc2011/shm/TESLA/assertions/audit/test.c
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/audit/test.c Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,92 @@
+/*-
+ * Copyright (c) 2011 Robert N. M. Watson
+ * All rights reserved.
+ *
+ * This software was developed by SRI International and the University of
+ * Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
+ * ("CTSRD"), as part of the DARPA CRASH research programme.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+ * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+ * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+ * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ *
+ * $Id$
+ */
+
+#include <stdarg.h>
+#include <stdio.h>
+
+#include <tesla/tesla_util.h>
+#include <tesla/tesla_state.h>
+
+#include "audit_defs.h"
+#include "syscalls.h"
+
+/*
+ * Test program for the 'audit' assertion. Run a number of times with various
+ * event sequences and see how it works out.
+ */
+void
+test(int scope)
+{
+ printf("\nScope: %s\n", scope == TESLA_SCOPE_GLOBAL ? "global" :
+ "per-thread");
+
+ audit_init(scope);
+ audit_setaction_debug(); /* Use printf(), not assert(). */
+
+ printf("test:\tno assertion or use\n");
+ syscall(0);
+
+ printf("test:\taudit_submit\n");
+ syscall(1, SUBMIT);
+
+ printf("test:\tassertion, no submit (should FAIL)\n");
+ syscall(1, ASSERT);
+
+ printf("test:\tassertion, submit\n");
+ syscall(2, ASSERT, SUBMIT);
+
+ printf("test:\tsubmit, assertion in wrong order (should FAIL)\n");
+ syscall(2, SUBMIT, ASSERT);
+
+ printf("test:\tdouble submit, assertion\n");
+ syscall(3, ASSERT, SUBMIT, SUBMIT);
+
+ printf("test:\tdouble assertion, submit\n");
+ syscall(3, ASSERT, ASSERT, SUBMIT);
+
+ printf("test:\tassert/submit/assert/submit\n");
+ syscall(4, ASSERT, SUBMIT, ASSERT, SUBMIT);
+
+ printf("test:\tassert/submit/assert (should FAIL)\n");
+ syscall(3, ASSERT, SUBMIT, ASSERT);
+
+ audit_destroy();
+}
+
+int
+main(int argc, char *argv[])
+{
+ test(TESLA_SCOPE_GLOBAL);
+ test(TESLA_SCOPE_PERTHREAD);
+
+ return (0);
+}
Added: soc2011/shm/TESLA/assertions/mac_template/Makefile
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/mac_template/Makefile Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,8 @@
+all: mac_assertion.c
+
+clean:
+ rm -f mac_assertion.c
+
+mac_assertion.c: mac_assertion.c.template ../mwc/syscalls.c.vars
+ ./generate.sh ../mwc/syscalls.c.vars $<
+
Added: soc2011/shm/TESLA/assertions/mac_template/generate.sh
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/mac_template/generate.sh Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,44 @@
+#!/bin/sh
+
+VARS=$1
+
+TEMPLATE=$2
+if [ "$TEMPLATE" == "" ]; then
+ echo "usage: generate.sh <vars> <template file>"
+ exit 1
+fi
+
+OUTPUT=`echo $TEMPLATE | sed 's/.template$//'`
+
+if [ "$OUTPUT" == "$TEMPLATE" ]; then
+ echo "Error: input filename does not end in .template"
+ exit 1
+fi
+
+echo "$TEMPLATE => $OUTPUT"
+
+SED_BACKUP=$OUTPUT.backup
+cp $TEMPLATE $OUTPUT
+
+cat $VARS | while read line
+do
+ case $line in
+ "") continue ;;
+ \#*) continue ;;
+ esac
+
+ name=`echo "$line" | awk -F: '{print $1}'`
+ value=`echo "$line" | awk -F: '{print $2}'`
+
+ if [ "" == "`grep %$name% $OUTPUT`" ]; then
+ echo Pattern %$name% not present in $OUTPUT
+ else
+ echo $name
+ fi
+
+ sed -i.backup -e "s/%$name%/$value/" $OUTPUT || exit 1
+done
+
+cat $OUTPUT | tr '$' '\n' > $SED_BACKUP
+mv $SED_BACKUP $OUTPUT
+
Added: soc2011/shm/TESLA/assertions/mac_template/instrumentation.spec
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/mac_template/instrumentation.spec Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,2 @@
+function,syscall
+function,%MACCHECK%
Added: soc2011/shm/TESLA/assertions/mac_template/mac_assertion.c.template
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/mac_template/mac_assertion.c.template Sun May 29 20:45:45 2011 (r222562)
@@ -0,0 +1,462 @@
+/*-
+ * Copyright (c) 2011 Robert N. M. Watson
+ * All rights reserved.
+ *
+ * This software was developed by SRI International and the University of
+ * Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
+ * ("CTSRD"), as part of the DARPA CRASH research programme.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+ * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+ * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+ * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ */
+
+#include <sys/types.h>
+
+#ifdef _KERNEL
+#include <sys/param.h>
+#include <sys/eventhandler.h>
+#include <sys/kernel.h>
+#include <sys/systm.h>
+#else
+#include <assert.h>
+#include <stdio.h>
+#endif
+
+#include <tesla/tesla.h>
+#include <tesla/tesla_registration.h>
+#include <tesla/tesla_state.h>
+#include <tesla/tesla_util.h>
+
+/*
+ * Provide compile-time checks on e.g. the size of tesla_instance.
+ */
+%COMPILE_TIME_CHECKS%
+
+/*
+ * This checker is modeled on an abstract "check-before-use" (CBU) checker
+ * template. The goal is to establish at the time of use whether, previously,
+ * an appropriate access control check occurred using the same credential and
+ * pertinent arguments.
+ */
+
+/*
+ * State associated with this assertion in flight.
+ */
+static struct tesla_state *cbu_state;
+
+/*
+ * This assertion has three automata: an implied system call automata, an
+ * implicit automata linking call and return for %INSTRUMENTED_FN%()
+ * so that we can confirm that the right arguments correspond to the right
+ * return value, and the explicit autaomata described by automata_states and
+ * cbu_%INSTRUMENTED_FN%_automata_rules.
+ *
+ * For more complex (multi-clause) assertions, there would be an additional
+ * automata for each clause.
+ *
+ * Note: non-zero constants.
+ */
+#define CBU_AUTOMATA_SYSCALL 1 /* In a system call. */
+#define CBU_AUTOMATA_MACCHECK 2 /* Call to return automata. */
+#define CBU_AUTOMATA_ASSERTION 3 /* Assertion clause. */
+
+/*
+ * Define the maximum number of instances of the assertion to implement
+ * per-thread. Should be prime, and must be at least 2 so that the system
+ * call automata works. Recursion is not used in the kernel, but if
+ * non-trivial recursion was likely, setting this to a significantly higher
+ * value might make sense.
+ */
+#define CBU_LIMIT 11
+
+/*
+ * Strings used when printing assertion failures.
+ */
+#define CBU_NAME "cbu-%INSTRUMENTED_FN%"
+#define CBU_DESCRIPTION "%ASSERT_FN% without previous %INSTRUMENTED_FN%"
+
+#ifdef _KERNEL
+static eventhandler_tag cbu_event_function_prologue_syscallenter_tag;
+static eventhandler_tag cbu_event_function_prologue_syscallret_tag;
+#endif
*** DIFF OUTPUT TRUNCATED AT 1000 LINES ***
More information about the svn-soc-all
mailing list