diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index d1322e2..336faf7 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -15,7 +15,7 @@ workflows: - 'actions/upload-pages-artifact@v5.0.0' - 'haskell-actions/setup@v2.12.1' '.github/workflows/codeql.yml': - - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7' + - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12' '.github/workflows/dashboard-check.yml': - 'actions/checkout@v7.0.1' - 'dtolnay/rust-toolchain@v1' @@ -30,21 +30,21 @@ workflows: - 'dtolnay/rust-toolchain@v1' - 'swatinem/rust-cache@v2.9.3' '.github/workflows/governance.yml': - - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7' + - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12' '.github/workflows/hypatia-scan.yml': - - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7' + - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12' '.github/workflows/idris-abi.yml': - 'actions/checkout@v7.0.1' '.github/workflows/label-triage.yml': [] '.github/workflows/labels.yml': [] '.github/workflows/mirror.yml': - - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7' + - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12' '.github/workflows/rust-ci.yml': - - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7' + - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12' '.github/workflows/scorecard.yml': - - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7' + - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12' '.github/workflows/secret-scanner.yml': - - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7' + - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12' '.github/workflows/squabble.yml': - 'actions/checkout@v7.0.1' - 'hyperpolymath/cicd-squabbler@79d7dbacc8a02b4a4388b4a36fe46893b5b7ce73' @@ -79,6 +79,11 @@ dependencies: commit: 'sha1-368f82528645a54fb793d4d04e342629a3f51346' owner_id: 44036562 repo_id: 438112499 + 'actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333': + ref: 'v8.0.2' + commit: 'sha1-9000827ccba6bdab643e8b6fd33ac0654aef8333' + owner_id: 44036562 + repo_id: 192626254 'actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f': ref: 'v7.0.0' commit: 'sha1-bbbca2ddaa5d8feaa63e36b76fdaad77386f024f' @@ -156,14 +161,15 @@ dependencies: commit: 'sha1-c1a34884054fabf0e9de81dbf68f4ba7874e85f1' owner_id: 6759885 repo_id: 1275650185 - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7': - ref: 'a85aa8e70326cceedae169013a47daee554918b7' - commit: 'sha1-a85aa8e70326cceedae169013a47daee554918b7' - owner_id: 6759885 + 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12': + ref: 'a797d308c0517d4e2d21cc7f1cb08d41f82b1a12' + commit: 'sha1-a797d308c0517d4e2d21cc7f1cb08d41f82b1a12' + owner_id: 297579217 repo_id: 1116521501 uses: - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9' - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' + - 'actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333' - 'actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9' - 'denoland/setup-deno@22d081ff2d3a40755e97629de92e3bcbfa7cf2ed' - 'dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8' @@ -173,7 +179,7 @@ dependencies: - 'goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406' - 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e' - 'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6' - - 'swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6' + - 'swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0' - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555' 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e': ref: 'v2.5.0' @@ -185,9 +191,9 @@ dependencies: commit: 'sha1-0c5077e51419868618aeaa5fe8019c62421857d6' owner_id: 108928776 repo_id: 512644635 - 'swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6': - ref: 'v2' - commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6' + 'swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0': + ref: 'v2.9.3' + commit: 'sha1-d1527c8f67ef9af357290475d4af4b0fab8f12e0' owner_id: 580492 repo_id: 298565987 'swatinem/rust-cache@v2.9.3': diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index ce0a91d..c55dccd 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -32,10 +32,10 @@ permissions: jobs: codeql-actions: - uses: hyperpolymath/standards/.github/workflows/codeql-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296) + uses: metadatastician/standards/.github/workflows/codeql-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 with: language: actions codeql-rust: - uses: hyperpolymath/standards/.github/workflows/codeql-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296) + uses: metadatastician/standards/.github/workflows/codeql-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 with: language: rust diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index fc91895..a114cbb 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -34,7 +34,7 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296) + uses: metadatastician/standards/.github/workflows/governance-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 permissions: actions: read contents: read diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index c2b4ebe..ffa84bc 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -28,5 +28,9 @@ permissions: jobs: hypatia: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296) - secrets: inherit + uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 + # Named, not `inherit`: GitHub refuses inheritance from a user account + # (hyperpolymath) into an organisation (metadatastician). The reusable + # declares this one optional secret. + secrets: + HYPATIA_SCAN_PAT: ${{ secrets.HYPATIA_SCAN_PAT }} diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml index 07ce99a..f2b820c 100644 --- a/.github/workflows/mirror.yml +++ b/.github/workflows/mirror.yml @@ -14,8 +14,21 @@ permissions: jobs: mirror: - uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296) - secrets: inherit + uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 + # Named, not `inherit`: metadatastician is an organisation and hyperpolymath a + # user account, and GitHub refuses `secrets: inherit` across that boundary. + # These are the ten secrets mirror-reusable.yml declares (all optional). + secrets: + GITLAB_SSH_KEY: ${{ secrets.GITLAB_SSH_KEY }} + BITBUCKET_SSH_KEY: ${{ secrets.BITBUCKET_SSH_KEY }} + CODEBERG_SSH_KEY: ${{ secrets.CODEBERG_SSH_KEY }} + SOURCEHUT_SSH_KEY: ${{ secrets.SOURCEHUT_SSH_KEY }} + DISROOT_SSH_KEY: ${{ secrets.DISROOT_SSH_KEY }} + GITEA_SSH_KEY: ${{ secrets.GITEA_SSH_KEY }} + RADICLE_KEY: ${{ secrets.RADICLE_KEY }} + R2_ACCESS_KEY_ID: ${{ secrets.R2_ACCESS_KEY_ID }} + R2_SECRET_ACCESS_KEY: ${{ secrets.R2_SECRET_ACCESS_KEY }} + R2_AGE_RECIPIENT: ${{ secrets.R2_AGE_RECIPIENT }} permissions: actions: read contents: read diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index 1817f74..96f6934 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -21,7 +21,7 @@ permissions: jobs: rust-ci: - uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296) + uses: metadatastician/standards/.github/workflows/rust-ci-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 permissions: actions: read contents: read diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 53e16f6..93560d1 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -17,5 +17,6 @@ jobs: contents: read security-events: write id-token: write - uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296) - secrets: inherit + uses: metadatastician/standards/.github/workflows/scorecard-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 + # No `secrets:` block: scorecard-reusable.yml declares none, and GitHub + # refuses `secrets: inherit` from a user account into an organisation. diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 7461542..9be47cd 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -22,4 +22,4 @@ jobs: actions: read security-events: write contents: read - uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296) + uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 32ae62f..6513abe 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -75,6 +75,11 @@ tables must agree. | T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path | T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked | T-8 | The operation metadata log is saved atomically, and an undo whose `+mark_undone+` fails to persist can be retried | OPEN | by inspection: the log now takes the same write, sync, rename path as the transaction log (`+crate::transaction::write_atomic+`), and `+metadata::tests::save_replaces_the_log_atomically+` asserts it, but the crate has not been built since that edit, so the row stays OPEN until the test is green in CI. Retry is unchanged: `+undo+` still runs the undo before `+mark_undone+` persists, so a failed persist still leaves the file undone and the log not +| S-1 | A content hash that is not `+sha256:+` plus 64 lowercase hex digits never resolves to a path outside the store root | TESTED | `+content_store::tests::malformed_hash_never_leaves_the_store_root+`; fixed in #163 after audit probe P5 showed `+delete+` removing a file outside the store (`+docs/reports/audit/proof-statement-audit-2026-10-27.adoc+`) +| S-2 | `+store+` repairs a blob a crash left damaged instead of deduplicating against it, and a successful store leaves no temporary file behind | TESTED | not claimed: cleanup after a failed write or rename, whose removal error `+store+` ignores, so a temporary file can remain; not claimed: that the write itself is atomic. `+store+` writes by temporary file, sync and rename, but by construction only; no test injects a failure mid-write. `+content_store::tests::store_repairs_a_blob_truncated_by_a_crash+`, `+store_leaves_no_temp_files_and_count_ignores_strays+`; fixed in #163 (probe P4) +| L-1 | Editing any field of any audit-log entry makes `+verify_integrity+` fail | OPEN | false today, probes P1 and P2: algorithm, purpose, old_state, new_state, rotated_to and rotated_from are in neither the MAC nor the chain hash, and key_id, fingerprint and reason are chain-hashed only, so on the last entry nothing protects them. The fix is a MAC over every field (a scheme version bump) +| L-2 | Removing trailing audit-log entries makes `+verify_integrity+` fail | OPEN | false today, probe P3: every prefix of a valid log verifies. Needs an anchor held outside the log (a design decision: signed head, external counter, or witness) +| O-1 | An `+ObliterationProof+` attests that the content it names was erased | OPEN | false today, probe P6: `+ObliterationProof::generate+` sets `+storage_cleared: true+` unconditionally and `+verify_commitment+` holds for content that was never stored. Either compute the field from the erasure, or stop calling the object a proof | V-1 | valence-shell depends on `+reversible-core+` for reversible operation data | DESIGNED | ARCHITECTURE.adoc §Consumption status — no repository outside this workspace depends on the crate; Phase 2 is unstarted | V-2 | ochrance verifies januskey A2ML manifests | DESIGNED | `+crates/reversible-core/src/manifest.rs+` — `+ManifestEmitter+` has never been parsed by ochrance; the SHA-256/BLAKE3 boundary mismatch is unresolved | V-3 | aletheia consumes `+reversible-core+` | DESIGNED | ARCHITECTURE.adoc §Deferred — Phase 0 research, no operation types yet @@ -119,17 +124,21 @@ their artefact is Agda (`+verification/proofs/agda/+`). They are **Grade 3**: each type-checks in Agda and none has been translated to an independent foundational system, which is mathesis §5's definition as written. The receipt is a green `+agda-proofs.yml+` run -(https://github.com/hyperpolymath/januskey/actions/runs/40867211509[40867211509]) -at commit `+4afb710e86646658f667f10bd6274ee47416bfc7+`, Agda 2.6.4.3, with -`+resource-algebra+` pinned at `+cf9235c+`. The modules, the gate script, the -sibling fetch and the workflow are byte-identical at that commit and at this -one, so the receipt covers these rows as they stand. Mathesis status for them: +(https://github.com/hyperpolymath/januskey/actions/runs/41687715055[41687715055]) +at commit `+fc188c4+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at +`+cf9235c+`. That run used the current gate (`+Reversibility+`, +`+TransactionAtomicity+` and `+Epistemic+` under `+--safe --without-K +--cubical-compatible+`), and the modules, the gate script, the sibling fetch and +the workflow are byte-identical at that commit and at this one, so the receipt +covers these rows, E-1m included, as they stand. (An earlier receipt cited here, +run 40867211509 at `+4afb710+`, predates `+Epistemic.agda+` and the +`+--cubical-compatible+` flag, so it never covered E-1m.) Mathesis status for them: `+AGDA-VERIFIED+`. The other seven PROVEN rows — A-1, A-2, C-1 to C-5 — are Idris2 theorems. Under PROOF-POLICY §1 those are interface and ABI contracts, so the theory ladder does not grade them: they are PROVEN in the vocabulary above and nothing more. The -same holds for the 23 TESTED rows, which record observed behaviour and never +same holds for the 27 TESTED rows, which record observed behaviour and never grading. First-party Rust behaviour belongs to **Creusot** (not SPARK, and not Idris2); no Creusot contract exists in this tree, which is why no Rust row is graded. @@ -175,11 +184,11 @@ below are still open. |Weak keys break the key store's security model. **Off the `jk` path** — tracked here only while `+keys.rs+` remains in this tree (ADR-0001) -|Attestation chain |Chain of custody proofs are unforgeable |Tampered +|Attestation chain |Chain of custody proofs are unforgeable (false as written: L-1 and L-2 are OPEN, see the 2026-10-27 proof-statement audit) |Tampered attestations undermine trust |Content store integrity |Content-addressed storage never returns wrong -content |Hash collisions or bugs corrupt stored data +content (paths confined to the store and damaged blobs repaired: S-1 and S-2 are TESTED; the write is atomic by construction, not by test; reads verify the hash) |Hash collisions or bugs corrupt stored data |Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the Rust is tested for partial-rollback retry, T-4, and failed saves, T-5; the premises T-6 and T-7 are assumed; the metadata log, T-8, now saves by rename but that is unverified) |Partial transactions corrupt state @@ -243,12 +252,19 @@ the status table above. |T-5: A save whose temporary file already exists (another writer's) fails without deleting that file or writing the log |TESTED |`crates/reversible-core/src/transaction.rs::a_save_never_removes_a_temporary_file_it_did_not_create` |`cargo test --locked -p reversible-core --lib a_save_never_removes_a_temporary_file_it_did_not_create` |T-5: The temporary file has the log's permissions from creation, before any content is written |TESTED |`crates/reversible-core/src/transaction.rs::the_temporary_file_is_restricted_before_any_content_is_written` |`cargo test --locked -p reversible-core --lib the_temporary_file_is_restricted_before_any_content_is_written` |T-5: The temporary file is opened with the log's mode, so it is never more readable than the log at any instant, not only after a later chmod (checked where the umask leaves owner read-write, the usual 022) |TESTED |`crates/reversible-core/src/transaction.rs::the_temporary_file_is_opened_with_the_logs_mode` |`cargo test --locked -p reversible-core --lib the_temporary_file_is_opened_with_the_logs_mode` +|S-1: A malformed content hash never resolves to a path outside the store root |TESTED |`crates/reversible-core/src/content_store.rs::malformed_hash_never_leaves_the_store_root` |`cargo test --locked -p reversible-core --lib malformed_hash_never_leaves_the_store_root` +|S-1: A well-formed content hash keeps the existing two-level blob layout |TESTED |`crates/reversible-core/src/content_store.rs::well_formed_hash_keeps_the_existing_layout` |`cargo test --locked -p reversible-core --lib well_formed_hash_keeps_the_existing_layout` +|S-2: Storing content again repairs a blob a crash left truncated |TESTED |`crates/reversible-core/src/content_store.rs::store_repairs_a_blob_truncated_by_a_crash` |`cargo test --locked -p reversible-core --lib store_repairs_a_blob_truncated_by_a_crash` +|S-2: A successful store leaves no temporary file behind, and count ignores stray ones |TESTED |`crates/reversible-core/src/content_store.rs::store_leaves_no_temp_files_and_count_ignores_strays` |`cargo test --locked -p reversible-core --lib store_leaves_no_temp_files_and_count_ignores_strays` |G-2: The Idris2 IsCNO / ReversibleOp pair corresponds to the Agda ReversiblePair (by transcription) |ASSUMED |`verification/proofs/agda/Reversibility.agda` |- |X-1: Hash one-wayness and physical erasure (cryptographic and physical assumptions) |ASSUMED |`src/abi/JanusKey/ABI/Proofs.idr` |- |G-3: The FFI bridge preserves grade 𝟙 (a homomorphism; resource-algebra lists homomorphisms as OPEN) |OPEN |`verification/proofs/agda/Reversibility.agda` |- |E-1: An attacker cannot recover obliterated content or use a revoked key (adversaryCannotKnow holds only by construction of the model) |OPEN |`src/abi/JanusKey/ABI/Types.idr` |- |E-1m: In a world model, an adversary whose observation excludes the store does not know what it holds (adversary-ignorant), obliteration leaves nothing to recover (obliterate-cuts-recovery, obliterate-ignorance), and rotation leaves no agent — the system included — able to use the old key (rotate-forgets-old); the fixtures AdversaryKnows and OldKeyStillUsable are refused |PROVEN |`verification/proofs/agda/Epistemic.agda::adversary-ignorant` |`bash scripts/check-agda.sh` |The six security obligations under "What Needs Proving" (obliteration, key derivation, attestation chain, content store, transaction atomicity, reversible-core) are proved |OPEN |`PROOF-NEEDS.adoc` |- +|L-1: Editing any field of any audit-log entry makes verify_integrity fail (false today: audit probes P1, P2) |OPEN |`crates/januskey-cli/src/attestation.rs` |- +|L-2: Removing trailing audit-log entries makes verify_integrity fail (false today: audit probe P3; needs an external anchor) |OPEN |`crates/januskey-cli/src/attestation.rs` |- +|O-1: An ObliterationProof attests that the content it names was erased (false today: storage_cleared is hard-coded, audit probe P6) |OPEN |`crates/januskey-cli/src/obliteration.rs` |- |T-8: The operation metadata log is saved atomically, and an undo whose `+mark_undone+` fails to persist can be retried (by inspection: `+MetadataStore::save+` calls `+crate::transaction::write_atomic+`, the path `+transaction.rs+` already tests in T-5; `+metadata::tests::save_replaces_the_log_atomically+` covers the log itself and has not been run) |OPEN |`crates/reversible-core/src/metadata.rs` |- |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |- |T-7: Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) |ASSUMED |`crates/reversible-core/src/transaction.rs` |- diff --git a/benches/crypto_shred.rs b/benches/crypto_shred.rs new file mode 100644 index 0000000..40e45f1 --- /dev/null +++ b/benches/crypto_shred.rs @@ -0,0 +1,327 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell +// +// Crypto-shredding experiment for ADR-0002 (proposed). Nothing here is used by +// `jk`: it measures the real code where it exists and a prototype where it +// does not, so the design is argued from numbers. +// +// store: ContentStore::store with compression off and with it on (the +// `jk` default), against the proposed path: gzip, then an +// AES-256-GCM seal under a fresh per-blob key, then the same +// temp/fsync/rename write for the blob, plus one synced append of +// its key to the key journal (the layout ADR-0002 §2 chooses). +// `seal_only` is the cipher with no I/O. +// erase: obliterate_file on a blob (3-pass overwrite, unlink: the current +// path) against crypto-shredding, in its two stages: +// pending: append a tombstone for the blob to the key journal +// and sync it; the old table, and so the key, can still +// be opened under the live epoch key; +// final: open the sealed table, drop the entry and re-seal +// every live key under a fresh epoch key, as one table +// (one synced write), plus folding in the journal. For +// contrast, the rejected layout: +// one file per key (one synced write each). +// +// Payloads are random, so incompressible: the worst case for gzip, which then +// costs time and saves nothing. Each is made unique per iteration, so dedupe +// never short-circuits a write. fsync cost depends on the device: numbers +// from a container's virtual disk say nothing about an SSD's flash +// translation layer. + +use aes_gcm::aead::{Aead, KeyInit}; +use aes_gcm::{Aes256Gcm, Nonce}; +use criterion::{ + black_box, criterion_group, criterion_main, BatchSize, BenchmarkId, Criterion, Throughput, +}; +use flate2::{write::GzEncoder, Compression}; +use hmac::{Hmac, Mac}; +use januskey::obliteration::obliterate_file; +use januskey::{ContentHash, ContentStore}; +use rand::RngCore; +use sha2::Sha256; +use std::fs; +use std::io::Write; +use std::path::Path; +use std::time::Duration; + +const SIZES: [usize; 4] = [4 << 10, 64 << 10, 1 << 20, 16 << 20]; +/// A plaintext key-table row: 32-byte content address and 32-byte blob key. +/// The table is sealed as one message, so its rows are not wrapped one by one. +const TABLE_ROW: usize = 32 + 32; +/// The random salt a journal entry carries to select its subkey (ADR §5). +const SALT: usize = 32; +/// A key-journal entry: one table row sealed on its own, since entries are +/// appended one at a time: salt, 12-byte nonce, the row, 16-byte tag. +const JOURNAL_ENTRY: usize = SALT + 12 + TABLE_ROW + 16; + +/// `size` random bytes: incompressible, the worst case for gzip. +fn random_payload(size: usize) -> Vec { + let mut data = vec![0u8; size]; + rand::rng().fill_bytes(&mut data); + data +} + +/// Make `data` differ from every earlier payload, so the store cannot dedupe. +fn make_unique(data: &mut [u8], n: &mut u64) { + *n += 1; + data[..8].copy_from_slice(&n.to_le_bytes()); +} + +/// Write `bytes` to `dir/name` the way the store does: temporary file, +/// fsync, rename, then fsync the directory. +fn write_synced(dir: &Path, name: &str, bytes: &[u8]) { + let tmp = dir.join(format!(".tmp-{name}")); + let mut f = fs::File::create(&tmp).unwrap(); + f.write_all(bytes).unwrap(); + f.sync_all().unwrap(); + fs::rename(&tmp, dir.join(name)).unwrap(); + fs::File::open(dir).unwrap().sync_all().unwrap(); +} + +/// Seal `data` under a fresh random key; returns (key, nonce || ciphertext). +fn seal(data: &[u8]) -> ([u8; 32], Vec) { + let mut key = [0u8; 32]; + let mut nonce = [0u8; 12]; + rand::rng().fill_bytes(&mut key); + rand::rng().fill_bytes(&mut nonce); + let cipher = Aes256Gcm::new_from_slice(&key).unwrap(); + let ct = cipher.encrypt(Nonce::from_slice(&nonce), data).unwrap(); + let mut out = Vec::with_capacity(12 + ct.len()); + out.extend_from_slice(&nonce); + out.extend_from_slice(&ct); + (key, out) +} + +/// Seal `data` under a given key; returns nonce || ciphertext. +fn seal_under(key: &[u8; 32], data: &[u8]) -> Vec { + let mut nonce = [0u8; 12]; + rand::rng().fill_bytes(&mut nonce); + let cipher = Aes256Gcm::new_from_slice(key).unwrap(); + let ct = cipher.encrypt(Nonce::from_slice(&nonce), data).unwrap(); + let mut out = Vec::with_capacity(12 + ct.len()); + out.extend_from_slice(&nonce); + out.extend_from_slice(&ct); + out +} + +/// The per-message subkey of ADR §5: HKDF-SHA-256 expand of the epoch key +/// with the message's random salt. One output block, so this is exactly +/// HMAC-SHA-256(epoch key, info || 0x01) with info = the salt. +fn subkey(epoch_key: &[u8; 32], salt: &[u8]) -> [u8; 32] { + let mut mac = as Mac>::new_from_slice(epoch_key).unwrap(); + mac.update(salt); + mac.update(&[1]); + mac.finalize().into_bytes().into() +} + +/// Open `nonce || ciphertext` sealed by [`seal`] under `key`. +fn open(key: &[u8; 32], sealed: &[u8]) -> Vec { + let cipher = Aes256Gcm::new_from_slice(key).unwrap(); + let (nonce, ct) = sealed.split_at(12); + cipher.decrypt(Nonce::from_slice(nonce), ct).unwrap() +} + +/// gzip at the store's level, as `ContentStore::write_blob` does. +fn gzip(data: &[u8]) -> Vec { + let mut enc = GzEncoder::new(Vec::new(), Compression::default()); + enc.write_all(data).unwrap(); + enc.finish().unwrap() +} + +/// Store cost per blob: today's `ContentStore::store`, with compression off and +/// on (the `jk` default), against the proposed gzip-then-seal path and the +/// cipher alone. +fn bench_store(c: &mut Criterion) { + let mut g = c.benchmark_group("crypto_shred/store"); + g.sample_size(10).measurement_time(Duration::from_secs(3)); + for size in SIZES { + g.throughput(Throughput::Bytes(size as u64)); + for (name, compression) in [("plaintext_raw", false), ("plaintext_default", true)] { + g.bench_with_input(BenchmarkId::new(name, size), &size, |b, &size| { + let dir = tempfile::tempdir().unwrap(); + let store = ContentStore::new(dir.path().to_path_buf(), compression).unwrap(); + let (mut data, mut n) = (random_payload(size), 0u64); + b.iter(|| { + make_unique(&mut data, &mut n); + black_box(store.store(&data).unwrap()); + }); + }); + } + g.bench_with_input( + BenchmarkId::new("sealed_default", size), + &size, + |b, &size| { + let dir = tempfile::tempdir().unwrap(); + let mut journal = fs::OpenOptions::new() + .create(true) + .append(true) + .open(dir.path().join("keys.journal")) + .unwrap(); + let (mut data, mut n) = (random_payload(size), 0u64); + b.iter(|| { + make_unique(&mut data, &mut n); + let hash = ContentHash::from_bytes(&data); + // Compress before sealing: ciphertext does not compress. + let (key, sealed) = seal(&gzip(&data)); + write_synced(dir.path(), hash.raw_hash(), &sealed); + // The key must be durable too. A store appends one entry + // to the key journal and syncs it; the sealed table is + // rewritten only by a shred, which rewrites it anyway. + // Wrapping the entry adds microseconds (E5). + let mut entry = [0u8; JOURNAL_ENTRY]; + entry[..32].copy_from_slice(&key); + journal.write_all(&entry).unwrap(); + journal.sync_all().unwrap(); + }); + }, + ); + g.bench_with_input(BenchmarkId::new("seal_only", size), &size, |b, &size| { + let (mut data, mut n) = (random_payload(size), 0u64); + b.iter(|| { + make_unique(&mut data, &mut n); + black_box(seal(&data)); + }); + }); + } + g.finish(); +} + +/// Erase cost: today's overwrite of a blob against the pending and final stages +/// of a crypto-shred, and the rejected one-file-per-key layout for contrast. +fn bench_erase(c: &mut Criterion) { + let mut g = c.benchmark_group("crypto_shred/erase"); + g.sample_size(10).measurement_time(Duration::from_secs(3)); + + // The current path: overwrite the blob itself, whatever its size. + for size in SIZES { + g.bench_with_input( + BenchmarkId::new("overwrite_blob", size), + &size, + |b, &size| { + let dir = tempfile::tempdir().unwrap(); + let data = random_payload(size); + b.iter_batched( + || { + let p = dir.path().join("blob"); + fs::write(&p, &data).unwrap(); + p + }, + |p| black_box(obliterate_file(&p).unwrap()), + BatchSize::PerIteration, + ); + }, + ); + } + + // Pending shred: append a tombstone for the blob to the key journal and + // sync it. The live epoch key still opens the old table. + g.bench_function("pending_journal_tombstone", |b| { + let dir = tempfile::tempdir().unwrap(); + let mut journal = fs::OpenOptions::new() + .create(true) + .append(true) + .open(dir.path().join("keys.journal")) + .unwrap(); + b.iter(|| { + journal.write_all(&random_payload(JOURNAL_ENTRY)).unwrap(); + journal.sync_all().unwrap(); + }); + }); + + // Final shred, one table: open (authenticate and decrypt) the sealed + // table, drop the entry, re-seal the rest under a fresh epoch key, one + // synced write. Not measured: folding in a non-empty journal (one more + // open per entry since the last shred) and destroying the old epoch + // secret, whose cost depends on where ADR §4 puts it. + for entries in [1_000usize, 10_000, 100_000] { + g.bench_with_input( + BenchmarkId::new("final_open_drop_reseal_table", entries), + &entries, + |b, &entries| { + let dir = tempfile::tempdir().unwrap(); + let (old_key, sealed_table) = seal(&random_payload(entries * TABLE_ROW)); + let mut victim = 0usize; + b.iter(|| { + victim = (victim + 1) % entries; + let table = open(&old_key, &sealed_table); + let mut next = Vec::with_capacity(table.len() - TABLE_ROW); + next.extend_from_slice(&table[..victim * TABLE_ROW]); + next.extend_from_slice(&table[(victim + 1) * TABLE_ROW..]); + let (epoch_key, sealed) = seal(&next); + write_synced(dir.path(), "keys", &sealed); + black_box(epoch_key); + }); + }, + ); + } + + // Folding the journal into the table during a final shred: open each entry + // stored since the last rotation (each under its own subkey) and start an + // empty journal, one synced write. Added to the table cost above. + for journal_len in [10usize, 100, 1_000, 10_000] { + g.bench_with_input( + BenchmarkId::new("fold_journal", journal_len), + &journal_len, + |b, &journal_len| { + let dir = tempfile::tempdir().unwrap(); + let mut epoch_key = [0u8; 32]; + rand::rng().fill_bytes(&mut epoch_key); + // Each entry is salt || nonce || ciphertext, sealed under the + // subkey its own salt selects (ADR §5), written to disk once. + let mut journal = Vec::with_capacity(journal_len * JOURNAL_ENTRY); + for _ in 0..journal_len { + let salt = random_payload(SALT); + journal.extend_from_slice(&salt); + let row = random_payload(TABLE_ROW); + journal.extend_from_slice(&seal_under(&subkey(&epoch_key, &salt), &row)); + } + let path = dir.path().join("keys.journal.full"); + fs::write(&path, &journal).unwrap(); + b.iter(|| { + // Timed: read the journal from disk, derive each subkey + // from the epoch key alone, open every entry, then start + // an empty journal. Merging the rows is in the table row. + let bytes = fs::read(&path).unwrap(); + let mut rows = Vec::with_capacity(journal_len * TABLE_ROW); + for entry in bytes.as_chunks::().0 { + let (salt, sealed) = entry.split_at(SALT); + rows.extend_from_slice(&open(&subkey(&epoch_key, salt), sealed)); + } + write_synced(dir.path(), "keys.journal", &[]); + black_box(rows.len()); + }); + }, + ); + } + + // Final shred, one file per key: rewrap every live key file under a fresh + // epoch key, one synced write each. + let entries = 1_000usize; + g.bench_with_input( + BenchmarkId::new("final_rewrap_files", entries), + &entries, + |b, &entries| { + let dir = tempfile::tempdir().unwrap(); + let names: Vec = (0..entries).map(|i| format!("{i:08}.key")).collect(); + b.iter(|| { + let mut epoch_key = [0u8; 32]; + rand::rng().fill_bytes(&mut epoch_key); + let cipher = Aes256Gcm::new_from_slice(&epoch_key).unwrap(); + for name in &names { + let mut nonce = [0u8; 12]; + rand::rng().fill_bytes(&mut nonce); + let blob_key = random_payload(32); + let wrapped = cipher + .encrypt(Nonce::from_slice(&nonce), blob_key.as_slice()) + .unwrap(); + write_synced(dir.path(), name, &wrapped); + } + black_box(epoch_key); + }); + }, + ); + g.finish(); +} + +criterion_group!(benches, bench_store, bench_erase); +criterion_main!(benches); diff --git a/crates/januskey-cli/Cargo.toml b/crates/januskey-cli/Cargo.toml index 3c98b8f..573416b 100644 --- a/crates/januskey-cli/Cargo.toml +++ b/crates/januskey-cli/Cargo.toml @@ -62,6 +62,11 @@ name = "januskey_benchmarks" harness = false path = "../../benches/januskey_benchmarks.rs" +[[bench]] +name = "crypto_shred" +harness = false +path = "../../benches/crypto_shred.rs" + [[bin]] name = "jk" path = "src/main.rs" diff --git a/docs/adr/0002-crypto-shredding.adoc b/docs/adr/0002-crypto-shredding.adoc new file mode 100644 index 0000000..97285b6 --- /dev/null +++ b/docs/adr/0002-crypto-shredding.adoc @@ -0,0 +1,240 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += ADR-0002 — Obliteration by crypto-shredding +:toc: left + +* *Status:* proposed. Not accepted, and nothing is built. The benchmark in `benches/crypto_shred.rs` is the only code. +* *Precondition for acceptance:* §2's key-table, journal and rotation protocol is a sketch refined through nine rounds of review, and §9 lists what is still open. Before acceptance it must be written as a state machine and checked mechanically for crash consistency at every step, either in TLA+ or in the Agda kernel beside T-1 to T-3. The checked properties are: every live (not tombstoned or shredded) blob has an openable key and every shredded blob has none, at least one openable generation, no reused subkey, and a final shred leaving no openable copy of the victim's key. Prose review cannot close this class of question; a model can. +* *Date:* 2026-11-04 +* *Related:* +** ADR-0001: `jk` is reversible file operations, not a key system. +** `PROOF-NEEDS.adoc` rows O-1 (OPEN), X-1 (ASSUMED) and E-1m (PROVEN). +** `docs/reports/audit/proof-statement-audit-2026-10-27.adoc` §5. + +== 1. Context + +`jk obliterate` today calls `secure_overwrite`: three passes over the file, an fsync after each pass, then an unlink. It records an `ObliterationProof` whose `storage_cleared` is hard-coded to `true` (row O-1). + +Two things are wrong with treating this as erasure. + +* *The overwrite does not reach the old bytes on the media that matter.* +** On an SSD, the flash translation layer writes each pass to fresh cells. +** On a copy-on-write file system (btrfs, ZFS, APFS) each pass is a new extent. +** A journal, a snapshot or a backup keeps its own copy. +** NIST SP 800-88 Rev. 1 warns that overwriting may not reach all of the storage on a flash device. DoD 5220.22-M, which the code cites, dropped its overwrite procedure in the 2006 revision. Row X-1 is therefore an assumption that is false on most current disks. +* *The content address survives the erasure.* A blob is addressed by SHA-256 of its plaintext. That address stays in `obliterations.json` and in the proof (`content_hash`). Anyone who can guess low-entropy content, such as a short password or a yes/no field, can confirm the guess after obliteration. + +== 2. Proposal + +*Crypto-shredding:* each blob is stored encrypted under its own random key, and erasing a blob means erasing its key. + +[arabic] +. *Sealing.* `store` seals the content with AES-256-GCM under a fresh 256-bit key from the OS CSPRNG and a 96-bit random nonce. The blob file is `version byte ‖ nonce ‖ ciphertext ‖ tag`. +** *Never* use a convergent key (key = H(content)). Such a key can be recomputed from the content, so it cannot be shredded. +. *Deduplication is unchanged.* The key belongs to the blob, not to a path. A blob shared by two paths keeps its key until the last path that needs it is obliterated, which is the rule `obliterate_path` already applies to blobs. +. *Key storage.* Keep all blob keys in *one key table* (`.januskey/keys`), sealed as a whole under the current *epoch key*, plus an append-only *key journal*. See §4 for where the epoch key comes from. +** A `store` appends one entry, sealed under the current epoch key, to the journal and syncs it. That costs the same at any number of keys; rewriting the whole table on every store would not. +** *Key before blob.* The journal entry is synced *before* the sealed blob is renamed into place. +*** A crash in between leaves a key with no blob. That is harmless, and the next fold drops it. +*** It never leaves a blob with no key. That case would be permanent loss, because deduplication would accept the existing blob on a retry. +*** Deduplication accepts an existing blob only if it *authenticates* (the AEAD open succeeds) under the key the table or journal maps to its address. Otherwise the blob is rewritten. A key merely being present is not enough: a repair can crash after syncing a new key but before replacing the old ciphertext, and that key would not open the old blob. +** A shred folds the journal into the table as part of the rewrite it does anyway. +** Journal entries are sealed under the same epoch key as the table, so the rotation below covers retained copies of the journal too. +** An earlier draft proposed one key file per blob, because dropping a single file is cheap. But making a shred final requires every live key to be re-sealed under a fresh epoch key. With per-blob files that is one synced write per live key: 1.2 s for only 1 000 keys (§3). The table makes a final shred one synced write. +. *Shred.* `obliterate` and `gc` drop the blob's entry, fold in the journal, and write the table again under a *fresh* epoch key, starting an empty journal. Then they destroy the old epoch key, then delete the blob. +** Destroying the old epoch key is what makes the shred final. A snapshot, a backup or a copy-on-write extent can keep an old copy of the table, but that copy is sealed under an epoch key that no longer exists. +** If the old epoch key is not destroyed, for example because the new table is written but the old key survives, the shred is only *pending*. Every retained copy of the old table, and so of the blob's key, can still be opened. +** The cost of a final shred is O(live keys + journal entries since the last rotation). +*** Opening, dropping and re-sealing the table took about 1 ms at 1 000 keys and 26 ms at 100 000. +*** Folding the journal adds 0.7 ms at 100 entries and 19 ms at 10 000 (§3). Each entry needs its own subkey derivation and AES key schedule. +** *Stores and rotations are serialised.* Suppose a `jk` process appended to the journal under generation _n_ after a concurrent shred had folded that journal but before it removed secret _n_. That blob's key would be in no table and sealed under a destroyed secret, and its undo content would be lost permanently. +*** So every journal append and every whole rotation runs under one exclusive store lock (`.januskey/keys.lock`, an OS file lock). +*** Readers take the same lock *shared*, for the whole of a `retrieve` or `undo` that uses a key. Without it, a process could open generation _n_, keep the victim's key or plaintext, and finish an undo after the shred reported the content gone. That would recreate obliterated data. A final shred waits for readers to finish. +*** As a second guard, each journal entry carries the generation it was sealed under. A store that finds `current` changed while it waited for the lock re-seals under the new generation. +*** This is stricter than the rest of `jk` today: concurrent writers are out of scope for the transaction log (T-5). It is required here because the failure is permanent key loss, not a lost update. +** *Rotation is crash-safe only with generations.* The keyring and the file system cannot be updated in one atomic step, so tables and epoch secrets are numbered by generation. +*** A shred moving from generation _n_ to _n+1_: +**** stores the new epoch secret in the keyring under _n+1_, keeping _n_; +**** writes `keys.`, with an empty journal for _n+1_, syncs both files, then syncs the directory so their entries are durable; +**** writes a small `current` pointer naming _n+1_ by temporary file, fsync and rename, then fsyncs the directory, so the switch is durable *before* the next step; +**** removes secret _n_ from the keyring; +**** deletes `keys.`, its journal, and the blob. +*** On open, a store whose keyring holds both _n_ and _n+1_ is mid-rotation: +**** recovery chooses the generation that actually opens, not merely the one `current` names: it tries `current`'s generation first, then the other; +**** it finishes or undoes the rotation from there, and never discards the only generation whose secret is still present. +*** A crash at any point leaves *at least one* openable generation. Between steps 2 and 4 both are openable by design. Recovery then selects deterministically: the generation `current` names if it opens, else the other. It then finishes or rolls back the rotation, so after recovery exactly one remains. +*** The shred is final only once secret _n_ has left the keyring. +** Shreds could instead be batched, so that one rotation finalises many. A batched shred appends a *tombstone* for the blob to the key journal and syncs it (0.2 ms, §3); the blob is unusable through `jk` at once, but the old table and journal, and so the key, stay openable under the live epoch key until the next rotation. The ADR's default is a final shred every time; batching, and how long a shred may stay pending, are decisions for acceptance. +. *Scope: content-store copies only.* The guarantee covers what JanusKey writes: blobs and keys. It does not cover the working file itself, which `jk obliterate` targets too. +** That file existed in plaintext on the same medium before JanusKey ever saw it, so CoW extents, flash remapping, snapshots or backups may still hold its plaintext. +** Covering it needs encryption from the file's creation, meaning an encrypted volume underneath, which is outside JanusKey. +** The record says which copies the shred covers, and the docs say the working file is overwritten best-effort only. +. *Addresses.* Use HMAC-SHA-256 under a per-store *index key* instead of a bare SHA-256, so that an address alone does not confirm a guessed plaintext. +** That only holds if the attacker who reads the store cannot also read the index key. The index key is therefore part of the protected hierarchy and never sits beside the store in plaintext. +** It is derived from the root of §4 with HKDF-SHA-256 under its own label. It is never written down, and is recomputed when the store is opened. +** It is stable for the store's lifetime, because rotating it would re-address every blob. So it is not rotated per shred. +** Destroying the root destroys it too, which is a whole-store erasure. +** The protection is exactly as strong as the root. An attacker who holds the store *and* the passphrase (or the hardware root) can still confirm guesses. +. *Proof object.* `ObliterationProof` loses `storage_cleared` and `overwrite_passes`. It records the key id that was destroyed, and is honestly named a *record*, not a proof. + +== 3. Measured cost (E1, done) + +`cargo bench -p januskey --bench crypto_shred` measured these figures on 2026-11-04, after eight rounds of review corrections. + +* *Conditions:* 4 vCPU, a container's virtual disk, one run, and medians, with Criterion's 95% intervals in the raw output. +* *Payloads:* random, so incompressible. That is the worst case for gzip: it costs time and saves nothing. Compressible content would make every gzip row faster, and the sealed row with it, since that row compresses before sealing. +* *Limits:* these figures are evidence about *shape*, not about real disks. fsync on a virtual disk is not fsync on an SSD. + +[cols="2,1,1,1,1",options="header"] +|=== +|Store (per blob) |4 KiB |64 KiB |1 MiB |16 MiB +|`ContentStore::store`, compression off |0.92 ms |2.10 ms |6.05 ms |40.1 ms +|`ContentStore::store`, compression on (the `jk` default, today) |1.34 ms |3.98 ms |36.3 ms |525 ms +|proposed: gzip, then seal, then a synced blob write and one synced append to the key journal (entry unwrapped) |1.63 ms |3.66 ms |39.1 ms |588 ms +|seal only, no I/O |3.7 µs |55 µs |1.65 ms |38.6 ms +|=== + +The default-store and proposed rows come from one paired re-run, made after the layout moved to the key journal. An earlier run of the default store measured 1.70 / 4.40 / 35.7 / 545 ms. The spread at 4 and 64 KiB between those runs is as large as the difference between the two rows, so read small-blob differences as noise. + +[cols="2,1",options="header"] +|=== +|Erase |Time +|today: `obliterate_file` on the blob, 4 KiB / 64 KiB / 1 MiB / 16 MiB |0.71 / 0.98 / 6.76 / 124 ms +|*pending* shred (batched): append a tombstone to the key journal and sync it |0.20 ms +|*final* shred, one table: open (authenticate and decrypt) the sealed table, drop the entry, re-seal it under a fresh epoch key, one synced write; 64-byte rows; 1 000 / 10 000 / 100 000 live keys |0.96 / 2.91 / 26.2 ms +|*final* shred, add for the journal (reading and clearing only; merging the rows into the table is part of the table row above, which re-seals the whole table anyway): read the journal from disk, derive each entry's subkey from the epoch key and its salt, open it, and start an empty journal, one synced write; 10 / 100 / 1 000 / 10 000 entries |0.48 / 0.74 / 2.43 / 19.1 ms +|*final* shred, one file per key: rewrap every key file under a fresh epoch key, 1 000 live keys |1 210 ms +|=== + +Not in any row: + +* *Destroying the old epoch secret.* Its cost depends on where it lives (§4). +* *The generation protocol's extra writes:* one keyring write and one pointer rename (§2). +* *Reading the sealed table from disk.* The table row opens a table already in memory, so the file read (up to about 6.4 MiB at 100 000 keys) is excluded. + +Adding the table row and the journal row also overcounts by one directory fsync: each row does its own, while §2's protocol syncs the directory once for both files. The sum is therefore an upper bound on that part, and a lower bound overall because of the exclusions above. + +The journal row is never zero in practice, even when every shred is final: any store since the last rotation leaves an entry, including the victim's own. An earlier version of this section claimed it was zero. An earlier journal row (0.42 / 0.45 / 0.77 / 3.44 ms) used keys derived before timing began; the current row reads the journal from disk and derives every subkey inside the measurement. + +What the numbers say: + +* *Sealing is cheap next to today's default.* Against the store `jk` actually runs (gzip on), the proposed path is within run-to-run noise at 4 and 64 KiB, and adds about 8% at 1 MiB and 12% at 16 MiB. The cost is in compression and fsync count, not in the cipher. +** Two earlier versions of this section were wrong. +** One said sealing doubles large-blob store time. That compared against the store with compression off, which is not the default. +** The other gave 1.7× at 4 KiB. That measured a separate key *file* per blob, with its own temp file, rename and directory fsync, which the chosen layout does not do. +* *Compression is the large-blob cost today.* gzip on incompressible input is the slowest step by an order of magnitude: 545 against 40 ms at 16 MiB. +** That observation is independent of this ADR. +** Skipping compression when it does not pay, or a faster codec, would help either design. +* *A final shred costs O(live keys), not O(blob size).* With one sealed table it is one synced write. The *measured portion* (opening, dropping and re-sealing the table: 26 ms at 100 000 keys) is below today's 124 ms overwrite of a 16 MiB blob and above the 6.8 ms overwrite of a 1 MiB blob. The complete shred adds the table read, a non-empty journal, the keyring writes and the pointer rename, and the keyring cost depends on §4's backend. So these figures do not establish that a complete shred beats overwriting at any size; E5 measures that. +* *Unlike overwriting, the claim holds on any medium*, subject to §4. +* *Key layout.* One file per key makes final shreds unworkable (1.2 s at 1 000 keys). It is why §2 chose the single table. +** The pending-shred row is only the first step of a batched shred, not an erasure. +** An earlier version measured a pending shred as deleting a per-blob key file (0.72 ms). That operation belongs to the rejected layout. +** An earlier version also compared that figure with today's overwrite (a "166×" saving). That comparison was wrong, and it is withdrawn. +** Earlier final-shred figures (1.17 / 3.91 / 33.8 ms) re-sealed rows sized as if each key were wrapped on its own (92 bytes). They also skipped opening the old table. The current row times the whole open, drop and re-seal on 64-byte rows. + +== 4. Where the recursion ends (the honest limit) + +Crypto-shredding does not remove the physical-erasure assumption. It *shrinks* it: from "every copy of every blob, of any size, on any medium" to "one small secret held where erasure is real". + +An old copy of the key table can itself survive on flash. That is why the table is sealed under an epoch key, why each shred rotates that key, and why the root of the epoch keys must live somewhere else. + +[cols="3,1,1,4",options="header"] +|=== +|Root of the key hierarchy |Elegance |Dependability |Aspects +|Passphrase plus a keyring-held epoch secret (see the hierarchy below) |★★ |★★ |Usable everywhere. Privacy is only as good as the passphrase. A shred becomes final when the epoch secret is replaced and the old one is gone from the keyring. +|OS keyring or TPM / Secure Enclave sealed key |★★★ |★★★ |Hardware erase semantics. Platform-specific, so a Rust/SPARK seam and an Idris2 ABI per platform. This is the estate's FFI pattern. +|No root at rest: the key is supplied per session, for example by a hardware token |★★★ |★★ |The strongest privacy. Undo needs the token present, which changes how `jk` is used, and ADR-0001 says that is not the product. +|=== + +Recommended for a first build: the passphrase plus epoch rotation, with the TPM/keyring root as a later, separate seam. + +*The hierarchy has two roots, because the index key must stay stable while epoch keys must change.* + +* *Store root.* Argon2id over the passphrase, with a salt fixed when the store is created and stored beside it. +** It never changes. +** It is never written down. +* *Index key.* HKDF-SHA-256 over the store root, under the label `"index"` (§2). +** It is stable for the store's lifetime, so rotation never re-addresses blobs. +* *Epoch secret.* 256 random bits, held in the OS keyring (or TPM), never on the store's medium. +** Every final shred replaces it. +** It is not derivable from the passphrase, so a retained copy of the store together with the passphrase does not recover it. +* *Epoch key.* HKDF-SHA-256 over the store root, salted with the epoch secret, under the label `"epoch"`. +** Opening the table needs both the passphrase and the current epoch secret. +** Removing the old epoch secret from the keyring finalises every shred made under it. +* *Erasure scope.* "Erasing the epoch secret is real erasure" is now an assumption about the keyring's storage, not about the store's medium. On platforms whose keyring persists to the same flash, the honest claim is no stronger than that keyring's own deletion. E2 must check this per platform. + +== 5. Statements this makes provable + +* *O-1, restated:* "after `shred(h)` and the epoch rotation that follows it, no reachable state, retained copies of the key table included, holds an openable key for `h`; and every stored copy of `h` is a sealed blob under a key with that id". The working file is outside this statement (§2). +** This is a finite-map model in the Agda kernel. +** It has the same shape as `obliterate-cuts-recovery` (E-1m): recovery needs the key, and the key is not in any reachable state. +** It is provable, and then TESTED against the Rust through a conformance test. +* *X-1 becomes three assumptions:* +** *AEAD security.* AES-256-GCM is IND-CPA and INT-CTXT for *one message per key*. +*** Blob keys meet that by construction. +*** The epoch key would not, because the table and every journal entry under one epoch are separate messages. +*** So each of them is sealed under its own subkey: HKDF-SHA-256 over the epoch key with a random 256-bit salt that the message carries in its header. +*** Every AEAD key therefore still encrypts exactly one message, and random-nonce collisions and per-key GCM usage limits stop being part of the assumption. +*** A salt rather than a sequence number, because a sequence can be reused. Recovery that drops a torn final journal entry would hand its number to the next append, while a snapshot or CoW extent may still hold the torn entry's ciphertext. Two messages would then share one subkey. A fresh random salt is reused only with negligible probability (2^-128 by the birthday bound at 2^64 messages), and needs no durable counter. +** *Erasure.* Erasing the epoch secret where §4 keeps it is real erasure. +** *Key derivation.* HKDF-SHA-256 is a PRF and Argon2id resists offline guessing at the chosen cost. +* *C-3 is unchanged:* obliteration stays by design irreversible, and `undo` after a shred has nothing to restore, as today. + +== 6. Consequences + +* *Identity (ADR-0001).* Encryption is a *storage* detail here, as SHA-256 addressing already is. `jk` gains no key lifecycle, rotation UI or key export. The `jk-keys` lifecycle manager stays out of the product. The only shared code is the AEAD and KDF crates already in the dependency graph, so no new dependency is needed. +* *Format and migration.* Blobs gain a version byte. A store with plaintext blobs is read as today, and new writes are sealed. Old plaintext blobs need an explicit `jk migrate` that seals and shreds them. Until that runs, the old plaintext is exactly as exposed as it is now, and the docs must say so. +** *Addresses are part of the history.* The operation log serialises each blob's `ContentHash`, and `undo` passes that exact value to `ContentStore::retrieve`. Moving blobs to HMAC addresses would leave every historical operation pointing at a blob that no longer exists. +** `ContentHash` therefore becomes versioned (`sha256:` or `hmac-sha256:`), and `retrieve` resolves either form. +** Migration proceeds in three steps: seal each blob at its new address; rewrite every reference in the operation log in one atomic save (the log already saves by write, sync and rename, row T-8); only then shred the SHA-addressed copies. +** A crash between the steps leaves both copies, never neither. That cuts both ways. +*** The old SHA-addressed blobs are plaintext with predictable names. Migration records itself as incomplete, in a marker it writes first and removes last. Every `jk` invocation resumes cleanup until no reachable old file remains. +*** Even then, cleanup removes only the *reachable* files. Plaintext the store wrote before migration may still exist in copy-on-write extents, on remapped flash, in snapshots and in backups. That is §1's own premise, and no epoch key covers those copies. +*** So a migrated store is never reported as unexposed. `jk status` reports "plaintext from before migration may persist on the medium, its snapshots and backups", permanently, for any store that ever held plaintext blobs. +*** Removing that exposure needs the medium, its snapshots and its backups to be sanitised outside JanusKey. +*** For data whose exposure matters, the ADR recommends starting a fresh sealed store over migrating an old one. +** *Obliteration records hold addresses too.* Each `ObliterationRecord` and its nested proof in `obliterations.json` carry the old SHA-256 `ContentHash`, together with the nonce and commitment derived from it. For a blob already obliterated there is no plaintext left from which to compute an HMAC address. +*** Rewriting those records is impossible, so migration must either *redact* or *retain*. +*** *Redact:* keep the record's id, time, reason and legal basis, and remove the hash, nonce and commitment. The record can then no longer answer "was this content obliterated?". +*** *Retain:* keep the hash, with the dictionary exposure stated in the docs. +*** Proposed default: redact, because the record exists to say *that* something was erased, not *what*. This is a decision for acceptance, because some legal-basis uses may need the "what". +*** New records written after migration carry only the key id and the HMAC address. +* *Reversibility.* Every `undo` now needs the store key. A lost passphrase loses history. That is a new failure mode, and it needs a recovery story (an escrow file, or an accepted loss) before acceptance. +* *Wording.* The DoD 5220.22-M and "cryptographic proof of erasure" claims are removed from the code, docs and ledger. + +== 7. Experiments before building (proposed) + +* *E2: real media.* Repeat E1 on ext4 over an NVMe SSD and on btrfs. Report the fsync share of store time. +* *E3: cipher choice.* Compare ChaCha20-Poly1305 with AES-256-GCM on a CPU without AES-NI. Check that the 16 MiB seal is limited by allocation, not by the cipher, by sealing in place (`encrypt_in_place`). +* *E4: forensic acceptance test.* This is the decisive one. Build a btrfs file system on a loop device, run the steps below, then scan the raw image for a marker payload. +** *Compression is off in both arms.* `jk` compresses by default, and a gzip stream would hide a literal marker from the scan even with no erasure at all. That false negative would make the sealed path look as if it passed. +** *A positive control is required.* Before any shred or obliterate, the scan must find the marker in today's store. If it does not, the run is invalid, not a pass. +** There are two cases. +** *Store-only.* Store the marker straight into the content store, then shred it and rotate the epoch. +*** Expected for today's overwrite: the marker is found, because the CoW extents survive. +*** Expected with sealing: the marker is never found, because the store never writes plaintext. +*** It becomes a TESTED row if it holds. +** *Product flow.* Create a working file containing the marker, record it with `jk`, then `jk obliterate` it. +*** Expected in both designs: the marker *is* found, from the working file's own extents. +*** This case is kept as a test of the scope limit in §2, so that no one later reads the store-only result as covering the working file. +* *E5: the full final shred.* Time the generation protocol of §2 end to end, including the keyring writes for §4's chosen root and the pointer rename. Confirm the cost stays independent of blob size and linear in live keys plus journal entries. +** Inject a crash after each of the protocol's steps. Check that every crash point leaves at least one openable generation, that recovery selects the committed one and ends with exactly one, and that no step leaves the shred reported final while secret _n_ is still in the keyring. +* *E6: compression.* Repeat the store rows with compressible payloads (text, source code). Then measure skipping gzip when it does not shrink the input. This is a candidate fix to today's store whatever happens to this ADR. + +== 8. Beyond this repository + +* The same erasure-on-flash problem applies to any estate repository that promises deletion: consent and retention tooling, and obliteration in other stores. If this ADR is accepted, the root-key seam (§4) is a candidate for a shared crate rather than a januskey-only module. +* `docs/security/THREAT_MODEL.adoc` covers only the key store. It needs a section on the obliteration path whichever way this ADR is decided. + +== 9. Open questions before acceptance + +These were raised in review and are *not* resolved by this proposal. Each belongs to the formal model required above, or to E5, rather than to further prose. + +* *Duplicate keys after a key-first crash.* A store can sync its journal entry and then crash before publishing the blob. A retry can then append a second key for the same address and publish under it. A fold must not keep the older key just because it exists. Either a retry reuses the pending key, or the fold keeps only the mapping that authenticates the published blob. +* *Hashes with no stored plaintext.* `Modify` and `Create` record a `new_content_hash` whose content is never stored, and the working file may since have changed or gone. Migration cannot compute an HMAC address for such references. Like legacy obliteration records (§6), they must be redacted or retained with the exposure stated. +* *Keys in process memory.* A rotation loads the old epoch secret, derives the epoch key and decrypts a table holding the victim's key. Under the threat model's memory-disclosure vector (AV-2: core dumps, swap, cold boot), dropping the old secret from the keyring is not enough. The secret, the derived keys, the decrypted table and the removed row must be held in locked memory and zeroized before the shred is reported final. +* *Benchmark completeness.* The exclusions listed in §3 (table I/O, the shared directory fsync, the keyring and pointer writes) are measured together in E5, as one end-to-end final shred. +* *Retrying a store after a key-first crash.* If the first attempt staged ciphertext before crashing, re-sealing under the same pending key would make that key protect two messages (a retained temporary file or CoW extent may keep the first). So a retry either publishes the exact authenticated staged ciphertext, or creates a new key and lets the fold discard the stale mapping. It never re-seals under a pending key. +* *Durable migration marker.* The marker must be written by temporary file, fsync, rename and directory fsync *before* any migration mutation, as the generation pointer is. Otherwise a power loss can lose it after the log has been rewritten, and nothing then resumes the cleanup. +* *Benchmark baselines.* Two comparisons in §3 are not like for like. The sealed-store arm writes every blob into one directory, while `ContentStore::store` uses its two-level hash-prefix layout. Today's erase baseline times `obliterate_file`, which also reads and hashes the whole file before overwriting it, whereas the content-store path (`ObliterationManager::obliterate`) already holds the hash. The first can distort small-blob overhead and its scaling; the second inflates today's overwrite figures. E2 and E5 use the product layout and the manager path. diff --git a/docs/reports/audit/proof-statement-audit-2026-10-27.adoc b/docs/reports/audit/proof-statement-audit-2026-10-27.adoc new file mode 100644 index 0000000..e3e72dc --- /dev/null +++ b/docs/reports/audit/proof-statement-audit-2026-10-27.adoc @@ -0,0 +1,266 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += JanusKey proof-statement audit (2026-10-27) +:toc: left + +[IMPORTANT] +.Status on 2026-11-04 — read this first +==== +This report records the audit as it was run on `main` at 10f0bc2. Since then: + +* *Fixed*: P4 and P5 (content store). A damaged blob is now repaired, writes go by temporary file and rename (by construction; no test injects a mid-write failure), and a malformed hash cannot leave the store root (#163). These are now ledger rows S-1 and S-2. +* *Fixed*: transaction-log persistence and resumable rollback (T-4 and T-5, #162 and #164). +* *Still open*: +** P1 to P3 (attestation log): uncovered fields, the last entry, and tail truncation. These are now ledger rows L-1 and L-2. +** P6 (`ObliterationProof` proves nothing about erasure). This is now ledger row O-1. + +The obligation statements in `PROOF-NEEDS.adoc` are the authority. Where this report and the ledger differ, the ledger wins. +==== + +Audited: januskey `main` at 10f0bc2, 2026-10-27. Purpose: before anyone proves anything, decide +which of the open obligations in `PROOF-NEEDS.adoc` are provable as written, which need a code +change first, and which are assumptions. No proofs were written. + +== How to read this + +* *Read*: `content_store.rs`, `obliteration.rs` (struct, `obliterate`, `obliterate_path`, +`secure_overwrite`), `transaction.rs`, `attestation.rs` (entry, hash, MAC, log, verify), +`keys.rs` (init/unlock/retrieve/rotate/revoke/KDF/wrap), `Types.idr` (`Knows`), +`PROOF-NEEDS.adoc`. +* *Not read*: the filesystem rollback executor (in `januskey-cli`), `metadata.rs`, +`operations.rs`, `keys.rs` `load_store`/`verify_kek`/`unwrap_key` bodies, `Proofs.idr` and +`Layout.idr` beyond the ledger, the Agda module beyond its header. +* *Run*: seven probe tests (a throwaway test file, not committed), on a +scratch copy of the repo, against the unmodified code. Each asserts what the code _does_, so a +passing probe is evidence the property is _false_. A control probe (an edit to a covered field is +detected) passes, so the harness itself is sound. P1 initially failed because my test edited a +protected field as well; I fixed the test and say so here. +* *Not run*: the Idris and Agda checkers. I rely on CI having passed on the #159 commits. +* Everything marked _unverified_ below is a hypothesis, not a finding. + +== Verdicts at a glance + +[cols=",,,",options="header",] +|=== +|# |Obligation (PROOF-NEEDS "What Needs Proving") |Verdict on the claim as written |Prove after +|1 |Content store integrity |Read-side is sound; *write side is not crash-safe* (P4) and a hash string can *steer paths outside the store* (P5) |code fix +|2 |Transaction atomicity |State machine already proven; *log persistence is not atomic*; rollback needs a failure model |code fix + model +|3 |Attestation chain "unforgeable" |*False as written*: three gaps confirmed by test (P1, P2, P3) |restate + code fix +|4 |Key derivation |Mostly not a proof job: parameters = compile-time assertion, nonces = bound, primitives = ASSUMED |restate +|5 |Obliteration |Logical (CAS) part provable as a model theorem; *"proof" object proves nothing* (P6); *key obliteration is not implemented*; physical erasure unprovable |restate + design +|6 |reversible-core undo/redo |Provable abstractly (nearly done: C-1 + per-op cancellation); the link to the Rust is the real work |model + conformance +|E-1 |Adversary cannot recover / revoked key unusable |*Vacuous as modelled*; revocation is an API guard, not a cryptographic one |delete or replace +|— |"Every operation is reversible (MPR)" |*Contradicts proven C-3* (obliteration is by design not reversible) |restate +|=== + +== Findings from the probes (evidence) + +[cols=",,",options="header",] +|=== +|Probe |Result |Meaning +|P0 control |actor edit detected |harness is valid +|P1 |editing `rotated_from` and `new_state` of a middle audit entry: `verify_integrity` still *valid* |those fields are in neither the MAC nor the chain hash +|P2 |editing `reason` of the *last* entry: still valid |the last entry's chain-hashed fields have no successor to protect them +|P3 |deleting trailing entries: still valid |verification accepts any prefix; no external anchor or count +|P4 |truncate a stored blob, call `store` again, `retrieve` -> integrity error |dedupe (`path.exists()`) never repairs a crash-truncated blob +|P5 |`ContentHash("sha256:ab" + absolute path)`: `content_path` is outside the root and `delete` removed my temp file |path is built by `Path::join`, and an absolute right-hand side replaces the root +|P6 |`ObliterationProof::generate` on content never stored: `verify_commitment` true, `storage_cleared` true |the proof is a public hash plus a hard-coded flag +|=== + +Reachability caveat for P5: it shows the _store API_ accepts such a hash. I have not shown that +attacker-controlled metadata can reach `delete`/`obliterate`. `ContentHash` derives `Deserialize` with a +public field and no validation, so that is where to look. Treat it as a security issue and fix it before +publishing details (the repository is public). + +[[1-content-store-integrity]] +== 1. Content store integrity + +*As written:* "Content-addressed storage never returns wrong content." + +* *Provable statement (R):* `retrieve(h) = Ok(x)` implies `H(x) = h`. This follows directly from the +guard in `retrieve`. It is true, cheap, and low value on its own. Combined with collision resistance +(X-1) it gives "x equals any content that was stored under h". +* *Round trip (W):* `store(c) = h` then `retrieve(h) = Ok(c)`. TESTED by the property test, *false under +a crash* (P4): a truncated file at the final path makes every later `store` of that content a no-op +and every `retrieve` fail. +* *Path confinement (C):* for every `h`, `content_path(h)` is inside `root`. *False* (P5). + +Do: fix C (validate `ContentHash` on construction/deserialization: `sha256:` plus 64 hex) and W (write to a +temp file, fsync, rename). Then prove R and C as lemmas about the validated type. Statements to avoid: +anything that restates the `verify` call. + +Difficulty: low. Kani or Verus can prove R and C +on the real function; unproven here (spike first). + +[[2-transaction-atomicity]] +== 2. Transaction atomicity + +*As written:* "Delta application is atomic and reversible." + +Split it: + +* *T1, lifecycle* (Pending -> Active -> Committed | RolledBack): PROVEN in `Proofs.idr`. Note the Rust +enum has three states (no `Pending`), so the Idris model and the Rust type already differ by one +state. The correspondence is assumed (same status as G-2). +* *T2, rollback restores state:* abstractly, undoing o1..on in reverse on state s gives s, given the +per-operation premise `undo o ∘ o = id`. That is C-1 (`seqCNO`) plus the TESTED premise +`execute_then_undo_is_identity`. Provable now; mostly done. What is missing is *partial failure*: what +if undo of o_k fails mid-way? The statement needs an error model (is undo idempotent and resumable?). +I did not read the executor, so I cannot say. +* *T3, crash atomicity of the log:* `TransactionManager::save` is `fs::write` (truncate, then write; no +temp file, no fsync, no rename). A crash mid-save leaves a truncated `transactions.json`, and +`TransactionManager::new` then fails with `MetadataCorrupted`. So "atomic" is *false for the +persistence layer*. After switching to temp + fsync + rename it is provable under a stated crash +model (POSIX rename atomicity is an assumption). + +Difficulty: T2 low-moderate; the crash model is the hard design choice (what does a crash do to a +directory and to file contents?). + +[[3-attestation-chain-unforgeable]] +== 3. Attestation chain "unforgeable" + +What the code actually does: each entry carries `attestation = HMAC-SHA256(k, scheme || 0 || event_id: timestamp:event_type:actor || 0 || previous_hash)`, and `previous_hash` is SHA-256 over a _different, +larger_ field set (adds `key_id`, `fingerprint`, `reason`). `k = SHA-256(KEK || "attestation")`, KEK from +Argon2id. + +Coverage, confirmed by probes: + +[cols=",,,",options="header",] +|=== +|Field |In MAC |In chain hash |Net +|event_id, timestamp, event_type, actor |yes |yes |protected +|key_id, fingerprint, reason |no |yes |protected except on the *last* entry (P2) +|algorithm, purpose, old_state, new_state, rotated_to, rotated_from |*no* |*no* |*unprotected* (P1) +|entries after the last kept one |n/a |n/a |*deletable* (P3) +|=== + +So "unforgeable" is false as written. Better statement, once fixed: + +____ +*A-1.* For an adversary without `k`: if `verify_integrity(L') = valid` then `L'` is a prefix of an +honestly produced log, or the adversary has forged an HMAC-SHA256 tag or found a SHA-256 collision. +____ + +Needed code changes first: MAC (or hash) over a canonical encoding of _every_ field; an anchor against +truncation (signed counter or head hash stored elsewhere, or an external witness). Also name the +adversary: the passphrase holder can always rewrite the log, since the MAC key is derived from the KEK +they hold. And `read_all` silently skips unparseable lines (a corrupted or injected line becomes a +deletion); decide whether that should fail. + +How to prove it, with ratings (first elegance/correctness, then dependability/security): + +[cols=",,,",options="header",] +|=== +|Option |Elegance |Dependability |Note +|Symbolic model in Agda (HMAC as an unforgeable function) |★★ |★★ |Cheap, but it assumes the conclusion for the crypto part. Same weakness as E-1. +|Game-based reduction on paper + conformance tests, mark HMAC security ASSUMED |★★★ |★★★ |Honest and sufficient for this repo. Recommended. +|Mechanised computational proof (EasyCrypt, CryptoVerif) |★★★ |★★★ |Correct but research-grade effort for a small gain. Different path, unexplored here. +|Replace the home-made chain with an existing transparency-log or signed-log design |★★ |★★★ |Removes the bespoke construction; real design change. +|=== + +Difficulty: statement and fix moderate; mechanised crypto proof very hard. + + +[[4-key-derivation]] +== 4. Key derivation + +"Sound keys" splits three ways, and only one part is a proof: + +* *Parameters* (Argon2id 64 MiB, t=3, p=4, 16-byte salt): a theorem about literals is exactly what the +ledger removed (`defaultMeetsOWASP`). Do it as a compile-time assertion +(`const _: () = assert!(...)`) in Rust. Status: TESTED (compile-time). +* *Nonce uniqueness* for AES-GCM key wrapping: nonces are random 96-bit per wrap. Statement: +after q wraps under one KEK, `P[collision] <= q(q-1)/2^97`. A birthday-bound lemma; paper-grade, and +NIST SP 800-38D caps random-nonce use near 2^32 invocations per key. Provable, practically irrelevant +at this scale; write it down as ASSUMED-with-bound unless you want a probability library in Agda. +* *Primitive security* (Argon2, AES-GCM, HMAC): ASSUMED (X-1 family). + +Smaller findings (unverified consequences): `attestation_key` is a plain `[u8;32]` in `AuditLog`, not +`Zeroize`d; the attestation key is `SHA-256(KEK || "attestation")` rather than HKDF (acceptable for a +uniform 32-byte KEK but non-standard). + +Not read: `load_store`, `verify_kek`, `unwrap_key`, and what the store-header `nonce` is used for. + +Difficulty: low. + +[[5-obliteration]] +== 5. Obliteration + +Three different claims are bundled: + +* *O-1, logical (CAS) completeness:* after `obliterate_path(p)`, no blob reachable only via `p` remains, +no log entry mentions `p`, shared blobs survive. TESTED today by three Rust tests. Provable as a model +theorem over (store map, log, reference sets): a partition argument, moderate. Ordering is sound +(shred, then purge) but not crash-atomic; a crash between them leaves entries that point to missing +blobs. Unverified hypothesis worth a test: if the store's compression flag differs from when a blob was +written, `content_path` misses the blob, `exists` is false, the shred is skipped silently, and the log +purge proceeds. +* *O-2, "proof of obliteration":* `ObliterationProof` is `SHA-256(content_hash || nonce || timestamp)` +plus a hard-coded `storage_cleared: true`. Anyone can produce one for any hash without erasing anything +(P6). The statement "a verifying proof implies the content was obliterated" is *false*. This is a +naming and documentation problem first (the module header says "formal obliteration proofs"). +* *O-3, physical erasure:* the code already says overwrite-in-place does not guarantee erasure on +CoW/journaling filesystems or flash. ASSUMED (X-1). Not provable. +* *Key obliteration:* `KeyState::Obliterated` is defined and read but *never assigned* anywhere in +`crates/`. The module comment itself recommends encrypt-then-shred. So the design that would make O-3 +tractable is not built. + +Options for the strong guarantee: + +[cols=",,,",options="header",] +|=== +|Option |Elegance |Dependability |Note +|Keep overwrite, relabel as best-effort, drop "proof" wording |★★ |★★ |Cheapest; honest. Does the least for users. +|Crypto-shredding: per-blob key, erasing the key is the erasure |★★★ |★★★ |Reduces the claim to AES-GCM secrecy + key erasure; key bytes still face the SSD problem, but 32 bytes can live in an OS keyring or memory only. Real design work. +|Two-tier: crypto-shred plus best-effort overwrite of blobs |★★ |★★★ |Defence in depth; most code. +|=== + +Difficulty: O-1 moderate; O-2 trivial once renamed (prove nothing, claim nothing); O-3 unprovable. + +[[6-reversible-core-undoredo-preserves-data-integrity]] +== 6. reversible-core: undo/redo preserves data integrity + +Same shape as T2. Abstract theorem: for a sequence of operations with the cancellation premise, undo +restores state. Provable now (nearly proven). I did not locate a "redo" in the code I read; the claim +should say what it covers. The expensive part is the *refinement link to the Rust* (G-2, G-3, capstone). + +Options for the link, with ratings: + +[cols=",,,",options="header",] +|=== +|Option |Elegance |Dependability |Note +|Keep the verified model; conformance tests against the Rust (current approach) |★★ |★★★ |Already working (`execute_then_undo_is_identity`); no proof of the code itself. +|Bounded model checking (Kani) on small kernels |★★★ |★★ |Proves the real code, bounded. Unproven on this repo; spike first. +|Verus/Creusot deductive proofs on kernels |★★★ |★★ |Heaviest; only for `content_store`-sized kernels. Not tried here. +|=== + +== E-1 and the capstone + +* *E-1 (`adversaryCannotKnow`):* `Knows` has no `Adversary` constructor, so `Knows Adversary a -> Void` +is true of _any_ model that omits the constructor. It states nothing. Delete it from the claims set (keep +as a note), or replace it with a symbolic derivability model plus an explicit assumption list. Likewise +`systemKnowsNewKey` is documented as not stating the negative. Revocation: `revoke`/`rotate` set a +`Revoked` flag and `retrieve` refuses it; the wrapped ciphertext stays in the store and anyone with the +KEK can unwrap it directly. So "a revoked key cannot be used" is an *API-level* property, not a +cryptographic one. Say that. +* *Capstone "every operation is reversible (MPR)":* C-3 proves a transaction containing an obliteration +is _not_ all-reversible. The capstone must be restated as the graded version G-1 already encodes: +every non-obliterating sequence is reversible; an obliterating step absorbs. + +== Recommended order + +[arabic] +. *Fix, then pin with tests* (no proof tooling): P5 path confinement, P4 atomic write, transaction log +atomic write, attestation field coverage + anchor, rename/qualify `ObliterationProof`. These are bugs, +not proof obligations; they change what is true. +. *Rewrite the six statements* in `PROOF-NEEDS.adoc` per this document, each with status +PROVEN / TESTED / ASSUMED / OPEN and the adversary named. This is the high-judgment step. +. *Then prove*, easiest first: R and C (content store), T2/item 6 (abstract), O-1 (model), A-1 (paper). +. Decide the crypto-shredding design before any proof of strong obliteration. + +== Beyond this repo (worth a list) + +* The five-status vocabulary and the dashboard-check ledger live in the estate canon (standards). +* `resource-algebra` must define homomorphisms before G-3 can move. +* The probe tests assert _current bad behaviour_. Do not merge them as-is. Turn each into a test that +fails today and passes after its fix.