Date: Sun, 29 May 2011 20:45:46 +0000 From: shm@FreeBSD.org To: svn-soc-all@FreeBSD.org Subject: 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... Message-ID: <20110529204546.66230106566B@hub.freebsd.org>
index | next in thread | raw e-mail
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 ***help
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20110529204546.66230106566B>