diff --git a/CHANGELOG.md b/CHANGELOG.md index 401222c4..17161160 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,22 @@ Version numbers follow [Semantic Versioning](https://semver.org/). ### Added +- S7comm function-code classification: `classify_job_ack_function` in + `src/analyzer/s7comm.rs` is a pure, total classifier over the Job/Ack_Data + parameter-block function-code byte, returning `S7ClassicFunction` (Setup + Communication, Read Var, Write Var with first-item `S7AreaCode`, the + Download and Upload triads, PLC Control with a byte-exact `PlcControlService` + decode, PLC Stop, `Unrecognized(fc)`, and `NoParameterBlock`). All reads are + bounded by `param_length`, so no decode reads into the data block + (BC-2.21.010-017, VP-052, VP-054, STORY-188). `S7commAnalyzer` also records + each bounds-valid Ack/Ack_Data `error_class`/`error_code` pair in a bounded, arrival-ordered + record (`ack_error_observations()`, capped at `MAX_S7_ACK_ERROR_OBSERVATIONS` + with a saturating `ack_error_observations_dropped()` count), each recorded + observation carries the frame's `pdu_reference`, and a per-(ROSCTR, error + class, error code) count map (`ack_error_counts()`, at most 131,072 keys) + counts every recorded pair, including those beyond the list cap, so a + non-zero error is never lost. No finding or stderr output is emitted for it + (BC-2.21.008 postcondition 4). - 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 diff --git a/docs/demo-evidence/STORY-188/AC-001-002-setup-read.gif b/docs/demo-evidence/STORY-188/AC-001-002-setup-read.gif new file mode 100644 index 00000000..04fb15b9 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-001-002-setup-read.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-001-002-setup-read.tape b/docs/demo-evidence/STORY-188/AC-001-002-setup-read.tape new file mode 100644 index 00000000..9154fdb5 --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-001-002-setup-read.tape @@ -0,0 +1,27 @@ +# STORY-188 AC-188-001/002: Setup Communication (0xF0) and Read Var (0x04) classification +# Library story: demonstration vehicle is the story_188 test harness +# (tests/s7comm_analyzer_tests.rs, mod story_188); no CLI surface until STORY-193. +# Test: cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_010_setup story_188::test_BC_2_21_011 + +Output AC-001-002-setup-read.gif +Output AC-001-002-setup-read.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 560 +Set FontSize 14 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms + +Require cargo + +Type "# STORY-188 AC-188-001/002: Setup Communication (0xF0) and Read Var (0x04) classification" +Enter +Sleep 300ms + +Type "cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_010_setup story_188::test_BC_2_21_011 2>&1 | grep -E 'running [0-9]+ tests|story_188::|test result:'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-001-002-setup-read.webm b/docs/demo-evidence/STORY-188/AC-001-002-setup-read.webm new file mode 100644 index 00000000..a2fc238f Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-001-002-setup-read.webm differ diff --git a/docs/demo-evidence/STORY-188/AC-003-write-var-area.gif b/docs/demo-evidence/STORY-188/AC-003-write-var-area.gif new file mode 100644 index 00000000..f6cfbfce Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-003-write-var-area.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-003-write-var-area.tape b/docs/demo-evidence/STORY-188/AC-003-write-var-area.tape new file mode 100644 index 00000000..6ac68c7e --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-003-write-var-area.tape @@ -0,0 +1,27 @@ +# STORY-188 AC-188-003: Write Var area-code extraction, descriptor boundary 11/12/13/14, exhaustive u8 +# Library story: demonstration vehicle is the story_188 test harness +# (tests/s7comm_analyzer_tests.rs, mod story_188); no CLI surface until STORY-193. +# Test: cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_012 area_exhaustive + +Output AC-003-write-var-area.gif +Output AC-003-write-var-area.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 600 +Set FontSize 13 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms + +Require cargo + +Type "# STORY-188 AC-188-003: Write Var area-code extraction, descriptor boundary 11/12/13/14, exhaustive u8" +Enter +Sleep 300ms + +Type "cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_012 area_exhaustive 2>&1 | grep -E 'running [0-9]+ tests|story_188::|test result:'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-003-write-var-area.webm b/docs/demo-evidence/STORY-188/AC-003-write-var-area.webm new file mode 100644 index 00000000..28262835 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-003-write-var-area.webm differ diff --git a/docs/demo-evidence/STORY-188/AC-004-005-download-upload-triads.gif b/docs/demo-evidence/STORY-188/AC-004-005-download-upload-triads.gif new file mode 100644 index 00000000..009a949a Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-004-005-download-upload-triads.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-004-005-download-upload-triads.tape b/docs/demo-evidence/STORY-188/AC-004-005-download-upload-triads.tape new file mode 100644 index 00000000..ed547329 --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-004-005-download-upload-triads.tape @@ -0,0 +1,27 @@ +# STORY-188 AC-188-004/005: Download and Upload triads, disjointness (VP-054 proptest) +# Library story: demonstration vehicle is the story_188 test harness +# (tests/s7comm_analyzer_tests.rs, mod story_188); no CLI surface until STORY-193. +# Test: cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_013 story_188::test_BC_2_21_014 vp054 + +Output AC-004-005-download-upload-triads.gif +Output AC-004-005-download-upload-triads.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 640 +Set FontSize 13 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms + +Require cargo + +Type "# STORY-188 AC-188-004/005: Download and Upload triads, disjointness (VP-054 proptest)" +Enter +Sleep 300ms + +Type "cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_013 story_188::test_BC_2_21_014 vp054 2>&1 | grep -E 'running [0-9]+ tests|story_188::|test result:'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-004-005-download-upload-triads.webm b/docs/demo-evidence/STORY-188/AC-004-005-download-upload-triads.webm new file mode 100644 index 00000000..900d27e6 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-004-005-download-upload-triads.webm differ diff --git a/docs/demo-evidence/STORY-188/AC-006-007-plc-control-stop.gif b/docs/demo-evidence/STORY-188/AC-006-007-plc-control-stop.gif new file mode 100644 index 00000000..493cc973 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-006-007-plc-control-stop.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-006-007-plc-control-stop.tape b/docs/demo-evidence/STORY-188/AC-006-007-plc-control-stop.tape new file mode 100644 index 00000000..ffd5c59a --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-006-007-plc-control-stop.tape @@ -0,0 +1,27 @@ +# STORY-188 AC-188-006/007: PLC Control service decode (incl. truncated/case/trailing) and PLC Stop +# Library story: demonstration vehicle is the story_188 test harness +# (tests/s7comm_analyzer_tests.rs, mod story_188); no CLI surface until STORY-193. +# Test: cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_015 story_188::test_BC_2_21_016 + +Output AC-006-007-plc-control-stop.gif +Output AC-006-007-plc-control-stop.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 640 +Set FontSize 13 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms + +Require cargo + +Type "# STORY-188 AC-188-006/007: PLC Control service decode (incl. truncated/case/trailing) and PLC Stop" +Enter +Sleep 300ms + +Type "cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_015 story_188::test_BC_2_21_016 2>&1 | grep -E 'running [0-9]+ tests|story_188::|test result:'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-006-007-plc-control-stop.webm b/docs/demo-evidence/STORY-188/AC-006-007-plc-control-stop.webm new file mode 100644 index 00000000..8d7075d7 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-006-007-plc-control-stop.webm differ diff --git a/docs/demo-evidence/STORY-188/AC-008-009-unrecognized-totality.gif b/docs/demo-evidence/STORY-188/AC-008-009-unrecognized-totality.gif new file mode 100644 index 00000000..2c7c640f Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-008-009-unrecognized-totality.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-008-009-unrecognized-totality.tape b/docs/demo-evidence/STORY-188/AC-008-009-unrecognized-totality.tape new file mode 100644 index 00000000..551757bc --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-008-009-unrecognized-totality.tape @@ -0,0 +1,27 @@ +# STORY-188 AC-188-008/009: unrecognized FC, empty and unsliceable block, 256-value totality, VP-052 proptest +# Library story: demonstration vehicle is the story_188 test harness +# (tests/s7comm_analyzer_tests.rs, mod story_188); no CLI surface until STORY-193. +# Test: cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_017 vp052 + +Output AC-008-009-unrecognized-totality.gif +Output AC-008-009-unrecognized-totality.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 640 +Set FontSize 13 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms + +Require cargo + +Type "# STORY-188 AC-188-008/009: unrecognized FC, empty and unsliceable block, 256-value totality, VP-052 proptest" +Enter +Sleep 300ms + +Type "cargo test --test s7comm_analyzer_tests -- story_188::test_BC_2_21_017 vp052 2>&1 | grep -E 'running [0-9]+ tests|story_188::|test result:'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-008-009-unrecognized-totality.webm b/docs/demo-evidence/STORY-188/AC-008-009-unrecognized-totality.webm new file mode 100644 index 00000000..34b84f37 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-008-009-unrecognized-totality.webm differ diff --git a/docs/demo-evidence/STORY-188/AC-010-ack-error-record.gif b/docs/demo-evidence/STORY-188/AC-010-ack-error-record.gif new file mode 100644 index 00000000..73e816d3 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-010-ack-error-record.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-010-ack-error-record.tape b/docs/demo-evidence/STORY-188/AC-010-ack-error-record.tape new file mode 100644 index 00000000..fe86f64e --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-010-ack-error-record.tape @@ -0,0 +1,27 @@ +# STORY-188 AC-188-010: Ack/Ack_Data error record, count map, cap/dropped, pdu_reference, non-recording paths +# Library story: demonstration vehicle is the story_188 test harness +# (tests/s7comm_analyzer_tests.rs, mod story_188); no CLI surface until STORY-193. +# Test: cargo test --test s7comm_analyzer_tests story_188::test_BC_2_21_008 + +Output AC-010-ack-error-record.gif +Output AC-010-ack-error-record.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 860 +Set FontSize 12 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms + +Require cargo + +Type "# STORY-188 AC-188-010: Ack/Ack_Data error record, count map, cap/dropped, pdu_reference, non-recording paths" +Enter +Sleep 300ms + +Type "cargo test --test s7comm_analyzer_tests story_188::test_BC_2_21_008 2>&1 | grep -E 'running [0-9]+ tests|story_188::|test result:'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-010-ack-error-record.webm b/docs/demo-evidence/STORY-188/AC-010-ack-error-record.webm new file mode 100644 index 00000000..247bbb18 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-010-ack-error-record.webm differ diff --git a/docs/demo-evidence/STORY-188/AC-011-canonical-frames.gif b/docs/demo-evidence/STORY-188/AC-011-canonical-frames.gif new file mode 100644 index 00000000..18c69eb9 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-011-canonical-frames.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-011-canonical-frames.tape b/docs/demo-evidence/STORY-188/AC-011-canonical-frames.tape new file mode 100644 index 00000000..bc728199 --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-011-canonical-frames.tape @@ -0,0 +1,27 @@ +# STORY-188 AC-188-011: canonical public-reference byte vectors (story_188::canonical) +# Library story: demonstration vehicle is the story_188 test harness +# (tests/s7comm_analyzer_tests.rs, mod story_188); no CLI surface until STORY-193. +# Test: cargo test --test s7comm_analyzer_tests story_188::canonical + +Output AC-011-canonical-frames.gif +Output AC-011-canonical-frames.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 640 +Set FontSize 13 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms + +Require cargo + +Type "# STORY-188 AC-188-011: canonical public-reference byte vectors (story_188::canonical)" +Enter +Sleep 300ms + +Type "cargo test --test s7comm_analyzer_tests story_188::canonical 2>&1 | grep -E 'running [0-9]+ tests|story_188::|test result:'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-011-canonical-frames.webm b/docs/demo-evidence/STORY-188/AC-011-canonical-frames.webm new file mode 100644 index 00000000..79f05b76 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-011-canonical-frames.webm differ diff --git a/docs/demo-evidence/STORY-188/AC-ALL-story_188-green.gif b/docs/demo-evidence/STORY-188/AC-ALL-story_188-green.gif new file mode 100644 index 00000000..2e8f1613 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-ALL-story_188-green.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-ALL-story_188-green.tape b/docs/demo-evidence/STORY-188/AC-ALL-story_188-green.tape new file mode 100644 index 00000000..877ad36f --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-ALL-story_188-green.tape @@ -0,0 +1,27 @@ +# STORY-188 full story_188 module: 34/34 green +# Library story: demonstration vehicle is the story_188 test harness +# (tests/s7comm_analyzer_tests.rs, mod story_188); no CLI surface until STORY-193. +# Test: cargo test --test s7comm_analyzer_tests story_188:: + +Output AC-ALL-story_188-green.gif +Output AC-ALL-story_188-green.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 1080 +Set FontSize 11 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms + +Require cargo + +Type "# STORY-188 full story_188 module: 34/34 green" +Enter +Sleep 300ms + +Type "cargo test --test s7comm_analyzer_tests story_188:: 2>&1 | grep -E 'running [0-9]+ tests|story_188::|test result:'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-ALL-story_188-green.webm b/docs/demo-evidence/STORY-188/AC-ALL-story_188-green.webm new file mode 100644 index 00000000..f68cc221 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-ALL-story_188-green.webm differ diff --git a/docs/demo-evidence/STORY-188/AC-FIXTURE-e2e-fc-classification-pcap.gif b/docs/demo-evidence/STORY-188/AC-FIXTURE-e2e-fc-classification-pcap.gif new file mode 100644 index 00000000..dd074fb6 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-FIXTURE-e2e-fc-classification-pcap.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-FIXTURE-e2e-fc-classification-pcap.tape b/docs/demo-evidence/STORY-188/AC-FIXTURE-e2e-fc-classification-pcap.tape new file mode 100644 index 00000000..8e98242c --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-FIXTURE-e2e-fc-classification-pcap.tape @@ -0,0 +1,27 @@ +# STORY-188 fixture pcap end-to-end FC classification (supporting AC-188-001..008) +# Library story: demonstration vehicle is the story_188 test harness +# (tests/s7comm_analyzer_tests.rs, mod story_188); no CLI surface until STORY-193. +# Test: cargo test --test s7comm_analyzer_tests story_188::test_BC_2_21_010_fc_classification_fixture + +Output AC-FIXTURE-e2e-fc-classification-pcap.gif +Output AC-FIXTURE-e2e-fc-classification-pcap.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 520 +Set FontSize 13 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms + +Require cargo + +Type "# STORY-188 fixture pcap end-to-end FC classification (supporting AC-188-001..008)" +Enter +Sleep 300ms + +Type "cargo test --test s7comm_analyzer_tests story_188::test_BC_2_21_010_fc_classification_fixture 2>&1 | grep -E 'running [0-9]+ tests|story_188::|test result:'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-FIXTURE-e2e-fc-classification-pcap.webm b/docs/demo-evidence/STORY-188/AC-FIXTURE-e2e-fc-classification-pcap.webm new file mode 100644 index 00000000..31820281 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-FIXTURE-e2e-fc-classification-pcap.webm differ diff --git a/docs/demo-evidence/STORY-188/AC-VP051-kani-slicing-safe.gif b/docs/demo-evidence/STORY-188/AC-VP051-kani-slicing-safe.gif new file mode 100644 index 00000000..23f1f093 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-VP051-kani-slicing-safe.gif differ diff --git a/docs/demo-evidence/STORY-188/AC-VP051-kani-slicing-safe.tape b/docs/demo-evidence/STORY-188/AC-VP051-kani-slicing-safe.tape new file mode 100644 index 00000000..e0e12e18 --- /dev/null +++ b/docs/demo-evidence/STORY-188/AC-VP051-kani-slicing-safe.tape @@ -0,0 +1,27 @@ +# STORY-188 VP-051 Kani harness: classify_job_ack_function parameter-slicing safety +# (supporting evidence for AC-188-008/009 totality and no-panic slicing) +# Test: cargo kani --tests --harness verify_classify_job_ack_function_param_slicing_safe + +Output AC-VP051-kani-slicing-safe.gif +Output AC-VP051-kani-slicing-safe.webm + +Set FontFamily "Menlo" +Set Theme "Dracula" +Set Width 1200 +Set Height 560 +Set FontSize 14 +Set Padding 24 +Set Shell "bash" +Set TypingSpeed 40ms +Set WaitTimeout 120s + +Require cargo + +Type "# STORY-188 VP-051: Kani proof, classify_job_ack_function param slicing is panic-free" +Enter +Sleep 300ms + +Type "cargo kani --tests --harness verify_classify_job_ack_function_param_slicing_safe 2>&1 | grep -E 'VERIFICATION|Harness Summary|successfully verified|cover properties'" +Enter +Wait +Sleep 3s diff --git a/docs/demo-evidence/STORY-188/AC-VP051-kani-slicing-safe.webm b/docs/demo-evidence/STORY-188/AC-VP051-kani-slicing-safe.webm new file mode 100644 index 00000000..86523ef8 Binary files /dev/null and b/docs/demo-evidence/STORY-188/AC-VP051-kani-slicing-safe.webm differ diff --git a/docs/demo-evidence/STORY-188/evidence-report.md b/docs/demo-evidence/STORY-188/evidence-report.md new file mode 100644 index 00000000..8a16743b --- /dev/null +++ b/docs/demo-evidence/STORY-188/evidence-report.md @@ -0,0 +1,117 @@ +# Demo Evidence Report — STORY-188 + +**Story:** STORY-188: S7comm Job/Ack_Data Function-Code Classification (v1.7, AC-188-001..011) +**Wave:** 91 +**Date:** 2026-10-05 +**Branch:** feature/STORY-188-s7comm-function-code-classification (HEAD c6bd91e3; per-story adversarial CONVERGED) +**Product type:** Library (pure-core `classify_job_ack_function` consumed by the effectful-shell +`S7commAnalyzer` in `src/analyzer/s7comm.rs`). There is no CLI subcommand or web UI surface for +S7comm yet (dispatcher wiring is STORY-193), so, following the STORY-187 precedent, the +demonstration vehicle is this story's own test harness: `tests/s7comm_analyzer_tests.rs`, +`mod story_188` (34 tests plus one Kani harness). +**Recording tool:** VHS 0.11.0 (terminal recordings of `cargo test --test s7comm_analyzer_tests`, +filtered per behavior group, piped through `grep` to show only the relevant `story_188::` lines) + +--- + +## Full story_188 Module: 34/34 PASS + +``` +cargo test --test s7comm_analyzer_tests story_188:: +``` + +Result: **34 passed; 0 failed; 0 ignored; 0 measured; 83 filtered out** (the 83 are the +`story_186` and `story_187` modules in the same file). Artifact: `AC-ALL-story_188-green.gif/.webm/.tape`. + +--- + +## AC → Test → Artifact Coverage Map + +| AC | Title (short) | Test(s) | Artifact | Path | Verdict | +|----|---------------|---------|----------|------|---------| +| AC-188-001 | FC 0xF0 -> Setup Communication | `test_BC_2_21_010_setup_communication_classified`; `canonical::test_BC_2_21_010_canonical_setup_communication_ack_data_classified` | `AC-001-002-setup-read`; `AC-011-canonical-frames`; `AC-FIXTURE-e2e-fc-classification-pcap` | Success | PASS | +| AC-188-002 | FC 0x04 -> Read Var, no area decode | `test_BC_2_21_011_read_var_classified_no_area_decode`; `canonical::test_BC_2_21_011_canonical_read_var_db_classified` | `AC-001-002-setup-read`; `AC-011-canonical-frames` | Success | PASS | +| AC-188-003 | FC 0x05 -> Write Var, first-item area code | `test_BC_2_21_012_write_var_area_code_extraction`; `test_BC_2_21_012_write_var_descriptor_length_boundary_11_12_13_14`; `area_exhaustive::test_BC_2_21_012_write_var_area_code_exhaustive_over_all_u8` | `AC-003-write-var-area` | Success + Error (descriptor lengths 11/12/13 below the 14-byte minimum are rejected; 14 accepted) + exhaustive u8 | PASS | +| AC-188-004 | Download triad classified independently | `test_BC_2_21_013_download_triad_classified_independently`; `vp054::proptest_vp054_download_upload_structural_disjointness` | `AC-004-005-download-upload-triads` | Success | PASS | +| AC-188-005 | Upload triad, disjoint from Download | `test_BC_2_21_014_upload_triad_classified_disjoint_from_download`; `vp054::proptest_vp054_download_upload_structural_disjointness` | `AC-004-005-download-upload-triads` | Success + disjointness (a Download FC never classifies as Upload and vice versa) | PASS | +| AC-188-006 | FC 0x28 PLC Control, PI-service decode | `test_BC_2_21_015_plc_control_service_string_decode`; `test_BC_2_21_015_plc_control_truncated_and_case_variants_unrecognized`; `test_BC_2_21_015_plc_control_trailing_bytes_after_service_string`; `canonical::test_BC_2_21_015_canonical_plc_control_p_program_classified` | `AC-006-007-plc-control-stop`; `AC-011-canonical-frames` | Success + Error (truncated service string, case variants -> unrecognized service) | PASS | +| AC-188-007 | FC 0x29 -> PLC Stop by FC byte only | `test_BC_2_21_016_plc_stop_classified`; `canonical::test_BC_2_21_016_canonical_plc_stop_classified` | `AC-006-007-plc-control-stop`; `AC-011-canonical-frames` | Success (FC-only; `param_length==1` -> PlcStop) | PASS | +| AC-188-008 | Unrecognized FC and empty block are distinct terminal outcomes | `test_BC_2_21_017_unrecognized_fc_and_empty_parameter_block`; `test_BC_2_21_017_unsliceable_parameter_block_returns_no_parameter_block` | `AC-008-009-unrecognized-totality`; `AC-VP051-kani-slicing-safe` (supporting) | Error / edge (unrecognized FC, empty block, unsliceable block) | PASS | +| AC-188-009 | Classification total over all 256 u8 values + empty block | `test_BC_2_21_017_fc_classification_total_over_all_256_values`; `vp052::proptest_vp052_fc_classification_totality` | `AC-008-009-unrecognized-totality`; `AC-VP051-kani-slicing-safe` (supporting) | Exhaustive 256-value + proptest | PASS | +| AC-188-010 | Ack/Ack_Data error_class/error_code -> bounded analyzer-side record + count map | eleven `test_BC_2_21_008_*` tests: `ack_error_class_code_consumed_and_logged`, `ack_data_error_class_code_consumed_and_logged`, `zero_error_class_code_logged_for_ack_and_ack_data`, `ack_error_observation_captures_pdu_reference`, `ack_error_counts_exact_for_mixed_frames`, `ack_error_histogram_counts_beyond_list_cap`, `ack_error_observations_bounded_by_cap_with_dropped_count`, `job_frames_record_no_ack_error_observation`, `userdata_frames_record_no_ack_error_observation`, `job_frames_contribute_no_histogram_key`, `bounds_failing_ack_data_records_no_ack_error_observation` | `AC-010-ack-error-record` | Success (record, count map, cap/dropped, pdu_reference) + Error/negative (Job/Userdata and bounds-failing frames record nothing) | PASS | +| AC-188-011 | Canonical public-reference byte vectors | `canonical::` six tests: Setup Comm Ack_Data (010), Write Var DB (012), Write Var Outputs (012), Read Var DB (011), PLC Control P_PROGRAM (015), PLC Stop (016) | `AC-011-canonical-frames` | Success | PASS | + +Additional artifacts: `AC-FIXTURE-e2e-fc-classification-pcap` runs +`test_BC_2_21_010_fc_classification_fixture_pcap_end_to_end` (committed fixture +`tests/fixtures/s7comm-fc-classification.pcap`, classified FCs through `S7commAnalyzer::on_data`; +supports AC-188-001..008). `AC-VP051-kani-slicing-safe` records the VP-051 Kani proof (below). + +**All 11 acceptance criteria (AC-188-001..011) map to at least one recorded artifact.** + +### Per-recording counts + +| Artifact | ACs | Tests shown | +|----------|-----|-------------| +| `AC-001-002-setup-read` | 001, 002 | 2 | +| `AC-003-write-var-area` | 003 | 3 | +| `AC-004-005-download-upload-triads` | 004, 005 | 3 | +| `AC-006-007-plc-control-stop` | 006, 007 | 4 | +| `AC-008-009-unrecognized-totality` | 008, 009 | 4 | +| `AC-010-ack-error-record` | 010 | 11 | +| `AC-011-canonical-frames` | 011 | 6 | +| `AC-FIXTURE-e2e-fc-classification-pcap` | 001..008 (supporting) | 1 | +| `AC-ALL-story_188-green` | 001..011 | 34 (de-duplicated total; 2+3+3+4+4+11+6+1 = 34) | +| `AC-VP051-kani-slicing-safe` | 008, 009 (supporting) | Kani harness | + +--- + +## VP-051 Kani Harness (recorded) + +`cargo kani --tests --harness verify_classify_job_ack_function_param_slicing_safe` (the +`#[cfg(kani)] mod vp051_kani` harness in `tests/s7comm_analyzer_tests.rs`) completes in about one +second of verification time locally: **VERIFICATION SUCCESSFUL; 4 of 4 cover properties satisfied; +1 successfully verified harness, 0 failures**. Recorded in `AC-VP051-kani-slicing-safe.gif/.webm`. +Scope per story v1.6/EC-012: the harness covers inputs that pass `s7comm_bounds_ok`; the unsliceable +`NoParameterBlock` path is covered by the unit test cited under AC-188-008. + +--- + +## Notes on the Human Rulings (why AC-188-010 evidence is test-assertion based) + +Human ruling 2026-10-04 (STORY-188 per-story adversarial pass 1): the AC-188-010 surface is an +**analyzer-side bounded record with NO stderr or log output** (ADR-0004 flooding rationale). +`S7commAnalyzer` keeps a bounded observation list (cap `MAX_S7_ACK_ERROR_OBSERVATIONS` = 1024, with +a saturating dropped count), an exact per-`(rosctr, error_class, error_code)` count map that keeps +counting beyond the cap, and a `pdu_reference` on each observation. Recording is bounds-gated: Job +and Userdata frames, and Ack/Ack_Data frames that fail the BC-2.21.009 bounds check, record +nothing. Because nothing is printed, a terminal recording has no visible side effect to show, so +the evidence for AC-188-010 is the passing assertions on the analyzer's accessors, named per +behavior in the `AC-010-ack-error-record` recording (11 tests). A zero error class/code is recorded +the same as any other value (BC-2.21.008 EC-004). For Write Var (AC-188-003) the 0xFF area-code +collision is an accepted residual (orchestrator decision, story v1.3). + +Classification in `dispatch_classic_s7comm` is a deliberate classification-only placeholder +consumed by STORY-191/192, so no Finding or user-visible output is produced by this story; this +is why no CLI recording exists. + +## Canonical-Frame Provenance (AC-188-011, DF-CANONICAL-FRAME-HOLDOUT-001) + +The six `story_188::canonical::*` byte vectors are sourced from public references recorded in the +story's canonical-FC-vectors research document (Write Var, PLC Control, PLC Stop, Read Var), plus +the Setup Communication Ack_Data vector cited in BC-2.21.008 Canonical Test Vectors. Per ADR-014 +Decision 4, public wire-capture bytes are used as test vectors only; parser design derives from +the permitted prose sources. + +## Recording Method + +VHS tapes run `cargo test --test s7comm_analyzer_tests [--] 2>&1 | grep -E +'running [0-9]+ tests|story_188::|test result:'`. The `grep` suppresses cargo's +`Running tests/... (/target/...)` line, which would otherwise leak an absolute host +path into rendered output. Tapes use Menlo, Dracula theme, 1200 px wide, matching STORY-187. +Multiple filters are passed after `--` because cargo accepts only one positional filter before it. + +## Path-Scrub Gate (PG-W70-DEMO-SCRUB) + +The mandatory absolute-host-path and tilde-home grep from the demo-evidence scrub-gate maintenance +document was run from the repo root against the demo-evidence tree and returned zero matches. The +gate command is not reproduced verbatim here because its regex literal would match this file. diff --git a/src/analyzer/s7comm.rs b/src/analyzer/s7comm.rs index 82058a62..edfaa883 100644 --- a/src/analyzer/s7comm.rs +++ b/src/analyzer/s7comm.rs @@ -31,9 +31,14 @@ //! CR/CC opposite-direction session tracking (F-01), sticky first-`Some(byte)`-wins //! protocol classification (F-02), and classic S7comm (`0x32`) header dissection //! gated on the flow's sticky `classified_protocol == Classic` (F-12) are fully -//! wired. The `Some(0x72)` (S7comm-plus) and unrecognized/`None`-`protocol_id` -//! branches remain deliberate, panic-free structural no-ops — their observable -//! behavior is STORY-190's scope. +//! wired. STORY-188 adds, for bounds-checked frames, Job/Ack_Data function-code +//! classification ([`classify_job_ack_function`], BC-2.21.010-017; the per-frame +//! result is not yet consumed, see STORY-191/192) and the Ack/Ack_Data error +//! record: a bounded, arrival-ordered list of [`S7AckErrorObservation`] (with +//! `pdu_reference`) plus an exact [`S7AckErrorKey`] count map covering every +//! recorded observation (BC-2.21.008 postcondition 4). The `Some(0x72)` (S7comm-plus) +//! and unrecognized/`None`-`protocol_id` branches remain deliberate, panic-free +//! structural no-ops — their observable behavior is STORY-190's scope. //! //! ## Behavioral contracts //! - BC-2.20.013: TPKT frames spanning TCP segment boundaries are reassembled via @@ -66,6 +71,11 @@ //! holdout ruling, DF-CANONICAL-FRAME-HOLDOUT-001). //! - BC-2.21.009: declared `param_length`/`data_length` are bounds-checked (via the //! pure [`s7comm_bounds_ok`] helper) before any parameter/data-block slice. +//! - BC-2.21.010-017: [`classify_job_ack_function`] maps the Job/Ack_Data +//! function-code byte (Setup Communication, Read/Write Var with first-item area, +//! download/upload family, PLC Control with PI-service, PLC Stop, unrecognized, +//! no parameter block) to [`S7ClassicFunction`]; pure, bounded to the parameter +//! block, no findings. use std::collections::HashMap; @@ -98,6 +108,47 @@ use crate::reassembly::handler::Direction; /// currently-live detection path. pub const MAX_S7_ISO_ON_TCP_CARRY_BYTES: usize = 65_535; +/// Maximum number of [`S7AckErrorObservation`] records retained by one +/// [`S7commAnalyzer`] (analyzer-wide, not per-flow). Observations beyond this cap +/// are counted in [`S7commAnalyzer::ack_error_observations_dropped`] instead of +/// stored, bounding memory on adversarial or long captures (ADR-0004: no per-packet +/// stderr flooding; BC-2.21.008 postcondition 4, AC-188-010). +pub const MAX_S7_ACK_ERROR_OBSERVATIONS: usize = 1024; + +/// Histogram key for Ack/Ack_Data error pairs: one entry per distinct +/// (ROSCTR, `error_class`, `error_code`) triple (F-07). +/// +/// The map keyed by this type ([`S7commAnalyzer::ack_error_counts`]) is bounded by +/// construction: ROSCTR is one of 2 values (`Ack`, `AckData`) and each error byte +/// has 256 values, so it holds at most 2 x 256 x 256 = 131,072 keys. It exists so +/// that a non-zero error observed after the ordered observation list reaches +/// [`MAX_S7_ACK_ERROR_OBSERVATIONS`] is never lost: every recorded observation is +/// counted here, including those beyond the list cap. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct S7AckErrorKey { + /// ROSCTR of the frame. + pub rosctr: Rosctr, + /// Header byte 10. + pub error_class: u8, + /// Header byte 11. + pub error_code: u8, +} + +/// One observed `error_class` / `error_code` pair from an Ack (0x02) or Ack_Data +/// (0x03) classic S7comm header (BC-2.21.008 postcondition 4). Zero values are +/// recorded like any other value. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct S7AckErrorObservation { + /// PDU reference of the frame (header bytes 4-5, F-07). + pub pdu_reference: u16, + /// The ROSCTR of the frame the pair was read from (`Ack` or `AckData`). + pub rosctr: Rosctr, + /// Header byte 10. + pub error_class: u8, + /// Header byte 11. + pub error_code: u8, +} + // --------------------------------------------------------------------------- // Per-flow state // --------------------------------------------------------------------------- @@ -187,7 +238,7 @@ pub enum S7Protocol { /// story models (BC-2.21.006/007/008), mirroring `CotpTpduType`'s /// exhaustive-but-bounded design (BC-2.20.011) — this is not exhaustive over all 256 /// `u8` values by design (BC-2.21.007 invariant 2). -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum Rosctr { /// `0x01` — Job (request). Job, @@ -234,6 +285,199 @@ pub struct S7commHeader { pub header_len: usize, } +// --------------------------------------------------------------------------- +// Job/Ack_Data function-code classification surface (STORY-188) +// --------------------------------------------------------------------------- + +/// S7 memory-area code decoded from a Write Var first address item +/// (BC-2.21.012). `0x80` DirectPeripheral, `0x81` Inputs, `0x82` Outputs, +/// `0x83` Markers, `0x84` DataBlock, `0x85` InstanceDb, `0x1C` Counters, +/// `0x1D` Timers; any other byte is `Unrecognized(byte)`. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum S7AreaCode { + /// `0x80`. + DirectPeripheral, + /// `0x81`. + Inputs, + /// `0x82`. + Outputs, + /// `0x83`. + Markers, + /// `0x84`. + DataBlock, + /// `0x85`. + InstanceDb, + /// `0x1C`. + Counters, + /// `0x1D`. + Timers, + /// Any other byte (also the `0xFF` placeholder when the item descriptor is + /// unreadable, BC-2.21.012 postcondition 3). + Unrecognized(u8), +} + +/// PI-service decoded from a PLC Control (FC `0x28`) parameter block (BC-2.21.015). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum PlcControlService { + /// `"P_PROGRAM"`. + ProgramStart, + /// `"_INSE"`. + BlockActivate, + /// `"_DELE"`. + BlockDelete, + /// `"_GARB"`. + MemoryCompress, + /// `"_MODU"`. + RamToRom, + /// Unreadable/truncated or non-matching service string. + Unrecognized, +} + +/// Classification of a Job/Ack_Data function-code byte (BC-2.21.010 through +/// BC-2.21.017). STORY-189 extends this enum with the `Userdata(..)` arm. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum S7ClassicFunction { + /// FC `0xF0` (BC-2.21.010). + SetupCommunication, + /// FC `0x04` (BC-2.21.011). + ReadVar, + /// FC `0x05` with first-item area code (BC-2.21.012). + WriteVar(S7AreaCode), + /// FC `0x1A` (BC-2.21.013). + RequestDownload, + /// FC `0x1B` (BC-2.21.013). + DownloadBlock, + /// FC `0x1C` (BC-2.21.013). + DownloadEnded, + /// FC `0x1D` (BC-2.21.014). + StartUpload, + /// FC `0x1E` (BC-2.21.014). + Upload, + /// FC `0x1F` (BC-2.21.014). + EndUpload, + /// FC `0x28` with decoded PI-service (BC-2.21.015). + PlcControl(PlcControlService), + /// FC `0x29` (BC-2.21.016). Carries no decoded payload. + /// + /// PLC Stop's wire layout differs from PLC Control (0x28): 5 reserved bytes, + /// no `0xFD` marker and no `u16` block-argument length. The 0x28 layout is + /// therefore never applied to 0x29; only the FC byte is classified. + PlcStop, + /// Any other FC byte, raw value preserved (BC-2.21.017). + Unrecognized(u8), + /// `param_length == 0`: no FC byte present (BC-2.21.017). Also returned + /// defensively when the parameter block cannot be sliced out of the input + /// (overflowing or out-of-range `header_len + param_length`); that case is + /// unreachable behind [`s7comm_bounds_ok`]. + NoParameterBlock, +} + +/// Pure-core classifier over the Job/Ack_Data function-code byte at +/// `data[header_len]` (BC-2.21.010 through BC-2.21.017). Total over all `u8` +/// values plus the `param_length == 0` case; emits no findings and reads no flow +/// state. +/// +/// The parameter block is `data[header_len..header_len + param_length]`; every +/// byte read is bounds-checked against that sub-slice (never against `data.len()`), +/// so decoders read only the `param` sub-slice (story_188 truncation/boundary tests). +/// A block that cannot be sliced out of `data` (caller bounds-check violated) yields +/// `NoParameterBlock`; panic-freedom on bounds-ok inputs is VP-051. +pub fn classify_job_ack_function( + data: &[u8], + header_len: usize, + param_length: u16, +) -> S7ClassicFunction { + if param_length == 0 { + return S7ClassicFunction::NoParameterBlock; + } + let Some(end) = header_len.checked_add(param_length as usize) else { + return S7ClassicFunction::NoParameterBlock; + }; + let Some(param) = data.get(header_len..end) else { + return S7ClassicFunction::NoParameterBlock; + }; + let Some(&fc) = param.first() else { + return S7ClassicFunction::NoParameterBlock; + }; + match fc { + 0xF0 => S7ClassicFunction::SetupCommunication, + 0x04 => S7ClassicFunction::ReadVar, + 0x05 => S7ClassicFunction::WriteVar(decode_write_var_area(param)), + 0x1A => S7ClassicFunction::RequestDownload, + 0x1B => S7ClassicFunction::DownloadBlock, + 0x1C => S7ClassicFunction::DownloadEnded, + 0x1D => S7ClassicFunction::StartUpload, + 0x1E => S7ClassicFunction::Upload, + 0x1F => S7ClassicFunction::EndUpload, + 0x28 => S7ClassicFunction::PlcControl(decode_plc_control_service(param)), + // PLC Stop (0x29): layout differs from PLC Control (5 reserved bytes, no + // 0xFD, no u16 block-arg length), so decode_plc_control_service is + // deliberately NOT applied here; the FC byte alone classifies it. + 0x29 => S7ClassicFunction::PlcStop, + other => S7ClassicFunction::Unrecognized(other), + } +} + +/// Maps an S7 memory-area byte to [`S7AreaCode`] (BC-2.21.012 invariant 1). +fn area_code_from_byte(byte: u8) -> S7AreaCode { + match byte { + 0x80 => S7AreaCode::DirectPeripheral, + 0x81 => S7AreaCode::Inputs, + 0x82 => S7AreaCode::Outputs, + 0x83 => S7AreaCode::Markers, + 0x84 => S7AreaCode::DataBlock, + 0x85 => S7AreaCode::InstanceDb, + 0x1C => S7AreaCode::Counters, + 0x1D => S7AreaCode::Timers, + other => S7AreaCode::Unrecognized(other), + } +} + +/// Decodes the first S7ANY item's area byte from a Write Var parameter block +/// (`param[0] == 0x05`). Layout: FC, item count, then the 12-byte item +/// `[0x12, len, syntax_id, transport, count(2), db(2), area, addr(3)]`, so the +/// syntax id is at offset 4 and the area byte at offset 10. Any shortfall or a +/// non-S7ANY syntax id (`!= 0x10`) yields the `Unrecognized(0xFF)` placeholder +/// (BC-2.21.012 postcondition 3); only the first item is decoded (postcondition 4). +/// +/// Accepted collision (F-09): `WriteVar(S7AreaCode::Unrecognized(0xFF))` is shared +/// by a genuine `0xFF` area byte and the not-decoded case; BC-2.21.012 +/// postcondition 3 mandates this placeholder, so the two are indistinguishable. +fn decode_write_var_area(param: &[u8]) -> S7AreaCode { + const NOT_DECODED: S7AreaCode = S7AreaCode::Unrecognized(0xFF); + // FC + count + 12-byte item. + if param.len() < 14 || param.get(4) != Some(&0x10) { + return NOT_DECODED; + } + param + .get(10) + .map_or(NOT_DECODED, |&b| area_code_from_byte(b)) +} + +/// Decodes the PI-service name from a PLC Control parameter block +/// (`param[0] == 0x28`). Layout: FC, 6 reserved bytes, `0xFD`, `u16` BE +/// block-argument length, the block arguments, a 1-byte service-name length, then +/// the service string. Byte-exact match only; every shortfall is `Unrecognized` +/// (BC-2.21.015 postconditions 2-3). +fn decode_plc_control_service(param: &[u8]) -> PlcControlService { + let decode = || -> Option { + let args_len = u16::from_be_bytes([*param.get(8)?, *param.get(9)?]) as usize; + let name_len_at = 10usize.checked_add(args_len)?; + let name_len = *param.get(name_len_at)? as usize; + let name_start = name_len_at.checked_add(1)?; + let name = param.get(name_start..name_start.checked_add(name_len)?)?; + Some(match name { + b"P_PROGRAM" => PlcControlService::ProgramStart, + b"_INSE" => PlcControlService::BlockActivate, + b"_DELE" => PlcControlService::BlockDelete, + b"_GARB" => PlcControlService::MemoryCompress, + b"_MODU" => PlcControlService::RamToRom, + _ => PlcControlService::Unrecognized, + }) + }; + decode().unwrap_or(PlcControlService::Unrecognized) +} + // --------------------------------------------------------------------------- // Pure-core parser (STORY-187) // --------------------------------------------------------------------------- @@ -366,14 +610,43 @@ pub struct S7commAnalyzer { /// malformed classic-S7comm-header finding (parse failure or bounds-check /// failure, BC-2.21.004/007/008/009, F-11). pub findings: Vec, + /// Analyzer-wide, arrival-ordered, bounded record of Ack/Ack_Data error pairs + /// (capped at [`MAX_S7_ACK_ERROR_OBSERVATIONS`]). + ack_error_observations: Vec, + /// Observations beyond the cap (saturating). + ack_error_observations_dropped: u64, + /// Exact per-(ROSCTR, error class, error code) counts of every recorded + /// observation, including those beyond the list cap. Bounded by construction + /// (at most 131,072 keys, see [`S7AckErrorKey`]); counters saturate. + ack_error_counts: std::collections::BTreeMap, } impl S7commAnalyzer { + /// Ack/Ack_Data error observations in arrival order, up to + /// [`MAX_S7_ACK_ERROR_OBSERVATIONS`]. + pub fn ack_error_observations(&self) -> &[S7AckErrorObservation] { + &self.ack_error_observations + } + + /// Exact per-key counts of every recorded Ack/Ack_Data error observation + /// (zeros included), regardless of the observation-list cap (F-07). + pub fn ack_error_counts(&self) -> &std::collections::BTreeMap { + &self.ack_error_counts + } + + /// Saturating count of observations dropped beyond the cap. + pub fn ack_error_observations_dropped(&self) -> u64 { + self.ack_error_observations_dropped + } + /// Construct a new, empty `S7commAnalyzer`. pub fn new() -> Self { Self { flows: HashMap::new(), findings: Vec::new(), + ack_error_observations: Vec::new(), + ack_error_observations_dropped: 0, + ack_error_counts: std::collections::BTreeMap::new(), } } @@ -389,24 +662,25 @@ impl S7commAnalyzer { /// `iso_on_tcp::parse_tpkt_header(&working[cursor..])`: a complete frame /// (`Some(header)` and enough trailing bytes) is extracted and dispatched to /// `iso_on_tcp::parse_cotp_header`, `cursor` advances by `header.length`, and - /// the loop continues; a declared-but-incomplete frame or a `None` result - /// breaks the loop. - /// 3. On a bad-version-byte reject (or immediately after a carry-overflow clear), - /// the shared 1-byte resync sub-routine (BC-2.20.015; see - /// [`Self::resync_one_byte`]) advances the cursor and retries. + /// the loop continues; a declared-but-incomplete frame or `None` breaks the loop. + /// 3. On a bad-version-byte reject (or after a carry-overflow clear), the shared 1-byte + /// resync (BC-2.20.015; see [`Self::resync_one_byte`]) advances the cursor and retries. /// 4. Whatever remains after the loop terminates is stashed to `carry[direction]`. /// - /// Each extracted frame's `CotpHeader` is then routed through the BC-2.21.002 - /// four-way dispatch (see [`Self::dispatch_cotp_frame`]): CR/CC frames update - /// session-tracking state, and Data Transfer frames drive sticky protocol - /// classification and, for classic (`0x32`) S7comm on a sticky-Classic flow, - /// header dissection via [`parse_s7comm_header`]. + /// Each extracted frame's `CotpHeader` is routed through the BC-2.21.002 four-way + /// dispatch (see [`Self::dispatch_cotp_frame`]): CR/CC frames update session state; + /// Data Transfer frames drive sticky classification and, for classic (`0x32`) S7comm + /// on a sticky-Classic flow, header dissection via [`parse_s7comm_header`]. After the + /// BC-2.21.009 bounds check, Ack/Ack_Data error pairs are recorded (bounded list + + /// count map) and Job/Ack_Data parameter blocks are FC-classified (classification-only + /// placeholder, consumed by STORY-191/192). pub fn on_data(&mut self, flow_key: FlowKey, data: &[u8], ts: u32, direction: Direction) { use crate::findings::{Confidence, ThreatCategory, Verdict}; // Collect frame-walk findings locally to avoid a borrow conflict between the // per-flow state entry (below) and `self.findings`. let mut local_findings: Vec = Vec::new(); + let mut local_acks: Vec = Vec::new(); { let state = self.flows.entry(flow_key).or_default(); @@ -527,6 +801,7 @@ impl S7commAnalyzer { direction, ts, &mut local_findings, + &mut local_acks, ); cursor += total; } else { @@ -557,6 +832,30 @@ impl S7commAnalyzer { } self.findings.extend(local_findings); + self.record_ack_error_observations(local_acks); + } + + /// Appends `observed` to the bounded analyzer-wide record, in arrival order, + /// up to [`MAX_S7_ACK_ERROR_OBSERVATIONS`]; the remainder increments the + /// saturating dropped counter. Every observation, capped or not, increments + /// its saturating [`S7AckErrorKey`] count (BC-2.21.008 postcondition 4, + /// AC-188-010, F-07). + fn record_ack_error_observations(&mut self, observed: Vec) { + for observation in observed { + let key = S7AckErrorKey { + rosctr: observation.rosctr, + error_class: observation.error_class, + error_code: observation.error_code, + }; + let count = self.ack_error_counts.entry(key).or_insert(0); + *count = count.saturating_add(1); + if self.ack_error_observations.len() < MAX_S7_ACK_ERROR_OBSERVATIONS { + self.ack_error_observations.push(observation); + } else { + self.ack_error_observations_dropped = + self.ack_error_observations_dropped.saturating_add(1); + } + } } /// Remove `flow_key`'s [`S7commFlowState`], discarding any carry bytes with no @@ -619,6 +918,7 @@ impl S7commAnalyzer { direction: Direction, ts: u32, findings: &mut Vec, + acks: &mut Vec, ) { match cotp { None => { @@ -670,7 +970,7 @@ impl S7commAnalyzer { if state.classified_protocol == Some(S7Protocol::Classic) { let payload = &tpkt_payload[header.payload_offset..]; Self::dispatch_classic_s7comm( - state, payload, direction, ts, findings, + state, payload, direction, ts, findings, acks, ); } } @@ -727,15 +1027,16 @@ impl S7commAnalyzer { /// payload slice beginning at `payload_offset`) and applies the BC-2.21.009 /// caller-side bounds check (`data.len() >= header_len + param_length + /// data_length`) before any parameter/data-block slice — malformed headers and - /// bounds failures emit one T0814 per flow direction via - /// `malformed_header_reported_c2s`/`_s2c` (BC-2.21.001). - /// + /// bounds failures emit one T0814 per flow direction via `malformed_header_reported_*` + /// (BC-2.21.001). On bounds pass, Ack/Ack_Data error pairs are recorded (bounded list + + /// count map) and Job/Ack_Data param blocks FC-classified (placeholder, STORY-191/192). fn dispatch_classic_s7comm( state: &mut S7commFlowState, payload: &[u8], direction: Direction, ts: u32, findings: &mut Vec, + acks: &mut Vec, ) { // F-15: this function is only ever reached from the `Some(0x32)` DT arm // above, whose `payload` is `&tpkt_payload[header.payload_offset..]` with @@ -769,8 +1070,30 @@ impl S7commAnalyzer { // checked-arithmetic comparison here, so this call site and the VP-051 // Kani harness share a single source of truth for the bounds decision. if s7comm_bounds_ok(&header, payload.len()) { - // Bounds check passes. Function-code/Userdata classification - // (BC-2.21.010 onward) is out of this story's scope (STORY-188/189). + // Bounds check passes (BC-2.21.009): the parameter block is safe to + // slice. Ack/Ack_Data error pairs are recorded (BC-2.21.008 PC4), and + // Job/Ack_Data parameter blocks are FC-classified (BC-2.21.010-017). + // Bare Ack frames carry no parameter block and are not FC-classified; + // Userdata is STORY-189's scope. + match header.rosctr { + Rosctr::Job => { + // Classification-only (STORY-188 B1 scope): the per-frame value + // is a deliberate placeholder with no consumer yet. STORY-191 + // (download-session correlation) and STORY-192 (cross-flow + // correlation) consume it; no state is kept here. + let _classified_function = + classify_job_ack_function(payload, header.header_len, header.param_length); + } + Rosctr::AckData => { + Self::record_ack_error(acks, &header); + // Classification-only placeholder, as for Job above: + // consumed by STORY-191 / STORY-192, not stored here. + let _classified_function = + classify_job_ack_function(payload, header.header_len, header.param_length); + } + Rosctr::Ack => Self::record_ack_error(acks, &header), + Rosctr::Userdata => {} + } } else { // Declared lengths exceed the bytes actually present (or, in the // unreachable overflow case, the sum would have overflowed `usize`) — @@ -791,6 +1114,20 @@ impl S7commAnalyzer { } } + /// Pushes the Ack/Ack_Data `error_class`/`error_code` pair (zeros included) + /// onto the per-call observation buffer (BC-2.21.008 postcondition 4). A header + /// whose error fields are `None` (Job/Userdata) records nothing. + fn record_ack_error(acks: &mut Vec, header: &S7commHeader) { + if let (Some(error_class), Some(error_code)) = (header.error_class, header.error_code) { + acks.push(S7AckErrorObservation { + pdu_reference: header.pdu_reference, + rosctr: header.rosctr, + error_class, + error_code, + }); + } + } + /// F-11: classifies *why* [`parse_s7comm_header`] rejected `payload`, purely to /// produce specific T0814 evidence text -- this classification never affects /// the accept/reject decision itself, which remains `parse_s7comm_header`'s diff --git a/tests/fixtures/mk_s7comm_pcap.py b/tests/fixtures/mk_s7comm_pcap.py index a79ca7fb..e93afa30 100644 --- a/tests/fixtures/mk_s7comm_pcap.py +++ b/tests/fixtures/mk_s7comm_pcap.py @@ -1,8 +1,9 @@ #!/usr/bin/env python3 """ -mk_s7comm_pcap.py — Generate tests/fixtures/s7comm-setup-comm.pcap +mk_s7comm_pcap.py — Generate tests/fixtures/s7comm-setup-comm.pcap and +tests/fixtures/s7comm-fc-classification.pcap -Produces a minimal libpcap (.pcap) file with classic magic (0xa1b2c3d4, +Produces minimal libpcap (.pcap) files with classic magic (0xa1b2c3d4, little-endian) and link-type 1 (Ethernet) containing a classic S7comm (protocol-ID 0x32) session over ISO-on-TCP (TPKT/COTP) on TCP/102. @@ -41,7 +42,7 @@ HOLDOUT-001); Kleinmann & Wool 2014 is a prose field-semantics source, not a test-vector source. Zero lines are borrowed from any external implementation. -This fixture is consumed by +The setup-comm capture (s7comm-setup-comm.pcap) is consumed by `test_BC_2_21_002_setup_comm_fixture_pcap_well_formed_no_findings` in `tests/s7comm_analyzer_tests.rs` — an end-to-end regression check that reads the committed capture, feeds every packet's TCP payload through @@ -49,7 +50,7 @@ findings, `session_established == true`, and `classified_protocol == Some(S7Protocol::Classic)`. -Packet sequence (all timestamps in seconds, realistic 2024-era epoch values): +Packet sequence of s7comm-setup-comm.pcap (all timestamps in seconds, realistic 2024-era epoch values): 1. [t=1_717_100_000] Client→Server SYN (TCP handshake — no payload) 2. [t=1_717_100_001] Server→Client SYN-ACK 3. [t=1_717_100_002] Client→Server ACK (handshake complete) @@ -65,9 +66,16 @@ 0x03, empty parameter/data blocks) 10. [t=1_717_100_009] Client→Server FIN-ACK +The function-code classification capture (s7comm-fc-classification.pcap, STORY-188) +is consumed by `test_BC_2_21_010_fc_classification_fixture_pcap_end_to_end`. Its +14-PDU S7comm sequence is: Job Setup Communication -> Ack_Data (setup response), +then Jobs 2..11 (one per classified function code), an Ack with reference 11, and +a final Ack_Data. + Usage: python3 tests/fixtures/mk_s7comm_pcap.py - # Writes tests/fixtures/s7comm-setup-comm.pcap + # Writes BOTH tests/fixtures/s7comm-setup-comm.pcap and + # tests/fixtures/s7comm-fc-classification.pcap """ import struct @@ -295,7 +303,7 @@ def setup_communication_response(pdu_reference: int) -> bytes: correctly emitted with the 12-byte Ack_Data header (error_class=0x00, error_code=0x00), matching the canonical cnblogs Ack_Data layout used by `test_BC_2_21_008_canonical_ack_data_setup_communication_response_on_data` - (parameter block at byte 12, per DF-CANONICAL-FRAME-HOLDOUT-001). + (parameter block at byte 12, per DF-CANONICAL-FRAME-HOLDOUT-001). Zero pair + parameter block: BC-2.21.008 EC-008. """ parameter = struct.pack("!BBHHH", 0xF0, 0x00, 0x0001, 0x0001, 0x01E0) return s7comm_pdu(ROSCTR_ACK_DATA, pdu_reference, parameter, b"") @@ -305,9 +313,9 @@ def minimal_job_pdu(pdu_reference: int) -> bytes: """ A minimal classic Job PDU with empty parameter/data blocks — the BC-2.21.006 EC-001 shape (`param_length == 0`, `data_length == 0`). - Function-code classification (Groups 3/4) is out of this story's scope - (STORY-188/189); this PDU exists only to exercise the header-level - Job/Ack_Data pairing this fixture models. + Function-code classification is STORY-188 (see the fc-classification + capture below) and Userdata classification is STORY-189; this PDU + exists only to exercise the header-level Job/Ack_Data pairing this fixture models. """ return s7comm_pdu(ROSCTR_JOB, pdu_reference, b"", b"") @@ -321,6 +329,97 @@ def minimal_ack_data_pdu(pdu_reference: int) -> bytes: return s7comm_pdu(ROSCTR_ACK_DATA, pdu_reference, b"", b"") +# --------------------------------------------------------------------------- +# STORY-188: Job/Ack_Data function-code classification frames (synthetic, +# CC0/MIT; field layout from ADR-014 Decision 4's permitted prose/design +# references only -- no copied dissector code). +# --------------------------------------------------------------------------- + + +def s7any_item(area: int, db_number: int = 0, address: int = 0) -> bytes: + """ + One 12-byte S7ANY address-item descriptor: var-spec 0x12, length 0x0A, + syntax-id 0x10 (S7ANY), transport size (1), element count (2 BE), + DB number (2 BE), area code (1), 3-byte bit address. The area-code byte is + at item offset 8, i.e. parameter-block offset 10 for a first item. + """ + return struct.pack( + "!BBBBHHB", 0x12, 0x0A, 0x10, 0x02, 0x0001, db_number, area + ) + address.to_bytes(3, "big") + + +def read_var_job(pdu_reference: int, area: int = 0x84) -> bytes: + return s7comm_pdu(ROSCTR_JOB, pdu_reference, bytes([0x04, 0x01]) + s7any_item(area), b"") + + +def write_var_job(pdu_reference: int, area: int) -> bytes: + parameter = bytes([0x05, 0x01]) + s7any_item(area) + data = bytes([0x00, 0x04, 0x00, 0x08, 0x2A]) # 1 data item, transport 0x04, 8 bits, value + return s7comm_pdu(ROSCTR_JOB, pdu_reference, parameter, data) + + +def simple_fc_job(pdu_reference: int, fc: int) -> bytes: + """Job whose parameter block is the bare function-code byte (download/upload triads, PLC Stop).""" + return s7comm_pdu(ROSCTR_JOB, pdu_reference, bytes([fc]), b"") + + +def plc_control_job(pdu_reference: int, service: bytes, block_args: bytes = b"") -> bytes: + """ + PLC Control (0x28) Job: FC (1) + 7 fixed bytes (00*6 + 0xFD) + + block-argument length (2 BE) + block arguments + service-name length (1) + + service-name ASCII. + """ + parameter = ( + bytes([0x28, 0, 0, 0, 0, 0, 0, 0xFD]) + + struct.pack("!H", len(block_args)) + + block_args + + bytes([len(service)]) + + service + ) + return s7comm_pdu(ROSCTR_JOB, pdu_reference, parameter, b"") + + +def ack_with_error(pdu_reference: int, error_class: int, error_code: int) -> bytes: + """Ack (0x02): 12-byte header, no parameter block, non-zero error pair.""" + return s7comm_pdu(ROSCTR_ACK, pdu_reference, b"", b"", error_class, error_code) + + +def ack_data_with_error_and_parameter( + pdu_reference: int, error_class: int, error_code: int +) -> bytes: + """ + Ack_Data (0x03): 12-byte header, non-zero error pair AND a Setup + Communication parameter block at data[12] (BC-2.21.008 EC-007). + """ + parameter = struct.pack("!BBHHH", 0xF0, 0x00, 0x0001, 0x0001, 0x01E0) + return s7comm_pdu(ROSCTR_ACK_DATA, pdu_reference, parameter, b"", error_class, error_code) + + +def build_fc_classification_pcap() -> bytes: + """ + tests/fixtures/s7comm-fc-classification.pcap: every STORY-188 function code + on one well-formed flow, plus an Ack and an Ack_Data frame carrying the + non-zero error pair 0x81/0x04 (AC-188-010). + """ + pdus = [ + (True, setup_communication_request(0x0001)), + (False, setup_communication_response(0x0001)), + (True, read_var_job(0x0002)), + (True, write_var_job(0x0003, 0x82)), + (True, simple_fc_job(0x0004, 0x1A)), + (True, simple_fc_job(0x0005, 0x1B)), + (True, simple_fc_job(0x0006, 0x1C)), + (True, simple_fc_job(0x0007, 0x1D)), + (True, simple_fc_job(0x0008, 0x1E)), + (True, simple_fc_job(0x0009, 0x1F)), + (True, plc_control_job(0x000A, b"P_PROGRAM")), + (True, simple_fc_job(0x000B, 0x29)), + (False, ack_with_error(0x000B, 0x81, 0x04)), + (False, ack_data_with_error_and_parameter(0x0001, 0x81, 0x04)), + ] + return _build_capture(pdus) + + # --------------------------------------------------------------------------- # TCP flag constants # --------------------------------------------------------------------------- @@ -338,6 +437,23 @@ def minimal_ack_data_pdu(pdu_reference: int) -> bytes: def build_pcap() -> bytes: + """tests/fixtures/s7comm-setup-comm.pcap (STORY-187) -- byte-for-byte unchanged.""" + return _build_capture( + [ + (True, setup_communication_request(0x0001)), + (False, setup_communication_response(0x0001)), + (True, minimal_job_pdu(0x0002)), + (False, minimal_ack_data_pdu(0x0002)), + ] + ) + + +def _build_capture(s7_pdus) -> bytes: + """ + Shared capture builder: TCP handshake, COTP CR/CC, then one DT-wrapped + classic S7comm PDU per `(client_to_server, pdu)` entry in `s7_pdus` (one TCP + segment each, t0+5+i), then a client FIN-ACK. + """ packets = [] # Base timestamp: 2024-05-30 20:13:20 UTC (Unix epoch 1717100000) @@ -402,22 +518,15 @@ def send(direction_client_to_server, payload, t_offset): # --- Packet 5: COTP Connect Confirm --- send(False, tpkt_frame(cotp_cc()), 4) - # --- Packet 6: Setup Communication request (Job) --- - send(True, tpkt_frame(cotp_dt(setup_communication_request(0x0001))), 5) - - # --- Packet 7: Setup Communication response (Ack_Data) --- - send(False, tpkt_frame(cotp_dt(setup_communication_response(0x0001))), 6) - - # --- Packet 8: minimal classic Job PDU (empty parameter/data blocks) --- - send(True, tpkt_frame(cotp_dt(minimal_job_pdu(0x0002))), 7) + # --- Packets 6..: one DT-wrapped S7comm PDU per entry --- + for i, (c2s, pdu) in enumerate(s7_pdus): + send(c2s, tpkt_frame(cotp_dt(pdu)), 5 + i) - # --- Packet 9: minimal classic Ack_Data PDU (empty parameter/data blocks) --- - send(False, tpkt_frame(cotp_dt(minimal_ack_data_pdu(0x0002))), 8) - - # --- Packet 10: Client->Server FIN-ACK --- + # --- Final packet (number 6 + len(s7_pdus); 10 for the 4-PDU setup-comm + # capture): Client->Server FIN-ACK --- packets.append( ( - t0 + 9, + t0 + 5 + len(s7_pdus), build_frame( CLIENT_MAC, SERVER_MAC, CLIENT_IP, SERVER_IP, CLIENT_PORT, SERVER_PORT, client_seq, server_seq, FIN_ACK, b"", @@ -443,3 +552,9 @@ def send(direction_client_to_server, payload, t_offset): print(" minimal Job/Ack_Data pair + FIN-ACK)") print(" - Port 102 (ISO-on-TCP / S7comm)") print(f" - Timestamps: {1_717_100_000} .. {1_717_100_009} (Unix epoch, 2024-05-30)") + + fc_path = os.path.join(script_dir, "s7comm-fc-classification.pcap") + fc_data = build_fc_classification_pcap() + with open(fc_path, "wb") as f: + f.write(fc_data) + print(f"Wrote {len(fc_data)} bytes to {fc_path}") diff --git a/tests/fixtures/s7comm-fc-classification.pcap b/tests/fixtures/s7comm-fc-classification.pcap new file mode 100644 index 00000000..601aa951 Binary files /dev/null and b/tests/fixtures/s7comm-fc-classification.pcap differ diff --git a/tests/s7comm_analyzer_tests.rs b/tests/s7comm_analyzer_tests.rs index 499ceeac..2b9c194f 100644 --- a/tests/s7comm_analyzer_tests.rs +++ b/tests/s7comm_analyzer_tests.rs @@ -4460,9 +4460,9 @@ mod story_187 { /// declared `param_length`/`data_length` are checked against. Proves /// `s7comm_bounds_ok` returns EXACTLY the right answer (the equality /// asserted directly, both directions, not merely one direction of an - /// implication) and that a `true` result implies the resulting - /// parameter/data sub-slice access is always `Some(..)`, never `None` and - /// never a construct that could panic. + /// implication). The former "`true` implies sub-slice access is `Some(..)`" + /// assertion was removed by STORY-188 (PRF-005); the slicing obligation is + /// now discharged by `story_188::vp051_kani::verify_classify_job_ack_function_param_slicing_safe`. /// /// Bounded per the VP-051 Kani Obligation note's own justification: /// `data_len <= u16::MAX as usize * 3` represents any hypothetical @@ -4496,20 +4496,16 @@ mod story_187 { false-reject" ); - if expected { - // A symbolic buffer of length data_len -- the hypothetical full - // delivery. When the bounds check passes, the parameter/data - // sub-slice access must always succeed. - let full: Vec = vec![0u8; data_len]; - let param_data_end = - header.header_len + header.param_length as usize + header.data_length as usize; - assert!( - full.get(header.header_len..param_data_end).is_some(), - "VP-051 F-18: when s7comm_bounds_ok is true, the parameter/data \ - sub-slice access data.get(header_len..header_len+param_length+ \ - data_length) must be Some(..), never None, never a panic" - ); - } + // PRF-005 (STORY-188 carry-forward): the former + // `vec![0u8; data_len].get(header_len..param_data_end).is_some()` + // assertion here only re-proved `Vec::get`'s own contract and exercised + // none of this crate's parameter/data-block slicing. The real + // "bounds-ok => parameter-block slicing is safe" obligation is now proven + // by `story_188::vp051_kani::verify_classify_job_ack_function_param_slicing_safe`, + // which drives the production parameter-block slicing performed by + // `classify_job_ack_function` (data[header_len..header_len+param_length]) + // under `s7comm_bounds_ok`. This harness keeps the exact-equality proof + // of `s7comm_bounds_ok` itself above. // NON-VACUITY (F-18, DF-KANI-NONVACUITY-001): both the bounds-ok-true and // bounds-ok-false outcomes must be reachable under the symbolic inputs, @@ -5217,3 +5213,1378 @@ mod story_187 { ); } } + +// ============================================================================= +// STORY-188: S7comm Job/Ack_Data Function-Code Classification. +// +// Covers BC-2.21.008 (postcondition 4 only: Ack/Ack_Data error_class/error_code +// consumption into the bounded record + count map (human ruling R1, 2026-10-04: no +// logging)), BC-2.21.010 .. BC-2.21.017, the VP-052 proptest +// (FC totality sub-part) and the VP-054 proptest (Download/Upload structural +// disjointness), and the PRF-005 Kani retarget. +// +// Authored Red-first against the `todo!()` stub of `classify_job_ack_function` +// and the not-yet-wired `on_data` Ack error recording (AC-188-010). +// +// Observation surface for AC-188-010 (human rulings 2026-10-04): the analyzer +// records Ack/Ack_Data error pairs ANALYZER-SIDE, with no stderr / eprintln! / +// child-process channel. Two surfaces are pinned: +// - `ack_error_observations()`: an arrival-ordered record, bounded at +// `MAX_S7_ACK_ERROR_OBSERVATIONS`, each entry carrying `pdu_reference`, +// `rosctr`, `error_class`, `error_code`; overflow is counted by +// `ack_error_observations_dropped()`. +// - `ack_error_counts()`: an exact per-`S7AckErrorKey` (rosctr, class, code) +// histogram of EVERY recorded observation, including those beyond the list +// cap (so a late distinct non-zero pair is never lost; counts saturate at +// u64::MAX). Zero pairs are counted like any other (EC-004/EC-007). +// Job/Userdata frames record nothing, and a frame failing the BC-2.21.009 bounds +// check records nothing (it is treated identically to a malformed header and +// yields the T0814 malformed finding instead). +// Provenance: an earlier revision of this module pinned a stderr line observed +// via a re-executed child process; that contract was superseded by the +// 2026-10-04 human rulings (bounded analyzer-side record, then the histogram). +// +// Wire layouts used (ADR-014 Decision 4: public wire-capture / prose-derived +// layouts only, no copied dissector code): +// - Write Var parameter block: FC 0x05, item count, then a 12-byte S7ANY item +// (0x12, 0x0A, 0x10 syntax-id, transport, count(2), db(2), AREA, addr(3)), so +// the first item's area byte is at parameter offset 10. +// - PLC Control parameter block: FC 0x28, 7 fixed bytes (00*6, 0xFD), block-arg +// length (u16 BE), block args, service-name length (1), service-name ASCII. +// ============================================================================= +mod story_188 { + use wirerust::analyzer::s7comm::{ + MAX_S7_ACK_ERROR_OBSERVATIONS, PlcControlService, Rosctr, S7AckErrorKey, + S7AckErrorObservation, S7AreaCode, S7ClassicFunction, S7commAnalyzer, + classify_job_ack_function, parse_s7comm_header, s7comm_bounds_ok, + }; + use wirerust::reassembly::flow::FlowKey; + use wirerust::reassembly::handler::Direction; + + use S7ClassicFunction as F; + + // --------------------------------------------------------------------- + // Frame builders + // --------------------------------------------------------------------- + + fn flow_key_default() -> FlowKey { + FlowKey::new( + "127.0.0.1".parse().unwrap(), + 1234, + "127.0.0.2".parse().unwrap(), + 102, + ) + } + + fn tpkt_frame(cotp_payload: &[u8]) -> Vec { + let len = (4 + cotp_payload.len()) as u16; + let mut f = vec![0x03u8, 0x00, (len >> 8) as u8, (len & 0xFF) as u8]; + f.extend_from_slice(cotp_payload); + f + } + + fn cr_frame() -> Vec { + tpkt_frame(&[0x01, 0xE0, 0x00]) + } + + fn cc_frame() -> Vec { + tpkt_frame(&[0x01, 0xD0, 0x00]) + } + + fn dt_frame(upper: &[u8]) -> Vec { + let mut cotp = vec![0x01u8, 0xF0]; + cotp.extend_from_slice(upper); + tpkt_frame(&cotp) + } + + const ROSCTR_JOB: u8 = 0x01; + const ROSCTR_ACK: u8 = 0x02; + const ROSCTR_ACK_DATA: u8 = 0x03; + const ROSCTR_USERDATA: u8 = 0x07; + + /// Builds a full classic S7comm PDU (starting at the 0x32 byte). Returns + /// `(pdu, header_len, param_length)`. Ack/Ack_Data use the 12-byte header with + /// `err = (error_class, error_code)`; Job uses the 10-byte header. + fn build_pdu( + rosctr: u8, + err: (u8, u8), + param: &[u8], + data_block: &[u8], + ) -> (Vec, usize, u16) { + let mut v = vec![0x32u8, rosctr, 0x00, 0x00, 0x00, 0x01]; + v.extend_from_slice(&(param.len() as u16).to_be_bytes()); + v.extend_from_slice(&(data_block.len() as u16).to_be_bytes()); + let mut header_len = 10; + if rosctr == ROSCTR_ACK || rosctr == ROSCTR_ACK_DATA { + v.push(err.0); + v.push(err.1); + header_len = 12; + } + v.extend_from_slice(param); + v.extend_from_slice(data_block); + (v, header_len, param.len() as u16) + } + + /// Classifies `param`/`data_block` under BOTH `Job` (header_len 10) and + /// `AckData` (header_len 12, with non-FC-looking error bytes 0xEE/0xEE so a + /// classifier that reads `data[10]` instead of `data[header_len]` is caught). + /// Returns `[job_result, ack_data_result]`. + fn classify_both(param: &[u8], data_block: &[u8]) -> [S7ClassicFunction; 2] { + let (job, jh, jp) = build_pdu(ROSCTR_JOB, (0, 0), param, data_block); + let (ack, ah, ap) = build_pdu(ROSCTR_ACK_DATA, (0xEE, 0xEE), param, data_block); + [ + classify_job_ack_function(&job, jh, jp), + classify_job_ack_function(&ack, ah, ap), + ] + } + + fn assert_both(param: &[u8], data_block: &[u8], expected: S7ClassicFunction, ctx: &str) { + let [job, ack_data] = classify_both(param, data_block); + assert_eq!(job, expected, "{ctx}: Job (header_len 10)"); + assert_eq!(ack_data, expected, "{ctx}: AckData (header_len 12)"); + } + + /// 12-byte S7ANY item descriptor with the given area byte at item offset 8. + fn s7any_item(area: u8) -> Vec { + vec![ + 0x12, 0x0A, 0x10, 0x02, 0x00, 0x01, 0x00, 0x00, area, 0x00, 0x00, 0x00, + ] + } + + /// Write Var parameter block: FC 0x05, 1 item, S7ANY item with `area`. + fn write_var_param(area: u8) -> Vec { + let mut p = vec![0x05u8, 0x01]; + p.extend(s7any_item(area)); + p + } + + /// PLC Control parameter block (see module comment for the layout). + fn plc_control_param(service: &[u8], block_args: &[u8]) -> Vec { + let mut p = vec![0x28u8, 0, 0, 0, 0, 0, 0, 0xFD]; + p.extend_from_slice(&(block_args.len() as u16).to_be_bytes()); + p.extend_from_slice(block_args); + p.push(service.len() as u8); + p.extend_from_slice(service); + p + } + + /// Classifies a PLC Control parameter block that has been cut to `keep` bytes + /// of parameter block; the cut-off remainder stays available in the data + /// block, proving the decode is bounded by `param_length`, not by `data.len()`. + fn classify_plc_control_cut(param: &[u8], keep: usize) -> [S7ClassicFunction; 2] { + classify_both(¶m[..keep], ¶m[keep..]) + } + + /// Observation literal for frames built by `build_pdu` (PDU reference 0x0001). + fn obs(rosctr: Rosctr, error_class: u8, error_code: u8) -> S7AckErrorObservation { + obs_ref(1, rosctr, error_class, error_code) + } + + fn obs_ref( + pdu_reference: u16, + rosctr: Rosctr, + error_class: u8, + error_code: u8, + ) -> S7AckErrorObservation { + S7AckErrorObservation { + pdu_reference, + rosctr, + error_class, + error_code, + } + } + + /// Feeds CR, CC, then each `(direction, pdu)` as its own DT frame into a fresh + /// analyzer; asserts no finding is ever emitted (BC-2.21.008 PC4 / BC-2.21.017 + /// PC3: recording and classification emit no `Finding`). Returns the analyzer. + fn drive_session(pdus: &[(Direction, Vec)]) -> S7commAnalyzer { + let mut analyzer = S7commAnalyzer::new(); + let key = flow_key_default(); + analyzer.on_data(key.clone(), &cr_frame(), 0, Direction::ClientToServer); + analyzer.on_data(key.clone(), &cc_frame(), 0, Direction::ServerToClient); + for (dir, pdu) in pdus { + analyzer.on_data(key.clone(), &dt_frame(pdu), 1, *dir); + } + assert!( + analyzer.findings.is_empty(), + "well-formed Job/Ack/Ack_Data frames must emit no Finding: {:?}", + analyzer.findings + ); + analyzer + } + + fn setup_comm_param() -> Vec { + vec![0xF0, 0x00, 0x00, 0x01, 0x00, 0x01, 0x03, 0xC0] + } + + // --------------------------------------------------------------------- + // AC-188-001 .. AC-188-008: unit tests + // --------------------------------------------------------------------- + + /// AC-188-001: FC 0xF0 -> SetupCommunication for Job and AckData; no further + /// parameter bytes interpreted (a bare `[0xF0]` and a garbage-trailed block + /// classify identically). + /// Traces: BC-2.21.010 postconditions 1-3. + #[test] + fn test_BC_2_21_010_setup_communication_classified() { + assert_both( + &setup_comm_param(), + &[], + F::SetupCommunication, + "full setup comm", + ); + assert_both(&[0xF0], &[], F::SetupCommunication, "bare FC byte"); + assert_both( + &[0xF0, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF], + &[], + F::SetupCommunication, + "arbitrary trailing parameter bytes are not interpreted", + ); + } + + /// AC-188-002: FC 0x04 -> ReadVar, never WriteVar, no area decode. + /// Traces: BC-2.21.011 postconditions 1-2 (canonical vectors Job/0x04, AckData/0x04). + #[test] + fn test_BC_2_21_011_read_var_classified_no_area_decode() { + let mut p = vec![0x04u8, 0x01]; + p.extend(s7any_item(0x84)); + assert_both(&p, &[], F::ReadVar, "read var with S7ANY item"); + assert_both(&[0x04], &[], F::ReadVar, "bare read var"); + } + + /// AC-188-003: FC 0x05 -> WriteVar(area) for the 8 named areas plus + /// unrecognized bytes (story EC-001: 0xFF; BC EC-002: 0x86; canonical 0x9A); + /// unreadable descriptor -> WriteVar(Unrecognized(0xFF)) placeholder, never a + /// reject; multi-item uses first item only; decode bounded by param_length. + /// Traces: BC-2.21.012 postconditions 1-4, BC EC-001/002/003, canonical vectors. + #[test] + fn test_BC_2_21_012_write_var_area_code_extraction() { + let table: [(u8, S7AreaCode); 8] = [ + (0x80, S7AreaCode::DirectPeripheral), + (0x81, S7AreaCode::Inputs), + (0x82, S7AreaCode::Outputs), + (0x83, S7AreaCode::Markers), + (0x84, S7AreaCode::DataBlock), + (0x85, S7AreaCode::InstanceDb), + (0x1C, S7AreaCode::Counters), + (0x1D, S7AreaCode::Timers), + ]; + for (byte, area) in table { + assert_both( + &write_var_param(byte), + &[0x00, 0x04, 0x00, 0x08, 0x2A], + F::WriteVar(area), + &format!("area byte {byte:#04x}"), + ); + } + for byte in [0xFFu8, 0x86, 0x9A, 0x00] { + assert_both( + &write_var_param(byte), + &[], + F::WriteVar(S7AreaCode::Unrecognized(byte)), + &format!("unrecognized area byte {byte:#04x} (no force-fit)"), + ); + } + + // Postcondition 3 / BC EC-003: undeterminable area -> WriteVar, placeholder 0xFF. + let placeholder = F::WriteVar(S7AreaCode::Unrecognized(0xFF)); + assert_both(&[0x05], &[], placeholder, "bare FC, no item at all"); + assert_both( + &[0x05, 0x01, 0x12, 0x0A, 0x10], + &[], + placeholder, + "truncated item", + ); + let mut bad_syntax = write_var_param(0x82); + bad_syntax[4] = 0x11; // non-S7ANY syntax id + assert_both( + &bad_syntax, + &[], + placeholder, + "non-S7ANY syntax id not decoded", + ); + + // Decode is bounded by param_length: the complete item sits in the data + // block, past param_length, and must not be read as parameter bytes. + let full = write_var_param(0x82); + assert_both( + &full[..5], + &full[5..], + placeholder, + "item bytes beyond param_length", + ); + + // Postcondition 4: multi-item block -> first item's area only. + let mut multi = vec![0x05u8, 0x02]; + multi.extend(s7any_item(0x82)); + multi.extend(s7any_item(0x84)); + assert_both( + &multi, + &[], + F::WriteVar(S7AreaCode::Outputs), + "first item only", + ); + } + + /// AC-188-003 / BC-2.21.012 Invariant 1 (no VP): every u8 area byte maps to exactly one `S7AreaCode` + /// (8 named + Unrecognized(byte) passthrough), no gaps, no force-fit. + /// Traces: BC-2.21.012 invariant 1. + mod area_exhaustive { + use super::*; + use proptest::prelude::*; + + fn expected_area(b: u8) -> S7AreaCode { + match b { + 0x80 => S7AreaCode::DirectPeripheral, + 0x81 => S7AreaCode::Inputs, + 0x82 => S7AreaCode::Outputs, + 0x83 => S7AreaCode::Markers, + 0x84 => S7AreaCode::DataBlock, + 0x85 => S7AreaCode::InstanceDb, + 0x1C => S7AreaCode::Counters, + 0x1D => S7AreaCode::Timers, + other => S7AreaCode::Unrecognized(other), + } + } + + proptest! { + #![proptest_config(ProptestConfig::with_cases(2000))] + #[test] + fn test_BC_2_21_012_write_var_area_code_exhaustive_over_all_u8( + area in any::(), + db in proptest::collection::vec(any::(), 0..8), + ) { + let param = write_var_param(area); + let [job, ack_data] = classify_both(¶m, &db); + prop_assert_eq!(job, F::WriteVar(expected_area(area))); + prop_assert_eq!(ack_data, F::WriteVar(expected_area(area))); + } + } + } + + /// AC-188-004: Download triad 0x1A/0x1B/0x1C classified independently, + /// never as an Upload variant; story EC-002: consecutive RequestDownload frames are + /// each classified independently (no cross-frame state). + /// Traces: BC-2.21.013 postconditions 1-4. + #[test] + fn test_BC_2_21_013_download_triad_classified_independently() { + let cases = [ + (0x1Au8, F::RequestDownload), + (0x1B, F::DownloadBlock), + (0x1C, F::DownloadEnded), + ]; + for (fc, expected) in cases { + assert_both(&[fc], &[], expected, &format!("download FC {fc:#04x}")); + assert_both( + &[fc, 0x01, 0x02, 0x03, 0x04], + &[0xAA, 0xBB], + expected, + &format!("download FC {fc:#04x} with trailing block bytes (no block decode)"), + ); + } + // EC-002: two RequestDownload frames back to back, no DownloadEnded between. + let first = classify_both(&[0x1A], &[]); + let second = classify_both(&[0x1A], &[]); + assert_eq!(first, [F::RequestDownload, F::RequestDownload]); + assert_eq!(second, [F::RequestDownload, F::RequestDownload]); + } + + /// AC-188-005: Upload triad 0x1D/0x1E/0x1F classified; disjoint from Download. + /// Traces: BC-2.21.014 postconditions 1-4, STORY-188 EC-003 (no collapsed 0x1A..=0x1F range). + #[test] + fn test_BC_2_21_014_upload_triad_classified_disjoint_from_download() { + let cases = [ + (0x1Du8, F::StartUpload), + (0x1E, F::Upload), + (0x1F, F::EndUpload), + ]; + let download = [F::RequestDownload, F::DownloadBlock, F::DownloadEnded]; + for (fc, expected) in cases { + assert_both(&[fc], &[], expected, &format!("upload FC {fc:#04x}")); + let [job, ack] = classify_both(&[fc, 0x09], &[]); + assert!(!download.contains(&job) && !download.contains(&ack)); + } + // Boundary neighbours: 0x19 and 0x20 are outside the triads. + assert_both( + &[0x19], + &[], + F::Unrecognized(0x19), + "just below Download triad", + ); + assert_both( + &[0x20], + &[], + F::Unrecognized(0x20), + "just above Upload triad", + ); + } + + /// AC-188-006: PLC Control (0x28) with PI-service decode: one case per named + /// string plus the unrecognized fallback. + /// Traces: BC-2.21.015 postconditions 1-4, EC-001..EC-005 (BC). + #[test] + fn test_BC_2_21_015_plc_control_service_string_decode() { + let named: [(&[u8], &[u8], PlcControlService); 5] = [ + (b"P_PROGRAM", &[], PlcControlService::ProgramStart), + ( + b"_INSE", + &[0x01, 0x00, 0x30, 0x42, 0x30, 0x30, 0x30, 0x30, 0x31, 0x41], + PlcControlService::BlockActivate, + ), + ( + b"_DELE", + &[0x01, 0x00, 0x30, 0x42, 0x30, 0x30, 0x30, 0x30, 0x31, 0x41], + PlcControlService::BlockDelete, + ), + (b"_GARB", &[], PlcControlService::MemoryCompress), + (b"_MODU", &[], PlcControlService::RamToRom), + ]; + for (name, args, svc) in named { + assert_both( + &plc_control_param(name, args), + &[], + F::PlcControl(svc), + &format!("service {}", String::from_utf8_lossy(name)), + ); + } + assert_both( + &plc_control_param(b"_XXXX", &[]), + &[], + F::PlcControl(PlcControlService::Unrecognized), + "unknown service string", + ); + assert_both( + &plc_control_param(b"P_PROGRAX", &[]), + &[], + F::PlcControl(PlcControlService::Unrecognized), + "near-miss service string", + ); + } + + /// AC-188-006: truncated / case-variant / prefix service strings are + /// `Unrecognized` (never a reject, no partial-prefix matching, no case-folding). + /// Traces: BC-2.21.015 postcondition 3, EC-006/007/008 (BC), EC-005 (story). + #[test] + fn test_BC_2_21_015_plc_control_truncated_and_case_variants_unrecognized() { + let unrec = F::PlcControl(PlcControlService::Unrecognized); + + // EC-006 (BC): "_INS" (length prefix 4, no final byte) -- no prefix match. + assert_both(&plc_control_param(b"_INS", &[]), &[], unrec, "_INS prefix"); + // EC-007 (BC): case variant. + assert_both( + &plc_control_param(b"p_program", &[]), + &[], + unrec, + "lowercase", + ); + assert_both( + &plc_control_param(b"_inse", &[]), + &[], + unrec, + "lowercase _inse", + ); + // EC-008 (BC): parameter block holds only the FC byte -> no service string. + assert_both(&[0x28], &[], unrec, "bare FC 0x28"); + assert_both( + &[0x28, 0, 0, 0, 0, 0, 0, 0xFD], + &[], + unrec, + "no service-length byte", + ); + + // EC-005 (story): the parameter block is cut mid-service-string while the + // remaining bytes stay present in the data block. + let full = plc_control_param(b"P_PROGRAM", &[]); + for keep in [full.len() - 1, full.len() - 4, 11] { + let [job, ack] = classify_plc_control_cut(&full, keep); + assert_eq!(job, unrec, "cut at {keep}: Job"); + assert_eq!(ack, unrec, "cut at {keep}: AckData"); + } + + // Length prefix claims more bytes than the parameter block holds. + let mut lying = plc_control_param(b"_INSE", &[]); + let idx = lying.len() - 6; // the service-length byte + lying[idx] = 9; + assert_both(&lying, &[], unrec, "length prefix exceeds available bytes"); + } + + /// AC-188-006: EC-004 (story): `"P_PROGRAM"` followed by additional undecoded + /// trailing parameter bytes is still `PlcControl(ProgramStart)`. + /// Traces: BC-2.21.015 postcondition 2, EC-004 (story). + #[test] + fn test_BC_2_21_015_plc_control_trailing_bytes_after_service_string() { + let mut p = plc_control_param(b"P_PROGRAM", &[]); + p.extend_from_slice(&[0x01, 0x02, 0x03, 0xFF]); + assert_both( + &p, + &[], + F::PlcControl(PlcControlService::ProgramStart), + "trailing bytes after P_PROGRAM", + ); + } + + /// AC-188-007: FC 0x29 -> PlcStop, no further decode. + /// Traces: BC-2.21.016 postconditions 1-2. + #[test] + fn test_BC_2_21_016_plc_stop_classified() { + assert_both(&[0x29], &[], F::PlcStop, "bare PLC stop"); + assert_both( + &[0x29, 0x00, 0x00, 0x00, 0x00, 0x00, 0x09, 0x50, 0x5F], + &[], + F::PlcStop, + "PLC stop with trailing (undecoded) bytes", + ); + } + + /// AC-188-008: unrecognized FC -> Unrecognized(fc) preserving the byte + /// (story EC-006: 0x00 with param_length 1; BC EC-002: 0x06; BC EC-004: 0xFF); + /// param_length == 0 -> NoParameterBlock, distinct from Unrecognized, even if + /// the data block begins with a byte that would be a named FC; emits no Finding. + /// Traces: BC-2.21.017 postconditions 1-3, invariant 2, BC EC-001..EC-004. + #[test] + fn test_BC_2_21_017_unrecognized_fc_and_empty_parameter_block() { + for fc in [0x00u8, 0x06, 0xFF, 0x03, 0x2A, 0x27, 0xF1, 0xEF] { + assert_both(&[fc], &[], F::Unrecognized(fc), &format!("FC {fc:#04x}")); + } + // param_length == 0 -> NoParameterBlock, regardless of what follows. + assert_both(&[], &[], F::NoParameterBlock, "empty param, empty data"); + assert_both( + &[], + &[0xF0, 0x04, 0x05], + F::NoParameterBlock, + "empty param, data block starting with a named FC byte", + ); + assert_ne!(F::NoParameterBlock, F::Unrecognized(0x00)); + + // No Finding at this layer for either case (through the public surface). + drive_session(&[ + ( + Direction::ClientToServer, + build_pdu(ROSCTR_JOB, (0, 0), &[0x06], &[]).0, + ), + ( + Direction::ServerToClient, + build_pdu(ROSCTR_ACK_DATA, (0, 0), &[], &[]).0, + ), + ]); + } + + // --------------------------------------------------------------------- + // AC-188-009 / VP-052 (FC totality sub-part) and AC-188-005 / VP-054 + // --------------------------------------------------------------------- + + /// Oracle for the FC match, independent of the implementation's structure. + fn fc_outcome_ok(fc: u8, r: S7ClassicFunction) -> bool { + match fc { + 0xF0 => r == F::SetupCommunication, + 0x04 => r == F::ReadVar, + 0x05 => matches!(r, F::WriteVar(_)), + 0x1A => r == F::RequestDownload, + 0x1B => r == F::DownloadBlock, + 0x1C => r == F::DownloadEnded, + 0x1D => r == F::StartUpload, + 0x1E => r == F::Upload, + 0x1F => r == F::EndUpload, + 0x28 => matches!(r, F::PlcControl(_)), + 0x29 => r == F::PlcStop, + other => r == F::Unrecognized(other), + } + } + + /// AC-188-009 (deterministic companion to the VP-052 proptest): every one of + /// the 256 FC byte values, under both header lengths, yields exactly the + /// oracle outcome and never `NoParameterBlock`; `param_length == 0` always + /// yields `NoParameterBlock`. + /// Traces: BC-2.21.017 invariant 1. + #[test] + fn test_BC_2_21_017_fc_classification_total_over_all_256_values() { + for fc in 0u8..=255 { + let [job, ack] = classify_both(&[fc], &[]); + assert!(fc_outcome_ok(fc, job), "Job fc {fc:#04x} -> {job:?}"); + assert!(fc_outcome_ok(fc, ack), "AckData fc {fc:#04x} -> {ack:?}"); + } + assert_both(&[], &[], F::NoParameterBlock, "param_length == 0"); + } + + mod vp052 { + use super::*; + use proptest::prelude::*; + + proptest! { + #![proptest_config(ProptestConfig::with_cases(2000))] + + /// AC-188-009 / VP-052 (FC totality sub-part, skeleton; full run in + /// STORY-194): for any FC byte, any trailing parameter bytes and any + /// data block, exactly one BC-2.21.010..017 outcome applies, and + /// `NoParameterBlock` appears iff `param_length == 0`. + #[test] + fn proptest_vp052_fc_classification_totality( + fc in any::(), + trailing in proptest::collection::vec(any::(), 0..40), + data_block in proptest::collection::vec(any::(), 0..8), + empty_param in proptest::bool::weighted(0.1), + ) { + if empty_param { + let [job, ack] = classify_both(&[], &data_block); + prop_assert_eq!(job, F::NoParameterBlock); + prop_assert_eq!(ack, F::NoParameterBlock); + } else { + let mut param = vec![fc]; + param.extend_from_slice(&trailing); + let [job, ack] = classify_both(¶m, &data_block); + prop_assert!(fc_outcome_ok(fc, job), "Job fc {:#04x} -> {:?}", fc, job); + prop_assert!(fc_outcome_ok(fc, ack), "AckData fc {:#04x} -> {:?}", fc, ack); + prop_assert_ne!(job, F::NoParameterBlock); + prop_assert_ne!(ack, F::NoParameterBlock); + } + } + } + } + + mod vp054 { + use super::*; + use proptest::prelude::*; + + fn is_download(r: S7ClassicFunction) -> bool { + matches!(r, F::RequestDownload | F::DownloadBlock | F::DownloadEnded) + } + + fn is_upload(r: S7ClassicFunction) -> bool { + matches!(r, F::StartUpload | F::Upload | F::EndUpload) + } + + proptest! { + #![proptest_config(ProptestConfig::with_cases(2000))] + + /// AC-188-005 / VP-054 (skeleton; full run in STORY-194): over every + /// FC byte, a Download variant is produced iff fc in 0x1A..=0x1C, an + /// Upload variant iff fc in 0x1D..=0x1F, mapped one-to-one in order; + /// no Download FC is ever an Upload variant and vice versa + /// (regression guard for a collapsed 0x1A..=0x1F range, STORY-188 EC-003). + #[test] + fn proptest_vp054_download_upload_structural_disjointness( + fc in any::(), + trailing in proptest::collection::vec(any::(), 0..16), + ) { + let mut param = vec![fc]; + param.extend_from_slice(&trailing); + let [job, ack] = classify_both(¶m, &[]); + for r in [job, ack] { + prop_assert_eq!(is_download(r), (0x1A..=0x1C).contains(&fc)); + prop_assert_eq!(is_upload(r), (0x1D..=0x1F).contains(&fc)); + prop_assert!(!(is_download(r) && is_upload(r))); + match fc { + 0x1A => prop_assert_eq!(r, F::RequestDownload), + 0x1B => prop_assert_eq!(r, F::DownloadBlock), + 0x1C => prop_assert_eq!(r, F::DownloadEnded), + 0x1D => prop_assert_eq!(r, F::StartUpload), + 0x1E => prop_assert_eq!(r, F::Upload), + 0x1F => prop_assert_eq!(r, F::EndUpload), + _ => {} + } + } + } + } + } + + // --------------------------------------------------------------------- + // AC-188-010: Ack / Ack_Data error_class / error_code consumed and recorded + // --------------------------------------------------------------------- + + /// AC-188-010: `on_data` records the observed Ack `error_class`/`error_code` + /// (0x81/0x04) in the analyzer-side record; the preceding Job frame records + /// nothing; no Finding. Traces: BC-2.21.008 postcondition 4 (Ack). + #[test] + fn test_BC_2_21_008_ack_error_class_code_consumed_and_logged() { + let analyzer = drive_session(&[ + // A Job first: it carries no error fields and must not be recorded. + ( + Direction::ClientToServer, + build_pdu(ROSCTR_JOB, (0, 0), &setup_comm_param(), &[]).0, + ), + // Ack (0x02): 12-byte header, no parameter block, error 0x81/0x04. + ( + Direction::ServerToClient, + build_pdu(ROSCTR_ACK, (0x81, 0x04), &[], &[]).0, + ), + ]); + assert_eq!( + analyzer.ack_error_observations(), + &[obs(Rosctr::Ack, 0x81, 0x04)], + "exactly one Ack observation (the Job frame must not be recorded)" + ); + assert_eq!(analyzer.ack_error_observations_dropped(), 0); + } + + /// AC-188-010 / story EC-008: Ack_Data error fields (0x81/0x04) are recorded; the + /// populated error pair does not suppress FC classification, which reads the + /// parameter block at `data[header_len] == data[12]` (not `data[10]`). + /// Traces: BC-2.21.008 postcondition 4 (Ack_Data, v1.2), EC-008 (story), + /// BC-2.21.010 (independent FC classification). + #[test] + fn test_BC_2_21_008_ack_data_error_class_code_consumed_and_logged() { + let (pdu, hl, pl) = build_pdu(ROSCTR_ACK_DATA, (0x81, 0x04), &setup_comm_param(), &[]); + assert_eq!(hl, 12); + assert_eq!( + classify_job_ack_function(&pdu, hl, pl), + F::SetupCommunication, + "EC-008: error fields must not suppress/alter FC classification" + ); + // Error bytes that look like named FCs must not be read as the FC. + let (pdu2, hl2, pl2) = build_pdu(ROSCTR_ACK_DATA, (0x28, 0x29), &[0x04], &[]); + assert_eq!(classify_job_ack_function(&pdu2, hl2, pl2), F::ReadVar); + + let analyzer = drive_session(&[ + ( + Direction::ClientToServer, + build_pdu(ROSCTR_JOB, (0, 0), &setup_comm_param(), &[]).0, + ), + (Direction::ServerToClient, pdu), + ]); + assert_eq!( + analyzer.ack_error_observations(), + &[obs(Rosctr::AckData, 0x81, 0x04)], + "exactly one Ack_Data observation" + ); + assert_eq!(analyzer.ack_error_observations_dropped(), 0); + } + + /// AC-188-010 / story EC-007: a zero error class/code is recorded exactly like any + /// other value, for both Ack and Ack_Data (not flagged, not suppressed). + /// Traces: BC-2.21.008 EC-004, story EC-007. + #[test] + fn test_BC_2_21_008_zero_error_class_code_logged_for_ack_and_ack_data() { + let analyzer = drive_session(&[ + ( + Direction::ServerToClient, + build_pdu(ROSCTR_ACK, (0x00, 0x00), &[], &[]).0, + ), + ( + Direction::ServerToClient, + build_pdu(ROSCTR_ACK_DATA, (0x00, 0x00), &setup_comm_param(), &[]).0, + ), + ]); + assert_eq!( + analyzer.ack_error_observations(), + &[obs(Rosctr::Ack, 0, 0), obs(Rosctr::AckData, 0, 0)] + ); + } + + /// AC-188-010: Job frames record nothing (they carry no error fields). + /// Traces: BC-2.21.008 postcondition 4 (scope: Ack/Ack_Data only). + #[test] + fn test_BC_2_21_008_job_frames_record_no_ack_error_observation() { + let analyzer = drive_session(&[ + ( + Direction::ClientToServer, + build_pdu(ROSCTR_JOB, (0, 0), &setup_comm_param(), &[]).0, + ), + ( + Direction::ClientToServer, + build_pdu(ROSCTR_JOB, (0, 0), &[0x04], &[]).0, + ), + // Anchor: an Ack in the same session IS recorded, so an always-empty + // record cannot satisfy this test. + ( + Direction::ServerToClient, + build_pdu(ROSCTR_ACK, (0x05, 0x06), &[], &[]).0, + ), + ]); + assert_eq!( + analyzer.ack_error_observations(), + &[obs(Rosctr::Ack, 0x05, 0x06)] + ); + } + + /// AC-188-010: Userdata (ROSCTR 0x07) frames record nothing (10-byte header, no + /// error fields; the `Rosctr::Userdata` arm of the dispatcher is a no-op for + /// STORY-188). An Ack anchor in the same session proves recording is live, and + /// the count map holds only the anchor key. + /// Traces: BC-2.21.008 postcondition 4 (scope: Ack/Ack_Data only), PC3 header shape. + #[test] + fn test_BC_2_21_008_userdata_frames_record_no_ack_error_observation() { + let userdata_hdr_only = build_pdu(ROSCTR_USERDATA, (0, 0), &[], &[]); + assert_eq!(userdata_hdr_only.1, 10, "Userdata uses the 10-byte header"); + let analyzer = drive_session(&[ + (Direction::ClientToServer, userdata_hdr_only.0), + ( + Direction::ClientToServer, + build_pdu(ROSCTR_USERDATA, (0, 0), &[0x00, 0x01, 0x12], &[]).0, + ), + ( + Direction::ServerToClient, + build_pdu(ROSCTR_ACK, (0x05, 0x06), &[], &[]).0, + ), + ]); + assert_eq!( + analyzer.ack_error_observations(), + &[obs(Rosctr::Ack, 0x05, 0x06)], + "only the Ack anchor is recorded; Userdata frames are not" + ); + assert_eq!(analyzer.ack_error_observations_dropped(), 0); + let counts = analyzer.ack_error_counts(); + assert_eq!(counts.len(), 1, "count map holds only the anchor key"); + assert_eq!(counts.values().copied().sum::(), 1); + } + + /// AC-188-010 (bounded memory): cap + N Ack frames yield exactly + /// `MAX_S7_ACK_ERROR_OBSERVATIONS` retained observations, the first `cap` in + /// arrival order, and `dropped == N`. + #[test] + fn test_BC_2_21_008_ack_error_observations_bounded_by_cap_with_dropped_count() { + const EXTRA: usize = 7; + let pdus: Vec<(Direction, Vec)> = (0..MAX_S7_ACK_ERROR_OBSERVATIONS + EXTRA) + .map(|i| { + ( + Direction::ServerToClient, + build_pdu(ROSCTR_ACK, ((i >> 8) as u8, (i & 0xFF) as u8), &[], &[]).0, + ) + }) + .collect(); + let analyzer = drive_session(&pdus); + let got = analyzer.ack_error_observations(); + assert_eq!(got.len(), MAX_S7_ACK_ERROR_OBSERVATIONS); + for (i, o) in got.iter().enumerate() { + assert_eq!(*o, obs(Rosctr::Ack, (i >> 8) as u8, (i & 0xFF) as u8)); + } + assert_eq!(analyzer.ack_error_observations_dropped(), EXTRA as u64); + } + + // --------------------------------------------------------------------- + // Committed-fixture end-to-end (tests/fixtures/s7comm-fc-classification.pcap, + // generated by tests/fixtures/mk_s7comm_pcap.py) + // --------------------------------------------------------------------- + + /// `(direction, tcp_payload, timestamp)` for every payload-bearing packet in + /// the fixture (Ethernet/IPv4/TCP, destination port 102 = client-to-server). + fn fixture_payloads() -> Vec<(Direction, Vec, u32)> { + let path = std::path::Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/fixtures/s7comm-fc-classification.pcap"); + let source = wirerust::reader::PcapSource::from_file(&path) + .expect("committed s7comm-fc-classification.pcap must parse"); + let mut out = Vec::new(); + for packet in &source.packets { + let f = &packet.data; + let ihl = usize::from(f[14] & 0x0F) * 4; + let tcp = 14 + ihl; + let dst_port = u16::from_be_bytes([f[tcp + 2], f[tcp + 3]]); + let payload_start = tcp + usize::from(f[tcp + 12] >> 4) * 4; + let ip_total = usize::from(u16::from_be_bytes([f[16], f[17]])); + let end = (14 + ip_total).min(f.len()); + if payload_start >= end { + continue; + } + let dir = if dst_port == 102 { + Direction::ClientToServer + } else { + Direction::ServerToClient + }; + out.push((dir, f[payload_start..end].to_vec(), packet.timestamp_secs)); + } + out + } + + /// End-to-end over the committed fixture: (1) every S7comm PDU's function code + /// classifies as expected; (2) driving the whole capture through `on_data` records + /// the error pair of each Ack/Ack_Data frame, in order, and emits no Finding. + /// Traces: AC-188-001, 002, 003 (Outputs area only), 004, 005, 006, 007, 008 (Ack + /// frame -> NoParameterBlock), 010; BC-2.21.008 PC4, BC-2.21.010..016. Does NOT + /// exercise AC-188-009 (totality sweep) or AC-188-011 (canonical vectors). + #[test] + fn test_BC_2_21_010_fc_classification_fixture_pcap_end_to_end() { + use wirerust::analyzer::s7comm::parse_s7comm_header; + + { + let mut got = Vec::new(); + for (_, payload, _) in fixture_payloads() { + // Skip COTP CR/CC (LI=6 fixed part) -- only DT (02 F0 80) frames carry S7comm. + if payload.len() < 8 || payload[5] != 0xF0 { + continue; + } + let pdu = &payload[7..]; + let header = parse_s7comm_header(pdu).expect("fixture PDU header must parse"); + got.push(classify_job_ack_function( + pdu, + header.header_len, + header.param_length, + )); + } + let expected = vec![ + F::SetupCommunication, + F::SetupCommunication, + F::ReadVar, + F::WriteVar(S7AreaCode::Outputs), + F::RequestDownload, + F::DownloadBlock, + F::DownloadEnded, + F::StartUpload, + F::Upload, + F::EndUpload, + F::PlcControl(PlcControlService::ProgramStart), + F::PlcStop, + F::NoParameterBlock, + F::SetupCommunication, + ]; + assert_eq!(got, expected, "fixture FC sequence"); + } + + let mut analyzer = S7commAnalyzer::new(); + let key = flow_key_default(); + for (dir, payload, ts) in fixture_payloads() { + analyzer.on_data(key.clone(), &payload, ts, dir); + } + assert!( + analyzer.findings.is_empty(), + "fixture is well-formed; classification/recording must emit no Finding: {:?}", + analyzer.findings + ); + assert_eq!( + analyzer.ack_error_observations(), + &[ + obs(Rosctr::AckData, 0x00, 0x00), + obs_ref(11, Rosctr::Ack, 0x81, 0x04), + obs(Rosctr::AckData, 0x81, 0x04), + ], + "three Ack/Ack_Data frames in capture order" + ); + assert_eq!(analyzer.ack_error_observations_dropped(), 0); + let counts: Vec<(S7AckErrorKey, u64)> = analyzer + .ack_error_counts() + .iter() + .map(|(k, v)| (*k, *v)) + .collect(); + let ek = |rosctr, error_class, error_code| S7AckErrorKey { + rosctr, + error_class, + error_code, + }; + for (k, n) in [ + (ek(Rosctr::AckData, 0x00, 0x00), 1u64), + (ek(Rosctr::Ack, 0x81, 0x04), 1), + (ek(Rosctr::AckData, 0x81, 0x04), 1), + ] { + assert!( + counts.contains(&(k, n)), + "missing count {k:?}={n}: {counts:?}" + ); + } + assert_eq!( + counts.len(), + 3, + "exactly three distinct ack-error keys: {counts:?}" + ); + } + + // --------------------------------------------------------------------- + // PASS-1 REMEDIATION (2026-10-04): F-02 boundary, F-06 pin, F-07 histogram + // --------------------------------------------------------------------- + + /// F-02: Write Var descriptor length boundary. The item decode needs the full + /// 14-byte block (FC + count + 12-byte item); lengths 11, 12, 13 have the area + /// byte present at offset 10 but a truncated address, and must yield the + /// `Unrecognized(0xFF)` placeholder (never the decoded area); length 14 decodes. + /// The cut-off remainder stays in the data block to prove `param_length` bounds + /// the decode. Traces: BC-2.21.012 postcondition 3. + #[test] + fn test_BC_2_21_012_write_var_descriptor_length_boundary_11_12_13_14() { + let full = write_var_param(0x84); + assert_eq!(full.len(), 14); + let placeholder = F::WriteVar(S7AreaCode::Unrecognized(0xFF)); + for keep in [11usize, 12, 13] { + assert_eq!(full[10], 0x84, "area byte is at offset 10"); + let [job, ack] = classify_both(&full[..keep], &full[keep..]); + assert_eq!(job, placeholder, "Job, param_length {keep}"); + assert_eq!(ack, placeholder, "AckData, param_length {keep}"); + } + assert_both( + &full, + &[], + F::WriteVar(S7AreaCode::DataBlock), + "param_length 14 decodes the area", + ); + } + + /// F-06: an Ack_Data frame with a non-zero error pair whose declared + /// data_length exceeds the bytes present fails BC-2.21.009 bounds: it yields + /// the T0814 malformed finding and records NO ack-error observation (neither + /// the list nor the histogram). Traces: BC-2.21.008 PC4 + BC-2.21.009 PC2 + /// ("treated identically to a malformed header"). + #[test] + fn test_BC_2_21_008_bounds_failing_ack_data_records_no_ack_error_observation() { + let (mut pdu, _, _) = build_pdu(ROSCTR_ACK_DATA, (0x81, 0x04), &setup_comm_param(), &[]); + // Header: [0x32, rosctr, red(2), pdu_ref(2), param_len(2), data_len(2), ec, ecode] + let param_len = u16::from_be_bytes([pdu[6], pdu[7]]); + assert_eq!(param_len as usize, setup_comm_param().len()); + pdu[8] = 0x00; + pdu[9] = 0x20; // data_length = 32, but no data block follows + let mut analyzer = S7commAnalyzer::new(); + let key = flow_key_default(); + analyzer.on_data(key.clone(), &cr_frame(), 0, Direction::ClientToServer); + analyzer.on_data(key.clone(), &cc_frame(), 0, Direction::ServerToClient); + analyzer.on_data(key, &dt_frame(&pdu), 1, Direction::ServerToClient); + assert_eq!(analyzer.findings.len(), 1, "{:?}", analyzer.findings); + assert!( + analyzer.findings[0] + .evidence + .iter() + .any(|e| e.contains("declared param_length/data_length exceed")), + "{:?}", + analyzer.findings[0].evidence + ); + assert!(analyzer.ack_error_observations().is_empty()); + assert_eq!(analyzer.ack_error_observations_dropped(), 0); + assert!(analyzer.ack_error_counts().is_empty()); + } + + fn key(rosctr: Rosctr, error_class: u8, error_code: u8) -> S7AckErrorKey { + S7AckErrorKey { + rosctr, + error_class, + error_code, + } + } + + /// Overwrites the PDU reference (header bytes 4-5) of a built PDU. + fn with_pdu_ref(mut pdu: Vec, pdu_ref: u16) -> Vec { + pdu[4..6].copy_from_slice(&pdu_ref.to_be_bytes()); + pdu + } + + /// F-07: exact per-(rosctr, class, code) counts for mixed Ack / Ack_Data / + /// zero frames; Job frames never counted. Traces: BC-2.21.008 PC4, BC EC-004, story EC-007. + #[test] + fn test_BC_2_21_008_ack_error_counts_exact_for_mixed_frames() { + let ack = |c, e| build_pdu(ROSCTR_ACK, (c, e), &[], &[]).0; + let ackd = |c, e| build_pdu(ROSCTR_ACK_DATA, (c, e), &setup_comm_param(), &[]).0; + let job = build_pdu(ROSCTR_JOB, (0, 0), &setup_comm_param(), &[]).0; + let s = Direction::ServerToClient; + let analyzer = drive_session(&[ + (Direction::ClientToServer, job.clone()), + (s, ack(0, 0)), + (s, ack(0, 0)), + (s, ack(0x81, 0x04)), + (s, ackd(0x81, 0x04)), + (s, ackd(0x81, 0x04)), + (s, ackd(0x81, 0x04)), + (s, ackd(0, 0)), + (Direction::ClientToServer, job), + ]); + let got: Vec<(S7AckErrorKey, u64)> = analyzer + .ack_error_counts() + .iter() + .map(|(k, v)| (*k, *v)) + .collect(); + let mut want = vec![ + (key(Rosctr::Ack, 0, 0), 2u64), + (key(Rosctr::Ack, 0x81, 0x04), 1), + (key(Rosctr::AckData, 0, 0), 1), + (key(Rosctr::AckData, 0x81, 0x04), 3), + ]; + want.sort(); + assert_eq!(got, want, "Job frames must contribute no key"); + } + + /// F-07 regression: after the list cap is reached, a late DISTINCT non-zero + /// pair is still counted in the histogram (count 1) even though its list entry + /// is dropped; histogram total == cap + N; list len == cap; dropped == N. + #[test] + fn test_BC_2_21_008_ack_error_histogram_counts_beyond_list_cap() { + const EXTRA: usize = 3; + let ack = |c, e| { + ( + Direction::ServerToClient, + build_pdu(ROSCTR_ACK, (c, e), &[], &[]).0, + ) + }; + let mut pdus: Vec<(Direction, Vec)> = (0..MAX_S7_ACK_ERROR_OBSERVATIONS) + .map(|_| ack(0, 0)) + .collect(); + pdus.push(ack(0x81, 0x04)); // first frame past the cap, distinct non-zero + pdus.push(ack(0, 0)); + pdus.push(ack(0, 0)); + let analyzer = drive_session(&pdus); + assert_eq!( + analyzer.ack_error_observations().len(), + MAX_S7_ACK_ERROR_OBSERVATIONS + ); + assert_eq!(analyzer.ack_error_observations_dropped(), EXTRA as u64); + assert!( + analyzer + .ack_error_observations() + .iter() + .all(|o| o.error_class == 0 && o.error_code == 0), + "the late 0x81/0x04 list entry is dropped by the cap" + ); + let counts = analyzer.ack_error_counts(); + assert_eq!( + counts.get(&key(Rosctr::Ack, 0x81, 0x04)), + Some(&1), + "late distinct pair must survive in the histogram" + ); + assert_eq!( + counts.get(&key(Rosctr::Ack, 0, 0)), + Some(&(MAX_S7_ACK_ERROR_OBSERVATIONS as u64 + 2)) + ); + assert_eq!( + counts.values().sum::(), + (MAX_S7_ACK_ERROR_OBSERVATIONS + EXTRA) as u64 + ); + } + + /// F-07: each retained observation carries the PDU reference parsed from its + /// own header. + #[test] + fn test_BC_2_21_008_ack_error_observation_captures_pdu_reference() { + let analyzer = drive_session(&[ + ( + Direction::ServerToClient, + with_pdu_ref(build_pdu(ROSCTR_ACK, (0x81, 0x04), &[], &[]).0, 0x1234), + ), + ( + Direction::ServerToClient, + with_pdu_ref( + build_pdu(ROSCTR_ACK_DATA, (0, 0), &setup_comm_param(), &[]).0, + 0xBEEF, + ), + ), + ]); + assert_eq!( + analyzer.ack_error_observations(), + &[ + obs_ref(0x1234, Rosctr::Ack, 0x81, 0x04), + obs_ref(0xBEEF, Rosctr::AckData, 0, 0), + ] + ); + } + + /// F-07: Job-only traffic yields an empty histogram. + #[test] + fn test_BC_2_21_008_job_frames_contribute_no_histogram_key() { + let analyzer = drive_session(&[( + Direction::ClientToServer, + build_pdu(ROSCTR_JOB, (0, 0), &setup_comm_param(), &[]).0, + )]); + assert!(analyzer.ack_error_counts().is_empty()); + } + + // --------------------------------------------------------------------- + // F-01 canonical sub-group (DF-CANONICAL-FRAME-HOLDOUT-001): VERBATIM public + // wire-capture byte sequences, used as TEST VECTORS ONLY per ADR-014 + // Decision 4 (+ F-40 reconciliation, 2026-09-24). Field semantics are NOT + // derived from these bytes. Research record: + // .factory/research/s7comm-canonical-fc-vectors.md. Retrieved 2026-10-04. + // --------------------------------------------------------------------- + mod canonical { + use super::*; + + /// Strips TPKT(4) + COTP DT(`02 F0 80`) and returns the S7 PDU starting + /// at the 0x32 byte. + fn s7_pdu(frame: &[u8]) -> &[u8] { + assert_eq!(&frame[..2], &[0x03, 0x00], "TPKT version/reserved"); + assert_eq!(frame[2..4], (frame.len() as u16).to_be_bytes(), "TPKT len"); + assert_eq!(&frame[4..7], &[0x02, 0xF0, 0x80], "COTP DT"); + &frame[7..] + } + + /// Parses, bounds-checks and classifies the S7 PDU of `frame`. + fn classify_frame(frame: &[u8]) -> S7ClassicFunction { + let pdu = s7_pdu(frame); + let header = parse_s7comm_header(pdu).expect("canonical frame header parses"); + assert!(s7comm_bounds_ok(&header, pdu.len()), "bounds ok"); + classify_job_ack_function(pdu, header.header_len, header.param_length) + } + + /// Feeds `frame` (full TPKT/COTP) through `on_data`: no findings, and + /// returns the analyzer for further assertions. + fn on_data_clean(frame: &[u8], dir: Direction) -> S7commAnalyzer { + let mut analyzer = S7commAnalyzer::new(); + analyzer.on_data(flow_key_default(), frame, 0, dir); + assert!( + analyzer.findings.is_empty(), + "canonical frame must be well-formed: {:?}", + analyzer.findings + ); + analyzer + } + + // Source: https://www.cnblogs.com/crcce-dncs/p/10659087.html, Setup + // Communication Ack_Data response (as already used in story_187). Test + // vector only (ADR-014 Decision 4). Retrieved 2026-10-04. + const SETUP_COMM_ACK_DATA: [u8; 27] = [ + 0x03, 0x00, 0x00, 0x1B, 0x02, 0xF0, 0x80, 0x32, 0x03, 0x00, 0x00, 0xFF, 0xFF, 0x00, + 0x08, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x00, 0x00, 0x01, 0x00, 0x01, 0x00, 0xF0, + ]; + + // Source: https://www.cnblogs.com/crcce-dncs/p/10659087.html, section + // "Write Demo 1" (DB10 Word18). Test vector only (ADR-014 Decision 4). + // Retrieved 2026-10-04. + const WRITE_DB: [u8; 37] = [ + 0x03, 0x00, 0x00, 0x25, 0x02, 0xF0, 0x80, 0x32, 0x01, 0x00, 0x00, 0x00, 0x05, 0x00, + 0x0E, 0x00, 0x06, 0x05, 0x01, 0x12, 0x0A, 0x10, 0x02, 0x00, 0x02, 0x00, 0x0A, 0x84, + 0x00, 0x00, 0x90, 0x00, 0x04, 0x00, 0x10, 0xFF, 0xFE, + ]; + + // Source: same page, section "Write Demo 3" (Output0). Test vector only + // (ADR-014 Decision 4). Retrieved 2026-10-04. + const WRITE_OUTPUTS: [u8; 36] = [ + 0x03, 0x00, 0x00, 0x24, 0x02, 0xF0, 0x80, 0x32, 0x01, 0x00, 0x00, 0x00, 0x08, 0x00, + 0x0E, 0x00, 0x05, 0x05, 0x01, 0x12, 0x0A, 0x10, 0x02, 0x00, 0x01, 0x00, 0x01, 0x82, + 0x00, 0x00, 0x00, 0x00, 0x04, 0x00, 0x08, 0x04, + ]; + + // Source: same page, section "Read Demo 1" (DB10). Test vector only + // (ADR-014 Decision 4). Retrieved 2026-10-04. + const READ_DB: [u8; 31] = [ + 0x03, 0x00, 0x00, 0x1F, 0x02, 0xF0, 0x80, 0x32, 0x01, 0x00, 0x00, 0x00, 0x1C, 0x00, + 0x0E, 0x00, 0x00, 0x04, 0x01, 0x12, 0x0A, 0x10, 0x02, 0x00, 0x11, 0x00, 0x0A, 0x84, + 0x00, 0x00, 0x98, + ]; + + // Source: https://www.cnblogs.com/ZHIZRL/p/18184553, section "PLC Run" + // (service P_PROGRAM). Test vector only (ADR-014 Decision 4). Retrieved + // 2026-10-04. + const PLC_RUN: [u8; 37] = [ + 0x03, 0x00, 0x00, 0x25, 0x02, 0xF0, 0x80, 0x32, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x14, 0x00, 0x00, 0x28, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xFD, 0x00, 0x00, 0x09, + 0x50, 0x5F, 0x50, 0x52, 0x4F, 0x47, 0x52, 0x41, 0x4D, + ]; + + // Source: https://www.cnblogs.com/ZHIZRL/p/18184553, section "PLC Stop". + // NOTE the 0x29 layout differs from 0x28 (5 reserved bytes, no 0xFD, no + // u16 block-length). Test vector only (ADR-014 Decision 4). Retrieved + // 2026-10-04. + const PLC_STOP: [u8; 33] = [ + 0x03, 0x00, 0x00, 0x21, 0x02, 0xF0, 0x80, 0x32, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x10, 0x00, 0x00, 0x29, 0x00, 0x00, 0x00, 0x00, 0x00, 0x09, 0x50, 0x5F, 0x50, 0x52, + 0x4F, 0x47, 0x52, 0x41, 0x4D, + ]; + + /// Canonical Setup Communication Ack_Data response classifies as + /// SetupCommunication via parse -> bounds -> classify at header_len 12. + #[test] + fn test_BC_2_21_010_canonical_setup_communication_ack_data_classified() { + let pdu = s7_pdu(&SETUP_COMM_ACK_DATA); + let h = parse_s7comm_header(pdu).unwrap(); + assert_eq!(h.rosctr, Rosctr::AckData); + assert_eq!(h.header_len, 12); + assert_eq!(classify_frame(&SETUP_COMM_ACK_DATA), F::SetupCommunication); + let a = on_data_clean(&SETUP_COMM_ACK_DATA, Direction::ServerToClient); + assert_eq!( + a.ack_error_observations(), + &[obs_ref(0xFFFF, Rosctr::AckData, 0, 0)], + "canonical response carries a zero error pair" + ); + } + + #[test] + fn test_BC_2_21_012_canonical_write_var_db_classified() { + assert_eq!( + classify_frame(&WRITE_DB), + F::WriteVar(S7AreaCode::DataBlock) + ); + let a = on_data_clean(&WRITE_DB, Direction::ClientToServer); + assert!(a.ack_error_observations().is_empty(), "Job records nothing"); + } + + #[test] + fn test_BC_2_21_012_canonical_write_var_outputs_classified() { + assert_eq!( + classify_frame(&WRITE_OUTPUTS), + F::WriteVar(S7AreaCode::Outputs) + ); + let a = on_data_clean(&WRITE_OUTPUTS, Direction::ClientToServer); + assert!(a.ack_error_observations().is_empty()); + } + + #[test] + fn test_BC_2_21_011_canonical_read_var_db_classified() { + assert_eq!(classify_frame(&READ_DB), F::ReadVar); + on_data_clean(&READ_DB, Direction::ClientToServer); + } + + #[test] + fn test_BC_2_21_015_canonical_plc_control_p_program_classified() { + assert_eq!( + classify_frame(&PLC_RUN), + F::PlcControl(PlcControlService::ProgramStart) + ); + on_data_clean(&PLC_RUN, Direction::ClientToServer); + } + + #[test] + fn test_BC_2_21_016_canonical_plc_stop_classified() { + assert_eq!(classify_frame(&PLC_STOP), F::PlcStop); + on_data_clean(&PLC_STOP, Direction::ClientToServer); + } + } + + // --------------------------------------------------------------------- + // PRF-005 (carry-forward): Kani harness over the REAL parameter-block slicing + // performed by `classify_job_ack_function` (retargets the former + // `vec![0u8; n].get(..)` assertion in story_187::vp051_kani, which only + // re-proved `Vec::get`). Compiled only under `cargo kani`. + // --------------------------------------------------------------------- + + #[cfg(kani)] + mod vp051_kani { + use wirerust::analyzer::s7comm::{ + S7ClassicFunction, classify_job_ack_function, parse_s7comm_header, s7comm_bounds_ok, + }; + + /// For any <= 32-byte symbolic buffer whose header parses and passes + /// `s7comm_bounds_ok`, `classify_job_ack_function` (which slices the + /// parameter block at `data[header_len..header_len + param_length]`) never + /// panics, and returns `NoParameterBlock` iff `param_length == 0`. + #[kani::proof] + fn verify_classify_job_ack_function_param_slicing_safe() { + let data: [u8; 32] = kani::any(); + let len: usize = kani::any(); + kani::assume(len <= 32); + let slice = &data[..len]; + + let Some(header) = parse_s7comm_header(slice) else { + return; + }; + if !s7comm_bounds_ok(&header, len) { + return; + } + + let result = classify_job_ack_function(slice, header.header_len, header.param_length); + if header.param_length == 0 { + assert!(result == S7ClassicFunction::NoParameterBlock); + } else { + assert!(result != S7ClassicFunction::NoParameterBlock); + } + + kani::cover!(header.param_length == 0); + kani::cover!(header.param_length >= 1); + kani::cover!(matches!(result, S7ClassicFunction::WriteVar(_))); + kani::cover!(matches!(result, S7ClassicFunction::PlcControl(_))); + } + } + + /// Traces BC-2.21.017 EC-005; AC-188-008 defensive bullet; STORY-188 EC-012. + /// + /// Pins the defensive `NoParameterBlock` return of `classify_job_ack_function` + /// when the parameter block cannot be sliced from `data` (offset arithmetic + /// overflows, or the block end exceeds `data.len()`). The VP-051 Kani harness + /// returns early unless `s7comm_bounds_ok`, so it does not cover this path. + #[test] + fn test_BC_2_21_017_unsliceable_parameter_block_returns_no_parameter_block() { + // End (12 + 5 = 17) exceeds data.len() (12). + assert_eq!( + classify_job_ack_function(&[0x32; 12], 12, 5), + S7ClassicFunction::NoParameterBlock + ); + // header_len + param_length overflows usize. + assert_eq!( + classify_job_ack_function(&[0x05], usize::MAX, 1), + S7ClassicFunction::NoParameterBlock + ); + // Partial: header present, block only partly delivered (12 + 3 = 15 > 14). + assert_eq!( + classify_job_ack_function(&[0x32; 14], 12, 3), + S7ClassicFunction::NoParameterBlock + ); + } +}