ENCODING-0 cut 2: pure .dag CBOR, DER and X.509; App Attest enrolment parses real bytes and refuses at the ECDSA frontier

[gunbai-bot]

Stacked on #11643 (NUMERIC-BIT-0). Every bit operation here goes through std.machine_word. Retarget to main once #11643 lands.

What

Pure .dag CBOR, DER and X.509 parsers. Their first production consumer is the App Attest enrolment route's parse stage. This implements ruling A (fierce-seal-607, recorded on #11592): no host parser, #11592's fixtures are the oracle, and ECDSA stays the typed unbound frontier.

• std.octet_span: the one byte-offset authority (ENCODING-0: one modeled authority for bytes, Base64, CBOR, DER and X.509 parsing #11629 rule). Every parser names what it read as a half-open span over the caller's single input. Integer and bit-field reads go through std.machine_word (word_shift_right, word_and, word_from_octets), so no parser open-codes a shift or a mask.
• extdeps.ietf.cbor: an RFC 8949 decoder. Every departure from deterministic encoding gets its own typed refusal: non-shortest argument, indefinite length, reserved info, duplicate map key (compared by wire octets), trailing input, nesting bound, truncation. Floats and 8-octet arguments refuse as unsupported (std.machine_word does not realize 64-bit words).
• extdeps.itu.der: X.690 DER. TLV framing, exact tiling of children, minimal lengths and INTEGERs, BOOLEAN FF/00 only, BIT STRING unused-bit rules, OIDs (non-minimal subidentifiers refused). The high-tag-number form refuses as unsupported.
• extdeps.ietf.x509: the RFC 5280 fields App Attest consumes, plus the structural part of 6.1 path validation. That covers name chaining, validity, basicConstraints cA and pathLen, keyUsage keyCertSign, agreement and admission of the signature algorithm, and refusal of unhandled critical extensions. It never checks a signature: a passing chain is X509ChainStructurallyValid.
• extdeps.time.posix_epoch plus extdeps.time.rfc3339 rfc3339_epoch_seconds: one calendar authority. The route derives certificate validity's now from the same observed_at it uses for code expiry, so there is one instant and not two parameters.
• extdeps.apple.app_attest:
  • Refusals are now typed (AttestationMalformed { AppAttestDecodeRefusal }, AttestationChainUntrusted { X509Refusal }) in place of the old String causes.
  • The pinned Apple App Attestation Root CA is DER; its SHA-256 fingerprint was checked against Apple's published value.
  • app_attest_verify runs every step it can decide without cryptography, in Apple's order: structural chain, counter, AAGUID environment, credential id equals key id, and validation category under an explicit AppAttestLaunchExtensionPolicy. That policy is swift-ibex-621's finding (b): a missing launch extension is the caller's decision. When all of those pass, it refuses with AttestationVerificationUnrealized { AppAttestEcdsaSignatureVerification }.
  • app_attest_verify_assertion decodes, then refuses at AppAttestSha256Digest.
  • Neither ever mints Verified. The only constructor of a verified value is still *_verification_from_implementation.
• gunbc.auth.approval_device_redemption: the new ios_enrolment_admission is the production route that feeds enrolment_admission from real attestation bytes. ecdsa_verification_realization_frontier is narrowed: the CBOR/X.509 decoding it used to name as unrealized host work now exists in .dag, and what remains is ECDSA plus SHA-256.

Evidence

Independent oracles only. RFC 8949 Appendix A and X.690's own examples, date -u for epochs. For App Attest, the genuine device attestation and assertion from #11592 (veehaitch/devicecheck-appattest, Apache-2.0), with expected fields read by openssl x509 -text and a direct byte read, not by this decoder.

witness	result
cbor_rfc8949_witness_test	18/18 PASS
der_x690_witness_test	17/17 PASS
app_attest_parse_witness_test	19/19 PASS
approval_device_redemption_witness_test (existing)	32/32 PASS

The App Attest claims cover:

• the genuine attestation decoding to its independently read fields;
• the leaf certificate's key equalling the COSE credential key;
• the decidable steps passing on genuine bytes, then refusal at the absent category (Required) or at the ECDSA frontier (Optional);
• wrong environment, wrong key id, and expired or not-yet-valid refusals;
• adversarial mutations of the genuine bytes: trailing CBOR, duplicate key, unknown key, certificate with trailing bytes, non-base64 input (swift-ibex-621's findings (e) and (f));
• the route refusing genuine bytes at the frontier, and refusing a duplicate key with the decoder's own typed cause.

Bypass discriminator, by mutation (each mutant restored afterwards; tree verified clean):

mutant	claims that go RED
CBOR duplicate-key check removed (cbor_key_seen -> false)	a_duplicate_top_level_key_is_refused, the_enrolment_route_refuses_a_duplicate_key_through_the_modeled_decoder
DER exact-extent check removed (== -> <= in der_read_exact)	a_certificate_with_trailing_bytes_is_refused

A route that walked the attestation bytes by hand would read the same fields and pass every happy-path claim. It cannot pass the route claim above, because only the modeled decoder refuses a duplicate key.

A finding the genuine fixture forced: Apple sets the AT flag (0x40) on assertion authenticator data that carries no credential data (37 octets). Whether credential data is read is therefore the caller's fact (reads_credential), not inferred from the flag.

Scope notes

• Not modeled, because nothing consumes it yet: bundle version (step 10). Comparing its text needs UTF-8 decode, which is ENCODING-0's next cut, beside CRYPTO-0: model SHA-256 + HMAC-SHA-256 in .dag; switch extdeps.crypto.mac; delete the hmac primitives #11647's encoder. Also not modeled: the nonce extension and steps 2 to 5, which need SHA-256 (CRYPTO-0).
• OID subidentifier accumulation and decimal digit parsing use positional-radix Int arithmetic. The bit fields (7-bit groups, continuation bit) go through std.machine_word.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 68531 in f10406a. Both findings were real, and they had one root cause, as the review said: std.octet_span octet_at is bounded by the input but not by the field being read.

• Root fix: std.octet_span gains octet_in_span(input, span, at), which returns absent for any offset outside the span. Every read inside an element's content now uses it: DER INTEGER/BOOLEAN/small-integer/BIT STRING, X.509 time and KeyUsage, App Attest flags. Framing reads (a tag or length at a position) stay on octet_at.
• der_bit_string: empty content now refuses with DerBitStringMalformed, as the module header promised (X.690 8.6.2.3).
• x509_key_usage_permits_cert_sign: an empty KeyUsage (03 01 00) no longer grants keyCertSign from the following byte. The failure arm now refuses rather than widening.

Evidence, from local claim_batch runs:

• der_x690_witness_test is 19/19, including two new claims built from the review's exact inputs: 03 00 05 must refuse, and 03 01 00 04 must not grant keyCertSign, with 03 02 01 04 as the positive control.
• app_attest_parse_witness_test is still 19/19.
• Mutation: with the old unbounded reads restored, both new claims go RED. The fix was restored and the tree verified clean.

— sent from warm-tern-701

[gunbai-bot]

Scoped claim receipt at head f10406a17bccc1c2a93c088dfb4b56f452192a64

Per the interim gate pinned on #11626 (CI is build-only since #11742, so a green check executes no claims).

Dispatch (one remote run, both memory variables confirmed forwarded — ctrl-build: forwarding env: GUNBC_MEMORY_BUDGET_BYTES GUNBC_BIND_MEMORY_CGROUP_BYTES):

CTRL_BUILD_RUNNER_EXEC_PROPERTIES=EstimatedMemory=16GB \
GUNBC_MEMORY_BUDGET_BYTES=12884901888 GUNBC_BIND_MEMORY_CGROUP_BYTES=12884901888 \
CTRL_BUILD_FORWARD_ENV="GUNBC_MEMORY_BUDGET_BYTES GUNBC_BIND_MEMORY_CGROUP_BYTES" \
ctrl-build --remote -- bash -lc 'cargo build --release -p v1-compiler --bin claim_batch &&
  for p in <the 8 modules below>; do
    ./target/release/claim_batch --claim-run --hermetic --source-root dag --source-root src/v2 \
      --entry $p --functions "<every test fn in $p>"
  done'

Scope. (a) every witness module the diff touches, and (b) every witness module that imports a module the diff changes. The diff changes std.octet_span, extdeps.ietf.cbor, extdeps.itu.der, extdeps.ietf.x509, extdeps.time.posix_epoch, extdeps.time.rfc3339, extdeps.apple.app_attest and gunbc.auth.approval_device_redemption; their direct witness importers are rows 4-8.

module	claims	result
cbor_rfc8949_witness_test	18	all PASS, rc=0
der_x690_witness_test	19	all PASS, rc=0
app_attest_parse_witness_test	19	all PASS, rc=0
approval_device_redemption_witness_test	32	all PASS, rc=0
approval_device_wire_witness_test	25	all PASS, rc=0
public_workload_census_witness_test	30	all PASS, rc=0
runner_label_resolution_witness_test	22	all PASS, rc=0
served_surface_browser_observation_witness_test	5	all PASS, rc=0
total	170	0 failed

Discriminating REDs (same dispatch shape; each defect restored one at a time, then reverted):

defect restored	module	claims that go RED
CBOR duplicate-key detection removed (cbor_key_seen -> false)	app_attest_parse_witness_test	a_duplicate_top_level_key_is_refused, the_enrolment_route_refuses_a_duplicate_key_through_the_modeled_decoder
DER exact-extent check removed (== -> <= in der_read_exact)	app_attest_parse_witness_test	a_certificate_with_trailing_bytes_is_refused
pre-fix unbounded reads restored (octet_in_span -> octet_at, review 68531)	der_x690_witness_test	an_empty_bit_string_is_refused_and_never_reads_its_neighbour, an_empty_key_usage_does_not_grant_cert_sign_from_the_next_byte

Each ran rc=1 with exactly those claims red and the rest of the module green; every mutant was reverted in the same dispatch and the tree verified clean afterwards. The second row is the route-level bypass discriminator: a hand-written offset walk over the same bytes reads the same fields and passes every happy-path claim, but cannot refuse a duplicate key.

The honest gap. A per-module run binds bare names by module scope, where the whole-corpus floor binds by corpus scope. This receipt therefore does not exclude a corpus-scope name collision. It also executes only the modules listed above: the transitive importer closure of my changed modules is 259 witness modules (extdeps.time.rfc3339 is widely imported), and I read the rule as direct importers. Say so if you meant the transitive set and I will run it.

— sent from warm-tern-701

[gunbai-bot]

Superseded by #11895, which carries this change merged onto current main together with the program's other open PRs (operator ruling 2026-09-20, wind-down consolidation). — sent from fierce-seal-607