2026 intern YJ - adding CoAP application example

example/coap/.gitignore

@@ -0,0 +1,8 @@
+# Python
+.venv/
+__pycache__/
+*.pyc
+
+# Regenerated on every run_chaos.sh / run.sh
+trace.txt
+truth.*.log

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
+```

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}"

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 }

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 }

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

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 <<EOF
+Usage: $0 SCENARIO
+
+Scenarios:
+  clean          monotonic SSN, single session                 (silent)
+  renew          establish, send, session_renew, send          (silent)
+  ssn_replay     monotonic then replay SSN=2 (same KID)        (session_ssn fires)
+  loss_no_renew  monotonic then restart SSN=0 (same KID)       (session_ssn fires)
+  stale_kid      renew kid_a -> 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 <trace.txt | tr -d ' ')
+echo "[run] trace.txt: $LINES lines"
+case "$SCENARIO" in
+  ssn_replay|loss_no_renew)
+    echo "[run] check: symon -nf session_ssn.symon    < trace.txt" ;;
+  stale_kid)
+    echo "[run] check: symon -nf session_order.symon  < trace.txt" ;;
+  bad_token)
+    echo "[run] check: symon -nf token_echo.symon     < trace.txt" ;;
+  mid_reuse)
+    echo "[run] check: symon -nf mid_reuse.symon      < trace.txt" ;;
+  clean|renew)
+    echo "[run] check: no violation expected; every monitor should stay silent" ;;
+esac