feat(iso-on-tcp): add RFC 1006 TPKT header parser (STORY-184)

CHANGELOG.md

@@ -7,6 +7,21 @@ Version numbers follow [Semantic Versioning](https://semver.org/).
 
 ## [Unreleased]
 
+### Added
+
+- S7comm ISO-on-TCP framing groundwork: `parse_tpkt_header` in the new
+  `src/analyzer/iso_on_tcp.rs` module parses the 4-byte RFC 1006 TPKT header
+  (version byte, big-endian `u16` total length), returning `None` for
+  under-length input, a non-`0x03` version byte (checked before length decode,
+  the SS-20 resync anchor), or a decoded length below RFC 1006 §6's stated
+  minimum packet length of 7 (4-byte TPKT header + 3-byte minimum COTP) —
+  accept range is `[7, 65535]` (BC-2.20.001-004, STORY-184, ADR-014). This is
+  a standalone, protocol-agnostic pure-core free function — no
+  `StreamAnalyzer` impl, no per-flow state — laying the framing groundwork
+  ahead of the COTP header parser (STORY-185) and the S7comm PDU dissector
+  (STORY-186). Includes a `#[cfg(kani)]` no-panic safety proof harness
+  (VP-048; execution deferred to STORY-194).
+
 ## [0.13.3] - 2026-09-05
 
 ### Changed

CLAUDE.md

@@ -253,7 +253,7 @@ Deferred or open findings — STATE.md Drift Items, spec contradictions, and rev
 | Path | Purpose |
 |------|---------|
 | `README.md` | Project overview |
-| `docs/adr/` | Architecture Decision Records (0001 stream dispatch, 0002 modular analyzers, 0003 reporting pipeline, 0004 process-wide warning atomics, 0005 binary ICS protocol integration, 0006 multi-technique finding attribution, 0007 DNP3 stream dispatch and parser design, 0009 pcapng reader design, 0010 EtherNet/IP CIP stream dispatch, 0011 TLS handshake reassembly, 0012 protocols catalog and coverage-gaps system, 0013 IEC-104 stream dispatch and parser design; 0008 is intentionally absent from this list — `docs/adr/0008-withdrawn-placeholder.md` exists on disk as a withdrawn placeholder stub, kept only to reserve the ID) |
+| `docs/adr/` | Architecture Decision Records (0001 stream dispatch, 0002 modular analyzers, 0003 reporting pipeline, 0004 process-wide warning atomics, 0005 binary ICS protocol integration, 0006 multi-technique finding attribution, 0007 DNP3 stream dispatch and parser design, 0009 pcapng reader design, 0010 EtherNet/IP CIP stream dispatch, 0011 TLS handshake reassembly, 0012 protocols catalog and coverage-gaps system, 0013 IEC-104 stream dispatch and parser design, 0014 S7comm over ISO-on-TCP (TPKT/COTP) stream dispatch and parser design — `proposed`, port-102 model = Support enum, ratified (Decision 3: per-entry `Support` enum {Supported, KnownUnsupported, DetectionOnly} on `KnownProtocol`, human-ratified 2026-09-06, supersedes original name-keyed-exclusion-list recommendation); 0008 is intentionally absent from this list — `docs/adr/0008-withdrawn-placeholder.md` exists on disk as a withdrawn placeholder stub, kept only to reserve the ID) |
 | `docs/superpowers/plans/` | Implementation plans (from the superpowers skill) |
 | `docs/superpowers/specs/` | Specifications (from the superpowers skill) |
 | `.github/workflows/ci.yml` | CI pipeline (test, clippy, fmt, semantic PR) |

docs/demo-evidence/STORY-184/AC-001-short-input-rejection.md

@@ -0,0 +1,76 @@
+# AC-184-001 — `parse_tpkt_header` Returns None for Input Shorter Than 4 Bytes
+
+**Story:** STORY-184: S7comm TPKT Core Parser: `parse_tpkt_header` Pure-Core Free
+Function + VP-048 Kani Skeleton
+**AC:** AC-184-001
+**Traces to:** BC-2.20.001 postconditions 1–3
+**Wave:** 87
+
+---
+
+## Acceptance Criterion
+
+- Given a `&[u8]` slice with `data.len() < 4` (including empty, 1-byte, 3-byte slices)
+- When `parse_tpkt_header(data)` is called
+- Then returns `None` without accessing any byte in `data`; no panics
+  (traces to BC-2.20.001 postcondition 2)
+
+---
+
+## Test Suite Execution
+
+Command:
+```
+cargo test --test iso_on_tcp_tests BC_2_20_001
+```
+
+Output:
+```
+    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s
+     Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...)
+
+running 5 tests
+test story_184::test_BC_2_20_001_invariant_no_panic_on_truncated_inputs ... ok
+test story_184::test_BC_2_20_001_returns_none_for_empty_slice ... ok
+test story_184::test_BC_2_20_001_returns_none_for_one_byte ... ok
+test story_184::test_BC_2_20_001_returns_none_for_three_bytes_canonical_vector ... ok
+test story_184::test_BC_2_20_001_returns_none_for_two_bytes ... ok
+
+test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 25 filtered out; finished in 0.00s
+```
+
+Result: **5/5 PASS**
+
+---
+
+## Test Coverage
+
+| Test Name | Canonical Vector | Condition Exercised | Result |
+|-----------|-------------------|----------------------|--------|
+| `test_BC_2_20_001_returns_none_for_empty_slice` | `[]` (0 bytes) | len=0 < 4 | PASS |
+| `test_BC_2_20_001_returns_none_for_one_byte` | `[0x03]` | len=1 < 4, even with valid version byte | PASS |
+| `test_BC_2_20_001_returns_none_for_two_bytes` | `[0x03, 0x00]` | len=2 < 4 | PASS |
+| `test_BC_2_20_001_returns_none_for_three_bytes_canonical_vector` | `[0x03, 0x00, 0x00]` | len=3 < 4, canonical BC-2.20.001 vector | PASS |
+| `test_BC_2_20_001_invariant_no_panic_on_truncated_inputs` | 7 inputs, len 0–3, varied content | No panic on any truncated input (purity invariant) | PASS |
+
+---
+
+## Error-Path Demonstration
+
+The error path is the primary path for this AC: all inputs with `len < 4` must return
+`None`.
+
+Key behavioral assertions verified:
+- Empty slice `&[]` -> `None` (EC-001: no bytes accessed).
+- 1-byte slice `&[0x03]` -> `None` (the valid version byte alone is insufficient; the
+  length-guard fires before the version byte is ever inspected).
+- 3-byte slice `[0x03, 0x00, 0x00]` -> `None` (one byte short of the 4-byte minimum;
+  BC-2.20.001 canonical vector, EC-002).
+- Purity invariant: no panic across 7 sampled truncated inputs (lengths 0–3, all-zero and
+  all-0xFF content).
+
+---
+
+## Verdict
+
+AC-184-001: **PASS** — All 5 BC-2.20.001 tests green; purity invariant verified.

docs/demo-evidence/STORY-184/AC-002-bad-version-byte.md

@@ -0,0 +1,79 @@
+# AC-184-002 — `parse_tpkt_header` Returns None for Version Byte != 0x03
+
+**Story:** STORY-184: S7comm TPKT Core Parser
+**AC:** AC-184-002
+**Traces to:** BC-2.20.002 postconditions 1–2, invariant 2
+**Wave:** 87
+
+---
+
+## Acceptance Criterion
+
+- Given `data.len() >= 4` and `data[0] != 0x03`
+- When `parse_tpkt_header(data)` is called
+- Then returns `None`; the length field (`data[2..4]`) is never decoded
+  (traces to BC-2.20.002 postcondition 2)
+- No panic for any `u8` value of `data[0]` (traces to BC-2.20.002 invariant 2)
+
+---
+
+## Test Suite Execution
+
+Command:
+```
+cargo test --test iso_on_tcp_tests BC_2_20_002
+```
+
+Output:
+```
+    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s
+     Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...)
+
+running 5 tests
+test story_184::test_BC_2_20_002_bad_version_short_circuits_before_length_decode ... ok
+test story_184::test_BC_2_20_002_invariant_no_panic_across_version_byte_sample ... ok
+test story_184::test_BC_2_20_002_returns_none_for_version_0x00_canonical_vector ... ok
+test story_184::test_BC_2_20_002_returns_none_for_version_0x04_off_by_one_canonical_vector ... ok
+test story_184::test_BC_2_20_002_returns_none_for_version_0xFF_canonical_vector ... ok
+
+test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 25 filtered out; finished in 0.00s
+```
+
+Result: **5/5 PASS**
+
+---
+
+## Test Coverage
+
+| Test Name | Canonical Vector | Condition Exercised | Result |
+|-----------|-------------------|----------------------|--------|
+| `test_BC_2_20_002_returns_none_for_version_0x00_canonical_vector` | `[0x00, 0x00, 0x00, 0x04]` | version=0x00 | PASS |
+| `test_BC_2_20_002_returns_none_for_version_0x04_off_by_one_canonical_vector` | `[0x04, 0x00, 0x00, 0x04]` | version=0x04 (off-by-one, no leniency) | PASS |
+| `test_BC_2_20_002_returns_none_for_version_0xFF_canonical_vector` | `[0xFF, 0x00, 0x00, 0x04]` | version=0xFF | PASS |
+| `test_BC_2_20_002_bad_version_short_circuits_before_length_decode` | `[0x02, 0x00, 0xFF, 0xFF]` | bad version with a length field that would otherwise decode to the maximally-legal 65535 — proves the version check short-circuits before length decode (postcondition 2) | PASS |
+| `test_BC_2_20_002_invariant_no_panic_across_version_byte_sample` | 8 sampled `u8` values (0x01, 0x02, 0x05, 0x10, 0x7F, 0x80, 0xFE, 0xFF) | No panic for any `data[0] != 0x03` (invariant 2 spot check) | PASS |
+
+---
+
+## Error-Path Demonstration
+
+Key behavioral assertions verified:
+- `data[0] == 0x00` -> `None`.
+- `data[0] == 0x04` (adjacent to the valid `0x03`) -> `None` — no off-by-one leniency.
+- `data[0] == 0xFF` -> `None`.
+- Version-check-before-length-decode ordering: `[0x02, 0x00, 0xFF, 0xFF]` (length bytes
+  decode to 65535, the maximum legal length) still returns `None` — the length field is
+  never inspected once the version guard fails (BC-2.20.002 postcondition 2).
+- Purity invariant: no panic across an 8-value sample of the `u8` domain excluding
+  `0x03` (full 256-value totality is the VP-048 Kani obligation — see AC-184-006).
+
+This AC also anchors SS-20's resync behavior: a non-`0x03` version byte is the signal
+the frame-walk loop (STORY-186) uses to attempt byte-at-a-time resynchronization on a
+malformed TPKT stream.
+
+---
+
+## Verdict
+
+AC-184-002: **PASS** — All 5 BC-2.20.002 tests green; version-before-length guard
+ordering and purity invariant verified.

docs/demo-evidence/STORY-184/AC-003-length-floor-rejection.md

@@ -0,0 +1,102 @@
+# AC-184-003 — `parse_tpkt_header` Returns None for Decoded Length < 7 (RFC 1006 §6 Minimum)
+
+**Story:** STORY-184: S7comm TPKT Core Parser
+**AC:** AC-184-003
+**Traces to:** BC-2.20.003 postcondition 1, invariant 2
+**Wave:** 87
+
+---
+
+## Acceptance Criterion
+
+- Given `data.len() >= 4`, `data[0] == 0x03`, and
+  `u16::from_be_bytes([data[2], data[3]]) < 7` (RFC 1006 §6 minimum)
+- When `parse_tpkt_header(data)` is called
+- Then returns `None`; no panic or overflow for any `u16` length value, including `0`
+  (traces to BC-2.20.003 invariant 2)
+
+RFC 1006 §6 states the minimum legal TPKT packet length is 7 (4-byte TPKT header +
+3-byte minimum COTP unit that must follow it). This AC covers the full sub-minimum
+range `[0, 6]`, including the genuine 6-vs-7 accept-floor boundary (paired with
+AC-184-004's `length == 7` accept case).
+
+---
+
+## Test Suite Execution
+
+Command:
+```
+cargo test --test iso_on_tcp_tests BC_2_20_003
+```
+
+Output:
+```
+    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s
+     Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...)
+
+running 8 tests
+test story_184::test_BC_2_20_003_invariant_no_panic_across_sub_minimum_lengths ... ok
+test story_184::test_BC_2_20_003_returns_none_for_length_five_below_rfc_minimum ... ok
+test story_184::test_BC_2_20_003_returns_none_for_length_four_below_rfc_minimum ... ok
+test story_184::test_BC_2_20_003_returns_none_for_length_one_canonical_vector ... ok
+test story_184::test_BC_2_20_003_returns_none_for_length_six_boundary_below_rfc_minimum ... ok
+test story_184::test_BC_2_20_003_returns_none_for_length_three_off_by_one_canonical_vector ... ok
+test story_184::test_BC_2_20_003_returns_none_for_length_two ... ok
+test story_184::test_BC_2_20_003_returns_none_for_length_zero_canonical_vector ... ok
+
+test result: ok. 8 passed; 0 failed; 0 ignored; 0 measured; 22 filtered out; finished in 0.00s
+```
+
+Also within scope of this AC — the independent RFC-1006-derived holdout vector
+(DF-CANONICAL-FRAME-HOLDOUT-001) for the length=4 header-only case:
+
+```
+cargo test --test iso_on_tcp_tests test_rfc1006_s6_length_four_below_minimum_returns_none
+```
+```
+running 1 test
+test story_184::test_rfc1006_s6_length_four_below_minimum_returns_none ... ok
+
+test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 29 filtered out; finished in 0.00s
+```
+
+Result: **9/9 PASS** (8 BC-tagged tests + 1 RFC-1006-derived holdout)
+
+---
+
+## Test Coverage
+
+| Test Name | Canonical Vector | Condition Exercised | Result |
+|-----------|-------------------|----------------------|--------|
+| `test_BC_2_20_003_returns_none_for_length_zero_canonical_vector` | `[0x03, 0x00, 0x00, 0x00]` | length=0 (most degenerate case) | PASS |
+| `test_BC_2_20_003_returns_none_for_length_one_canonical_vector` | `[0x03, 0x00, 0x00, 0x01]` | length=1 | PASS |
+| `test_BC_2_20_003_returns_none_for_length_two` | `[0x03, 0x00, 0x00, 0x02]` | length=2 | PASS |
+| `test_BC_2_20_003_returns_none_for_length_three_off_by_one_canonical_vector` | `[0x03, 0x00, 0x00, 0x03]` | length=3 | PASS |
+| `test_BC_2_20_003_returns_none_for_length_four_below_rfc_minimum` | `[0x03, 0x00, 0x00, 0x04]` | length=4 (the TPKT header's own structural floor, still below the RFC §6 floor of 7) | PASS |
+| `test_BC_2_20_003_returns_none_for_length_five_below_rfc_minimum` | `[0x03, 0x00, 0x00, 0x05]` | length=5 | PASS |
+| `test_BC_2_20_003_returns_none_for_length_six_boundary_below_rfc_minimum` | `[0x03, 0x00, 0x00, 0x06]` | length=6 (one below the RFC §6 minimum; the genuine 6-vs-7 boundary) | PASS |
+| `test_BC_2_20_003_invariant_no_panic_across_sub_minimum_lengths` | 7 length-byte pairs, decoded 0–6 | No overflow/panic for any sub-minimum `u16` length (invariant 2) | PASS |
+| `test_rfc1006_s6_length_four_below_minimum_returns_none` | `[0x03, 0x00, 0x00, 0x04]` | RFC-1006-derived independent holdout (DF-CANONICAL-FRAME-HOLDOUT-001), authored independently of the BC text | PASS |
+
+---
+
+## Error-Path Demonstration
+
+Key behavioral assertions verified:
+- `length == 0` (all-zero length field) -> `None` (EC-005, most degenerate case).
+- `length == 6` (one below the RFC 1006 §6 minimum of 7) -> `None` (EC-006) — this is
+  the genuine accept-floor boundary; `length == 7` is the paired accept case
+  demonstrated in `AC-004-valid-accept-path.md`.
+- Purity/overflow invariant: no panic or overflow across all sub-minimum `u16` length
+  values sampled (0–6), including the all-zero length-field byte pattern.
+- Spec-independent grounding: `test_rfc1006_s6_length_four_below_minimum_returns_none`
+  is derived directly from RFC 1006 §6 rather than reusing BC-2.20.003 vector text
+  verbatim (DF-CANONICAL-FRAME-HOLDOUT-001), reducing the risk that a shared
+  spec-transcription error in the BC would go undetected.
+
+---
+
+## Verdict
+
+AC-184-003: **PASS** — All 8 BC-2.20.003 tests plus the 1 independent RFC-1006 holdout
+green; the 6-vs-7 accept-floor boundary and overflow-safety invariant verified.

docs/demo-evidence/STORY-184/AC-004-valid-accept-path.md

@@ -0,0 +1,104 @@
+# AC-184-004 — `parse_tpkt_header` Returns Some(TpktHeader) for Valid Input
+
+**Story:** STORY-184: S7comm TPKT Core Parser
+**AC:** AC-184-004
+**Traces to:** BC-2.20.004 postconditions 1–4, invariants 1–2
+**Wave:** 87
+
+---
+
+## Acceptance Criterion
+
+- Given `data.len() >= 4`, `data[0] == 0x03`, and the decoded `length` in `[7, 65535]`
+  (`7` is the RFC 1006 §6 minimum accept floor)
+- When `parse_tpkt_header(data)` is called
+- Then returns `Some(TpktHeader { version: 3, length })` where `length` is exactly the
+  big-endian `u16` decoded from `data[2..4]`
+- `data[1]` (reserved byte) is never inspected; any value is accepted
+  (traces to BC-2.20.004 invariant 1)
+- `length == 65535` (maximum representable `u16`) is a legal accept
+  (traces to BC-2.20.004 invariant 2)
+
+---
+
+## Test Suite Execution
+
+Command:
+```
+cargo test --test iso_on_tcp_tests BC_2_20_004
+```
+
+Output (filtered to the BC-tagged accept-path tests; excludes `four_way_partition`,
+which is AC-184-005's obligation):
+```
+    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s
+     Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...)
+
+running 5 tests
+test story_184::test_BC_2_20_004_exact_length_match_no_trailing_bytes ... ok
+test story_184::test_BC_2_20_004_reserved_byte_nonzero_parses_identically_to_zero ... ok
+test story_184::test_BC_2_20_004_trailing_bytes_beyond_declared_length_still_accepted_canonical_vector ... ok
+test story_184::test_BC_2_20_004_valid_input_returns_some_header_length_65535_max_canonical_vector ... ok
+test story_184::test_BC_2_20_004_valid_input_returns_some_header_length_7_canonical_vector ... ok
+
+test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 25 filtered out; finished in 0.00s
+```
+
+Plus the 4 independent RFC-1006-derived holdout vectors (DF-CANONICAL-FRAME-HOLDOUT-001)
+and 1 proptest exercising the accept path (`_holdout` and `proptests` are excluded from
+the `BC_2_20_004` substring filter above, so run separately):
+```
+cargo test --test iso_on_tcp_tests test_rfc1006_s6_minimum_valid_length_holdout
+cargo test --test iso_on_tcp_tests test_rfc1006_s6_ten_byte_tpkt_holdout
+cargo test --test iso_on_tcp_tests test_rfc1006_s6_wide_length_field_holdout
+cargo test --test iso_on_tcp_tests proptest_accepted_length_matches_decoded_bytes
+```
+```
+test story_184::test_rfc1006_s6_minimum_valid_length_holdout ... ok
+test story_184::test_rfc1006_s6_ten_byte_tpkt_holdout ... ok
+test story_184::test_rfc1006_s6_wide_length_field_holdout ... ok
+test story_184::proptests::test_BC_2_20_004_proptest_accepted_length_matches_decoded_bytes ... ok
+```
+
+Result: **9/9 PASS** (5 BC-tagged tests + 3 RFC-1006 holdouts + 1 proptest)
+
+---
+
+## Test Coverage
+
+| Test Name | Canonical Vector | Condition Exercised | Result |
+|-----------|-------------------|----------------------|--------|
+| `test_BC_2_20_004_valid_input_returns_some_header_length_7_canonical_vector` | `[0x03, 0x00, 0x00, 0x07]` | length=7 (RFC §6 minimum accept floor; 6-vs-7 boundary) | PASS |
+| `test_BC_2_20_004_valid_input_returns_some_header_length_65535_max_canonical_vector` | `[0x03, 0xFF, 0xFF, 0xFF]` | length=65535 (max `u16`), reserved byte=0xFF | PASS |
+| `test_BC_2_20_004_reserved_byte_nonzero_parses_identically_to_zero` | `[0x03, 0x00, 0x00, 0x07]` vs `[0x03, 0xFF, 0x00, 0x07]` | Reserved byte never inspected — identical decode regardless of value | PASS |
+| `test_BC_2_20_004_exact_length_match_no_trailing_bytes` | `[0x03, 0x00, 0x00, 0x07, 0xAA, 0xBB, 0xCC]` (7 bytes total) | `data.len() == length` exactly | PASS |
+| `test_BC_2_20_004_trailing_bytes_beyond_declared_length_still_accepted_canonical_vector` | 14-byte input, declared length=10, second frame's header trails | `data.len() > length` — only the first frame's declared length is decoded; trailing bytes ignored | PASS |
+| `test_rfc1006_s6_minimum_valid_length_holdout` | `[0x03, 0x00, 0x00, 0x07]` | RFC-1006-derived independent holdout for the length=7 minimum | PASS |
+| `test_rfc1006_s6_ten_byte_tpkt_holdout` | 10-byte frame, length=10 | RFC-1006-derived holdout, header + 6 payload octets | PASS |
+| `test_rfc1006_s6_wide_length_field_holdout` | `[0x03, 0x00, 0x02, 0x05]` (length=517) | Independent holdout covering a length-field bit pattern absent from any BC vector | PASS |
+| `test_BC_2_20_004_proptest_accepted_length_matches_decoded_bytes` | Randomized `(len_hi, len_lo, reserved)` with decoded length >= 7 | Property: accepted `length` always exactly matches the big-endian decode of `data[2..4]`, reserved byte ignored | PASS |
+
+---
+
+## Accept-Path Demonstration
+
+Key behavioral assertions verified:
+- `length == 7` (RFC 1006 §6 minimum) -> `Some(TpktHeader { version: 3, length: 7 })`.
+- `length == 65535` (maximum representable `u16`, the "oversized-length-field" edge
+  case) -> `Some(TpktHeader { version: 3, length: 65535 })` — a legal accept.
+- Reserved byte (`data[1]`) at `0x00` and `0xFF` decode to identical `TpktHeader`
+  values — the reserved byte is never validated (BC-2.20.004 invariant 1).
+- `data.len() > length as usize` (a second frame follows immediately) still returns
+  `Some` describing only the first frame — frame-walk advance across multi-frame
+  buffers is out of scope for this function (STORY-186 concern).
+- Property-based coverage: for any randomized 4-byte header with a decoded length
+  `>= 7`, the accepted `TpktHeader.length` exactly matches the big-endian decode of
+  `data[2..4]`, with the reserved byte ignored across the sampled space.
+
+---
+
+## Verdict
+
+AC-184-004: **PASS** — All 5 BC-2.20.004 tests, all 3 RFC-1006 accept-path holdouts,
+and the accept-path proptest green; reserved-byte invariant and multi-frame trailing-
+bytes behavior verified.