feat(iso-on-tcp): add S7comm ISO-on-TCP carry-buffer reassembly (STORY-186)

CHANGELOG.md

@@ -33,6 +33,29 @@ Version numbers follow [Semantic Versioning](https://semver.org/).
   no S7comm-specific interpretation of the extracted protocol-ID byte.
   Includes a `#[cfg(kani)]` no-panic safety proof harness (VP-049; execution
   deferred to STORY-194).
+- `S7commAnalyzer` (SS-21, `src/analyzer/s7comm.rs`, new module): the
+  effectful shell built on SS-20's stateless TPKT/COTP parsing library,
+  proving directional carry-buffer TPKT reassembly across TCP segment
+  boundaries. `S7commFlowState` holds the per-flow `carry_c2s`/`carry_s2c`
+  buffers (never merged) plus per-direction overflow-reported latches.
+  `on_data` implements walk-first, residual-bound frame extraction: it
+  appends incoming bytes to the directional carry, repeatedly calls
+  `iso_on_tcp::parse_tpkt_header`/`parse_cotp_header` to extract and dispatch
+  complete frames, advances the cursor, and stashes only the leftover
+  partial-frame residual back to carry — never an aggregate
+  `carry.len() + data.len()` pre-check (BC-2.20.013, STORY-186, ADR-014
+  Decision 8). A bad TPKT version byte triggers the shared 1-byte resync
+  sub-routine (BC-2.20.015), reused verbatim for both an ordinary mid-stream
+  reject and post-overflow resync. The residual carry is bounded by
+  `MAX_S7_ISO_ON_TCP_CARRY_BYTES = 65,535` (derived from TPKT's own `u16`
+  length maximum); exceeding it clears the carry and emits one T0814 finding
+  per direction (BC-2.20.014) — retained as a defense-in-depth guard against
+  future design regressions, since it is unreachable via `on_data` under the
+  current walk-first/resync design (BC-2.20.014 v1.1 Invariant 5).
+  `on_flow_close` removes a flow's `S7commFlowState` and discards any
+  carry bytes with no finding emitted (BC-2.21.003). Protocol-specific
+  dispatch on the extracted `protocol_id` is out of scope for this story
+  (STORY-187).
 
 ## [0.13.3] - 2026-09-05
 

docs/adr/0014-s7comm-iso-on-tcp-stream-dispatch-and-parser-design.md

@@ -421,9 +421,10 @@ T0836 (Modify Parameter, `Write Var 0x05` → `0x84`/`0x83`), T0858 (Change Oper
 restart PI-service string), T0888 (Remote System Information Discovery, Userdata
 `0x07`/CPU-group `0x04`/subfn `0x01` Read SZL, or Block-group `0x03`), T0846 (Remote
 System Discovery, multi-host TCP/102 sweep evidence only, not single-PDU), T0814 (Denial
-of Service, connection-flood/malformed-length burst thresholds), T1692.001 (Unauthorized
-Message: Command Message, successor to revoked T0855, any command from an unauthorized
-source).
+of Service, connection-flood/malformed-length burst thresholds — see Decision 8's
+carry-overflow reconciliation note for the carry-overflow trigger specifically),
+T1692.001 (Unauthorized Message: Command Message, successor to revoked T0855, any
+command from an unauthorized source).
 
 **Group-`0x03` block-function correction:** the Userdata (ROSCTR `0x07`) subfunction
 group table must read group `0x03` = **Block functions** (`0x01` List blocks, `0x02`
@@ -553,6 +554,21 @@ to the next `0x03` candidate (drop-and-rescan, not a permanent desync latch), an
 carry-overflow dedup flag, distinct from the malformed-length dedup flag used for
 in-range TPKT-length validation failures.
 
+> **RECONCILIATION NOTE (2026-09-07, STORY-186 adversarial finding F-02; BC-2.20.014
+> v1.1):** A two-independent-pass STORY-186 adversarial gate found this carry-overflow
+> → T0814 branch **unreachable via the real `on_data` path**: BC-2.20.013's walk-first
+> frame extraction and BC-2.20.015's 1-byte resync both consume at least one byte of
+> input on every call, and the TPKT `length` field is u16-capped — so the residual
+> carry stashed back into `carry_c2s`/`carry_s2c` can never exceed 65,534 bytes, one
+> byte below `MAX_S7_ISO_ON_TCP_CARRY_BYTES = 65,535`. Per human ruling (Option B), this
+> paragraph describes a **defense-in-depth, unreachable-by-construction guard** —
+> retained against a future design regression that removed the walk-first/resync
+> per-call consumption guarantee — **not a live, observable runtime detection** under
+> the current design. Product-owner has amended BC-2.20.014 → v1.1 and BC-2.20.013 →
+> v1.1 accordingly. The paragraph above is left as-is as the guard's specified reaction
+> *if* it were ever reached; it must not be read as evidence that T0814 fires from carry
+> overflow in practice today.
+
 ### Decision 9: Pure-core free-fn design for verification amenability
 
 Three functions are pure-core free `fn`s (module scope, not `impl` methods), following
@@ -725,7 +741,7 @@ critical caveat) remains out of scope until F4 (Decision 10).
 | T0816 | Device Restart/Shutdown | Decoded `0x28` restart PI-service | Pre-existing EMITTED (ENIP); add S7comm call-site |
 | T0888 | Remote System Information Discovery | Userdata `0x07`/`0x04`/`0x01` Read SZL; `0x07`/`0x03`/* block-list | Pre-existing EMITTED (Modbus); add S7comm call-site |
 | T0846 | Remote System Discovery | Multi-host TCP/102 sweep evidence only | Pre-existing EMITTED (ENIP); emit only on sweep evidence |
-| T0814 | Denial of Service | Connection flood; malformed-length burst threshold | Pre-existing EMITTED; add S7comm call-site |
+| T0814 | Denial of Service | Connection flood; malformed-length burst threshold | Pre-existing EMITTED; add S7comm call-site (the carry-overflow call-site specifically is defense-in-depth / unreachable-by-construction — see Decision 8's reconciliation note and BC-2.20.014 v1.1) |
 | T1692.001 | Unauthorized Message: Command Message | Any command from a source outside an allowlist | Pre-existing EMITTED; co-tag only with positive unauthorized-source evidence |
 
 CWE set: CWE-306 (no authentication — classic S7comm has none), CWE-319 (cleartext

docs/demo-evidence/STORY-186/AC-001-003-carry-reassembly.tape

@@ -0,0 +1,36 @@
+# STORY-186 AC-186-001/002/003: carry-buffer reassembly, walk-first extraction (BC-2.20.013)
+#
+# Demonstrates:
+#   - test_BC_2_20_013_walk_first_no_aggregate_precheck: no aggregate carry+incoming
+#     pre-check exists anywhere -- the walk always runs first (AC-186-001)
+#   - test_BC_2_20_013_adversarial_burst_head_frame_not_dropped: a complete 7-byte CR
+#     frame followed by 60,000 bytes of trailing garbage in ONE on_data call is still
+#     extracted (anti-evasion property, AC-186-002)
+#   - test_BC_2_20_013_split_frame_across_two_calls: a 4-byte TPKT header delivered in
+#     call 1 is stashed to carry; call 2 completes the 10-byte frame and empties carry
+#     (AC-186-003)
+#
+# Traces to: BC-2.20.013 postconditions 1-2, invariant 1, edge case EC-002
+
+Output AC-001-003-carry-reassembly.gif
+Output AC-001-003-carry-reassembly.webm
+
+Set FontFamily "Menlo"
+Set Theme "Dracula"
+Set Width 1200
+Set Height 500
+Set FontSize 14
+Set Padding 24
+Set Shell "bash"
+Set TypingSpeed 50ms
+
+Require cargo
+
+Type "# AC-186-001/002/003: walk-first carry-buffer reassembly (BC-2.20.013)"
+Enter
+Sleep 300ms
+
+Type "cargo test --test s7comm_analyzer_tests BC_2_20_013 2>&1 | grep -E 'story_186::test|test result:'"
+Enter
+Wait
+Sleep 2s

docs/demo-evidence/STORY-186/AC-004-006-defense-in-depth.tape

@@ -0,0 +1,48 @@
+# STORY-186 AC-186-004/005/006: carry bound + defense-in-depth overflow guard (BC-2.20.014)
+#
+# Demonstrates:
+#   - test_BC_2_20_014_at_bound_residual_no_overflow: residual == 65,535 (the u16::MAX
+#     ceiling) is LIVE, reachable via real on_data traffic -- no overflow fires, strict
+#     '>' not '>=' (AC-186-004, the only reachable-via-on_data case in this group)
+#   - test_BC_2_20_014_overflow_clear_resync_one_t0814_per_direction: [SYNTHETIC] guard
+#     mechanics via direct flow-state injection -- clear-not-truncate, resync, exactly
+#     one T0814 (AC-186-005)
+#   - test_BC_2_20_014_repeated_overflow_dedup_same_direction: [SYNTHETIC] second
+#     injected overflow in the same direction does not re-emit (AC-186-005)
+#   - test_BC_2_20_014_overflow_dedup_independent_per_direction: [SYNTHETIC] c2s and
+#     s2c dedup flags are independent (AC-186-006)
+#   - test_BC_2_20_014_overflow_unreachable_via_on_data: positive on_data-path proof --
+#     a real 200,000-byte non-anchored garbage flood emits NO T0814 and carry stays
+#     bounded <= 65,534 (AC-186-005 positive assertion, VP-050 reachability property)
+#
+# Reclassification: BC-2.20.014 v1.1 (human ruling 2026-09-07, Option B) -- the
+# residual.len() > 65,535 guard is a structural defense-in-depth safety net, provably
+# unreachable via the real on_data data path under BC-2.20.013 walk-first + BC-2.20.015
+# 1-byte-resync (TPKT length is u16-capped, so carry is bounded <= 65,534 by
+# construction). AC-186-004 (at-bound) remains live; AC-186-005/006 (over-bound) are
+# exercised only via direct flow-state injection, named SYNTHETIC below.
+#
+# Traces to: BC-2.20.014 invariant 1, postconditions 1/3/4, edge cases EC-001/EC-004/EC-005
+
+Output AC-004-006-defense-in-depth.gif
+Output AC-004-006-defense-in-depth.webm
+
+Set FontFamily "Menlo"
+Set Theme "Dracula"
+Set Width 1200
+Set Height 560
+Set FontSize 14
+Set Padding 24
+Set Shell "bash"
+Set TypingSpeed 50ms
+
+Require cargo
+
+Type "# AC-186-004 (LIVE at-bound) + AC-186-005/006 (SYNTHETIC guard mechanics) (BC-2.20.014)"
+Enter
+Sleep 300ms
+
+Type "cargo test --test s7comm_analyzer_tests BC_2_20_014 2>&1 | grep -E 'story_186::test|test result:'"
+Enter
+Wait
+Sleep 2s

docs/demo-evidence/STORY-186/AC-007-009-resync.tape

@@ -0,0 +1,37 @@
+# STORY-186 AC-186-007/008/009: 1-byte resync, never 2 (BC-2.20.015)
+#
+# Demonstrates:
+#   - test_BC_2_20_015_resync_advances_exactly_one_byte: bytes
+#     [0x01, 0x03, 0x00, 0x00, 0x07] -- a spurious 0x01 immediately followed by a valid
+#     length=7 frame at offset 1; a 2-byte advance would skip it entirely (AC-186-007)
+#   - test_BC_2_20_015_single_resync_implementation_shared: the same 1-byte-advance
+#     sub-routine is invoked for both bad-version-byte and post-overflow conditions --
+#     exactly one resync implementation, not two (AC-186-008)
+#   - test_BC_2_20_015_resync_terminates_no_valid_anchor: 200 bytes of non-0x03 garbage
+#     with no valid frame anywhere -- resync advances to the end without an infinite
+#     loop (AC-186-009)
+#
+# Traces to: BC-2.20.015 postcondition 1, invariants 1-3
+
+Output AC-007-009-resync.gif
+Output AC-007-009-resync.webm
+
+Set FontFamily "Menlo"
+Set Theme "Dracula"
+Set Width 1200
+Set Height 500
+Set FontSize 14
+Set Padding 24
+Set Shell "bash"
+Set TypingSpeed 50ms
+
+Require cargo
+
+Type "# AC-186-007/008/009: resync advances exactly 1 byte, never 2 (BC-2.20.015)"
+Enter
+Sleep 300ms
+
+Type "cargo test --test s7comm_analyzer_tests BC_2_20_015 2>&1 | grep -E 'story_186::test|test result:'"
+Enter
+Wait
+Sleep 2s

docs/demo-evidence/STORY-186/AC-010-011-module-boundary.tape

@@ -0,0 +1,34 @@
+# STORY-186 AC-186-010/011: frozen SS-20/SS-21 module boundary (BC-2.20.016)
+#
+# Demonstrates:
+#   - test_BC_2_20_016_iso_on_tcp_has_no_stream_analyzer_impl: static regression-guard
+#     confirms src/analyzer/iso_on_tcp.rs contains zero `impl StreamAnalyzer` blocks and
+#     zero DispatchTarget::IsoOnTcp-shaped references (AC-186-010)
+#   - test_BC_2_20_016_no_iso_on_tcp_flow_state_type_exists: static regression-guard
+#     confirms no `IsoOnTcpFlowState` type exists anywhere in the tree -- carry buffers
+#     live exclusively on S7commFlowState (SS-21) (AC-186-011)
+#
+# Traces to: BC-2.20.016 postconditions 1 and 3
+
+Output AC-010-011-module-boundary.gif
+Output AC-010-011-module-boundary.webm
+
+Set FontFamily "Menlo"
+Set Theme "Dracula"
+Set Width 1200
+Set Height 460
+Set FontSize 14
+Set Padding 24
+Set Shell "bash"
+Set TypingSpeed 50ms
+
+Require cargo
+
+Type "# AC-186-010/011: iso_on_tcp.rs frozen module boundary regression guards (BC-2.20.016)"
+Enter
+Sleep 300ms
+
+Type "cargo test --test s7comm_analyzer_tests BC_2_20_016 2>&1 | grep -E 'story_186::test|test result:'"
+Enter
+Wait
+Sleep 2s

docs/demo-evidence/STORY-186/AC-012-flow-close.tape

@@ -0,0 +1,34 @@
+# STORY-186 AC-186-012: on_flow_close teardown + double-close idempotency (BC-2.21.003)
+#
+# Demonstrates:
+#   - test_s7comm_on_flow_close_removes_state_discards_carry: on_flow_close removes
+#     S7commFlowState from the per-flow map and discards carry bytes with no finding
+#     emitted (AC-186-012)
+#   - test_BC_2_21_003_double_close_same_flow_key_is_idempotent_no_op: calling
+#     on_flow_close a second time for the same flow_key (or an unknown flow_key) is a
+#     no-op -- does not panic, does not re-emit
+#
+# Traces to: BC-2.21.003 postconditions 1-4
+
+Output AC-012-flow-close.gif
+Output AC-012-flow-close.webm
+
+Set FontFamily "Menlo"
+Set Theme "Dracula"
+Set Width 1200
+Set Height 460
+Set FontSize 14
+Set Padding 24
+Set Shell "bash"
+Set TypingSpeed 50ms
+
+Require cargo
+
+Type "# AC-186-012: on_flow_close removes state, discards carry, double-close is a no-op (BC-2.21.003)"
+Enter
+Sleep 300ms
+
+Type "cargo test --test s7comm_analyzer_tests close 2>&1 | grep -E 'story_186::test|test result:'"
+Enter
+Wait
+Sleep 2s

docs/demo-evidence/STORY-186/AC-ALL-18-green.tape

@@ -0,0 +1,28 @@
+# STORY-186 full suite: all 18 tests green (15 unit/regression-guard tests + 3 VP-050
+# proptests) across BC-2.20.013/014/015/016 and BC-2.21.003
+#
+# This is the top-level artifact showing the complete s7comm_analyzer_tests.rs suite
+# passing in one run -- every AC-186-001..012 test is represented in this output.
+
+Output AC-ALL-18-green.gif
+Output AC-ALL-18-green.webm
+
+Set FontFamily "Menlo"
+Set Theme "Dracula"
+Set Width 1200
+Set Height 900
+Set FontSize 13
+Set Padding 24
+Set Shell "bash"
+Set TypingSpeed 40ms
+
+Require cargo
+
+Type "# STORY-186: full s7comm_analyzer_tests suite -- 18/18 green"
+Enter
+Sleep 300ms
+
+Type "cargo test --test s7comm_analyzer_tests 2>&1 | grep -E 'running [0-9]+ tests|story_186::|test result:'"
+Enter
+Wait
+Sleep 3s

docs/demo-evidence/STORY-186/VP-050-proptests.tape

@@ -0,0 +1,36 @@
+# STORY-186 VP-050: proptest obligation (direction isolation, walk-first residual bound,
+# resync one-byte-advance) over randomized inputs
+#
+# Demonstrates:
+#   - proptest_vp050_walk_first_residual_bound: carry stays <= MAX_S7_ISO_ON_TCP_CARRY_BYTES
+#     across randomized delivery patterns
+#   - proptest_vp050_direction_isolation: carry_c2s only ever contains C2S-routed bytes,
+#     carry_s2c only ever contains S2C-routed bytes, across 0..300-byte random payloads
+#   - proptest_vp050_resync_one_byte_advance: resync never advances by more than 1 byte
+#     per iteration, across randomized garbage-length inputs
+#
+# Method: proptest (randomized property-based testing, anchored in this story;
+# the full walk-first equivalence property lands in STORY-194)
+
+Output VP-050-proptests.gif
+Output VP-050-proptests.webm
+
+Set FontFamily "Menlo"
+Set Theme "Dracula"
+Set Width 1200
+Set Height 460
+Set FontSize 14
+Set Padding 24
+Set Shell "bash"
+Set TypingSpeed 50ms
+
+Require cargo
+
+Type "# VP-050: proptest harnesses -- direction isolation, walk-first bound, resync advance"
+Enter
+Sleep 300ms
+
+Type "cargo test --test s7comm_analyzer_tests vp050 2>&1 | grep -E 'story_186::vp050|test result:'"
+Enter
+Wait
+Sleep 2s