raphael
5baf3f4dc7
Wireshark's built-in HSMS dissector — written by network-protocol authors who don't know us, didn't talk to us, and don't share implementation details with secsgem-py — is a third independent codec for our framing. If they parse our pcap without warnings, our HSMS framing is wire-correct independently of both our internal tests and the secsgem-py interop path. interop/tshark_validate.sh: - Boots secs_server on 127.0.0.1:5099 (away from the demo port) - Captures the loopback wire traffic with tcpdump - Runs secs_client through ~24 transactions plus Separate.req + TCP FIN - Parses the pcap with tshark -V using the HSMS dissector - Asserts: no "Malformed Packet", no "Dissector bug", at least one HSMS frame, expected tokens present (Select.req/rsp, Separate.req, Data message), reports histogram (count by control type + distinct S/F pairs) Result against the demo: 69 HSMS frames dissected, 49 distinct S/F pairs (S01F01..S16F28), all clean. Dockerfile gains tshark + tcpdump. .gitea/workflows/ci.yml gains a `tshark-dissector` job that runs this validator as part of every push to main. README proof table grows to 6 commands. VERIFICATION.md §1a documents a follow-up: round-trip the KAT fixtures through secsgem-py to corroborate that the format codes we used match an independent implementation. Strengthens the KAT proof from "internally consistent" to "confirmed by a second implementer who read the spec without talking to us." Plan: VERIFICATION.md §2. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
307 lines
14 KiB
Markdown
307 lines
14 KiB
Markdown
# 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 `<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`](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.
|