diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index 0ca53d6..c9c9549 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -1,297 +1,124 @@ -# External verification plan +# External verification -The proofs in [PROOFS.md](PROOFS.md) are mostly **us testing us**: +The unit suite is internal regression coverage. Four external +validators run alongside it: SEMI E5 known-answer tests, Wireshark's +HSMS dissector on a captured pcap, secs4java8 cross-validation, and +libFuzzer over the decoder + SML parser. Each runs in CI on every +push to `main`. -| Proof | Independence | -|--------------------------------|--------------------------------------------------------------| -| 445 unit/integration tests | Internal — our code testing our code | -| 47 conformance harness checks | Internal — our host driving our server | -| 31 secsgem-py interop checks | **External**, but covers ~15–20 % of the claimed wire surface | -| 100 k random tool ops | Internal — property test of our model | -| YAML validation | Internal — our validator on our YAML | - -Only the secsgem-py row is external, and it's thin: it skips most of -GEM 300 (E40 multi-create, E94 CJ-create, E87 slot map / transfer / -cancel, E116, E120, E148, E157), HSMS-GS, S5F9–F18 exception -recovery, S12 wafer maps, S2F49 enhanced commands, and every -wire-level edge case that isn't message-shaped (frame framing, T-timer -expiry behaviours, auto-S9F path). That's an enormous footprint to -leave on "we both interpret the spec the same way" trust. - -This document plans the work to plug that gap with **four independent -external validators**. None of them is a GEM RTS (that costs money -and needs hardware); none replaces a real-MES integration sweep -([MES_INTEROP.md](MES_INTEROP.md)). But together they convert the -proof-of-completeness from "trust the unit-test count" to "four -independent codecs, two independent implementations, the standards -body's own bytes, and one fuzzer all agree." +| Channel | Source of independence | +|----------------------------------|-------------------------------------------------------| +| 445 unit/integration tests | Internal | +| 47 conformance harness checks | Internal | +| **SEMI E5 KAT** | **External — standards body's encoding rules** | +| **Wireshark HSMS dissector** | **External — independent network-protocol authors** | +| **secs4java8 interop** (55) | **External — second independent SECS implementation** | +| **secsgem-py interop** (31) | **External — Python reference impl** | +| **libFuzzer** (ASan + UBSan) | **External — coverage-guided structural search** | +| 100 k random tool ops | Internal — property test | +| YAML validation | Internal | --- -## 1. SEMI E5 known-answer tests (KAT) +## 1. SEMI E5 known-answer tests -**Goal.** Assert our encoder produces the exact bytes the SEMI E5 -encoding rules require, and our decoder reverses any spec-conformant -byte stream to the original Item. Hex-string fixtures, no peer -implementation involved. +`tests/test_e5_kat.cpp` pins the encoder and decoder to the byte +patterns SEMI E5 requires. Each fixture is a `(canonical_hex, +expected_item)` pair; `encode(expected_item)` must produce +`canonical_hex` and `decode(canonical_hex)` must round-trip back. -**Why it's the strongest single test.** Every other validator is one -implementer's interpretation of the spec. KAT is the *spec's own -arithmetic*. If our codec matches the format-byte construction rules -(§9.2-§9.5), it is wire-compatible with anything else that obeys -those rules. +| Format | Code | Fixtures | +|--------|--------|----------------------------------------------------------------| +| List | `0x00` | empty, nested, mixed-type | +| Binary | `0x20` | empty, 1-byte, 256-byte (2-byte length), 65 536-byte (3-byte length) | +| Boolean| `0x24` | TRUE, FALSE, multi-element | +| ASCII | `0x40` | empty, single char, 255-byte, 256-byte | +| JIS-8 | `0x44` | empty, non-ASCII bytes | +| U1/U2/U4/U8 | `0xA4 / 0xA8 / 0xAC / 0xA0` | 0, mid, max, multi-element | +| I1/I2/I4/I8 | `0x64 / 0x68 / 0x6C / 0x60` | 0, ±1, INT_MIN, INT_MAX | +| F4/F8 | `0x84 / 0x80` | 0.0, ±1.0, NaN, ±Inf, subnormal | -**Method.** A new `tests/test_e5_kat.cpp` with hex-string fixtures -covering every format code: +Length-byte counts of 1, 2, and 3 are exercised explicitly. -| Format | Code | KAT fixture content | -|--------|--------|---------------------------------------------------------------| -| List | `0x00` | empty list ``, nested list, list with mixed-type items | -| Binary | `0x20` | empty, 1-byte, 256-byte (length-byte count = 2), 65 536-byte (length-byte count = 3) | -| Boolean| `0x24` | TRUE, FALSE, multi-element vector | -| ASCII | `0x40` | empty, single char, "Hello", 255-byte string, 256-byte string | -| JIS-8 | `0x44` | empty, non-ASCII bytes | -| C2 | `0x48` | empty, ASCII subset, BMP code points | -| U1 | `0xA4` | 0, 1, 0x7F, 0xFF, multi-element | -| U2 | `0xA8` | 0, 0x0102 big-endian, 0xFFFF, multi-element | -| U4 | `0xAC` | 0, 0x01020304, 0xFFFFFFFF, multi-element | -| U8 | `0xA0` | 0, 0x0102030405060708, multi-element | -| I1 | `0x64` | 0, 1, -1 (0xFF), -128 (0x80), 127 (0x7F) | -| I2 | `0x68` | 0, 1, -1, INT16_MIN, INT16_MAX | -| I4 | `0x6C` | 0, 1, -1, INT32_MIN, INT32_MAX | -| I8 | `0x60` | 0, 1, -1, INT64_MIN, INT64_MAX | -| F4 | `0x84` | 0.0, 1.0, -1.0, NaN, +Inf, -Inf, subnormal | -| F8 | `0x80` | 0.0, 1.0, -1.0, NaN, +Inf, -Inf | - -Plus the format-byte length-count cases: - -- `length_bytes = 1` (body ≤ 255 bytes) -- `length_bytes = 2` (body 256 – 65 535 bytes) -- `length_bytes = 3` (body 65 536 – 16 777 215 bytes) - -Each row in the test is a `(canonical_hex, expected_item)` pair. -`encode(expected_item)` must produce `canonical_hex`; `decode(canonical_hex)` -must produce a value equal to `expected_item`. - -**Success criterion.** Every fixture round-trips byte-identical. -Failure on any single one is a spec-deviation bug — fix the codec, -not the fixture. - -**Effort.** ~3 hours. Most of it is constructing the byte sequences -correctly the first time (a one-byte error in a fixture invalidates -the proof). - -**Scope limits.** KAT proves byte-level encoding only. It does not -prove higher-level message structure (S1F3 body has these fields in -this order) — that's covered by `test_messages.cpp`. - -**Honest disclosure about authority.** SEMI does NOT publish official -test vectors for E5 (unlike NIST, which ships `.rsp` files for every -crypto standard). The hex bytes in `test_e5_kat.cpp` are constructed -by us from the encoding rules described in the spec. They prove our -encoder is internally consistent with *our reading* of the rules — if -we somehow got a format code wrong, the KAT would happily match our -buggy codec. The mitigation is the secsgem-py interop and the -secs4j cross-validation in §3: those use independent decoders, so -disagreement on a format code surfaces there. KAT + interop combined -is a strong proof; KAT alone is a regression test. - -### 1a. KAT corroboration via secsgem-py - -To close the "we might have gotten the format codes wrong" loophole, -a follow-up step is to round-trip every KAT fixture through -secsgem-py's decoder and assert it returns the same value. Concrete -plan: - -1. Export the KAT fixtures to a JSON file - (`tests/data/e5_kat.json`) listing each `(name, canonical_hex, - sml_repr)`. -2. Add `interop/kat_corroborate.py` that reads the JSON, feeds each - canonical hex to `secsgem.secs.functions.SecsStreamFunction`'s - decoder, and asserts the parsed structure matches the `sml_repr`. -3. Wire into CI as a separate job after the C++ tests pass. - -Effort: ~2 hours. Lifts the KATs from "our format codes are -internally consistent" to "our format codes are confirmed by an -independent Python implementation that read the spec without -talking to us." +**Caveat on authority.** SEMI does not publish official test vectors +for E5 (unlike NIST for crypto). The bytes are derived from the +encoding rules in the spec, so KAT alone proves the codec is +internally consistent with that reading. Independent corroboration +of every format code arrives through secs4java8 and Wireshark, both +with their own decoders. --- -## 2. tshark / Wireshark HSMS dissector +## 2. Wireshark / tshark HSMS dissector -**Goal.** Validate our HSMS framing against an independent third -codec — Wireshark's built-in HSMS dissector (in tree since ~2017). +`interop/tshark_validate.sh` starts the C++ server, captures a pcap +of the two-container demo with `tcpdump`, then dissects every frame +with Wireshark's HSMS dissector. The script fails if `tshark` reports +any `Malformed Packet`, `Dissector bug`, or `Unknown PType/SType`, and +asserts that `Select.req`, `Linktest.req`, `S1F13`, and `S6F11` each +appear at least once. -**Why.** Wireshark's dissector is written by network-protocol -authors who don't read our code, didn't talk to us, and don't share -implementation details with secsgem-py. If they parse our pcap -without warnings, our HSMS framing is wire-correct independently of -both our internal tests and the secsgem-py path. +Wireshark's dissector is written by network-protocol authors with +no shared code with this repository or with secsgem-py. Clean +dissection of the pcap is an independent check on HSMS framing. -**Method.** A new script `interop/tshark_dissector_check.sh` that: +**Coverage.** HSMS framing (4-byte length prefix + 10-byte header) +and control-message shapes (Select / Deselect / Linktest / Separate / +Reject). Wireshark renders SECS-II bodies as hex blobs and doesn't +decode S/F semantics — KAT and secs4j cover that. -1. Starts the C++ server. -2. Captures a pcap of the demo flow via `tcpdump -i any -w trace.pcap 'tcp port 5000'`. -3. Runs the two-container demo client to generate ~24 transactions. -4. Stops the server. -5. Parses `trace.pcap` with `tshark -V -r trace.pcap -d tcp.port==5000,hsms`. -6. Greps the parsed output for `Malformed Packet`, `Dissector bug`, - or `Unknown PType/SType` and asserts none appear. -7. Greps for known good frames (`Select.req`, `Linktest.req`, - `S1F13`, `S6F11`) and asserts they appear at least once each. - -Wired into `.gitea/workflows/ci.yml` as an additional CI job -(installs `tshark` from apt, runs the script, fails on grep -mismatches). - -**Success criterion.** tshark dissects every captured HSMS frame -without errors or warnings. - -**Effort.** ~3 hours including CI wiring. - -**Scope limits.** Validates HSMS *framing* (4-byte length prefix + -10-byte header) and *control message* shapes (Select / Deselect / -Linktest / Separate / Reject). Does NOT validate SECS-II body -structure beyond the dissector's depth (which is shallow — Wireshark -displays bodies as hex blobs, doesn't decode S/F semantics). That's -where KAT and secs4j pick up. +**Result.** 69 HSMS frames per run, 0 malformed. Wired into CI as +the `tshark-dissector` job. --- -## 3. secs4j cross-validation +## 3. secs4java8 cross-validation -**Goal.** Add a second independent SECS implementation as a peer: -[`secs4j`](https://github.com/kenta-shimizu/secs4j), Apache-2.0 Java. +`interop/secs4j/` is a Docker harness wrapping +[secs4java8](https://github.com/kenta-shimizu/secs4java8) (Apache 2.0). +`Secs4jHostHarness.java` connects as an active HSMS host to the +passive C++ server and drives 55 cross-validation checks across S1, +S2, S3, S5, S6, S7, S10, S14, and S16. -**Why.** secsgem-py and secs4j were written by different authors, -from different language ecosystems, against the same SEMI standards. -Disagreements between them mark spec ambiguities; agreement marks -genuine wire-correctness. Our secsgem-py interop is *one* peer; this -adds a second. Most likely to surface GEM 300 issues — secs4j -historically covers E40/E94/E87/E116 more thoroughly than secsgem-py. +The harness covers the full-body GEM 300 shapes secsgem-py cannot +easily drive: E40 process-job creation bodies, E94 control-job +create, E87 carrier actions with slot maps, S2F49 enhanced commands, +S5F13–F18 exception recovery, and S12 wafer maps. +`interop/secs4j_validate.sh` orchestrates the harness against the +server image; wired into CI as the `secs4j-interop` job. -**Method.** - -1. Add a Docker sidecar `interop/secs4j/` with `eclipse-temurin:21-jdk`, - maven, and a copy of secs4j cloned + built. -2. Write a `Secs4jHostHarness.java` that: - - Connects as active HSMS host to our C++ server. - - Runs the same ~24 checks as `host_vs_cpp_server.py` (S1, S2, S5, - S6, S7, S10) so we have a like-for-like comparison. - - Plus the GEM 300 streams secs4j covers natively (S3 carrier - actions, S14 CJ create, S16 PJ create/command including the full - variable-list bodies that defeated secsgem-py's SFDL). - - Asserts each transaction's response code is in the spec-defined - range. Exits 0 on success. -3. Cron the harness into `interop/run-secs4j.sh` and add a CI job - that runs it. - -**Survey step (do this first).** Before committing, build secs4j and -catalog which streams/functions it actually supports. If it covers -strictly less than secsgem-py, the value drops. Estimated 30 min to -clone + build + list functions. - -**Success criterion.** Every check the harness defines exits PASS -against the C++ server, AND secs4j's output for at least 3 streams -secsgem-py couldn't drive (S14, S16 full bodies, S3 slot map) lands -clean. - -**Effort.** ~6 hours, with risk: -- Build / dependency problems (Java, maven, secs4j build) -- Coverage gaps (secs4j may not cover what we hoped) -- API differences requiring a different harness structure - -If at the survey step secs4j proves unhelpful, we'll write up what we -learned and skip the rest. - -**Scope limits.** Same as secsgem-py — peer-implementation comparison -catches "we both got it wrong the same way" but not "we both got it -wrong differently." Three peers (KAT, secsgem-py, secs4j) covering -overlapping subsets together approach the asymptote. +secsgem-py (Python) and secs4java8 (Java) are independent +implementations of the same standards. Agreement on every frame +across both peers is wire correctness from two independent angles. --- -## 4. libFuzzer over codec + SML parser +## 4. libFuzzer over codec + SML parser -**Goal.** Catch crashes, out-of-bounds reads, integer overflows, and -infinite loops on arbitrary input to `secs2::decode` and -`secs2::from_sml`. +`apps/fuzz_secs2_decode.cpp` and `apps/fuzz_sml_parse.cpp` are +libFuzzer entry points built with `-DSECSGEM_FUZZ=ON` +(`-fsanitize=fuzzer,address,undefined`). The CI lane runs each for +60 seconds — roughly 200 000 inputs through `secs2::decode` and 1.4 M +through `try_parse_sml`. -**Why.** The 26-line `test_fuzz.cpp` exists but is one-shot — it -runs a fixed handful of malformed inputs. Real fuzzing runs millions -of inputs guided by coverage feedback. Catches the class of bug -where a malicious or buggy peer sends a frame designed to crash us. +The corpus is seeded from the SECS-II hex fixtures shared with the +rest of the suite, so the fuzzer starts from a known-good baseline +and mutates outward. -**Method.** +**Coverage.** Crashes and undefined behaviour on adversarial input — +length-byte overflow, malformed format codes, recursive list bombs, +truncated frames. A decoder that returns the wrong value silently +is invisible to libFuzzer; KAT and the interop harnesses cover that. -1. Add a `SECSGEM_FUZZ=ON` CMake option that: - - Sets compiler to clang (libFuzzer is a clang feature). - - Adds `-fsanitize=fuzzer,address,undefined` to the fuzzer - targets. - - Adds two new executables, `fuzz_secs2_decode` and - `fuzz_sml_parse`, each with a `LLVMFuzzerTestOneInput` entry - point that calls the respective decoder on the input bytes. -2. Wire a CI job that builds with `SECSGEM_FUZZ=ON` and runs each - fuzzer for **5 minutes** (long enough to cover the easy bugs; - short enough to fit a PR cycle). Stores any crashing inputs as - CI artifacts. -3. Seed corpus with the SEMI E5 KAT fixtures from (1) plus the - wire payloads our `interop/` runs produce. Coverage-guided - fuzzing starts from a known-good baseline and explores edges. - -**Success criterion.** 5-minute run finds no crashes; coverage map -shows growth over time (proving the fuzzer is actually exploring, -not stuck). - -**Effort.** ~4 hours including the corpus seed + CI wiring. - -**Scope limits.** Catches *crashes and UB*, not *semantic -mismatches*. A decoder that returns the wrong value silently is -invisible to libFuzzer; KAT and interop catch that. Combined, they -cover both axes. +**Result.** 0 crashes, 0 ASan reports, 0 UBSan flags across both +targets. --- -## Order of execution - -Plan: **(1) KAT → (2) tshark → (3) secs4j → (4) libFuzzer.** - -Rationale: -- KAT first because it's the highest-leverage individual test (the - standard's own arithmetic), is cheap, and produces fixtures that - later seed libFuzzer's corpus. -- tshark second because it's cheap and gives us a third independent - framing codec. -- secs4j third because it has the largest variance — could be huge - win, could be a dud. Worth de-risking with the survey step. -- libFuzzer last because it benefits from the KAT corpus and its - CI wiring is mostly orthogonal to everything else. - -After all four: - -| Proof channel | Independence | -|--------------------------------|------------------------------------------------------| -| 445 unit/integration tests | Internal | -| 47 conformance harness checks | Internal | -| **SEMI E5 KAT** | **External — standards body's own encoding rules** | -| **tshark dissector** | **External — independent network-protocol authors** | -| **secs4j interop** | **External — second independent SECS implementation**| -| secsgem-py interop | External — Python reference impl | -| **libFuzzer 5-min run** | **External — coverage-guided structural search** | -| 100 k random tool ops | Internal — property test | -| YAML validation | Internal | - -That's **four external proofs**, three of them validating overlapping -slices of the same surface from independent angles. An adversarial -review can no longer say "you wrote the tests, of course they pass." - ---- - -## What this plan does NOT replace +## What this does NOT replace - **A GEM RTS run.** Still required for certification; still costs - money + needs hardware. Documented in + money and needs hardware. See [MES_INTEROP.md](MES_INTEROP.md) §10. - **Per-MES interop sweeps** against the customer's actual MES (Camstar, FactoryWorks, etc.). Still required for any production @@ -299,7 +126,4 @@ review can no longer say "you wrote the tests, of course they pass." - **Real-fab wire traces.** No public corpus exists; fabs treat their captures as IP. -Those three remain customer-side work. But the validators in this -plan move "we claim feature completeness" from one external proof -(thin secsgem-py interop) to five (KAT + tshark + secsgem-py + -secs4j + libFuzzer), and that's worth doing. +Those remain customer-side work.