Repository navigation
Platform measurement evidence: not-established outcomes from a TPM quote verifier (implementation evidence, from #279) #431
Description
Separate item following my comment on #279. This is implementation evidence and a question, not yet a proposed normative change; opening it does not mean TRACE agrees to add anything.
Spec section affected
§3.1 (logical schema), schema/trace-claim.json #/properties/runtime
Problem
Per-PCR coverage (holds measurements / separator only / not selected) is decidable by any verifier that has the reference, but runtime cannot carry it, so the next hop sees only a matching digest. A match on a PCR that holds a separator only confirms that nothing was recorded, not what ran.
Proposed change
None yet. The question: should per-PCR coverage stay on the verifier's surface, or does TRACE want the record to say which layers a matching measurement actually covers?
Backward compatibility
Not applicable until the question is answered.
Motivation: the example
Published evidence from one board (Rock 5A, discrete Infineon TPM, TactiQ OS v2.1.0-rc13), checked offline with standard tools only:
- Release: https://github.com/revenue7-eng/tactiq-os/releases/tag/v2.1.0-rc13
- Procedure:
VERIFY-L3-rc13.mdin that release - Checker:
verify-l3-rc13.shin that release, SHA-256665028580ca025dffdcf760a6b22094b518bc817a582a1c1fc775a28ad852633
It needs bash, curl, OpenSSL 3, Python 3 and tpm2-tools, no TPM, and downloads everything else from the release:
bash verify-l3-rc13.sh
Every check prints PASS, FAIL or NOT ESTABLISHED with a reason. NOT ESTABLISHED is never counted as either. Exit codes: 0 nothing failed and the boot state matched the reference, 1 a check failed, 2 nothing failed but the boot state was not established, so a caller cannot reach a positive verdict by default.
Expected: PASS: 29 FAIL: 0 NOT ESTABLISHED: 8. Where pki.infineon.com is unreachable, the checker falls back to certificate copies in the archive and adds a ninth line saying the EK chain is then not independent of us.
What the checker establishes: the AK is registered to a TPM whose EK chains to the Infineon root; both quotes verify under that AK and are bound to their records; the quoted PCR 0-9 digest equals the signed reference for this release.
What it reports as not established, and why:
- Layers never measured (case 1 in my Absence of evidence needs a name on every verifier surface: six threads, one primitive #279 comment). PCR 2, 3, 5 and 7 in the signed reference hold a single separator and nothing else. The digest matches, so a checker comparing digests passes them. PCR 10 to 23 are outside the quote's selection. Each is its own line.
- Evidence spanning more than one boot (case 3). This TPM is not reset by a warm reboot, so
resetCountdoes not change either, and the agent record carries no field that changes per boot. A digest mismatch therefore cannot be told apart from a warm reboot, and the checker reports it as NOT ESTABLISHED with exit 2, not as FAIL. Limitation: the published quotes match, so I could exercise this branch only by forcing the comparison in a copy of the script. There is no signed quote with a different boot state in this evidence. - Freshness (qualifying data is the hash of the agent's own record), EK revocation (
revocation_checked: falsein the record), and files on the root filesystem, which the checker states it does not check.
What remains unknown: case 2 from my comment (measured but not appraised) is not shown here. The production image loads no IMA policy and PCR 10 is not quoted, so this evidence is "not measured", not "measured without appraisal".
Activity
revenue7-eng commentedon Oct 1, 2026
Correction to my own wording above. "The AK is registered to a TPM whose EK chains to the Infineon root" overstates what the checker establishes. It establishes that our signed registration record binds this AK to this EK, and that the EK chains to the Infineon root. That the registration happened as the record states is not established: VERIFY-L3-rc13.md lists it first under "Not established", and the checker does not yet print it as a NOT ESTABLISHED line. If useful, I will publish a versioned checker that does, alongside the current one, without changing the published evidence.
imran-siddique commentedon Oct 1, 2026
@revenue7-eng coverage stays on the verifier's surface, not in the record.
runtimestays closed, and so doesappraisal, whosestatuscarries only the EAR values (affirming,warning,contraindicated,none) and so cannot hold "not established" without collapsing it into one of them.Your three cases are verifier outcomes, each reported with its reason and never scored as a pass or a failure: an unmeasured layer, a measured but unappraised layer, and a two-boot evidence mix. They are now the platform-measurement row on #279. If you want to take it, the next step is a PR adding those reason codes to the verifier result, citing your rc13 checker run as the evidence.
revenue7-eng commentedon Oct 2, 2026
@imran-siddique update since the opening post, with the evidence published:
Case 2 now has signed evidence. Development image on the same board, quotes under the registered AK (PCR 0-12): four IMA entries in PCR 11 and 12 replay to the quoted values, and the policy that leaves them unappraised is not measured into the log, so a verifier can establish measurement and not appraisal. Record and offline checker: https://github.com/revenue7-eng/tactiq-os/blob/main/measurements/tpm-quotes-dev-20261002.md
Case 3 does not occur on this platform: SPL resets the TPM before measuring. A signed warm-reboot pair shows
resetCount242 to 243 with PCR 0-9 identical. The warm-reboot sentence in #431 no longer holds; the disclosure is corrected in revenue7-eng/tactiq-os#224. The case stays valid for platforms without that reset, but I cannot supply a fixture for it. A related limit: the reset line is a GPIO the running system can also drive, so a reset is not by itself evidence of a reboot.verify-l3-rc13-v2.shis in the rc13 release beside v1: a digest mismatch is now a failure, and the registration event and the reset origin are reported as not established.On the PR:
verify_recordnever sees the quote, log or reference, so the codes cannot be computed there. Followingcitation.py, I would add a platform-measurement check that takes a caller-supplied appraiser and records outcome and cause per surface (layer_not_measured,measured_not_appraised,evidence_spans_multiple_boots), defaulting tonot_attemptedwithout one, with fixtures from the rc13 and 2026-10-02 sets. Is that the shape you mean?imran-siddique commentedon Oct 2, 2026
@revenue7-eng yes, that is the shape. Two conditions for the PR. Each cause needs a fixture that produces it and a twin that differs only in that condition and does not. For
evidence_spans_multiple_boots, which this board cannot produce, a synthetic fixture labelled as synthetic is fine; without one, leave that code out until a fixture exists. Andnot_attemptedmust stay distinct from a pass wherever the result is summarised. Correcting case 3 against your own evidence before anyone asked was the right call for the record.feat(verify): record a caller-supplied appraiser's per-layer report o…
feat(verify): record a caller-supplied appraiser's per-layer report o…
imran-siddique commentedon Oct 8, 2026
@revenue7-eng closing as delivered. #457 records a caller-supplied appraiser's per-layer report, and #477 put the three reasons into §3.1.5 with a twin for every rejection, the multiple-boots case labelled synthetic, and
not-establishedkept apart from a pass in every summary, which were the two conditions from October 2.