secs-gem/VERIFICATION.md

External verification plan

The proofs in PROOFS.md are mostly us testing us:

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). 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 <L[0]>, 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."

---

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, 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
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

• A GEM RTS run. Still required for certification; still costs money + needs hardware. Documented in 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.
• 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.