Date: Thu, 14 Jul 2011 17:51:35 +0000 From: shm@FreeBSD.org To: svn-soc-all@FreeBSD.org Subject: socsvn commit: r224226 - soc2011/shm/TESLA/assertions/80211 Message-ID: <20110714175135.DE6CB1065670@hub.freebsd.org>
next in thread | raw e-mail | index | archive | help
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@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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20110714175135.DE6CB1065670>