spec(appraisal): 3.1.5, a layer is established by its event log or by a reference value (#279)

[revenue7-eng]

Section 3.1.5, as discussed with @imran-siddique: a layer is established by its event log or by a reference value, and the condition that it holds measurements binds both routes. To land before the next tag.

What changes

• Two routes. A layer that holds measurements is established when its event log replays from the initial value to the quoted value, or when the quoted value equals a reference value for that layer from a source the verifier's policy trusts and not taken from the evidence under appraisal (appraisal against reference values, RFC 9334).
• Holds measurements binds both. A quoted value equal to the initial value, or on a TPM to the value a separator alone produces, is layer-not-measured even when a reference matches it.
• Per layer, not composite. A quoted composite establishes each layer's value only through the reference's per-layer values over the same selection. A reference that gives only a composite establishes no layer, because it does not show which layers hold measurements.
• Order with rule 3. A presented log that does not replay is decided under rule 3 first; a matching reference does not then establish the layer.
• Unchanged. Neither route shows that what ran was appraised; measured-not-appraised reads as before. The reasons table names both routes in the measured-not-appraised row. "Out of scope" adds the reference-value format to what this section does not fix.

This narrows the BREAKING entry of #477: a verifier that reports affirming after a reference match is conformant when each layer its policy requires holds measurements and equals its reference value. Records do not change. It also brings the text in line with vector 09, which already reads PCR 0, 1, 4, 6, 8 and 9 of the rc13 release reference as established without an event log.

Test vector

examples/platform-measurement-appraisal/45-rc14-established-by-reference.json, from published evidence (TactiQ OS v2.1.0-rc14 release, Rock 5A, Infineon SLB9670): the attestation agent's quotes over PCR 0 to 9 on slot B, appraised against the signed release reference with no event log. PCR 0, 1, 4, 6, 8 and 9 established by reference; PCR 2, 3, 5 and 7 equal the value a separator alone produces and are layer-not-measured although the reference matches them; status affirming. Sourced, so no twin, as with 09 and 10.

The evidence and an offline checker: release assets l3-evidence-rc14.tar.gz (19 quotes and the AK), rim-rock5a.json and rim-rock5a.json.p7s at https://github.com/revenue7-eng/tactiq-os/releases/tag/v2.1.0-rc14, checked with scripts/appraise-layers.py in that repository. All 19 quotes carry pcrDigest dc7051b2...83438, the composite of the reference's slot B values.

Tests

test_a_reference_equal_to_a_separator_alone_is_not_measured pins the reference's per-layer values, checks that vector 45's measurement is their composite, and that the layer-not-measured layers are exactly those whose reference value is the initial value or a separator alone (both TCG EV_SEPARATOR data values), with every other layer established and status affirming. Switched off by writing every layer of 45 as established in the generator, it fails and nothing else does. The vector count is 45. The set regenerates byte for byte; the full suite, ruff and tools/check_dashes.py pass.

Text changes cannot be observed by a test beyond the vector: no validator decides routes, since the record carries no evidence.

Independent read

A fresh agent session given the repository and this diff, with no other context, reported: the composite sentence first allowed a composite-only reference to establish layers (fixed: a composite-only reference establishes none); the source of a reference was unbounded, so a verifier could take the observed value as its own reference (fixed: from a trusted source, not taken from the evidence); the precedence between layer-not-measured and rule 3 was unstated (fixed: rule 3 first); the CHANGELOG did not say what this does to the #477 BREAKING entry (fixed); the test checked one separator value only (fixed: both); the README list of sourced vectors (rewritten).

Proposed and written by @revenue7-eng; sponsoring maintainer @imran-siddique.