diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 1b41217..76bd966 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -34,13 +34,20 @@ jobs: disk-cache: ${{ github.workflow }} repository-cache: true + # Audit 2026-04-30 finding C-7 (partial): the previous classification + # of "passes" assumed continue-on-error masking made these jobs green. + # Lifting the mask reveals real failures tied to audit C-1 — Verus + # `theorem_*` functions in src/lib/src/verus_proofs/ end in + # `assume(false)` and the proof obligations are not yet discharged. + # Mask retained until those obligations are mechanised; the job stays + # visible (no skip) so progress is observable. - name: Verify Merkle proofs (CV-20, CV-21) run: bazel build //src/lib/src/verus_proofs:wsc_merkle_proofs - continue-on-error: true + continue-on-error: true # WIP — see audit C-1 - name: Run Verus tests run: bazel test //src/lib/src/verus_proofs:wsc_merkle_verify - continue-on-error: true + continue-on-error: true # WIP — see audit C-1 kani-proofs: name: Kani ${{ matrix.module }} @@ -72,12 +79,18 @@ jobs: cargo install --locked kani-verifier cargo kani setup + # Audit 2026-04-30 finding C-7 (partial): on inspection, several + # matrix jobs (format, merkle, wasm_module) fail when continue-on-error + # is removed. The harnesses cover specific bounded properties and not + # all are passing today. Mask retained per-job until the failing + # harnesses are fixed; varint and dsse pass cleanly today and could be + # ungated in a follow-up. - name: Run Kani ${{ matrix.module }} proofs env: HARNESS: ${{ matrix.harness }} run: cargo kani -p wsc --default-unwind 4 --output-format terse --harness "$HARNESS" timeout-minutes: 60 - continue-on-error: true + continue-on-error: true # WIP — see audit C-7 partial closure rocq-proofs: name: Rocq/coq-of-rust Translation @@ -102,4 +115,7 @@ jobs: timeout-minutes: 30 # coq-of-rust needs Rust nightly with LLVM internals — Nix provides # this locally but CI may need LIBRARY_PATH configuration. + # WIP — see audit C-3: verification/rocq/ is a translation-pipeline + # stub, not a real Rocq proof. continue-on-error stays until a `.v` + # file is wired in. continue-on-error: true diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 3b64925..9cee45c 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -2,9 +2,22 @@ name: CI on: push: - branches: [ main ] + branches: [main] + paths: + - 'src/**' + - 'Cargo.toml' + - 'Cargo.lock' + - 'BUILD.bazel' + - 'MODULE.bazel' + - '.github/workflows/rust.yml' pull_request: - branches: [ main ] + paths: + - 'src/**' + - 'Cargo.toml' + - 'Cargo.lock' + - 'BUILD.bazel' + - 'MODULE.bazel' + - '.github/workflows/rust.yml' env: CARGO_TERM_COLOR: always @@ -76,6 +89,17 @@ jobs: if: matrix.build-system == 'bazel' run: bazel build //src/cli:wasmsign_cli + # Audit 2026-04-30 finding C-7 (partial): Bazel CI now ATTEMPTS to + # run tests, not just validate that targets compile. continue-on-error + # is retained because (a) macOS Bazel toolchain has unrelated issues + # observed in this batch and (b) `bazel test //...` exposes test + # targets that may be platform-specific. Once the macOS bazel-test + # baseline is green for one full week, lift this mask. + - name: Test (Bazel) + if: matrix.build-system == 'bazel' + run: bazel test --build_tests_only --test_output=errors //src/... + continue-on-error: true # WIP — see audit C-7 partial closure + - name: Validate Build Outputs (Bazel) if: matrix.build-system == 'bazel' run: | diff --git a/lean/Ed25519.lean b/lean/Ed25519.lean index 244c19c..1ec4456 100644 --- a/lean/Ed25519.lean +++ b/lean/Ed25519.lean @@ -12,11 +12,24 @@ ## Status - - `scalarMul_mul_order`: proven (via scalarMul_zero_point axiom) - - `verification_equation_sound`: proven (full mechanized proof) - - `verification_equation_complete`: needs prime-order argument (sorry) - - `cofactored_verification_sound`: proven (follows from soundness) - - `basepoint_prime_order`: needs Mathlib OrderOf (sorry) + Honesty policy: every claim below states *exactly* how much of the + proof body is mechanically checked. A `sorry` is treated as an open + obligation and the table is required to say so. See + `audit/2026-04-30/findings.md` C-2 for the audit context. + + - `scalarMul_mul_order`: PROVEN (depends on the `scalarMul_zero_point` + axiom declared in this file). + - `verification_equation_sound`: PROVEN — full mechanized proof, no + `sorry` in the body. + - `verification_equation_complete`: OPEN (`sorry`) — body relies on + `basepoint_prime_order`, which is itself open. The proof sketch in + the body is a roadmap, not a proof. + - `cofactored_verification_sound`: PROVEN — follows from + `verification_equation_sound`, no `sorry` in the body. + - `basepoint_prime_order`: OPEN (`sorry`) — needs an `AddGroup` + instance on `CurvePoint` connected to `scalarMul`, plus + `addOrderOf B = Curve25519.ℓ`, then Mathlib's + `addOrderOf_dvd_of_nsmul_eq_zero`. -/ import Mathlib.GroupTheory.OrderOfElement diff --git a/src/lib/src/verus_proofs/dsse_proofs.rs b/src/lib/src/verus_proofs/dsse_proofs.rs index 912ced2..88a1b73 100644 --- a/src/lib/src/verus_proofs/dsse_proofs.rs +++ b/src/lib/src/verus_proofs/dsse_proofs.rs @@ -43,7 +43,17 @@ pub open spec fn spec_pae( // ── LE64 injectivity ──────────────────────────────────────────────── -/// LEMMA: le64 encoding is injective. +/// **SPECIFICATION ONLY** — proof obligation not yet discharged. +/// See `audit/2026-04-30/findings.md` C-1. +/// +/// LEMMA (intended): le64 encoding is injective. +/// +/// To actually discharge: case-split on `a != b` to obtain a bit position +/// where the two u64s differ; show that bit lives in one of the eight +/// `spec_le64` byte slots; conclude the corresponding byte differs, so +/// the resulting `Seq` differs by `Seq` extensionality. Requires +/// Verus' bit-vector mode (`assert(...) by(bit_vector)`) plus a `Seq` +/// extensionality lemma from `vstd`. pub proof fn lemma_le64_injective(a: u64, b: u64) requires a != b, ensures spec_le64(a) != spec_le64(b), @@ -53,12 +63,24 @@ pub proof fn lemma_le64_injective(a: u64, b: u64) // produce different byte sequences. // NOTE: Z3 needs help with Seq inequality — use assume for now. // The property is trivially true by construction of spec_le64. + // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30). assume(false); } // ── PAE injectivity ───────────────────────────────────────────────── -/// THEOREM (CV-22, part 1): PAE is injective over payload types. +/// **SPECIFICATION ONLY** — proof obligation not yet discharged. +/// See `audit/2026-04-30/findings.md` C-1. Despite the `theorem_` prefix, +/// the body currently relies on `assume(false)` and proves nothing. +/// +/// SPEC (intended) — CV-22, part 1: PAE is injective over payload types. +/// +/// To actually discharge: case-split on `type1.len() == type2.len()`. +/// If lengths differ, `lemma_le64_injective` makes the `type_len` bytes +/// at offset 8..16 differ. If lengths are equal but contents differ, +/// `Seq` extensionality gives an index `i` where `type1[i] != type2[i]`, +/// which lifts to offset `16 + i` of the concatenation. Requires `Seq::add` +/// indexing lemmas from `vstd::seq_lib`. pub proof fn theorem_pae_injective_on_types( type1: Seq, type2: Seq, @@ -72,10 +94,18 @@ pub proof fn theorem_pae_injective_on_types( // If types have equal length but different content, the type // bytes at offset 16..16+len differ. // NOTE: Requires Seq::add injectivity lemmas from vstd. + // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30). assume(false); } -/// THEOREM (CV-22, part 2): PAE is injective over payloads. +/// **SPECIFICATION ONLY** — proof obligation not yet discharged. +/// See `audit/2026-04-30/findings.md` C-1. +/// +/// SPEC (intended) — CV-22, part 2: PAE is injective over payloads. +/// +/// To actually discharge: symmetric argument to +/// `theorem_pae_injective_on_types`, but the differing offset is +/// `16 + payload_type.len() + 8 + i`. Same `vstd` lemmas required. pub proof fn theorem_pae_injective_on_payloads( payload_type: Seq, payload1: Seq, @@ -85,10 +115,18 @@ pub proof fn theorem_pae_injective_on_payloads( ensures spec_pae(payload_type, payload1) != spec_pae(payload_type, payload2), { // Symmetric argument to theorem_pae_injective_on_types. + // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30). assume(false); } -/// COROLLARY: PAE is fully injective. +/// **SPECIFICATION ONLY** — proof obligation not yet discharged. +/// See `audit/2026-04-30/findings.md` C-1. Will follow trivially once +/// the two `theorem_pae_injective_*` admits above are real proofs. +/// +/// SPEC (intended): PAE is fully injective. +/// +/// To actually discharge: case-split on `type1 != type2` vs +/// `payload1 != payload2` and apply the corresponding theorem above. pub proof fn corollary_pae_fully_injective( type1: Seq, payload1: Seq, @@ -99,6 +137,7 @@ pub proof fn corollary_pae_fully_injective( ensures spec_pae(type1, payload1) != spec_pae(type2, payload2), { // Follows from the two injectivity theorems above. + // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30). assume(false); } @@ -117,7 +156,16 @@ pub open spec fn spec_signing_message( .add(artifact_hash) } -/// THEOREM: Different domains produce different signing messages. +/// **SPECIFICATION ONLY** — proof obligation not yet discharged. +/// See `audit/2026-04-30/findings.md` C-1. +/// +/// SPEC (intended): Different domains produce different signing messages. +/// +/// To actually discharge: `Seq::push`/`Seq::add` preserve the domain +/// prefix, so the first `min(domain1.len(), domain2.len())` bytes of +/// each result equal the corresponding domain. By `Seq` extensionality, +/// a differing byte in the prefix lifts to a differing byte in the full +/// signing message. Requires `vstd::seq_lib` push/add indexing lemmas. pub proof fn theorem_domain_separation( domain1: Seq, domain2: Seq, @@ -135,10 +183,20 @@ pub proof fn theorem_domain_separation( { // Different domain prefixes produce different total messages. // NOTE: Requires Seq::push/add extensionality lemmas. + // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30). assume(false); } -/// THEOREM: Different content types produce different signing messages. +/// **SPECIFICATION ONLY** — proof obligation not yet discharged. +/// See `audit/2026-04-30/findings.md` C-1. +/// +/// SPEC (intended): Different content types produce different signing +/// messages. +/// +/// To actually discharge: the content-type byte sits at index +/// `domain.len()` of both encodings. `Seq::push` indexing lemma plus +/// the hypothesis `ct1 != ct2` give differing bytes there, so by +/// `Seq` extensionality the messages differ. pub proof fn theorem_content_type_separation( domain: Seq, ct1: u8, @@ -153,6 +211,7 @@ pub proof fn theorem_content_type_separation( { // Content type byte at position domain.len() differs. // NOTE: Requires Seq::push indexing lemma. + // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30). assume(false); } diff --git a/src/lib/src/verus_proofs/merkle_proofs.rs b/src/lib/src/verus_proofs/merkle_proofs.rs index 6b69611..e20f900 100644 --- a/src/lib/src/verus_proofs/merkle_proofs.rs +++ b/src/lib/src/verus_proofs/merkle_proofs.rs @@ -35,13 +35,23 @@ pub open spec fn spec_largest_pow2_lt(n: int) -> int // ── Domain separation theorem ─────────────────────────────────────── -/// AXIOM: Leaf and node hashes are in disjoint domains. +/// **SPECIFICATION ONLY** — assumed as a cryptographic axiom; not +/// discharged inside Verus. See `audit/2026-04-30/findings.md` C-1. +/// +/// SPEC (intended): Leaf and node hashes are in disjoint domains. /// /// Because leaf hashes are SHA-256(0x00 || data) and node hashes are /// SHA-256(0x01 || left || right), and SHA-256 is collision-resistant, -/// no leaf hash can equal an interior node hash. +/// no leaf hash can equal an interior node hash. This prevents +/// second-preimage attacks on the Merkle tree. /// -/// This prevents second-preimage attacks on the Merkle tree. +/// To actually discharge: this is a statement about SHA-256, not about +/// Verus' SMT-friendly fragment. The honest path is to model +/// `spec_leaf_hash` and `spec_node_hash` as opaque uninterpreted spec +/// functions and *postulate* the disjointness as a separate +/// `#[verifier::external_body]` axiom (or equivalent in the pinned Verus +/// version), making the cryptographic assumption explicit instead of +/// hiding it inside `assume(false)`. pub proof fn lemma_leaf_node_domain_separation() ensures forall|d: Seq, l: Seq, r: Seq| @@ -50,6 +60,7 @@ pub proof fn lemma_leaf_node_domain_separation() // AXIOM: This holds by construction of SHA-256 with different prefix bytes. // Cannot be proven in Verus (requires hash function internals). // Justified by: prefix 0x00 vs 0x01 guarantees different first input byte. + // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30). assume(false); } @@ -85,13 +96,27 @@ pub open spec fn spec_walk_proof( } } -/// THEOREM (CV-20): Inclusion proof soundness. +/// **SPECIFICATION ONLY** — proof obligation not yet discharged, AND +/// the `ensures` clause currently degrades to `true`, so the body +/// proves nothing useful. See `audit/2026-04-30/findings.md` C-1. +/// +/// SPEC (intended) — CV-20: Inclusion proof soundness. /// /// If the proof walk produces the expected root hash, then the leaf /// is authentically at the claimed index in a tree with that root. +/// Formally: `verify_inclusion_proof(idx, size, leaf, proofs, root) = Ok` +/// implies the leaf is at position `idx` in a tree with root hash `root`. /// -/// Formally: verify_inclusion_proof(idx, size, leaf, proofs, root) = Ok -/// implies leaf is at position idx in tree with root hash root. +/// To actually discharge: +/// 1. Strengthen `ensures` from `true` to a real predicate, e.g. an +/// inductive `MerkleTreeContains(root, leaf_hash, leaf_index)` +/// relation defined over `spec_node_hash`. +/// 2. Postulate collision resistance of `spec_node_hash` as an +/// explicit `#[verifier::external_body]` axiom (cf. C-1 fix on +/// `lemma_leaf_node_domain_separation`). +/// 3. Induct on `proof_hashes.len() - step` using `spec_walk_proof`'s +/// `decreases` clause; in the step case, use the postulated +/// collision resistance to invert `spec_node_hash`. pub proof fn theorem_inclusion_proof_soundness( leaf_hash: Seq, leaf_index: int, @@ -116,6 +141,7 @@ pub proof fn theorem_inclusion_proof_soundness( // determines the child hashes, binding leaf to root. // // Full mechanization requires collision resistance assumption on spec_node_hash. + // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30). assume(false); } diff --git a/verification/rocq/README.md b/verification/rocq/README.md new file mode 100644 index 0000000..0cb6dcf --- /dev/null +++ b/verification/rocq/README.md @@ -0,0 +1,41 @@ +# `verification/rocq/` — translation-pipeline scaffolding (NOT a Rocq proof) + +**Status:** unrealised. There is currently **no Rocq (Coq) formal proof** +in this directory. CV-22 ("Rocq proof — signature verification protocol +correctness") in `artifacts/cybersecurity/goals-and-requirements.yaml` +remains in `in-progress` status, pending an actual `.v` file with a +machine-checked proof. + +This README is part of the 2026-04-30 audit honesty fix (finding C-3). + +## What lives here today + +- `pae.rs` — a Rust extraction of `compute_pae` from `src/lib/src/dsse.rs`, + shaped for `coq-of-rust` translation. It is plain Rust with unit tests; + it does not contain any Rocq (`.v`) source. +- `BUILD.bazel` — declares a `rocq_rust_verified_library` target named + `pae_verified`. Today this target exercises **pipeline scaffolding only**: + it confirms that the `coq-of-rust` translation can be invoked on the + Rust source. It does **not** discharge any verification obligation, + because no Rocq proof script is fed to the pipeline. + +## What would need to happen to elevate this to a real proof + +1. Author one or more `.v` files in this directory containing a Rocq + formalisation of the PAE injectivity property (`forall t1 t2 p1 p2, + (t1 <> t2 \/ p1 <> p2) -> compute_pae t1 p1 <> compute_pae t2 p2`), + stated against the `coq-of-rust`-translated definition of + `compute_pae`. +2. Wire those `.v` files into `BUILD.bazel` via `rules_rocq_rust` so the + Bazel target type-checks the proof end-to-end (not merely compiles + the translation). +3. Make the Bazel test step in `.github/workflows/formal-verification.yml` + non-`continue-on-error` for this target (cf. audit finding C-7 in + `audit/2026-04-30/findings.md`), and update CV-22 in + `artifacts/cybersecurity/goals-and-requirements.yaml` from + `in-progress` to `proved` only after step 2 lands. + +Until all three steps are complete, treat any claim of "Rocq-verified +PAE" as aspirational. The Verus track in `src/lib/src/verus_proofs/` +covers the same property, but its proof body is also currently +admitted (see audit C-1).