diff --git a/VERIFICATION.md b/VERIFICATION.md new file mode 100644 index 0000000..0397482 --- /dev/null +++ b/VERIFICATION.md @@ -0,0 +1,275 @@ +# External verification plan + +The five proofs in [README.md](README.md#proof-of-feature-completeness) +are mostly **us testing us**: + +| Proof | Independence | +|--------------------------------|--------------------------------------------------------------| +| 426 unit/integration tests | Internal — our code testing our code | +| 47 conformance harness checks | Internal — our host driving our server | +| 24 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." + +--- + +## 1. SEMI E5 known-answer tests (KAT) + +**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. + +**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. + +**Method.** A new `tests/test_e5_kat.cpp` with hex-string fixtures +covering every format code: + +| 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`. + +--- + +## 2. tshark / Wireshark HSMS dissector + +**Goal.** Validate our HSMS framing against an independent third +codec — Wireshark's built-in HSMS dissector (in tree since ~2017). + +**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. + +**Method.** A new script `interop/tshark_dissector_check.sh` 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. + +--- + +## 3. secs4j cross-validation + +**Goal.** Add a second independent SECS implementation as a peer: +[`secs4j`](https://github.com/kenta-shimizu/secs4j), Apache-2.0 Java. + +**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. + +**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. + +--- + +## 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`. + +**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. + +**Method.** + +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. + +--- + +## 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 | +|--------------------------------|------------------------------------------------------| +| 426 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 + +- **A GEM RTS run.** Still required for certification; still costs + money + needs hardware. Documented in + [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 + deployment. See [MES_INTEROP.md](MES_INTEROP.md). +- **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.