socsvn commit: r224226 - soc2011/shm/TESLA/assertions/80211
shm at FreeBSD.org
shm at FreeBSD.org
Thu Jul 14 17:51:38 UTC 2011
Author: shm
Date: Thu Jul 14 17:51:35 2011
New Revision: 224226
URL: http://svnweb.FreeBSD.org/socsvn/?view=rev&rev=224226
Log:
* merged from (soc-g-head)
Added:
soc2011/shm/TESLA/assertions/80211/80211proto.spec
soc2011/shm/TESLA/assertions/80211/80211proto.spl
soc2011/shm/TESLA/assertions/80211/80211proto_assert.c
soc2011/shm/TESLA/assertions/80211/80211proto_automata.c
soc2011/shm/TESLA/assertions/80211/80211proto_defs.h
soc2011/shm/TESLA/assertions/80211/instrumentation.spec
Added: soc2011/shm/TESLA/assertions/80211/80211proto.spec
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto.spec Thu Jul 14 17:51:35 2011 (r224226)
@@ -0,0 +1,10 @@
+field_assign,v,iv_nstate,IEEE80211_S_ASSOC
+field_assign,v,iv_nstate,IEEE80211_S_ASSOC
+field_assign,v,iv_nstate,IEEE80211_S_AUTH
+field_assign,v,iv_nstate,IEEE80211_S_SCAN
+field_assign,v,iv_nstate,IEEE80211_S_AUTH
+field_assign,v,iv_nstate,IEEE80211_S_SCAN
+field_assign,v,iv_nstate,IEEE80211_S_CSA
+field_assign,v,iv_nstate,IEEE80211_S_SLEEP
+field_assign,v,iv_nstate,IEEE80211_S_RUN
+field_assign,v,iv_nstate,IEEE80211_S_INIT
Added: soc2011/shm/TESLA/assertions/80211/80211proto.spl
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto.spl Thu Jul 14 17:51:35 2011 (r224226)
@@ -0,0 +1,31 @@
+/* experimental */
+automaton ieee80211proto() {
+ void main(struct ieee80211vap *v) {
+ v->iv_nstate = IEEE80211_S_INIT;
+ multiple {
+ v->iv_nstate = IEEE80211_S_RUN;
+ either {
+ v->iv_nstate = IEEE80211_S_SLEEP;
+ } or {
+ v->iv_nstate = IEEE80211_S_CSA;
+ } or {
+ v->iv_nstate = IEEE80211_S_SCAN;
+ } or {
+ v->iv_nstate = IEEE80211_S_AUTH;
+ } or {
+ multiple {
+ either {
+ v->iv_nstate = IEEE80211_S_SCAN;
+ } or {
+ v->iv_nstate = IEEE80211_S_AUTH;
+ optional {
+ v->iv_nstate = IEEE80211_S_ASSOC;
+ }
+ }
+ }
+ } or {
+ v->iv_nstate = IEEE80211_S_ASSOC;
+ }
+ }
+ }
+}
Added: soc2011/shm/TESLA/assertions/80211/80211proto_assert.c
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto_assert.c Thu Jul 14 17:51:35 2011 (r224226)
@@ -0,0 +1,104 @@
+/*
+ * Copyright (c) 2011, Mateusz Kocielski <shm at FreeBSD.org>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ */
+
+#include <tesla/tesla_state.h>
+#include <tesla/tesla_util.h>
+#include "80211proto_defs.h"
+
+#include <sys/param.h>
+#include <sys/kernel.h>
+#include <sys/systm.h>
+
+#include <sys/socket.h>
+#include <sys/sockio.h>
+
+#include <net/if.h>
+#include <net/if_media.h>
+#include <net/ethernet.h> /* XXX for ether_sprintf */
+
+#include <net80211/ieee80211_var.h>
+#include <net80211/ieee80211_adhoc.h>
+#include <net80211/ieee80211_sta.h>
+#include <net80211/ieee80211_hostap.h>
+#include <net80211/ieee80211_wds.h>
+#ifdef IEEE80211_SUPPORT_MESH
+#include <net80211/ieee80211_mesh.h>
+#endif
+#include <net80211/ieee80211_monitor.h>
+#include <net80211/ieee80211_input.h>
+
+
+static struct tesla_state *_80211_state;
+
+#define _80211_PROTO_LIMIT 23
+#define _80211_PROTO_NAME "802.11 proto"
+#define _80211_PROTO_DESC \
+ "checks if state transitions is not violating 802.11 proto"
+
+void
+_80211_init(int scope)
+{
+ KASSERT(tesla_state_new(&_80211_state, scope, _80211_PROTO_LIMIT,
+ _80211_PROTO_NAME, _80211_PROTO_DESC) == 0, ("tesla_state_new failed"));
+}
+
+void __tesla_event_function_prologue_ieee80211_new_state(void **t,
+ void *x, int state, int z)
+{
+ struct tesla_instance *tip;
+ int alloc;
+ int event;
+ switch(state)
+ {
+ case IEEE80211_S_AUTH:
+ event = _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_AUTH;
+ break;
+ case IEEE80211_S_RUN:
+ event = _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_RUN;
+ break;
+ case IEEE80211_S_CSA:
+ event = _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_CSA;
+ break;
+ case IEEE80211_S_SLEEP:
+ event = _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SLEEP;
+ break;
+ case IEEE80211_S_SCAN:
+ event = _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SCAN;
+ break;
+ case IEEE80211_S_ASSOC:
+ event = _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_ASSOC;
+ break;
+ case IEEE80211_S_INIT:
+ event = _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_INIT;
+ break;
+ default:
+ KASSERT(0, ("Unknown state"));
+ /*NOTREACHED*/
+ }
+
+ KASSERT(tesla_instance_get1(_80211_state, (register_t)x, &tip, &alloc) ==
+ 0, ("no instances left"));
+
+ if (alloc == 1)
+ _80211proto_automata_init(tip);
+
+ if(_80211proto_automata_prod(tip, event))
+ tesla_assert_fail(_80211_state, tip);
+
+ tesla_instance_put(_80211_state, tip);
+}
+
+void __tesla_event_function_return_ieee80211_new_state(void **t) {}
Added: soc2011/shm/TESLA/assertions/80211/80211proto_automata.c
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto_automata.c Thu Jul 14 17:51:35 2011 (r224226)
@@ -0,0 +1,296 @@
+/*
+ * This file is autogenerated by the Tesla CFA compiler
+ * via: ../../cfa/splc -t tesla -s 80211proto 80211proto.spl
+ */
+
+
+#include <sys/types.h>
+
+#ifdef _KERNEL
+#include <sys/systm.h>
+#else
+#include <assert.h>
+#include <stdlib.h>
+#include <stdint.h>
+#include <string.h>
+#endif
+
+#include <tesla/tesla_state.h>
+#include <tesla/tesla_util.h>
+
+#include "80211proto_defs.h"
+
+struct main {
+ u_int state : 4;
+} __attribute__((__packed__));
+
+#define MAIN_PTR(tip) ((unsigned char *)((tip)->ti_state))
+#define MAIN_STATE(tip,off) ((struct main *)(MAIN_PTR(tip)+(off)+1))
+#define MAIN_NUM_STATES(tip) (MAIN_PTR(tip)[0])
+
+void
+_80211proto_automata_init(struct tesla_instance *tip) {
+ MAIN_NUM_STATES(tip) = 1;
+ MAIN_STATE(tip,0)->state = 2; /* 1 */
+}
+
+int
+_80211proto_automata_prod(struct tesla_instance *tip, u_int event)
+{
+ unsigned char newstate[16];
+ u_int i, curpos=1;
+ struct main tmpstate;
+ bzero(newstate, sizeof(newstate));
+ switch (event) {
+ case 0: /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_AUTH */
+ for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+ switch (MAIN_STATE(tip,i)->state) {
+ case 8:
+ /* event 30 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 30 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 30 -> 28 */
+ tmpstate.state = 1;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 30 -> 30 */
+ tmpstate.state = 8;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 30 -> 32 */
+ tmpstate.state = 10;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ case 9:
+ /* event 18 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 18 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ default:
+ break;
+ }
+ }
+ newstate[0] = curpos-1;
+ if (newstate[0] == 0)
+ return 1; /* TESLA_ERROR */
+ memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+ return 0;
+
+ case 1: /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_RUN */
+ for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+ switch (MAIN_STATE(tip,i)->state) {
+ case 5:
+ /* event 5 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 5 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 5 -> 28 */
+ tmpstate.state = 1;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 5 -> 30 */
+ tmpstate.state = 8;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 5 -> 12 */
+ tmpstate.state = 4;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 5 -> 14 */
+ tmpstate.state = 6;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 5 -> 16 */
+ tmpstate.state = 7;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 5 -> 18 */
+ tmpstate.state = 9;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 5 -> 35 */
+ tmpstate.state = 11;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ default:
+ break;
+ }
+ }
+ newstate[0] = curpos-1;
+ if (newstate[0] == 0)
+ return 1; /* TESLA_ERROR */
+ memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+ return 0;
+
+ case 2: /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_CSA */
+ for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+ switch (MAIN_STATE(tip,i)->state) {
+ case 6:
+ /* event 14 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 14 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ default:
+ break;
+ }
+ }
+ newstate[0] = curpos-1;
+ if (newstate[0] == 0)
+ return 1; /* TESLA_ERROR */
+ memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+ return 0;
+
+ case 3: /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SLEEP */
+ for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+ switch (MAIN_STATE(tip,i)->state) {
+ case 4:
+ /* event 12 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 12 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ default:
+ break;
+ }
+ }
+ newstate[0] = curpos-1;
+ if (newstate[0] == 0)
+ return 1; /* TESLA_ERROR */
+ memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+ return 0;
+
+ case 4: /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SCAN */
+ for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+ switch (MAIN_STATE(tip,i)->state) {
+ case 1:
+ /* event 28 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 28 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 28 -> 28 */
+ tmpstate.state = 1;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 28 -> 30 */
+ tmpstate.state = 8;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ case 7:
+ /* event 16 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 16 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ default:
+ break;
+ }
+ }
+ newstate[0] = curpos-1;
+ if (newstate[0] == 0)
+ return 1; /* TESLA_ERROR */
+ memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+ return 0;
+
+ case 5: /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_ASSOC */
+ for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+ switch (MAIN_STATE(tip,i)->state) {
+ case 10:
+ /* event 32 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 32 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 32 -> 28 */
+ tmpstate.state = 1;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 32 -> 30 */
+ tmpstate.state = 8;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ case 11:
+ /* event 35 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 35 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ default:
+ break;
+ }
+ }
+ newstate[0] = curpos-1;
+ if (newstate[0] == 0)
+ return 1; /* TESLA_ERROR */
+ memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+ return 0;
+
+ case 6: /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_INIT */
+ for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+ switch (MAIN_STATE(tip,i)->state) {
+ case 2:
+ /* event 1 -> 2 */
+ tmpstate.state = 3;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ /* event 1 -> 5 */
+ tmpstate.state = 5;
+ memcpy(&(newstate[curpos]), &tmpstate, 1);
+ curpos++;
+ break;
+ default:
+ break;
+ }
+ }
+ newstate[0] = curpos-1;
+ if (newstate[0] == 0)
+ return 1; /* TESLA_ERROR */
+ memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+ return 0;
+
+ default:
+ return 1; /* TESLA_UNKNOWN_EVENT */
+ }
+}
+
Added: soc2011/shm/TESLA/assertions/80211/80211proto_defs.h
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto_defs.h Thu Jul 14 17:51:35 2011 (r224226)
@@ -0,0 +1,38 @@
+/*
+ * This file is autogenerated by the Tesla CFA compiler
+ * via: ../../cfa/splc -t tesla -s 80211proto 80211proto.spl
+ */
+
+#ifndef _80211PROTO_DEFS_H
+#define _80211PROTO_DEFS_H
+
+#include <sys/types.h>
+
+/*
+ * Names for events that will trigger 80211PROTO rules
+ */
+#define _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_AUTH 0
+#define _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_RUN 1
+#define _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_CSA 2
+#define _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SLEEP 3
+#define _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SCAN 4
+#define _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_ASSOC 5
+#define _80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_INIT 6
+
+/*
+ * Prod the 80211PROTO state machine, return (1) if the assertion failed
+ */
+struct tesla_instance;
+void _80211proto_automata_init(struct tesla_instance *);
+int _80211proto_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 _80211proto_init(int scope);
+void _80211proto_destroy(void);
+void _80211proto_setaction_debug(void);
+#endif
+#endif /* 80211PROTO_DEFS_H */
Added: soc2011/shm/TESLA/assertions/80211/instrumentation.spec
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/instrumentation.spec Thu Jul 14 17:51:35 2011 (r224226)
@@ -0,0 +1 @@
+function,ieee80211_new_state
More information about the svn-soc-all
mailing list