◇ OpenCyber Academy
Engineering · Chapter 30 · English

Chapter 30 — Verification laboratory I

Open, free learning for anyone who wants to protect people and technology. No account is required to read this text or its worked answers.

Chapter 30 — Verification laboratory I

Lesson map

Lesson 30 published. Map, example, EX059.

flowchart TD
  N0["Learning outcomes"]
  N1["30.1 Known-answer tests"]
  N2["30.2 Practical activity — Lab V"]
  N3["30.3 Interoperability"]
  N4["30.4 Evidence"]
  N5["Engineering note"]
  N6["Synthesis"]
  N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6
  N6 --> EX["Worked example"]
  EX --> Q["Exercise EX059"]

Logical drawing

flowchart LR
  N0["Learning outcomes"]
  N1["30.1 Known-answer tests"]
  N2["30.2 Practical activity — Lab V"]
  N3["30.3 Interoperability"]
  N4["30.4 Evidence"]
  N5["Engineering note"]
  N6["Synthesis"]
  N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6 --> Q["EX059"]
[Learning outcomes]
    |
    v
[30.1 Known-answer tests]
    |
    v
[30.2 Practical activity — Lab V]
    |
    v
[30.3 Interoperability]
    |
    v
[30.4 Evidence]
    |
    v
[Engineering note]
    |
    v
[Synthesis]
    |
    v
[Worked example] --> [Exercise EX059]

Learning outcomes

You will (1) verify implementations with known-answer tests; (2) write negative tests for malformed inputs; (3) test interoperability across libraries; and (4) record verification evidence. It builds on Chapters 9, 28 and 29.

30.1 Known-answer tests

Known-answer tests (KATs) feed fixed inputs and compare outputs with published values. Standards bodies and the NIST Cryptographic Algorithm Validation Program publish vectors; for ML-KEM, deterministic test modes allow fixed randomness so outputs can be compared byte for byte.

Deterministic modes exist only for testing; production code must use fresh randomness, and a build check ensures the test hooks are not reachable in release builds. BPA runs the vector suite on every library update and blocks the upgrade if any vector fails, which catches regressions such as the draft-to-final changes in ML-KEM's encoding.

30.2 Practical activity — Lab V

# Lab V (ch 30): known-answer and negative tests - the habit behind validating PQC libraries.
import hashlib
KATS = [  # (function, input, expected hex prefix) - published test values for SHA-3 / SHAKE on empty input
    ("sha3_256", b"", "a7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a"),
    ("shake_128/32", b"", "7f9c2ba4e88f827d616045507605853ed73b8093f6efbc88eb1a6eacfa66ef26"),
]
def run(name, data):
    if name == "sha3_256": return hashlib.sha3_256(data).hexdigest()
    return hashlib.shake_128(data).hexdigest(32)
for name, data, want in KATS:
    print(f"KAT {name:13s}", "PASS" if run(name, data) == want else "FAIL")
SIZES = {"ML-KEM-512": 800, "ML-KEM-768": 1184, "ML-KEM-1024": 1568}   # encapsulation-key bytes, FIPS 203
def validate_ek(param, ek):
    if len(ek) != SIZES[param]: raise ValueError(f"{param}: expected {SIZES[param]} bytes, got {len(ek)}")
    return True
for param, n in [("ML-KEM-768", 1184), ("ML-KEM-768", 1183), ("ML-KEM-512", 1184)]:
    try: validate_ek(param, bytes(n)); print(f"negative/positive test {param} len {n}: accepted")
    except ValueError as e: print(f"negative/positive test {param} len {n}: rejected ({e})")

Expected output:

KAT sha3_256      PASS
KAT shake_128/32  PASS
negative/positive test ML-KEM-768 len 1184: accepted
negative/positive test ML-KEM-768 len 1183: rejected (ML-KEM-768: expected 1184 bytes, got 1183)
negative/positive test ML-KEM-512 len 1184: rejected (ML-KEM-512: expected 800 bytes, got 1184)

The length validator is only the first check: FIPS 203 also requires checking that encoded coefficients of an encapsulation key are below q (the modulus check) and a hash check on decapsulation keys. Real libraries implement these; your tests should confirm they reject bad keys.

The third test case is the important one: a correctly sized ML-KEM-768 key presented as ML-KEM-512 must be rejected, because a parser that trusts the key's length to choose the parameter set can be steered by an attacker.

30.3 Interoperability

Run handshakes between every pair of client and server implementations in scope; encapsulate with one library and decapsulate with another; sign with the HSM and verify in partner software. Record the matrix. Interoperability failures early in the programme are cheap; in production they are outages.

Testing a library only against itself proves little, since an encoding bug on one side is mirrored on the other and cancels out. Pairs of different implementations expose such mismatches. The matrix also records versions, so when a library is upgraded, only the affected rows are rerun.

30.4 Evidence

Each test run records: implementation and version, test vectors used, result, date, operator. Evidence feeds the verification column of the traceability matrix (Chapter 21).

Evidence must be reproducible: another engineer should be able to rerun the same test with the same versions and vectors and get the same result. BPA stores the test configuration with the result, so an auditor asking how REQ-KE-01 was verified receives the query, its output and the date rather than a statement that testing was done. Results older than the current library version are marked stale and rerun before release.

30.5 Worked example

BPA's interoperability matrix for edge TLS: three server stacks × five client families. Two failures: an old partner library offered the obsolete pre-standard codepoint and could not complete hybrid handshakes; a load balancer stripped unknown groups. Both get work items; neither blocks rollout, because fallback to X25519 works and is logged.

The obsolete codepoint belongs to a draft Kyber implementation, which is why final ML-KEM peers cannot complete the handshake; the partner must update the library. The load balancer problem is more serious because it affects all traffic through it, so its fix is scheduled before the rollout passes that path.

30.6 Common errors and limits

Positive tests alone would pass a validator that accepts every key, while Lab V's rejection cases show the validator actually discriminates. Testing a library against itself hides encoding mismatches, which appear only when a different implementation is on the other side, as the obsolete-codepoint failure showed. Unrecorded results cannot support the traceability matrix, so a passed test that nobody wrote down counts for nothing in review. BPA's pipeline stores each run with versions and vectors.

Engineering note

Verification evidence should be reproducible by someone else. Store the exact test vectors, tool versions and command lines alongside results, and rerun the suite automatically whenever a library, provider or HSM firmware changes. When a vendor publishes an advisory, the team can then answer within hours whether the affected version is deployed and whether its tests still pass, instead of reconstructing the original verification from memory and screenshots.

Exercises

Synthesis

Verification combines known-answer tests, negative tests and cross-implementation interoperability, all recorded as evidence traced to requirements.

Continue studying — chapter 30 of 50

← Chapter 29 (draft) · Course chapter index · Chapter 31 (draft) →