From 8b7725913801ebdc7f07cadf7f0ee22272528b0e Mon Sep 17 00:00:00 2001 From: Yeahjun Heo Date: Tue, 14 Jul 2026 02:18:01 +0900 Subject: [PATCH 1/4] 2026 intern YJ - adding CoAP monitoring tests with SyMon --- example/coap/.gitignore | 8 + example/coap/README.md | 78 ++++++++ example/coap/check_violations.sh | 29 +++ example/coap/con_ack.symon | 48 +++++ example/coap/individual_violations.sh | 56 ++++++ example/coap/mid_reuse.symon | 48 +++++ example/coap/retransmit_count.symon | 94 +++++++++ example/coap/run.sh | 97 +++++++++ example/coap/run_chaos.sh | 88 ++++++++ example/coap/run_clients.sh | 20 ++ example/coap/session_chaos.py | 278 ++++++++++++++++++++++++++ example/coap/session_driver.py | 199 ++++++++++++++++++ example/coap/session_order.symon | 57 ++++++ example/coap/session_server.py | 167 ++++++++++++++++ example/coap/session_ssn.symon | 91 +++++++++ example/coap/token_echo.symon | 55 +++++ 16 files changed, 1413 insertions(+) create mode 100644 example/coap/.gitignore create mode 100644 example/coap/README.md create mode 100755 example/coap/check_violations.sh create mode 100755 example/coap/con_ack.symon create mode 100755 example/coap/individual_violations.sh create mode 100644 example/coap/mid_reuse.symon create mode 100644 example/coap/retransmit_count.symon create mode 100755 example/coap/run.sh create mode 100755 example/coap/run_chaos.sh create mode 100755 example/coap/run_clients.sh create mode 100644 example/coap/session_chaos.py create mode 100644 example/coap/session_driver.py create mode 100644 example/coap/session_order.symon create mode 100644 example/coap/session_server.py create mode 100644 example/coap/session_ssn.symon create mode 100644 example/coap/token_echo.symon 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..ab34f5f --- /dev/null +++ b/example/coap/README.md @@ -0,0 +1,78 @@ +# 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 +bash individual_violations.sh # cross-agent isolation proof +``` + +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..4132652 --- /dev/null +++ b/example/coap/check_violations.sh @@ -0,0 +1,29 @@ +#!/usr/bin/env bash +# check_violations.sh — show what got injected, then show what the +# monitors caught. Run after run_chaos.sh has produced trace.txt and +# truth.*.log. +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..e2777a6 --- /dev/null +++ b/example/coap/con_ack.symon @@ -0,0 +1,48 @@ +#!/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. +# +# Requires parametric timing mode (-p) because of `p: param`. +# `p` anchors each match to the timestamp of the saveCON event; the +# within (< 5) block then checks for a matching ACK relative to p. + +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/individual_violations.sh b/example/coap/individual_violations.sh new file mode 100755 index 0000000..4390232 --- /dev/null +++ b/example/coap/individual_violations.sh @@ -0,0 +1,56 @@ +#!/usr/bin/env bash +# individual_violations.sh — cross-agent isolation proof. Show which +# agent injected which violation classes, then find ANY (agent, monitor) +# pair where the agent did NOT inject the violation that monitor +# catches, and prove zero matches for that agent's KIDs in that +# monitor's output. Run after run_chaos.sh. +set -eo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")" + +echo "=== which agents injected which? ===" +for f in truth.*.log; do + a=$(basename "$f" .log | sed 's/truth\.//') + printf "a%s: " "$a" + grep -hvE '^#|^$' "$f" | awk -F'\t' '{print $3}' | sort | uniq -c | tr '\n' '|' + echo +done + +watches_for() { + case "$1" in + token_echo) echo "bad_token" ;; + mid_reuse) echo "mid_reuse" ;; + session_order) echo "stale_kid" ;; + session_ssn) echo "ssn_replay loss_no_renew" ;; + esac +} + +target_agent="" +target_monitor="" +for f in truth.*.log; do + a=$(basename "$f" .log | sed 's/truth\.//') + injected=$(grep -hvE '^#|^$' "$f" | awk -F'\t' '{print $3}' | sort -u) + for m in token_echo mid_reuse session_order session_ssn; do + saw=0 + for kind in $(watches_for "$m"); do + if echo "$injected" | grep -qx "$kind"; then saw=1; break; fi + done + if [[ $saw -eq 0 ]]; then + target_agent="$a" + target_monitor="$m" + break 2 + fi + done +done + +if [[ -z "$target_agent" ]]; then + echo + echo "(every agent injected every monitored class this run; rerun act4)" + exit 0 +fi + +echo +echo "=== isolation proof ===" +echo "agent ${target_agent} did NOT inject anything ${target_monitor} catches" +echo "expected: 0 ${target_monitor} matches with c${target_agent}_ prefix" +n=$(symon -nf "${target_monitor}.symon" < trace.txt 2>/dev/null | grep -c "c${target_agent}_" || true) +echo "actual: ${n}" diff --git a/example/coap/mid_reuse.symon b/example/coap/mid_reuse.symon new file mode 100644 index 0000000..0174935 --- /dev/null +++ b/example/coap/mid_reuse.symon @@ -0,0 +1,48 @@ +# 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). The encoding here +# is slightly stronger than "any two same-MID sends": it requires a +# completed exchange in between (saveCON → matchingACK → reuseCON), +# so genuine retransmissions before the ACK are absorbed by +# retransmit_count.symon rather than double-flagged here. + +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..d6e2e6b --- /dev/null +++ b/example/coap/retransmit_count.symon @@ -0,0 +1,94 @@ +# 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. +# +# Encoding (mirrors example/withdraw/withdraw.symon): +# start — first send_CON; pin (src, dest, mid), set total := 1 +# ignoreOther — any event that is not a matching retransmit +# addRetransmit — send_CON with matching tuple; total := total + 1 +# violation — send_CON with matching tuple AND total >= 5 +# (this is the 6th send overall) +# +# A successful recv_ACK for the saved tuple is NOT consumed by any rule. +# When it arrives the branch dies silently, which is what we want: the +# exchange completed legally so there is no violation to report. +# +# 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..8a0483d --- /dev/null +++ b/example/coap/run.sh @@ -0,0 +1,97 @@ +#!/usr/bin/env bash +# run.sh — launch session_server + session_driver for one scenario, +# then leave trace.txt for SyMon to run against. + +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" +echo " bash individual_violations.sh # cross-agent isolation" diff --git a/example/coap/run_clients.sh b/example/coap/run_clients.sh new file mode 100755 index 0000000..2364ac4 --- /dev/null +++ b/example/coap/run_clients.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +# run_clients.sh — reset state, run the multi-agent chaos, then show +# that the trace grew and that agents interleave (different client +# ports on the first few events). Convenience wrapper around +# run_chaos.sh for demo runs. +set -eo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")" + +echo "=== resetting trace + truth logs ===" +rm -f trace.txt truth.*.log + +echo +echo "=== launching multi-agent chaos (~15s) ===" +bash run_chaos.sh 2>&1 | tail -12 + +echo +echo "=== trace size + one peek at the interleaving ===" +wc -l trace.txt +echo "--- first 6 events (notice the client ports differ) ---" +head -6 trace.txt 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..84b2dc7 --- /dev/null +++ b/example/coap/session_driver.py @@ -0,0 +1,199 @@ +"""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): + """Establish a session and send `count` messages with strictly + increasing SSN. No renewal. Monitor stays silent.""" + 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): + """Establish on kid_a, send half a session, renew to kid_b, send the + rest. Legal: renewal flips the kid and resets SSN. Monitor stays + silent because the saved (kid_a) state and the new (kid_b) stream + don't overlap on kid.""" + 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): + """Send 0..count-1, then send SSN=2 again — same KID, non-increasing. + Violates RFC 8613 §3.2.2 SSN monotonicity. Monitor fires.""" + 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): + """Send 0..count-1, then restart at SSN=0 with the SAME KID — no + session_renew event. Models RFC 8613 §7.5 "loss of mutable Security + Context" where the sender reboots and resumes without rekeying. + Monitor fires; this is the replay-vulnerability footgun §7.5 names.""" + 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): + """Establish a session, then send one request tagged + ?inject=bad_token so the server echoes a wrong token in the + response. Violates RFC 7252 §5.3.1; token_echo.symon fires. + `count` is used to precede the injection with `count - 1` clean + messages so the flagged response is visibly the odd one out.""" + 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): + """Send `count` requests all under the same fixed Message ID. + Violates RFC 7252 §4.5 MID non-reuse; mid_reuse.symon fires. + + aiocoap clears any user-set MID before sending (messagemanager.py + _next_message_id), so the escape hatch is to spin up a fresh + sub-context and monkey-patch its MessageManager instance's + _next_message_id to return a fixed value. Uses per-request + wait_for because after the first exchange the server replays + cached responses (dedup layer) and the client's token correlator + can't match them — subsequent requests hang until timeout, which + is expected here. + + The passed-in `ctx` is unused (a fresh sub-context is required to + isolate the monkey-patch); keeping the signature uniform with the + other scenarios.""" + 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)}" + ) + 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): + """Establish on kid_a, renew to kid_b, then send another message + with kid_a — the rotated-out KID. Violates session_order: post-renewal + use of an old Security Context. Monitor (session_order.symon) fires.""" + 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) + + # The violation: a stray oscore_msg on the rotated-out kid_a. + 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..3632ac1 --- /dev/null +++ b/example/coap/session_order.symon @@ -0,0 +1,57 @@ +# 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. +# +# Encoding mirrors mid_reuse.symon: save the renew, then look for any +# oscore_msg using the now-stale old_kid within the window. +# +# Note (future work): the related "no oscore_msg with kid=K before its +# session_start(K)" property requires checking absence of a past event, +# which SyMon's forward-matching model can't easily express. Parametric +# encoding (or an off-line trace pre-pass) is the likely path. + +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..206350f --- /dev/null +++ b/example/coap/session_ssn.symon @@ -0,0 +1,91 @@ +# 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. +# +# Encoding — "immediately-preceding-msg check": +# saveMsg — pin the (client, server, kid, ssn) of some oscore_msg. +# tupleNoise — same as the global noise expression EXCEPT it refuses +# to skip past another oscore_msg with the same tuple. +# ssnReplay — the very next same-tuple oscore_msg has ssn <= seenSsn. +# +# tupleNoise is what stops the over-matching. With unrestricted noise, +# every earlier msg for the same context anchored an independent check +# against the same replay (24 matches for 4 real replays). By blocking +# noise from swallowing same-tuple msgs, each anchor's check has to +# fire on the very next same-tuple msg — so the only anchor that can +# accept a replay is the one immediately before it. +# +# Trade-off: this catches non-monotonic transitions between adjacent +# msgs, not "any replay ever". Two back-to-back replays in the same +# context would only surface once. In practice — chaos injects a +# single replay per context, and the strict-monotonicity contract is +# only ever broken one step at a time — so this is the right shape. +# Legitimate renewals are absorbed by the kid mismatch (new context ⇒ +# new KID), so session_renew followed by fresh traffic never fires. + +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))* +} + +# Same as noise, but oscore_msg only matches when the tuple DIFFERS +# from the saved (seenClient, seenServer, seenKid). This forces +# ssnReplay to fire on the next same-tuple oscore_msg — no skipping. +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))* +} + +# 1-day within bound is a SyMon-syntactic finite window; OSCORE has +# no spec-level "OK to replay after T" cutoff — strict monotonicity +# holds for the entire context lifetime. +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..16d1e6d --- /dev/null +++ b/example/coap/token_echo.symon @@ -0,0 +1,55 @@ +# 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. +# +# The badResp checks bind on the SAVED mid so we only inspect the +# response that belongs to this saveReq. Without the mid constraint, +# intervening noise lets the matcher pair unrelated req/resp pairs +# and flag every clean send_resp whose token differs from the last +# saveReq's (produced ~38k false positives in an early run). + +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))* +} + +# Internal noise between saveReq and badResp lets the matcher skip past +# session-layer events (session_start, oscore_msg, ...) that +# session_server.py emits between send_req and send_resp. +noise; saveReq; noise; badResp From ecb076d313f141ad24046a39fe984fcdd902bd29 Mon Sep 17 00:00:00 2001 From: Yeahjun Heo Date: Tue, 14 Jul 2026 02:31:54 +0900 Subject: [PATCH 2/4] trimmed down on comments to clear out fluff --- example/coap/check_violations.sh | 4 +-- example/coap/con_ack.symon | 4 --- example/coap/individual_violations.sh | 6 +--- example/coap/mid_reuse.symon | 6 +--- example/coap/retransmit_count.symon | 11 ------- example/coap/run.sh | 3 +- example/coap/run_chaos.sh | 6 +--- example/coap/run_clients.sh | 5 +--- example/coap/session_driver.py | 42 ++++----------------------- example/coap/session_order.symon | 8 ----- example/coap/session_ssn.symon | 27 ----------------- example/coap/token_echo.symon | 9 ------ 12 files changed, 12 insertions(+), 119 deletions(-) diff --git a/example/coap/check_violations.sh b/example/coap/check_violations.sh index 4132652..b15be81 100755 --- a/example/coap/check_violations.sh +++ b/example/coap/check_violations.sh @@ -1,7 +1,5 @@ #!/usr/bin/env bash -# check_violations.sh — show what got injected, then show what the -# monitors caught. Run after run_chaos.sh has produced trace.txt and -# truth.*.log. +# Injected (truth) vs caught (monitors). Run after run_chaos.sh. set -eo pipefail cd "$(dirname "${BASH_SOURCE[0]}")" diff --git a/example/coap/con_ack.symon b/example/coap/con_ack.symon index e2777a6..432a477 100755 --- a/example/coap/con_ack.symon +++ b/example/coap/con_ack.symon @@ -5,10 +5,6 @@ # 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. -# -# Requires parametric timing mode (-p) because of `p: param`. -# `p` anchors each match to the timestamp of the saveCON event; the -# within (< 5) block then checks for a matching ACK relative to p. var { seenSrc: string; diff --git a/example/coap/individual_violations.sh b/example/coap/individual_violations.sh index 4390232..b831b02 100755 --- a/example/coap/individual_violations.sh +++ b/example/coap/individual_violations.sh @@ -1,9 +1,5 @@ #!/usr/bin/env bash -# individual_violations.sh — cross-agent isolation proof. Show which -# agent injected which violation classes, then find ANY (agent, monitor) -# pair where the agent did NOT inject the violation that monitor -# catches, and prove zero matches for that agent's KIDs in that -# monitor's output. Run after run_chaos.sh. +# Cross-agent isolation proof. Run after run_chaos.sh. set -eo pipefail cd "$(dirname "${BASH_SOURCE[0]}")" diff --git a/example/coap/mid_reuse.symon b/example/coap/mid_reuse.symon index 0174935..410523b 100644 --- a/example/coap/mid_reuse.symon +++ b/example/coap/mid_reuse.symon @@ -1,11 +1,7 @@ # 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). The encoding here -# is slightly stronger than "any two same-MID sends": it requires a -# completed exchange in between (saveCON → matchingACK → reuseCON), -# so genuine retransmissions before the ACK are absorbed by -# retransmit_count.symon rather than double-flagged here. +# second send_CON within EXCHANGE_LIFETIME (247 s). var { seenSrc: string; diff --git a/example/coap/retransmit_count.symon b/example/coap/retransmit_count.symon index d6e2e6b..bd6f202 100644 --- a/example/coap/retransmit_count.symon +++ b/example/coap/retransmit_count.symon @@ -5,17 +5,6 @@ # (src, dest, mid) are legal. The 6th send_CON for the same triple # within MAX_TRANSMIT_SPAN (~45 s) is a violation. # -# Encoding (mirrors example/withdraw/withdraw.symon): -# start — first send_CON; pin (src, dest, mid), set total := 1 -# ignoreOther — any event that is not a matching retransmit -# addRetransmit — send_CON with matching tuple; total := total + 1 -# violation — send_CON with matching tuple AND total >= 5 -# (this is the 6th send overall) -# -# A successful recv_ACK for the saved tuple is NOT consumed by any rule. -# When it arrives the branch dies silently, which is what we want: the -# exchange completed legally so there is no violation to report. -# # 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). diff --git a/example/coap/run.sh b/example/coap/run.sh index 8a0483d..e18f49f 100755 --- a/example/coap/run.sh +++ b/example/coap/run.sh @@ -1,6 +1,5 @@ #!/usr/bin/env bash -# run.sh — launch session_server + session_driver for one scenario, -# then leave trace.txt for SyMon to run against. +# One-scenario end-to-end: server + driver + trace.txt. set -eo pipefail diff --git a/example/coap/run_chaos.sh b/example/coap/run_chaos.sh index f434caf..be0b4b1 100755 --- a/example/coap/run_chaos.sh +++ b/example/coap/run_chaos.sh @@ -1,9 +1,5 @@ #!/usr/bin/env bash -# run_chaos.sh — launch session_server + N parallel session_chaos agents. -# Each agent gets its own truth log; trace.txt is the single shared trace -# the server writes (each event tagged with the agent's ephemeral port -# via remote.hostinfo). The session_ssn / session_order monitors key on -# (client, server, kid), so interleaved per-agent streams stay disjoint. +# N parallel chaos agents against one server; per-agent truth.i.log. set -eo pipefail diff --git a/example/coap/run_clients.sh b/example/coap/run_clients.sh index 2364ac4..91fb745 100755 --- a/example/coap/run_clients.sh +++ b/example/coap/run_clients.sh @@ -1,8 +1,5 @@ #!/usr/bin/env bash -# run_clients.sh — reset state, run the multi-agent chaos, then show -# that the trace grew and that agents interleave (different client -# ports on the first few events). Convenience wrapper around -# run_chaos.sh for demo runs. +# Reset state, run multi-agent chaos, peek at the interleaved trace. set -eo pipefail cd "$(dirname "${BASH_SOURCE[0]}")" diff --git a/example/coap/session_driver.py b/example/coap/session_driver.py index 84b2dc7..a5f4223 100644 --- a/example/coap/session_driver.py +++ b/example/coap/session_driver.py @@ -30,8 +30,6 @@ async def _send(ctx, kid, ssn, action=None, old_kid=None): async def drive_clean(ctx, count, gap): - """Establish a session and send `count` messages with strictly - increasing SSN. No renewal. Monitor stays silent.""" kid = new_kid() await _send(ctx, kid, 0, action="start") for i in range(1, count): @@ -40,10 +38,6 @@ async def drive_clean(ctx, count, gap): async def drive_renew(ctx, count, gap): - """Establish on kid_a, send half a session, renew to kid_b, send the - rest. Legal: renewal flips the kid and resets SSN. Monitor stays - silent because the saved (kid_a) state and the new (kid_b) stream - don't overlap on kid.""" half = max(1, count // 2) kid_a = new_kid() await _send(ctx, kid_a, 0, action="start") @@ -60,8 +54,6 @@ async def drive_renew(ctx, count, gap): async def drive_ssn_replay(ctx, count, gap): - """Send 0..count-1, then send SSN=2 again — same KID, non-increasing. - Violates RFC 8613 §3.2.2 SSN monotonicity. Monitor fires.""" kid = new_kid() await _send(ctx, kid, 0, action="start") for i in range(1, count): @@ -72,10 +64,6 @@ async def drive_ssn_replay(ctx, count, gap): async def drive_loss_no_renew(ctx, count, gap): - """Send 0..count-1, then restart at SSN=0 with the SAME KID — no - session_renew event. Models RFC 8613 §7.5 "loss of mutable Security - Context" where the sender reboots and resumes without rekeying. - Monitor fires; this is the replay-vulnerability footgun §7.5 names.""" kid = new_kid() await _send(ctx, kid, 0, action="start") for i in range(1, count): @@ -86,11 +74,6 @@ async def drive_loss_no_renew(ctx, count, gap): async def drive_bad_token(ctx, count, gap): - """Establish a session, then send one request tagged - ?inject=bad_token so the server echoes a wrong token in the - response. Violates RFC 7252 §5.3.1; token_echo.symon fires. - `count` is used to precede the injection with `count - 1` clean - messages so the flagged response is visibly the odd one out.""" kid = new_kid() await _send(ctx, kid, 0, action="start") for i in range(1, max(1, count - 1)): @@ -105,21 +88,9 @@ async def drive_bad_token(ctx, count, gap): async def drive_mid_reuse(ctx, count, gap): - """Send `count` requests all under the same fixed Message ID. - Violates RFC 7252 §4.5 MID non-reuse; mid_reuse.symon fires. - - aiocoap clears any user-set MID before sending (messagemanager.py - _next_message_id), so the escape hatch is to spin up a fresh - sub-context and monkey-patch its MessageManager instance's - _next_message_id to return a fixed value. Uses per-request - wait_for because after the first exchange the server replays - cached responses (dedup layer) and the client's token correlator - can't match them — subsequent requests hang until timeout, which - is expected here. - - The passed-in `ctx` is unused (a fresh sub-context is required to - isolate the monkey-patch); keeping the signature uniform with the - other scenarios.""" + # 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() @@ -135,6 +106,9 @@ async def drive_mid_reuse(ctx, count, gap): 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 @@ -147,9 +121,6 @@ async def drive_mid_reuse(ctx, count, gap): async def drive_stale_kid(ctx, count, gap): - """Establish on kid_a, renew to kid_b, then send another message - with kid_a — the rotated-out KID. Violates session_order: post-renewal - use of an old Security Context. Monitor (session_order.symon) fires.""" kid_a = new_kid() await _send(ctx, kid_a, 0, action="start") for i in range(1, max(1, count // 2)): @@ -163,7 +134,6 @@ async def drive_stale_kid(ctx, count, gap): await asyncio.sleep(gap) await _send(ctx, kid_b, i) - # The violation: a stray oscore_msg on the rotated-out kid_a. await asyncio.sleep(gap) await _send(ctx, kid_a, 99) diff --git a/example/coap/session_order.symon b/example/coap/session_order.symon index 3632ac1..64718a4 100644 --- a/example/coap/session_order.symon +++ b/example/coap/session_order.symon @@ -8,14 +8,6 @@ # is producing fresh messages under the rotated-out KID. # # Either way it is a violation: post-renewal, the old KID is dead. -# -# Encoding mirrors mid_reuse.symon: save the renew, then look for any -# oscore_msg using the now-stale old_kid within the window. -# -# Note (future work): the related "no oscore_msg with kid=K before its -# session_start(K)" property requires checking absence of a past event, -# which SyMon's forward-matching model can't easily express. Parametric -# encoding (or an off-line trace pre-pass) is the likely path. var { seenClient: string; diff --git a/example/coap/session_ssn.symon b/example/coap/session_ssn.symon index 206350f..5bad206 100644 --- a/example/coap/session_ssn.symon +++ b/example/coap/session_ssn.symon @@ -8,27 +8,6 @@ # - 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. -# -# Encoding — "immediately-preceding-msg check": -# saveMsg — pin the (client, server, kid, ssn) of some oscore_msg. -# tupleNoise — same as the global noise expression EXCEPT it refuses -# to skip past another oscore_msg with the same tuple. -# ssnReplay — the very next same-tuple oscore_msg has ssn <= seenSsn. -# -# tupleNoise is what stops the over-matching. With unrestricted noise, -# every earlier msg for the same context anchored an independent check -# against the same replay (24 matches for 4 real replays). By blocking -# noise from swallowing same-tuple msgs, each anchor's check has to -# fire on the very next same-tuple msg — so the only anchor that can -# accept a replay is the one immediately before it. -# -# Trade-off: this catches non-monotonic transitions between adjacent -# msgs, not "any replay ever". Two back-to-back replays in the same -# context would only surface once. In practice — chaos injects a -# single replay per context, and the strict-monotonicity contract is -# only ever broken one step at a time — so this is the right shape. -# Legitimate renewals are absorbed by the kid mismatch (new context ⇒ -# new KID), so session_renew followed by fresh traffic never fires. var { seenClient: string; @@ -69,9 +48,6 @@ expr noise { oscore_msg(client, server, kid, ssn))* } -# Same as noise, but oscore_msg only matches when the tuple DIFFERS -# from the saved (seenClient, seenServer, seenKid). This forces -# ssnReplay to fire on the next same-tuple oscore_msg — no skipping. expr tupleNoise { (send_CON(src, dest, mid) || send_NON(src, dest, mid) || @@ -85,7 +61,4 @@ expr tupleNoise { oscore_msg(client, server, kid, ssn | kid != seenKid))* } -# 1-day within bound is a SyMon-syntactic finite window; OSCORE has -# no spec-level "OK to replay after T" cutoff — strict monotonicity -# holds for the entire context lifetime. noise; saveMsg; within (< 86400) { tupleNoise; ssnReplay } diff --git a/example/coap/token_echo.symon b/example/coap/token_echo.symon index 16d1e6d..3b687c0 100644 --- a/example/coap/token_echo.symon +++ b/example/coap/token_echo.symon @@ -4,12 +4,6 @@ # 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. -# -# The badResp checks bind on the SAVED mid so we only inspect the -# response that belongs to this saveReq. Without the mid constraint, -# intervening noise lets the matcher pair unrelated req/resp pairs -# and flag every clean send_resp whose token differs from the last -# saveReq's (produced ~38k false positives in an early run). var { currToken: string; @@ -49,7 +43,4 @@ expr noise { oscore_msg(client, server, kid, ssn))* } -# Internal noise between saveReq and badResp lets the matcher skip past -# session-layer events (session_start, oscore_msg, ...) that -# session_server.py emits between send_req and send_resp. noise; saveReq; noise; badResp From 71a1cb16dc6c5f63527eed34325b9a4c0c2c54e9 Mon Sep 17 00:00:00 2001 From: Yeahjun Heo Date: Tue, 14 Jul 2026 13:44:54 +0900 Subject: [PATCH 3/4] deleted some scripts not significant --- example/coap/individual_violations.sh | 52 --------------------------- example/coap/run_clients.sh | 17 --------- 2 files changed, 69 deletions(-) delete mode 100755 example/coap/individual_violations.sh delete mode 100755 example/coap/run_clients.sh diff --git a/example/coap/individual_violations.sh b/example/coap/individual_violations.sh deleted file mode 100755 index b831b02..0000000 --- a/example/coap/individual_violations.sh +++ /dev/null @@ -1,52 +0,0 @@ -#!/usr/bin/env bash -# Cross-agent isolation proof. Run after run_chaos.sh. -set -eo pipefail -cd "$(dirname "${BASH_SOURCE[0]}")" - -echo "=== which agents injected which? ===" -for f in truth.*.log; do - a=$(basename "$f" .log | sed 's/truth\.//') - printf "a%s: " "$a" - grep -hvE '^#|^$' "$f" | awk -F'\t' '{print $3}' | sort | uniq -c | tr '\n' '|' - echo -done - -watches_for() { - case "$1" in - token_echo) echo "bad_token" ;; - mid_reuse) echo "mid_reuse" ;; - session_order) echo "stale_kid" ;; - session_ssn) echo "ssn_replay loss_no_renew" ;; - esac -} - -target_agent="" -target_monitor="" -for f in truth.*.log; do - a=$(basename "$f" .log | sed 's/truth\.//') - injected=$(grep -hvE '^#|^$' "$f" | awk -F'\t' '{print $3}' | sort -u) - for m in token_echo mid_reuse session_order session_ssn; do - saw=0 - for kind in $(watches_for "$m"); do - if echo "$injected" | grep -qx "$kind"; then saw=1; break; fi - done - if [[ $saw -eq 0 ]]; then - target_agent="$a" - target_monitor="$m" - break 2 - fi - done -done - -if [[ -z "$target_agent" ]]; then - echo - echo "(every agent injected every monitored class this run; rerun act4)" - exit 0 -fi - -echo -echo "=== isolation proof ===" -echo "agent ${target_agent} did NOT inject anything ${target_monitor} catches" -echo "expected: 0 ${target_monitor} matches with c${target_agent}_ prefix" -n=$(symon -nf "${target_monitor}.symon" < trace.txt 2>/dev/null | grep -c "c${target_agent}_" || true) -echo "actual: ${n}" diff --git a/example/coap/run_clients.sh b/example/coap/run_clients.sh deleted file mode 100755 index 91fb745..0000000 --- a/example/coap/run_clients.sh +++ /dev/null @@ -1,17 +0,0 @@ -#!/usr/bin/env bash -# Reset state, run multi-agent chaos, peek at the interleaved trace. -set -eo pipefail -cd "$(dirname "${BASH_SOURCE[0]}")" - -echo "=== resetting trace + truth logs ===" -rm -f trace.txt truth.*.log - -echo -echo "=== launching multi-agent chaos (~15s) ===" -bash run_chaos.sh 2>&1 | tail -12 - -echo -echo "=== trace size + one peek at the interleaving ===" -wc -l trace.txt -echo "--- first 6 events (notice the client ports differ) ---" -head -6 trace.txt From d629c769cfd4fe6fdb921e051e2433e82313476a Mon Sep 17 00:00:00 2001 From: Yeahjun Heo Date: Wed, 15 Jul 2026 14:54:40 +0900 Subject: [PATCH 4/4] stripped references to a deleted script --- example/coap/README.md | 1 - example/coap/run_chaos.sh | 1 - 2 files changed, 2 deletions(-) diff --git a/example/coap/README.md b/example/coap/README.md index ab34f5f..22fe894 100644 --- a/example/coap/README.md +++ b/example/coap/README.md @@ -60,7 +60,6 @@ Multi-agent chaos, then post-hoc analysis: ```sh bash run_chaos.sh # writes trace.txt + truth.*.log bash check_violations.sh # injected vs caught -bash individual_violations.sh # cross-agent isolation proof ``` Chaos tunables via env vars: `N_AGENTS`, `STAGGER_STEP`, `DURATION`, diff --git a/example/coap/run_chaos.sh b/example/coap/run_chaos.sh index be0b4b1..375a0c9 100755 --- a/example/coap/run_chaos.sh +++ b/example/coap/run_chaos.sh @@ -81,4 +81,3 @@ for ((i=0; i