diff --git a/example/coap/.gitignore b/example/coap/.gitignore new file mode 100644 index 0000000..8be46c5 --- /dev/null +++ b/example/coap/.gitignore @@ -0,0 +1,8 @@ +# Python +.venv/ +__pycache__/ +*.pyc + +# Regenerated on every run_chaos.sh / run.sh +trace.txt +truth.*.log diff --git a/example/coap/README.md b/example/coap/README.md new file mode 100644 index 0000000..22fe894 --- /dev/null +++ b/example/coap/README.md @@ -0,0 +1,77 @@ +# CoAP + OSCORE session monitoring with SyMon + +Runtime monitoring of a CoAP / OSCORE-shape server against RFC 7252 +(CoAP) and RFC 8613 (OSCORE). A chaos generator injects violations, +an instrumented aiocoap server captures a mixed wire-layer + +OSCORE-layer trace, and SyMon specs check the trace against six spec +properties. + +## Properties monitored + +| Spec file | Property | RFC | +|---|---|---| +| `con_ack.symon` | Every CON is followed by a matching ACK within the ACK window. | RFC 7252 §4.4, §5.2.2 | +| `mid_reuse.symon` | No two CONs with the same `(src, dest, mid)` after a completed exchange within `EXCHANGE_LIFETIME`. | RFC 7252 §4.5 | +| `retransmit_count.symon` | At most `MAX_RETRANSMIT = 4` retransmissions of the same CON. | RFC 7252 §4.8 | +| `token_echo.symon` | Every response echoes its request's token and uses the flipped endpoints. | RFC 7252 §5.3.1 | +| `session_ssn.symon` | SSN strictly increases within an OSCORE Security Context. Also catches loss-of-mutable-state, wire-indistinguishable from a replay. | RFC 8613 §3.2.2, §7.2.1, §7.5 | +| `session_order.symon` | The rotated-out KID is not used after `session_renew`. | RFC 8613 App. B | + +## Trace format + +Tab-separated: predicate, then string args, then number args, then a +timestamp in seconds since server start. Every `.symon` file shares +an identical 8-signature block covering all events emitted by +`session_server.py`. + +| Predicate | Strings | Numbers | +|-----------------|-------------------------------|--------------| +| `send_CON` | src, dest | mid | +| `send_NON` | src, dest | mid | +| `recv_ACK` | src, dest | mid | +| `send_req` | src, dest, token | mid | +| `send_resp` | src, dest, token | mid, status | +| `session_start` | client, server, kid | — | +| `session_renew` | client, server, old_kid, new_kid | — | +| `oscore_msg` | client, server, kid | ssn | + +## Setup + +```sh +python3 -m venv .venv +./.venv/bin/pip install aiocoap +``` + +The shell runners autodetect `./.venv/` (falling back to `../.venv/`, +then system `python3`). + +## Running + +Single scenario end-to-end: + +```sh +bash run.sh SCENARIO +# SCENARIO ∈ {clean, renew, ssn_replay, loss_no_renew, +# stale_kid, bad_token, mid_reuse} +``` + +Multi-agent chaos, then post-hoc analysis: + +```sh +bash run_chaos.sh # writes trace.txt + truth.*.log +bash check_violations.sh # injected vs caught +``` + +Chaos tunables via env vars: `N_AGENTS`, `STAGGER_STEP`, `DURATION`, +`RATE`, `VIOLATION_PROB`, `CLEAN_BURST`. + +Direct monitor invocation: + +```sh +symon -nf mid_reuse.symon < trace.txt +symon -nf token_echo.symon < trace.txt +symon -nf session_ssn.symon < trace.txt +symon -nf session_order.symon < trace.txt +symon -nf retransmit_count.symon < trace.txt +./con_ack.symon < trace.txt # parametric mode via shebang +``` diff --git a/example/coap/check_violations.sh b/example/coap/check_violations.sh new file mode 100755 index 0000000..b15be81 --- /dev/null +++ b/example/coap/check_violations.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash +# Injected (truth) vs caught (monitors). Run after run_chaos.sh. +set -eo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")" + +echo "=== injection breakdown (truth) ===" +grep -hvE '^#|^$' truth.*.log | awk -F'\t' '{print $3}' | sort | uniq -c + +echo +echo "=== monitor matches ===" +for m in mid_reuse token_echo session_ssn session_order; do + out=$(symon -nf "${m}.symon" < trace.txt 2>&1) + matches=$(echo "$out" | grep -cE '^@') + warns=$(echo "$out" | grep -c '^Undefined' || true) + printf "%-15s matches=%s warnings=%s\n" "$m" "$matches" "$warns" +done + +echo +echo "=== expected vs actual (session_ssn) ===" +# session_ssn.symon catches both ssn_replay AND loss_no_renew: RFC 8613 +# §7.5 treats loss-of-mutable-state as a spec violation, indistinguish- +# able on the wire from a replay (same tuple, non-increasing SSN). +# Each real violation now produces exactly one match. +lnr=$(grep -hvE '^#|^$' truth.*.log | awk -F'\t' '$3 == "loss_no_renew"' | wc -l | tr -d ' ') +sr=$(grep -hvE '^#|^$' truth.*.log | awk -F'\t' '$3 == "ssn_replay"' | wc -l | tr -d ' ') +ssn_matches=$(symon -nf session_ssn.symon < trace.txt 2>/dev/null | grep -cE '^@') +echo " loss_no_renew (${lnr}) + ssn_replay (${sr}) = $((lnr + sr)) vs session_ssn matches: ${ssn_matches}" diff --git a/example/coap/con_ack.symon b/example/coap/con_ack.symon new file mode 100755 index 0000000..432a477 --- /dev/null +++ b/example/coap/con_ack.symon @@ -0,0 +1,44 @@ +#!/usr/bin/env symon -pnf +# Property #1 — CON-ACK matching (RFC 7252 §4.4, §5.2.2). +# +# Every send_CON(src, dest, mid) must be answered by a +# recv_ACK(dest, src, mid) within the ACK window; absence of the +# matching ACK indicates a dropped ACK, an unresponsive server, or a +# response arriving too late. + +var { + seenSrc: string; + seenDest: string; + seenMid: number; + p: param; +} + +signature send_CON { src: string; dest: string; mid: number; } +signature send_NON { src: string; dest: string; mid: number; } +signature recv_ACK { src: string; dest: string; mid: number; } +signature send_req { src: string; dest: string; token: string; mid: number; } +signature send_resp { src: string; dest: string; token: string; mid: number; status: number; } +signature session_start { client: string; server: string; kid: string; } +signature session_renew { client: string; server: string; old_kid: string; new_kid: string; } +signature oscore_msg { client: string; server: string; kid: string; ssn: number; } + +expr saveCON { + send_CON(src, dest, mid | | seenSrc := dest; seenDest := src; seenMid := mid) +} + +expr matchingACK { + recv_ACK(src, dest, mid | src == seenSrc && dest == seenDest && mid = seenMid) +} + +expr noise { + (send_CON(src, dest, mid) || + send_NON(src, dest, mid) || + recv_ACK(src, dest, mid) || + send_req(src, dest, token, mid) || + send_resp(src, dest, token, mid, status) || + session_start(client, server, kid) || + session_renew(client, server, old_kid, new_kid) || + oscore_msg(client, server, kid, ssn))* +} + +(noise; saveCON)%(=p); within (< 5) { noise; matchingACK } diff --git a/example/coap/mid_reuse.symon b/example/coap/mid_reuse.symon new file mode 100644 index 0000000..410523b --- /dev/null +++ b/example/coap/mid_reuse.symon @@ -0,0 +1,44 @@ +# Property #4 — Message ID non-reuse (RFC 7252 §4.5). +# +# For a given (src, dest) pair, the same MID must not be sent in a +# second send_CON within EXCHANGE_LIFETIME (247 s). + +var { + seenSrc: string; + seenDest: string; + seenMid: number; +} + +signature send_CON { src: string; dest: string; mid: number; } +signature send_NON { src: string; dest: string; mid: number; } +signature recv_ACK { src: string; dest: string; mid: number; } +signature send_req { src: string; dest: string; token: string; mid: number; } +signature send_resp { src: string; dest: string; token: string; mid: number; status: number; } +signature session_start { client: string; server: string; kid: string; } +signature session_renew { client: string; server: string; old_kid: string; new_kid: string; } +signature oscore_msg { client: string; server: string; kid: string; ssn: number; } + +expr saveCON { + send_CON(src, dest, mid | | seenSrc := src; seenDest := dest; seenMid := mid) +} + +expr matchingACK { + recv_ACK(src, dest, mid | src == seenDest && dest == seenSrc && mid = seenMid) +} + +expr reuseCON { + send_CON(src, dest, mid | src == seenSrc && dest == seenDest && mid = seenMid) +} + +expr noise { + (send_CON(src, dest, mid) || + send_NON(src, dest, mid) || + recv_ACK(src, dest, mid) || + send_req(src, dest, token, mid) || + send_resp(src, dest, token, mid, status) || + session_start(client, server, kid) || + session_renew(client, server, old_kid, new_kid) || + oscore_msg(client, server, kid, ssn))* +} + +noise; saveCON; within (< 247) { noise; matchingACK; noise; reuseCON } diff --git a/example/coap/retransmit_count.symon b/example/coap/retransmit_count.symon new file mode 100644 index 0000000..bd6f202 --- /dev/null +++ b/example/coap/retransmit_count.symon @@ -0,0 +1,83 @@ +# Property #2 — Retransmission count (RFC 7252 §4.8). +# +# A sender MAY retransmit a CON up to MAX_RETRANSMIT = 4 times before +# giving up. So at most 5 total transmissions of the same +# (src, dest, mid) are legal. The 6th send_CON for the same triple +# within MAX_TRANSMIT_SPAN (~45 s) is a violation. +# +# Time window is EXCHANGE_LIFETIME (~247 s, RFC 7252 §4.8.2): within +# that span every same-(src, dest, mid) belongs to the same exchange; +# beyond it, the MID may be reused legitimately (property #4's concern). + +var { + seenSrc: string; + seenDest: string; + seenMid: number; + total: number; +} + +signature send_CON { src: string; dest: string; mid: number; } +signature send_NON { src: string; dest: string; mid: number; } +signature recv_ACK { src: string; dest: string; mid: number; } +signature send_req { src: string; dest: string; token: string; mid: number; } +signature send_resp { src: string; dest: string; token: string; mid: number; status: number; } +signature session_start { client: string; server: string; kid: string; } +signature session_renew { client: string; server: string; old_kid: string; new_kid: string; } +signature oscore_msg { client: string; server: string; kid: string; ssn: number; } + +expr noise { + (send_CON(src, dest, mid) || + send_NON(src, dest, mid) || + recv_ACK(src, dest, mid) || + send_req(src, dest, token, mid) || + send_resp(src, dest, token, mid, status) || + session_start(client, server, kid) || + session_renew(client, server, old_kid, new_kid) || + oscore_msg(client, server, kid, ssn))* +} + +expr start { + send_CON(src, dest, mid | | + seenSrc := src; seenDest := dest; seenMid := mid; total := 1) +} + +# Any event that cannot be the retransmit we are counting: different +# CoAP tuple, unrelated CoAP layer, or any session/OSCORE event. +expr ignoreOther { + send_req(src, dest, token, mid) || + send_resp(src, dest, token, mid, status) || + send_NON(src, dest, mid) || + send_CON(src, dest, mid | src != seenSrc) || + send_CON(src, dest, mid | dest != seenDest) || + send_CON(src, dest, mid | mid <> seenMid) || + recv_ACK(src, dest, mid | src != seenDest) || + recv_ACK(src, dest, mid | dest != seenSrc) || + recv_ACK(src, dest, mid | mid <> seenMid) || + session_start(client, server, kid) || + session_renew(client, server, old_kid, new_kid) || + oscore_msg(client, server, kid, ssn) +} + +expr addRetransmit { + send_CON(src, dest, mid | + src == seenSrc && dest == seenDest && mid = seenMid | + total := total + 1) +} + +expr violation { + send_CON(src, dest, mid | + src == seenSrc && dest == seenDest && mid = seenMid && total >= 5) +} + +expr main { + noise; + start; + within (< 247) { + zero_or_more { + one_of { ignoreOther } or { addRetransmit } + }; + violation + } +} + +main diff --git a/example/coap/run.sh b/example/coap/run.sh new file mode 100755 index 0000000..e18f49f --- /dev/null +++ b/example/coap/run.sh @@ -0,0 +1,96 @@ +#!/usr/bin/env bash +# One-scenario end-to-end: server + driver + trace.txt. + +set -eo pipefail + +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +cd "$SCRIPT_DIR" + +SERVER_LOG=/tmp/session_server.log +PORT_WAIT=1.0 +COUNT=5 +GAP=0.2 + +usage() { + cat < kid_b, then send under kid_a (session_order fires) + bad_token server echoes wrong token in response (token_echo fires) + mid_reuse two send_CON with same (src, dst, mid) (mid_reuse fires) + +Defaults: count=$COUNT requests, gap=${GAP}s. +Output: trace.txt in $SCRIPT_DIR. + +After running, run whichever monitor(s) match the scenario: + symon -nf session_ssn.symon < trace.txt + symon -nf session_order.symon < trace.txt + symon -nf token_echo.symon < trace.txt + symon -nf mid_reuse.symon < trace.txt + ./con_ack.symon < trace.txt # parametric mode +EOF +} + +# Parse args first so --help works even without Python deps. +if [[ $# -ne 1 ]]; then usage; exit 1; fi +case "$1" in + -h|--help) usage; exit 0 ;; + clean|renew|ssn_replay|loss_no_renew|stale_kid|bad_token|mid_reuse) ;; + *) echo "Unknown scenario: $1" >&2; echo; usage; exit 1 ;; +esac +SCENARIO="$1" + +# Prefer a local venv if present, else system python. +if [[ -x "./.venv/bin/python" ]]; then PYTHON="./.venv/bin/python" +elif [[ -x "../.venv/bin/python" ]]; then PYTHON="../.venv/bin/python" +else PYTHON="python3" +fi + +if ! "$PYTHON" -c 'import aiocoap' 2>/dev/null; then + echo "Error: aiocoap not importable via $PYTHON." >&2 + echo " Install it into a virtualenv (recommended):" >&2 + echo " python3 -m venv .venv && ./.venv/bin/pip install aiocoap" >&2 + echo " Or install into your system Python: pip install aiocoap" >&2 + exit 1 +fi + +existing=$(lsof -ti :5683 2>/dev/null || true) +if [[ -n "$existing" ]]; then + echo "[run] killing leftover :5683 (PID $existing)" + kill $existing 2>/dev/null || true + sleep 0.3 +fi + +echo "[run] scenario=$SCENARIO count=$COUNT gap=$GAP" +"$PYTHON" session_server.py --trace trace.txt >"$SERVER_LOG" 2>&1 & +SERVER_PID=$! +trap "kill $SERVER_PID 2>/dev/null || true" EXIT + +sleep "$PORT_WAIT" + +"$PYTHON" session_driver.py "$SCENARIO" --count "$COUNT" --gap "$GAP" \ + || echo "[run] driver exited non-zero" + +sleep 0.2 +kill "$SERVER_PID" 2>/dev/null || true +wait "$SERVER_PID" 2>/dev/null || true + +LINES=$(wc -l /dev/null; then + echo "Error: aiocoap not importable via $PYTHON." >&2 + echo " Install it into a virtualenv (recommended):" >&2 + echo " python3 -m venv .venv && ./.venv/bin/pip install aiocoap" >&2 + echo " Or install into your system Python: pip install aiocoap" >&2 + exit 1 +fi + +SERVER_LOG=/tmp/session_chaos_server.log + +# Fleet + agent tunables — all overridable via env vars. +N_AGENTS="${N_AGENTS:-5}" +STAGGER_STEP="${STAGGER_STEP:-0.2}" + +# Per-agent chaos knobs (forwarded to session_chaos.py). Empty ⇒ +# use session_chaos.py's own DEFAULT_* fallback for that knob. +DURATION="${DURATION:-}" +RATE="${RATE:-}" +VIOLATION_PROB="${VIOLATION_PROB:-}" +CLEAN_BURST="${CLEAN_BURST:-}" + +extra_args=() +[[ -n "$DURATION" ]] && extra_args+=(--duration "$DURATION") +[[ -n "$RATE" ]] && extra_args+=(--rate "$RATE") +[[ -n "$VIOLATION_PROB" ]] && extra_args+=(--violation-prob "$VIOLATION_PROB") +[[ -n "$CLEAN_BURST" ]] && extra_args+=(--clean-burst "$CLEAN_BURST") + +existing=$(lsof -ti :5683 2>/dev/null || true) +if [[ -n "$existing" ]]; then + echo "[chaos] killing leftover :5683 (PID $existing)" + kill $existing 2>/dev/null || true + sleep 0.3 +fi + +echo "[chaos] launching session_server (log: $SERVER_LOG)" +"$PYTHON" session_server.py --trace trace.txt >"$SERVER_LOG" 2>&1 & +SERVER_PID=$! +trap "kill $SERVER_PID 2>/dev/null || true" EXIT + +for _ in 1 2 3 4 5 6 7 8 9 10; do + lsof -i :5683 >/dev/null 2>&1 && break + sleep 0.2 +done + +echo "[chaos] server ready; launching $N_AGENTS agents" +AGENT_PIDS=() +for ((i=0; i/dev/null || echo 0) + TRUTH_TOTAL=$((TRUTH_TOTAL + n)) +done +echo "[chaos] trace.txt: $TRACE_LINES lines, $N_AGENTS truth logs, $TRUTH_TOTAL total injection records" +echo "[chaos] check: bash check_violations.sh # injected vs caught" diff --git a/example/coap/session_chaos.py b/example/coap/session_chaos.py new file mode 100644 index 0000000..971ad2c --- /dev/null +++ b/example/coap/session_chaos.py @@ -0,0 +1,278 @@ +"""session_chaos.py — randomized multi-agent chaos generator. + +One process per agent, driven by --agent-id. Each iteration either: + - exercises a clean session (establish + a few monotonic messages), or + - injects one of five violations, logged to truth.log for later + comparison against the SyMon monitors. + +All injections are client-side: the server faithfully records whatever +URI query the client sends (see session_server.py), so violations +manifest in the trace as the client-shaped events the SyMon specs +expect. + +Injections: + ssn_replay — replay an earlier SSN within an open session + (RFC 8613 §3.2.2; session_ssn.symon fires) + loss_no_renew — restart SSN at 0 without session_renew, same KID + (§7.5 loss-of-mutable-state; session_ssn.symon fires) + stale_kid — renew kid_a -> kid_b, then send under kid_a + (stale Security Context use; session_order.symon fires) + mid_reuse — two send_CON with the same (src, dst, mid) after + the first exchange's ACK (RFC 7252 §4.5; + mid_reuse.symon fires) + bad_token — server lies about the response token + (RFC 7252 §5.3.1; token_echo.symon fires) +""" + +import argparse +import asyncio +import random +import secrets +import sys +import time + +import aiocoap +from aiocoap.messagemanager import MessageManager + +URI = "coap://127.0.0.1/hello" + +# Defaults for CLI-configurable tunables. Overridable via +# --rate / --violation-prob / --duration / --clean-burst on the +# command line; the actual runtime values end up in every truth +# log's header line so downstream analysis can trust them. +DEFAULT_RATE = 1.0 +DEFAULT_VIOLATION_PROB = 0.4 +DEFAULT_DURATION = 15.0 +DEFAULT_CLEAN_BURST = 3 + +MID_BURST_COUNT = 2 +MID_RANGE = 10000 + +INJECTION_WEIGHTS = { + "ssn_replay": 1.0, + "loss_no_renew": 1.0, + "stale_kid": 1.0, + "mid_reuse": 1.0, + "bad_token": 1.0, +} + + +def new_kid(agent_id): + return f"c{agent_id}_{secrets.token_hex(3)}" + + +async def _send(ctx, kid, ssn, action=None, old_kid=None, timeout=2.0): + query = [f"kid={kid}", f"ssn={ssn}"] + if action is not None: + query.append(f"action={action}") + if old_kid is not None: + query.append(f"old_kid={old_kid}") + msg = aiocoap.Message(code=aiocoap.GET, uri=f"{URI}?{'&'.join(query)}") + try: + await asyncio.wait_for(ctx.request(msg).response, timeout=timeout) + except Exception as e: + print(f"[chaos] send failed ({type(e).__name__}): {e}", file=sys.stderr) + + +class Chaos: + def __init__(self, truth_fh, agent_id, rate, violation_prob, clean_burst): + self.truth = truth_fh + self.agent_id = agent_id + self.rate = rate + self.violation_prob = violation_prob + self.clean_burst = clean_burst + self.start = time.monotonic() + self._mid_base = 1000 + agent_id * MID_RANGE + self._mid = self._mid_base + + def alloc_mid(self): + self._mid += 1 + if self._mid >= self._mid_base + MID_RANGE: + self._mid = self._mid_base + 1 + return self._mid + + def t(self): + return time.monotonic() - self.start + + def log(self, kind, **fields): + bits = "\t".join(f"{k}={v}" for k, v in fields.items()) + self.truth.write(f"{self.t():.6f}\tagent={self.agent_id}\t{kind}\t{bits}\n") + self.truth.flush() + + def pick_injection(self): + names = list(INJECTION_WEIGHTS.keys()) + weights = [INJECTION_WEIGHTS[n] for n in names] + return random.choices(names, weights=weights, k=1)[0] + + async def clean(self, ctx): + kid = new_kid(self.agent_id) + await _send(ctx, kid, 0, action="start") + for i in range(1, self.clean_burst): + await asyncio.sleep(0.1) + await _send(ctx, kid, i) + + async def ssn_replay_inject(self, ctx): + kid = new_kid(self.agent_id) + self.log("ssn_replay", kid=kid) + print(f"[chaos a{self.agent_id}] {self.t():7.2f}s INJECT ssn_replay kid={kid}") + await _send(ctx, kid, 0, action="start") + for i in range(1, 4): + await asyncio.sleep(0.1) + await _send(ctx, kid, i) + await asyncio.sleep(0.1) + await _send(ctx, kid, 2) # replay + + async def loss_no_renew_inject(self, ctx): + kid = new_kid(self.agent_id) + self.log("loss_no_renew", kid=kid) + print(f"[chaos a{self.agent_id}] {self.t():7.2f}s INJECT loss_no_renew kid={kid}") + await _send(ctx, kid, 0, action="start") + for i in range(1, 4): + await asyncio.sleep(0.1) + await _send(ctx, kid, i) + await asyncio.sleep(0.1) + await _send(ctx, kid, 0) # restart, same kid, no renew + + async def stale_kid_inject(self, ctx): + kid_a, kid_b = new_kid(self.agent_id), new_kid(self.agent_id) + self.log("stale_kid", old_kid=kid_a, new_kid=kid_b) + print(f"[chaos a{self.agent_id}] {self.t():7.2f}s INJECT stale_kid {kid_a}->{kid_b}->{kid_a}") + await _send(ctx, kid_a, 0, action="start") + await asyncio.sleep(0.1) + await _send(ctx, kid_a, 1) + await asyncio.sleep(0.1) + await _send(ctx, kid_b, 0, action="renew", old_kid=kid_a) + await asyncio.sleep(0.1) + await _send(ctx, kid_b, 1) + await asyncio.sleep(0.1) + await _send(ctx, kid_a, 99) # stale KID use + + async def bad_token_inject(self, ctx): + """Wire-layer violation: server lies about the response token. + RFC 7252 §5.3.1. Caught by token_echo.symon. One injection = one + request flagged with ?inject=bad_token; one expected match.""" + kid = new_kid(self.agent_id) + self.log("bad_token", kid=kid) + print(f"[chaos a{self.agent_id}] {self.t():7.2f}s INJECT bad_token kid={kid}") + # Use a fresh session so the bad_token request is self-contained + # (session_start + a single oscore_msg, no SSN-class confusion). + await _send(ctx, kid, 0, action="start") + await asyncio.sleep(0.1) + # Pass inject=bad_token alongside the regular session params. + query = f"kid={kid}&ssn=1&inject=bad_token" + msg = aiocoap.Message(code=aiocoap.GET, uri=f"{URI}?{query}") + try: + await asyncio.wait_for(ctx.request(msg).response, timeout=2.0) + except Exception as e: + print(f"[chaos a{self.agent_id}] bad_token send failed: {type(e).__name__}", file=sys.stderr) + + async def mid_reuse_burst_inject(self, ctx): + """Wire-layer violation: two send_CON events with the same + (src, dst, mid) after the first exchange's ACK. RFC 7252 §4.5. + Caught by mid_reuse.symon. + + aiocoap clears any user-set MID before sending (see + messagemanager.py's `_next_message_id`), so the escape hatch + is to spin up a fresh sub-context, monkey-patch its + MessageManager instance so `_next_message_id` returns a fixed + MID, send a short burst under that MID, and tear the + sub-context down. Isolating this to a sub-context keeps the + agent's main context clean for other injections.""" + mid = self.alloc_mid() + kid = new_kid(self.agent_id) + self.log("mid_reuse", kid=kid, mid=mid, count=MID_BURST_COUNT) + print(f"[chaos a{self.agent_id}] {self.t():7.2f}s INJECT mid_reuse kid={kid} mid={mid}") + + burst_ctx = await aiocoap.Context.create_client_context() + try: + for ri in burst_ctx.request_interfaces: + ti = getattr(ri, "token_interface", None) + if isinstance(ti, MessageManager): + ti._next_message_id = lambda m=mid: m + for i in range(MID_BURST_COUNT): + action = "start" if i == 0 else None + query = [f"kid={kid}", f"ssn={i}"] + if action: + query.append(f"action={action}") + msg = aiocoap.Message(code=aiocoap.GET, uri=f"{URI}?{'&'.join(query)}") + try: + await asyncio.wait_for(burst_ctx.request(msg).response, timeout=0.5) + except asyncio.TimeoutError: + pass + await asyncio.sleep(0.3) + finally: + await burst_ctx.shutdown() + + INJECTORS = { + "ssn_replay": ssn_replay_inject, + "loss_no_renew": loss_no_renew_inject, + "stale_kid": stale_kid_inject, + "mid_reuse": mid_reuse_burst_inject, + "bad_token": bad_token_inject, + } + + async def loop(self, duration): + ctx = await aiocoap.Context.create_client_context() + end = self.start + duration if duration > 0 else float("inf") + gap = 1.0 / self.rate + try: + while time.monotonic() < end: + if random.random() < self.violation_prob: + name = self.pick_injection() + await self.INJECTORS[name](self, ctx) + else: + await self.clean(ctx) + await asyncio.sleep(gap) + finally: + await ctx.shutdown() + + +async def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--agent-id", type=int, default=0) + parser.add_argument("--truth", default="truth.log") + parser.add_argument("--duration", type=float, default=DEFAULT_DURATION, + help="Seconds to run before stopping.") + parser.add_argument("--rate", type=float, default=DEFAULT_RATE, + help="Iterations per second (gap = 1/rate).") + parser.add_argument("--violation-prob", type=float, + default=DEFAULT_VIOLATION_PROB, + help="Per-iteration probability of injecting a violation.") + parser.add_argument("--clean-burst", type=int, + default=DEFAULT_CLEAN_BURST, + help="Messages per clean session (SSN 0..clean_burst-1).") + parser.add_argument("--stagger", type=float, default=0.0) + args = parser.parse_args() + + if args.stagger > 0: + await asyncio.sleep(args.stagger) + + with open(args.truth, "w") as truth_fh: + truth_fh.write( + f"# session_chaos agent={args.agent_id} RATE={args.rate} " + f"VIOLATION_PROB={args.violation_prob} DURATION={args.duration} " + f"CLEAN_BURST={args.clean_burst} STAGGER={args.stagger}\n" + f"# weights: {INJECTION_WEIGHTS}\n" + ) + truth_fh.flush() + chaos = Chaos( + truth_fh, + args.agent_id, + rate=args.rate, + violation_prob=args.violation_prob, + clean_burst=args.clean_burst, + ) + print( + f"[chaos a{args.agent_id}] starting " + f"(rate={args.rate} violation_prob={args.violation_prob} " + f"duration={args.duration}s)" + ) + try: + await chaos.loop(args.duration) + except KeyboardInterrupt: + print(f"[chaos a{args.agent_id}] interrupted at {chaos.t():.2f}s") + print(f"[chaos a{args.agent_id}] done; truth log: {args.truth}") + + +if __name__ == "__main__": + asyncio.run(main()) diff --git a/example/coap/session_driver.py b/example/coap/session_driver.py new file mode 100644 index 0000000..a5f4223 --- /dev/null +++ b/example/coap/session_driver.py @@ -0,0 +1,169 @@ +"""Manual scenario driver for session_server.py: pick one OSCORE-shape +scenario, exercise the server end-to-end, exit. Each scenario leaves +a deterministic trace segment SyMon can be run against. Use this for +per-property demos; session_chaos.py is the randomized multi-agent +generator.""" + +import argparse +import asyncio +import secrets +import aiocoap +from aiocoap.messagemanager import MessageManager + +MID_REUSE_FIXED = 12345 + +URI = "coap://127.0.0.1/hello" + + +def new_kid(): + return secrets.token_hex(4) + + +async def _send(ctx, kid, ssn, action=None, old_kid=None): + query = [f"kid={kid}", f"ssn={ssn}"] + if action is not None: + query.append(f"action={action}") + if old_kid is not None: + query.append(f"old_kid={old_kid}") + msg = aiocoap.Message(code=aiocoap.GET, uri=f"{URI}?{'&'.join(query)}") + await ctx.request(msg).response + + +async def drive_clean(ctx, count, gap): + kid = new_kid() + await _send(ctx, kid, 0, action="start") + for i in range(1, count): + await asyncio.sleep(gap) + await _send(ctx, kid, i) + + +async def drive_renew(ctx, count, gap): + half = max(1, count // 2) + kid_a = new_kid() + await _send(ctx, kid_a, 0, action="start") + for i in range(1, half): + await asyncio.sleep(gap) + await _send(ctx, kid_a, i) + + await asyncio.sleep(gap) + kid_b = new_kid() + await _send(ctx, kid_b, 0, action="renew", old_kid=kid_a) + for i in range(1, max(1, count - half)): + await asyncio.sleep(gap) + await _send(ctx, kid_b, i) + + +async def drive_ssn_replay(ctx, count, gap): + kid = new_kid() + await _send(ctx, kid, 0, action="start") + for i in range(1, count): + await asyncio.sleep(gap) + await _send(ctx, kid, i) + await asyncio.sleep(gap) + await _send(ctx, kid, 2) + + +async def drive_loss_no_renew(ctx, count, gap): + kid = new_kid() + await _send(ctx, kid, 0, action="start") + for i in range(1, count): + await asyncio.sleep(gap) + await _send(ctx, kid, i) + await asyncio.sleep(gap) + await _send(ctx, kid, 0) + + +async def drive_bad_token(ctx, count, gap): + kid = new_kid() + await _send(ctx, kid, 0, action="start") + for i in range(1, max(1, count - 1)): + await asyncio.sleep(gap) + await _send(ctx, kid, i) + await asyncio.sleep(gap) + msg = aiocoap.Message( + code=aiocoap.GET, + uri=f"{URI}?kid={kid}&ssn={max(1, count - 1)}&inject=bad_token", + ) + await ctx.request(msg).response + + +async def drive_mid_reuse(ctx, count, gap): + # Fresh sub-context required: monkey-patching _next_message_id on + # the shared ctx would poison every other scenario. See + # aiocoap_gotchas: Message(mid=N) is cleared by the library. + del ctx + kid = new_kid() + burst_ctx = await aiocoap.Context.create_client_context() + try: + for ri in burst_ctx.request_interfaces: + ti = getattr(ri, "token_interface", None) + if isinstance(ti, MessageManager): + ti._next_message_id = lambda m=MID_REUSE_FIXED: m + for i in range(count): + query = [f"kid={kid}", f"ssn={i}"] + if i == 0: + query.append("action=start") + msg = aiocoap.Message( + code=aiocoap.GET, uri=f"{URI}?{'&'.join(query)}" + ) + # Requests 2..N hang until timeout: the server's dedup + # replays the cached response, whose token belongs to + # request 1, so the client can't correlate. Expected. + try: + await asyncio.wait_for( + burst_ctx.request(msg).response, timeout=gap + ) + except asyncio.TimeoutError: + pass + await asyncio.sleep(gap) + finally: + await burst_ctx.shutdown() + + +async def drive_stale_kid(ctx, count, gap): + kid_a = new_kid() + await _send(ctx, kid_a, 0, action="start") + for i in range(1, max(1, count // 2)): + await asyncio.sleep(gap) + await _send(ctx, kid_a, i) + + await asyncio.sleep(gap) + kid_b = new_kid() + await _send(ctx, kid_b, 0, action="renew", old_kid=kid_a) + for i in range(1, max(1, count - count // 2)): + await asyncio.sleep(gap) + await _send(ctx, kid_b, i) + + await asyncio.sleep(gap) + await _send(ctx, kid_a, 99) + + +SCENARIOS = { + "clean": drive_clean, + "renew": drive_renew, + "ssn_replay": drive_ssn_replay, + "loss_no_renew": drive_loss_no_renew, + "stale_kid": drive_stale_kid, + "bad_token": drive_bad_token, + "mid_reuse": drive_mid_reuse, +} + + +async def main(): + parser = argparse.ArgumentParser() + parser.add_argument("scenario", choices=SCENARIOS.keys()) + parser.add_argument("--count", type=int, default=5, + help="Number of messages per session segment.") + parser.add_argument("--gap", type=float, default=0.2, + help="Seconds to sleep between requests.") + args = parser.parse_args() + + ctx = await aiocoap.Context.create_client_context() + try: + await SCENARIOS[args.scenario](ctx, args.count, args.gap) + finally: + await ctx.shutdown() + + +if __name__ == "__main__": + asyncio.run(main()) diff --git a/example/coap/session_order.symon b/example/coap/session_order.symon new file mode 100644 index 0000000..64718a4 --- /dev/null +++ b/example/coap/session_order.symon @@ -0,0 +1,49 @@ +# Stale-KID use after session_renew (RFC 8613 App. B). +# +# After session_renew(client, server, old_kid, new_kid) completes, the +# old Security Context is rotated out. Any subsequent +# oscore_msg(client, server, old_kid, _) is either: +# - a replay of pre-renewal messages, or +# - a sender bug: the peer still holds a stale Security Context and +# is producing fresh messages under the rotated-out KID. +# +# Either way it is a violation: post-renewal, the old KID is dead. + +var { + seenClient: string; + seenServer: string; + seenOldKid: string; +} + +signature send_CON { src: string; dest: string; mid: number; } +signature send_NON { src: string; dest: string; mid: number; } +signature recv_ACK { src: string; dest: string; mid: number; } +signature send_req { src: string; dest: string; token: string; mid: number; } +signature send_resp { src: string; dest: string; token: string; mid: number; status: number; } +signature session_start { client: string; server: string; kid: string; } +signature session_renew { client: string; server: string; old_kid: string; new_kid: string; } +signature oscore_msg { client: string; server: string; kid: string; ssn: number; } + +expr saveRenew { + session_renew(client, server, old_kid, new_kid | | + seenClient := client; seenServer := server; seenOldKid := old_kid) +} + +expr staleKidUse { + oscore_msg(client, server, kid, ssn | + client == seenClient && server == seenServer && + kid == seenOldKid) +} + +expr noise { + (send_CON(src, dest, mid) || + send_NON(src, dest, mid) || + recv_ACK(src, dest, mid) || + send_req(src, dest, token, mid) || + send_resp(src, dest, token, mid, status) || + session_start(client, server, kid) || + session_renew(client, server, old_kid, new_kid) || + oscore_msg(client, server, kid, ssn))* +} + +noise; saveRenew; within (< 86400) { noise; staleKidUse } diff --git a/example/coap/session_server.py b/example/coap/session_server.py new file mode 100644 index 0000000..47ef522 --- /dev/null +++ b/example/coap/session_server.py @@ -0,0 +1,167 @@ +"""OSCORE-shape session server: instrumented aiocoap server emitting a +mixed wire-layer + OSCORE-layer trace for SyMon monitoring. + +Two layers of events in one trace: + - Wire layer: send_CON, send_NON, recv_ACK captured from instance + hooks on aiocoap's MessageManager (dispatch_message and + _send_via_transport). send_req, send_resp captured inside + HelloResource.render_get. The MessageManager hooks sit BELOW + aiocoap's dedup layer, so retransmits and MID reuse appear on the + wire faithfully. + - OSCORE-shape layer: session_start, session_renew, oscore_msg, + driven by URI query parameters (kid, ssn, action, old_kid) that + the client (driver or chaos) sets. The server just faithfully + records what the client claims — a trace-layer simulation, not + real OSCORE cryptography. Good enough for monitor development. + +Trace-layer injection: ?inject=bad_token asks the server to lie about +the response token, letting a client trigger a §5.3.1 violation +without restarting the server. Same trade-off applies: it's a lie in +the trace, not on the wire. + +Predicate signatures (field names match the .symon canon): + send_CON src dest mid # 2 strings, 1 number + send_NON src dest mid # 2 strings, 1 number + recv_ACK src dest mid # 2 strings, 1 number + send_req src dest token mid # 3 strings, 1 number + send_resp src dest token mid status # 3 strings, 2 numbers + session_start client server kid # 3 strings + session_renew client server old_kid new_kid # 4 strings + oscore_msg client server kid ssn # 3 strings, 1 number +""" + +import argparse +import asyncio +import time +import aiocoap +import aiocoap.resource as resource +from aiocoap.numbers.types import Type +from aiocoap.messagemanager import MessageManager + +SERVER_ADDR = "127.0.0.1:5683" + + +class TraceEmitter: + """Owns the trace file and the run-start clock. Passed into the + resource and the MessageManager hooks so no module-level state + escapes main().""" + + def __init__(self, trace_fh, server_addr): + self.fh = trace_fh + self.start = time.monotonic() + self.server_addr = server_addr + + def emit(self, predicate, *strings, nums=()): + if isinstance(nums, int): + nums = (nums,) + t = time.monotonic() - self.start + line = "\t".join( + [predicate, *strings, *(str(n) for n in nums), f"{t:.6f}"] + ) + self.fh.write(line + "\n") + self.fh.flush() + + +def _parse_query(uri_query): + out = {} + for q in uri_query: + if isinstance(q, bytes): + q = q.decode() + if "=" in q: + k, v = q.split("=", 1) + out[k] = v + return out + + +def install_message_layer_hooks(ctx, emitter): + for ri in ctx.request_interfaces: + ti = getattr(ri, "token_interface", None) + if isinstance(ti, MessageManager): + _wrap(ti, emitter) + + +def _wrap(mman, emitter): + original_dispatch = mman.dispatch_message + original_send = mman._send_via_transport + + def traced_dispatch(message): + if message.mtype is Type.CON: + emitter.emit("send_CON", message.remote.hostinfo, + emitter.server_addr, nums=message.mid) + elif message.mtype is Type.NON: + emitter.emit("send_NON", message.remote.hostinfo, + emitter.server_addr, nums=message.mid) + return original_dispatch(message) + + def traced_send(message): + if message.mtype is Type.ACK: + emitter.emit("recv_ACK", emitter.server_addr, + message.remote.hostinfo, nums=message.mid) + return original_send(message) + + mman.dispatch_message = traced_dispatch + mman._send_via_transport = traced_send + + +class HelloResource(resource.Resource): + def __init__(self, emitter): + super().__init__() + self.emitter = emitter + + async def render_get(self, request): + emit = self.emitter.emit + server_addr = self.emitter.server_addr + + client_addr = request.remote.hostinfo + token_hex = request.token.hex() or "00" + mid = request.mid + q = _parse_query(request.opt.uri_query) + + emit("send_req", client_addr, server_addr, token_hex, nums=mid) + + kid = q.get("kid", "00") + ssn = int(q.get("ssn", "0")) + action = q.get("action", "msg") + + if action == "start": + emit("session_start", client_addr, server_addr, kid) + elif action == "renew": + old_kid = q.get("old_kid", "??") + emit("session_renew", client_addr, server_addr, old_kid, kid) + + emit("oscore_msg", client_addr, server_addr, kid, nums=ssn) + + response = aiocoap.Message(payload=b"ok", code=aiocoap.CONTENT) + status = response.code.value if hasattr(response.code, "value") else int(response.code) + # Per-request trace-layer injection: URI-query-driven so + # multi-agent chaos can mix clean and lying responses without + # restarting the server. + resp_token = "BAD!" if q.get("inject") == "bad_token" else token_hex + emit("send_resp", server_addr, client_addr, resp_token, nums=(mid, status)) + return response + + +async def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--trace", default="trace.txt") + args = parser.parse_args() + + with open(args.trace, "w") as trace_fh: + emitter = TraceEmitter(trace_fh, SERVER_ADDR) + root = resource.Site() + root.add_resource(["hello"], HelloResource(emitter)) + ctx = await aiocoap.Context.create_server_context( + root, bind=("127.0.0.1", 5683) + ) + install_message_layer_hooks(ctx, emitter) + print(f"[session_server] writing to {args.trace}") + try: + await asyncio.get_event_loop().create_future() + except asyncio.CancelledError: + pass + finally: + await ctx.shutdown() + + +if __name__ == "__main__": + asyncio.run(main()) diff --git a/example/coap/session_ssn.symon b/example/coap/session_ssn.symon new file mode 100644 index 0000000..5bad206 --- /dev/null +++ b/example/coap/session_ssn.symon @@ -0,0 +1,64 @@ +# Property #9 — OSCORE Sender Sequence Number monotonicity +# (RFC 8613 §3.2.2, §7.2.1). +# +# Within an OSCORE Security Context — identified here by +# (client, server, kid) — the Sender Sequence Number MUST be strictly +# increasing. A receiver that observes a non-increasing SSN with the +# same tuple is seeing either: +# - a replay attack, or +# - a loss-of-mutable-state (§7.5) where the sender resumed without +# re-establishing a new Security Context — itself a spec violation. + +var { + seenClient: string; + seenServer: string; + seenKid: string; + seenSsn: number; +} + +signature send_CON { src: string; dest: string; mid: number; } +signature send_NON { src: string; dest: string; mid: number; } +signature recv_ACK { src: string; dest: string; mid: number; } +signature send_req { src: string; dest: string; token: string; mid: number; } +signature send_resp { src: string; dest: string; token: string; mid: number; status: number; } +signature session_start { client: string; server: string; kid: string; } +signature session_renew { client: string; server: string; old_kid: string; new_kid: string; } +signature oscore_msg { client: string; server: string; kid: string; ssn: number; } + +expr saveMsg { + oscore_msg(client, server, kid, ssn | | + seenClient := client; seenServer := server; + seenKid := kid; seenSsn := ssn) +} + +expr ssnReplay { + oscore_msg(client, server, kid, ssn | + client == seenClient && server == seenServer && + kid == seenKid && ssn <= seenSsn) +} + +expr noise { + (send_CON(src, dest, mid) || + send_NON(src, dest, mid) || + recv_ACK(src, dest, mid) || + send_req(src, dest, token, mid) || + send_resp(src, dest, token, mid, status) || + session_start(client, server, kid) || + session_renew(client, server, old_kid, new_kid) || + oscore_msg(client, server, kid, ssn))* +} + +expr tupleNoise { + (send_CON(src, dest, mid) || + send_NON(src, dest, mid) || + recv_ACK(src, dest, mid) || + send_req(src, dest, token, mid) || + send_resp(src, dest, token, mid, status) || + session_start(client, server, kid) || + session_renew(client, server, old_kid, new_kid) || + oscore_msg(client, server, kid, ssn | client != seenClient) || + oscore_msg(client, server, kid, ssn | server != seenServer) || + oscore_msg(client, server, kid, ssn | kid != seenKid))* +} + +noise; saveMsg; within (< 86400) { tupleNoise; ssnReplay } diff --git a/example/coap/token_echo.symon b/example/coap/token_echo.symon new file mode 100644 index 0000000..3b687c0 --- /dev/null +++ b/example/coap/token_echo.symon @@ -0,0 +1,46 @@ +# Property #5 — Token echo (RFC 7252 §5.3.1). +# +# Every send_resp must carry the same token as its originating +# send_req and use the flipped endpoints. Catches wrong-token +# responses, misrouted replies, and multiplexing bugs where the +# server correlates a response to the wrong outstanding request. + +var { + currToken: string; + exptSrc: string; + exptDest: string; + seenMid: number; +} + +signature send_CON { src: string; dest: string; mid: number; } +signature send_NON { src: string; dest: string; mid: number; } +signature recv_ACK { src: string; dest: string; mid: number; } +signature send_req { src: string; dest: string; token: string; mid: number; } +signature send_resp { src: string; dest: string; token: string; mid: number; status: number; } +signature session_start { client: string; server: string; kid: string; } +signature session_renew { client: string; server: string; old_kid: string; new_kid: string; } +signature oscore_msg { client: string; server: string; kid: string; ssn: number; } + +expr saveReq { + send_req(src, dest, token, mid | | + currToken := token; exptSrc := dest; exptDest := src; seenMid := mid) +} + +expr badResp { + send_resp(src, dest, token, mid, status | mid = seenMid && token != currToken) || + send_resp(src, dest, token, mid, status | mid = seenMid && dest != exptDest) || + send_resp(src, dest, token, mid, status | mid = seenMid && src != exptSrc) +} + +expr noise { + (send_CON(src, dest, mid) || + send_NON(src, dest, mid) || + recv_ACK(src, dest, mid) || + send_req(src, dest, token, mid) || + send_resp(src, dest, token, mid, status) || + session_start(client, server, kid) || + session_renew(client, server, old_kid, new_kid) || + oscore_msg(client, server, kid, ssn))* +} + +noise; saveReq; noise; badResp