Repository navigation
feat(attestation): hash intent and evidence as JCS and bind them on verify - #247
Conversation
…erify Seals now hash the intent and evidence records as their JCS (RFC 8785) bytes, so anyone holding the sidecar can recompute them in any language (jq -cjS ... | sha256sum). The sidecar itself is written as I-JSON/JCS. `attest verify` now rehashes the embedded intent and evidence. Before, it only checked the chain hash against the three stored digests, so both records could be edited after sealing without detection. The seal records a `hash_scheme` (`jcs-sha256`), prefixed into the chain hash so any Ed25519 signature covers it: dropping the field to skip the content check breaks the chain hash. Sidecars from before the field verify as legacy, reported as not rehashed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k
|
Caution Review failedThe pull request is closed. Finishing Touches
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b2770d5755
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| hasher.update(report_hash.as_bytes()); | ||
| hex::encode(hasher.finalize()) | ||
| }; | ||
| let chain_hash = chain_hash(HASH_SCHEME_JCS, &intent_hash, &evidence_hash, &report_hash); |
There was a problem hiding this comment.
This changes the signed chain digest to include hash_scheme, but src/abi/AttestationUnforgeability.idr:7-12,44-67 still claims to mirror this implementation while modeling chainHash as a function of only intent, evidence, and report. Consequently, the proof no longer covers the new security-critical property that changing the scheme invalidates the seal. Add the scheme as a modeled input and update the associated integrity/collision statements so the formal attestation guarantee matches this implementation.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Partly addressed in d88ccd9. The model's doc now states the scheme-prefixed formula and its scope. chainHash is the hash for one fixed scheme, so integrity, authenticity and nonRepudiation hold per scheme. Scheme binding (no downgrade) is explicitly listed as not modelled, and the doc says which verifier check it rests on.
I haven't changed the proof terms. Adding a fourth chainHash input plus a no-downgrade lemma needs an Idris2 type-check, which I couldn't run in this environment, and no workflow here type-checks src/abi/. I've left this thread open for the owner to decide whether that lands in this PR or as a follow-up.
Generated by Claude Code
|
Add Carrot credits or activate Agent usage billing to use Autofix |
The legacy chain hashes `i || e || r` and the JCS chain hashes `"jcs-sha256" || i || e || r`. With variable-width digest fields, moving the scheme name into `intent_hash` and dropping `hash_scheme` reproduced the signed bytes exactly while falling back to the legacy path, which skips the content rehash. A signed sidecar could then be edited and still verify. (Codex review finding on #247.) `attest verify` now requires every digest to be 64 lowercase hex characters, so the two chain inputs (192 and 202 bytes) cannot coincide. A test reproduces the attack; it verified as OK before this change. The Idris2 model's doc now states the scheme-prefixed formula and that it covers one scheme at a time; scheme binding is not yet modelled. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k
Stacked PR E of the estate-format series: - A: `.kyaml` loaders - B: example profiles - C: JCS reports - C2: deterministic reports (#245) - D: JCS attestation (#247) This PR is independent of #245 and #247 and branches from `main`. ## What changes - **New module `src/kyaml.rs`.** A KYAML emitter that follows mikefarah `yq` v4's KYAML encoder (`pkg/yqlib/encoder_kyaml.go`, v4.54.1): flow style, two-space indent, a trailing comma on every entry, bare keys only for `^[A-Za-z_][A-Za-z0-9_-]*$`, and every string double-quoted. - **Same data as the JCS report.** Keys follow JCS order (UTF-16 code units) and numbers are in JCS form, so the KYAML and JSON reports of a scan differ only in syntax. - **New format value.** `ReportOutputFormat::Kyaml` adds `--output-format kyaml`, extension `.kyaml`, parsed from `"kyaml"`. Loaders have read `.kyaml` since PR A. - **README fix.** `README.adoc` listed `--output-format` values `markdown` and `text`, which never existed. It now lists the real ones. ## Contract, checked against the real tools | Check | Result | |---|---| | Fixed point of `yq -p yaml -o kyaml`, the test `scripts/kyaml-format.sh --check` runs | ✅ on all reports below | | standards `scripts/kyaml-format.sh --check`, run for real | ✅ `all 4 file(s) are KYAML` | | Byte-identical to `yq -p json -o kyaml` of the JCS report | ✅ two historical `reports/*.yaml` assault reports, plus assail of `src/` (52 KB) and `tests/` | | Read back through `crate::yaml` (serde-saphyr) | ✅ same data as the JCS report | The test `real_report_is_byte_identical_to_yq` pins this in CI without yq. `tests/fixtures/kyaml/assail-report.kyaml` is yq's output for the checked-in JCS report next to it. ## Two documented differences from yq 1. **Non-printables.** YAML's non-printables (U+007F–U+009F, U+FFFE, U+FFFF) are escaped as `\uXXXX`. yq writes them raw, which YAML 1.2 does not allow. A raw **U+0085 (NEL)** reads back as a line break, so yq turns `"x\u0085y"` into `"x y"`. When a file contains one, `kyaml-format.sh` reports `REFUSED … the KYAML rendering does not parse to the same data` (exit 2). The gate therefore already treats yq's output there as untrustworthy. I chose data integrity over gate cleanliness for this rare case. - **Alternative:** write them raw like yq. The gate stays quiet, but NEL is silently corrupted. - **Root-cause fix (beyond this repo):** escape these in yq's `escapeDoubleQuotedString` upstream. 2. **Floats read from JSON.** `yq -p json` reformats some floats (`1e-7` becomes `1e-07`, Go style). The KYAML report keeps the JCS form (`1e-7`), which `yq -p yaml` preserves, so the fixed point holds. Byte identity with yq's JSON→KYAML path holds whenever yq doesn't reformat, which covers every report checked. ## Validation - `cargo fmt --check`: clean. - `cargo clippy --all-targets -D warnings`, with and without `--all-features`: clean. - `cargo test --all-features`: all 20 suites green. - 8 new unit tests in `kyaml::tests`: - yq layout (expected text from yq); - scalars and lists at the top level; - C0 escapes; - non-printable escapes, including NEL read back intact; - JCS key order with a supplementary-plane key; - JCS and I-JSON numbers; - the real-report golden; - a report round trip. - `--output-format bogus` now lists `json, yaml, kyaml, nickel, sarif`. ## Follow-ups (outside this PR) - `assail` ignores `--output-format` and always writes JCS JSON. Honouring it means deciding which bytes the `--attest` seal hashes. - **Upstream (mikefarah/yq):** escape C1, DEL and NEL in the KYAML encoder. - **standards:** `kyaml-format.sh` could explain its refusal for this case. --- _Generated by [Claude Code](https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k)_ Co-authored-by: Claude <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
Stacked PR D of the estate-format series:
.kyamlloadersA, B, C and E are merged. This PR builds on
crate::jsonfrom the JCS-reports PR.What changes
assail --attesthashes the intent and evidence records as their JCS (RFC 8785) bytes via the newcrate::json::to_canonical_bytes. It previously hashedserde_json::to_vecstruct order. The.attestation.jsonsidecar itself is now written as I-JSON/JCS (J-1).attest verifyused to recompute onlychain_hashfrom the three stored digests, so the embedded intent and evidence could be edited after sealing without detection. It now rehashes both from the file and fails on a mismatch. It hashes the parsed JSON tree rather than the typed structs, so fields this build doesn't know about stay inside the hash.hash_schemeon the seal (jcs-sha256). The scheme is prefixed into the chain hash:SHA-256(hash_scheme || intent_hash || evidence_hash || report_hash). Any Ed25519 signature therefore covers it too.attest verifyrejects any digest field that isn't exactly 64 lowercase hex characters. Without that check, an attacker could move the scheme name intointent_hashand drophash_scheme. That reproduced the signed bytes on the legacy path, which skips the content rehash. With fixed widths, the legacy chain input (192 bytes) and the scheme-prefixed one (202 bytes) can't coincide.hash_schemedeserialise asserde-json-sha256, use the old chain-hash formula, and verify as before, reported asContent: not rehashed (legacy hash scheme). An unknown scheme fails.Validation
cargo fmt --check, pluscargo clippy --all-targets -D warningsboth with--all-featuresand without: clean.cargo test --all-features: all suites green after merging main (lib: 509 passed).src/attestation/mod.rs:intent_hashequals SHA-256 of a hand-written JCS string.jq -cjS .attestation.intent | sha256sumand the same for evidence match the seal.sha256sum report.jsonmatchesreport_hash.printf 'jcs-sha256%s%s%s' I E R | sha256summatcheschain_hash.intent_hash is not a SHA-256 digest).Proof angle
src/abi/AttestationUnforgeability.idris parametric inchainHashunder thechainCR(injectivity) hypothesis. Its doc now states the scope: the model covers one scheme at a time, andintegrity,authenticityandnonRepudiationhold per scheme.Scheme binding (no downgrade) is not modelled. In the code it rests on the fixed-width digest check. The Codex P1 was a failure of exactly the injectivity
chainCRassumes: the bug was in the encoding, not in SHA-256.The model can be extended with a fourth
chainHashinput and a no-downgrade lemma. That needs an Idris2 type-check, which this environment couldn't run, and no workflow here type-checkssrc/abi/. The open review thread onseal.rsholds that decision for the owner.Follow-ups (outside this PR)
attest verify --report <file>to recomputereport_hashfrom the report itself; today it is only cross-checked againstdecision_hash.--require-boundmode (or a policy default) that rejects legacy, unbound seals.src/abi/in CI.evidence.evidence_hashhashesusize::to_le_bytes, whose width depends on the platform. That is harmless for the seal, which uses JCS, but not portable.hash_scheme. That work is in other repositories.🤖 Generated with Claude Code
https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k