raphael/secs-gem
Public Access
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

docs: rewrite VERIFICATION.md to describe shipped validators

Browse Source 
Previously written as a forward-looking plan ("Plan: (1) KAT → (2)
tshark → (3) secs4j → (4) libFuzzer", "Effort: ~3 hours", "Survey
step (do this first)").  All four validators have shipped —
test_e5_kat.cpp, interop/secs4j/Secs4jHostHarness.java,
interop/tshark_validate.sh, apps/fuzz_*.cpp.  Rewritten as
documentation of what's there: file paths, CI job names, actual
result numbers.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
Raphael Maenle
2026-06-09 23:59:54 +02:00
parent 0355c73211
commit d63c92166d
1 changed files with 88 additions and 264 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/VERIFICATION.md
+88 -264
View File
@@ -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 | | Channel | Source of independence |
|--------------------------------|--------------------------------------------------------------| |----------------------------------|-------------------------------------------------------|
| 445 unit/integration tests | Internal — our code testing our code | | 445 unit/integration tests | Internal |
| 47 conformance harness checks | Internal — our host driving our server | | 47 conformance harness checks | Internal |
| 31 secsgem-py interop checks | **External**, but covers ~15–20 % of the claimed wire surface | | **SEMI E5 KAT** | **External — standards body's encoding rules** |
| 100 k random tool ops | Internal — property test of our model | | **Wireshark HSMS dissector** | **External — independent network-protocol authors** |
| YAML validation | Internal — our validator on our YAML | | **secs4java8 interop** (55) | **External — second independent SECS implementation** |
| **secsgem-py interop** (31) | **External — Python reference impl** |
Only the secsgem-py row is external, and it's thin: it skips most of | **libFuzzer** (ASan + UBSan) | **External — coverage-guided structural search** |
GEM 300 (E40 multi-create, E94 CJ-create, E87 slot map / transfer / | 100 k random tool ops | Internal — property test |
cancel, E116, E120, E148, E157), HSMS-GS, S5F9–F18 exception | YAML validation | Internal |
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) ## 1. SEMI E5 known-answer tests
**Goal.** Assert our encoder produces the exact bytes the SEMI E5 `tests/test_e5_kat.cpp` pins the encoder and decoder to the byte
encoding rules require, and our decoder reverses any spec-conformant patterns SEMI E5 requires. Each fixture is a `(canonical_hex,
byte stream to the original Item. Hex-string fixtures, no peer expected_item)` pair; `encode(expected_item)` must produce
implementation involved. `canonical_hex` and `decode(canonical_hex)` must round-trip back.
**Why it's the strongest single test.** Every other validator is one | Format | Code | Fixtures |
implementer's interpretation of the spec. KAT is the *spec's own |--------|--------|----------------------------------------------------------------|
arithmetic*. If our codec matches the format-byte construction rules | List | `0x00` | empty, nested, mixed-type |
(§9.2-§9.5), it is wire-compatible with anything else that obeys | Binary | `0x20` | empty, 1-byte, 256-byte (2-byte length), 65 536-byte (3-byte length) |
those rules. | 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 Length-byte counts of 1, 2, and 3 are exercised explicitly.
covering every format code:
| Format | Code | KAT fixture content | **Caveat on authority.** SEMI does not publish official test vectors
|--------|--------|---------------------------------------------------------------| for E5 (unlike NIST for crypto). The bytes are derived from the
| List | `0x00` | empty list `<L[0]>`, nested list, list with mixed-type items | encoding rules in the spec, so KAT alone proves the codec is
| Binary | `0x20` | empty, 1-byte, 256-byte (length-byte count = 2), 65 536-byte (length-byte count = 3) | internally consistent with that reading. Independent corroboration
| Boolean| `0x24` | TRUE, FALSE, multi-element vector | of every format code arrives through secs4java8 and Wireshark, both
| ASCII | `0x40` | empty, single char, "Hello", 255-byte string, 256-byte string | with their own decoders.
| 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 ## 2. Wireshark / tshark HSMS dissector
**Goal.** Validate our HSMS framing against an independent third `interop/tshark_validate.sh` starts the C++ server, captures a pcap
codec — Wireshark's built-in HSMS dissector (in tree since ~2017). 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 Wireshark's dissector is written by network-protocol authors with
authors who don't read our code, didn't talk to us, and don't share no shared code with this repository or with secsgem-py. Clean
implementation details with secsgem-py. If they parse our pcap dissection of the pcap is an independent check on HSMS framing.
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: **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. **Result.** 69 HSMS frames per run, 0 malformed. Wired into CI as
2. Captures a pcap of the demo flow via `tcpdump -i any -w trace.pcap 'tcp port 5000'`. the `tshark-dissector` job.
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 ## 3. secs4java8 cross-validation
**Goal.** Add a second independent SECS implementation as a peer: `interop/secs4j/` is a Docker harness wrapping
[`secs4j`](https://github.com/kenta-shimizu/secs4j), Apache-2.0 Java. [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, The harness covers the full-body GEM 300 shapes secsgem-py cannot
from different language ecosystems, against the same SEMI standards. easily drive: E40 process-job creation bodies, E94 control-job
Disagreements between them mark spec ambiguities; agreement marks create, E87 carrier actions with slot maps, S2F49 enhanced commands,
genuine wire-correctness. Our secsgem-py interop is *one* peer; this S5F13–F18 exception recovery, and S12 wafer maps.
adds a second. Most likely to surface GEM 300 issues — secs4j `interop/secs4j_validate.sh` orchestrates the harness against the
historically covers E40/E94/E87/E116 more thoroughly than secsgem-py. server image; wired into CI as the `secs4j-interop` job.
**Method.** secsgem-py (Python) and secs4java8 (Java) are independent
implementations of the same standards. Agreement on every frame
1. Add a Docker sidecar `interop/secs4j/` with `eclipse-temurin:21-jdk`, across both peers is wire correctness from two independent angles.
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 ## 4. libFuzzer over codec + SML parser
**Goal.** Catch crashes, out-of-bounds reads, integer overflows, and `apps/fuzz_secs2_decode.cpp` and `apps/fuzz_sml_parse.cpp` are
infinite loops on arbitrary input to `secs2::decode` and libFuzzer entry points built with `-DSECSGEM_FUZZ=ON`
`secs2::from_sml`. (`-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 The corpus is seeded from the SECS-II hex fixtures shared with the
runs a fixed handful of malformed inputs. Real fuzzing runs millions rest of the suite, so the fuzzer starts from a known-good baseline
of inputs guided by coverage feedback. Catches the class of bug and mutates outward.
where a malicious or buggy peer sends a frame designed to crash us.
**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: **Result.** 0 crashes, 0 ASan reports, 0 UBSan flags across both
- Sets compiler to clang (libFuzzer is a clang feature). targets.
- 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 ## What this does NOT replace
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 - **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. [MES_INTEROP.md](MES_INTEROP.md) §10.
- **Per-MES interop sweeps** against the customer's actual MES - **Per-MES interop sweeps** against the customer's actual MES
(Camstar, FactoryWorks, etc.). Still required for any production (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 - **Real-fab wire traces.** No public corpus exists; fabs treat
their captures as IP. their captures as IP.
Those three remain customer-side work. But the validators in this Those remain customer-side work.
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.