From 2b4cc26a9b0a0d6999b0552de3ee9a208a0e9ea5 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 19 May 2026 19:27:04 +0100 Subject: [PATCH] =?UTF-8?q?vcl-ut=20#25=20P5d:=20Tier-2=20C-ABI=20Ed25519?= =?UTF-8?q?=20attestation=20fallback=20(RESOLVED)=20=E2=80=94=20closes=20t?= =?UTF-8?q?he=20workstream?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Tier-2 fallback of the two-tier boundary model (VERIFICATION-STANCE.adoc). For consumers that cannot run the Tier-1 recompute wasm: a C ABI cannot carry a re-checkable proof, so the honest ceiling is trusted-certifier attestation — and it is now reached. This was the last NAMED-OWED item under #25. New crate src/interface/attest (vcltotal-attest; standalone workspace; deps contained, never touch the zero-dep #![forbid(unsafe_code)] core): - mint(stmt_wire, schema_wire, sk): decode (vcltotal-parse), run the conformance-pinned certified_level, and sign IFF 0..=10. Token = Ed25519 over DOMAIN("VCLT-ATTEST-v1") ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level. Fail-closed: decode failure / Reject ⇒ no token, never a signed unestablished level. - verify(...): recompute the bound message + Ed25519-verify vs the certifier pubkey. Unforgeable + bound: tampered query/schema/level/ sig or wrong key all reject. Does not re-run the decider (Tier-2 trusts the certifier — by construction of a C ABI; weaker than Tier-1, labelled as such). - vclut_rs_verify C-ABI: the previously declared-but-unlinked backend. One audited, documented host/guest unsafe block; all logic in the forbid-unsafe parse crate + audited ed25519-dalek. - Crypto: ed25519-dalek (de-facto standard, audited — maintainer decision 2026-05-19) + sha2, default-features minimal, contained to this Tier-2 crate. Cargo.lock pins them (trust surface). - 9 tests: roundtrip; 5 tamper variants (query/schema/level/sig/key); fail-closed garbage; C-ABI roundtrip+fail-closed; C-ABI small-out/ null. clippy -D warnings + fmt clean. ffi/zig wiring (P5d-2): build.zig cargo-builds libvcltotal_attest.a and links it (with gcc_s for std's _Unwind_* under panic=abort) into every artefact incl. the test runner. lib.zig: extern vclut_rs_verify + new export vclut_verify_wire (fail-closed wrapper, last-error set). New end-to-end Zig test: garbage wire ⇒ -1 across the Zig↔Rust boundary, out untouched. `zig build test` 4/4 (real backend linked, not a stub). Docs / authoritative flip (P5d-3/4): - src/interface/attest/ATTESTATION-FORMAT.adoc (normative wire spec) + README.adoc; .gitignore /target. - VERIFICATION-STANCE.adoc: Tier-2/P5d OWED→RESOLVED across the canonical two-tier model, headline, NAMED-OWED, consumer guidance, roadmap, provenance, closing. Both tiers now RESOLVED; the only remaining items are the precisely-scoped DISCLOSED limits (NaN payload; find/elemBy cross-module Refl non-reduction; L9/L10 predicate depth; additive↔ceil sliver; Idris→wire encode — needed by neither tier) — not gaps. - ADR-0002 status → both tiers RESOLVED; CHANGELOG/PROOF-NEEDS currency. Verified: corpus idris2 --build exit 0 (12 modules, escape-scan OK, unchanged); parse 6/6, recompute-wasm 3/3, attest 9/9 (all clippy -D warnings + fmt clean); `zig build test` 4/4 end-to-end. This closes the vcl-ut#25 boundary-reinforcement workstream: both the Tier-1 recompute-PCC path and the Tier-2 attestation fallback are RESOLVED, every limitation disclosed not faked. Refs hyperpolymath/vcl-ut#25. Co-Authored-By: Claude Opus 4.7 (1M context) --- CHANGELOG.md | 22 +- PROOF-NEEDS.md | 12 +- .../0002-ffi-attestation-trust-boundary.adoc | 36 +- ffi/zig/build.zig | 27 +- ffi/zig/src/lib.zig | 86 ++++ src/interface/attest/.gitignore | 1 + src/interface/attest/ATTESTATION-FORMAT.adoc | 93 +++++ src/interface/attest/Cargo.lock | 324 +++++++++++++++ src/interface/attest/Cargo.toml | 40 ++ src/interface/attest/README.adoc | 54 +++ src/interface/attest/src/lib.rs | 386 ++++++++++++++++++ verification/proofs/VERIFICATION-STANCE.adoc | 174 +++++--- 12 files changed, 1168 insertions(+), 87 deletions(-) create mode 100644 src/interface/attest/.gitignore create mode 100644 src/interface/attest/ATTESTATION-FORMAT.adoc create mode 100644 src/interface/attest/Cargo.lock create mode 100644 src/interface/attest/Cargo.toml create mode 100644 src/interface/attest/README.adoc create mode 100644 src/interface/attest/src/lib.rs diff --git a/CHANGELOG.md b/CHANGELOG.md index 253809d..585602a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -63,11 +63,23 @@ CI-gated and green: recomputation, not proof transport. Plain `wasm32` suffices (type system not load-bearing under recompute); `affinescriptiser` N/A (resource-required + wasm-backend-pending; disclosed in - `AFFINESCRIPTISER-NA.adoc`, not faked). **OWED — P5d (Tier-2 - fallback):** the C-ABI signed-attestation contract + - `vclut_rs_verify` linkage for consumers that cannot run the wasm. - A re-checkable proof is impossible *only* over the C-ABI fallback - tier (canonical two-tier model: + `AFFINESCRIPTISER-NA.adoc`, not faked). +- Phase 5 / vcl-ut#25 — **Tier-2 (P5d) RESOLVED**: `src/interface/attest` + (`vcltotal-attest`) mints/verifies an Ed25519 attestation over + `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level` (level = + the conformance-pinned `certified_level`, signed iff `0..=10`, + fail-closed); the previously-OWED `vclut_rs_verify` backend is this + crate, linked into `ffi/zig/src/lib.zig` (`vclut_verify_wire`) by + `build.zig` (`zig build test` 4/4, end-to-end). Unforgeable + bound + (roundtrip + 5 tamper variants + fail-closed + C-ABI tests). + `ed25519-dalek`/`sha2` contained to the Tier-2 crate; zero-dep + forbid-unsafe core untouched; one audited host/guest `unsafe` block. + Spec `src/interface/attest/ATTESTATION-FORMAT.adoc`; ADR-0002 → + both tiers RESOLVED. **The vcl-ut#25 boundary-reinforcement + workstream is complete** (only the precisely-scoped disclosed limits + remain — not gaps). A re-checkable proof is impossible *only* over + the C-ABI fallback tier; Tier-2 is honestly its weaker + trusted-certifier ceiling (canonical two-tier model: `verification/proofs/VERIFICATION-STANCE.adoc`). `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative, diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 6bdf054..91b0665 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -61,10 +61,14 @@ runtime + the once-proved corpus (offline-re-checkable) — *not* a trusted tag, *not* a transported proof object. Plain `wasm32` suffices (type system not load-bearing under recompute); - `affinescriptiser` N/A (disclosed). **P5d — OWED (Tier-2 fallback):** - the C-ABI signed-attestation contract + `vclut_rs_verify` linkage, - for consumers that cannot run the wasm; the `ffi/zig` fail-closed - shim is its scaffolding. See the canonical two-tier boundary model + `affinescriptiser` N/A (disclosed). **P5d — RESOLVED (Tier-2 + fallback):** `src/interface/attest` mints/verifies an Ed25519 + attestation bound to `(sha256(stmt_wire), sha256(schema_wire), + level)` (fail-closed); the `vclut_rs_verify` backend is linked into + `ffi/zig` (`vclut_verify_wire`, `zig build test` green end-to-end). + Trusted-certifier (weaker than Tier-1), crypto contained. **The + vcl-ut#25 workstream is complete** — only precisely-scoped disclosed + limits remain (not gaps). See the canonical two-tier boundary model in `verification/proofs/VERIFICATION-STANCE.adoc` (authoritative). - Optional future work: prove the ReScript frontend faithfully tracks the Idris2 grammar (low priority; it is a convenience frontend, not a diff --git a/docs/decisions/0002-ffi-attestation-trust-boundary.adoc b/docs/decisions/0002-ffi-attestation-trust-boundary.adoc index f27c3a5..7c388ae 100644 --- a/docs/decisions/0002-ffi-attestation-trust-boundary.adoc +++ b/docs/decisions/0002-ffi-attestation-trust-boundary.adoc @@ -8,8 +8,10 @@ Date: 2026-05-19 ## Status -Accepted (Tier-1 RESOLVED; Tier-2 / P5d OWED). Tracked: -hyperpolymath/vcl-ut#25. Authoritative companion: +Accepted (**both tiers RESOLVED** — Tier-1 recompute-PCC over `wasm32`; +Tier-2 / P5d C-ABI Ed25519 attestation fallback, `src/interface/attest` +linked into the Zig shim). Tracked: hyperpolymath/vcl-ut#25. +Authoritative companion: `verification/proofs/VERIFICATION-STANCE.adoc` (canonical two-tier boundary model) — this ADR records *why*; the stance records *what is and is not proven*. @@ -75,12 +77,22 @@ fabricated level. The only `unsafe` is one audited host/guest memory-ABI block — the declared trust boundary — with all decode/decision logic in the `#![forbid(unsafe_code)]` crate. -**Tier-2 — C-ABI trusted-certifier attestation (fallback, P5d, OWED).** -For consumers that cannot run the Tier-1 wasm: a signed token bound to -`(sha256(query), schema_id, level)`, verified against the certifier's -public key. Strictly weaker (pure trust in the minting certifier), and -labelled as such. The fail-closed `ffi/zig` shim (Phase 3d) is its -scaffolding; the signed contract + `vclut_rs_verify` linkage are OWED. +**Tier-2 — C-ABI trusted-certifier attestation (fallback, P5d, +RESOLVED).** For consumers that cannot run the Tier-1 wasm: +`src/interface/attest` (`vcltotal-attest`) mints an Ed25519 signature +over `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level`, where +`level` is the conformance-pinned `vcltotal_parse::certified_level` +(signed iff `0..=10`, fail-closed); the consumer Ed25519-verifies +against the certifier's public key. Unforgeable and bound (tamper / +wrong-key all reject — machine-tested). The previously-OWED +`vclut_rs_verify` backend is this crate, linked into the `ffi/zig` +shim (`vclut_verify_wire`) by `build.zig`; `zig build test` exercises +the boundary end-to-end. Strictly weaker than Tier-1 (pure trust in +the minting certifier + that it ran the pinned decider), and labelled +as such everywhere. Spec: +`src/interface/attest/ATTESTATION-FORMAT.adoc`; crypto +(`ed25519-dalek`/`sha2`) contained to this Tier-2 crate, the +zero-dep forbid-unsafe core untouched. ## Consequences @@ -99,8 +111,12 @@ scaffolding; the signed contract + `vclut_rs_verify` linkage are OWED. Rust-side + by input-value conformance; L9/L10 predicate depth; additive↔ceil `alignUp` sliver). These are stated in VERIFICATION-STANCE.adoc, not faked. -- P5d (Tier-2) is the remaining boundary work; until it lands, - non-wasm consumers receive only the fail-closed shim (no fabricated +- P5d (Tier-2) is **delivered**: non-wasm consumers get a verifiable + bound attestation (fail-closed) instead of only the bare shim. The + vcl-ut#25 boundary-reinforcement workstream is complete; what + remains are the precisely-scoped disclosed limits above, not gaps. +- (historical) Until P5d landed, non-wasm consumers received only the + fail-closed shim (no fabricated level). - Revisit only if a future revision genuinely introduces a tracked resource at this boundary (none foreseen for a pure verdict diff --git a/ffi/zig/build.zig b/ffi/zig/build.zig index 4fa7b6e..2fc1305 100644 --- a/ffi/zig/build.zig +++ b/ffi/zig/build.zig @@ -7,6 +7,13 @@ // - libvclut_ffi.so shared library for Idris2 / OCaml / SPARK consumers // - libvclut_ffi.a static library variant // - test runner `zig build test` +// +// P5d (vcl-ut#25): the Tier-2 attestation backend `vclut_rs_verify` +// (previously declared-but-unlinked, NAMED OWED) is now the Rust +// `vcltotal-attest` crate (`src/interface/attest`). build.zig compiles +// that staticlib via cargo and links it into every artefact (incl. the +// test runner), so the shim's `vclut_verify_wire` calls a real, +// conformance-pinned, fail-closed backend — not a stub. const std = @import("std"); @@ -14,12 +21,27 @@ pub fn build(b: *std.Build) void { const target = b.standardTargetOptions(.{}); const optimize = b.standardOptimizeOption(.{}); + // Build the Rust Tier-2 backend staticlib (libvcltotal_attest.a). + const cargo = b.addSystemCommand(&.{ + "cargo", "build", + "--release", "--manifest-path", + "../../src/interface/attest/Cargo.toml", + }); + + const attest_a = b.path("../../src/interface/attest/target/release/libvcltotal_attest.a"); + const lib_mod = b.createModule(.{ .root_source_file = b.path("src/lib.zig"), .target = target, .optimize = optimize, .link_libc = true, }); + // Link the Rust Tier-2 staticlib. glibc (link_libc) covers + // pthread/dl/m/rt; `gcc_s` provides the `_Unwind_*` personality + // symbols Rust `std` references (backtrace/personality) even under + // `panic = "abort"`. This is the standard Rust-staticlib companion. + lib_mod.addObjectFile(attest_a); + lib_mod.linkSystemLibrary("gcc_s", .{}); // Shared library variant const shared = b.addLibrary(.{ @@ -27,6 +49,7 @@ pub fn build(b: *std.Build) void { .root_module = lib_mod, .linkage = .dynamic, }); + shared.step.dependOn(&cargo.step); b.installArtifact(shared); // Static library variant @@ -35,12 +58,14 @@ pub fn build(b: *std.Build) void { .root_module = lib_mod, .linkage = .static, }); + static.step.dependOn(&cargo.step); b.installArtifact(static); - // Tests + // Tests (linked against the real Rust backend) const tests = b.addTest(.{ .root_module = lib_mod, }); + tests.step.dependOn(&cargo.step); const run_tests = b.addRunArtifact(tests); const test_step = b.step("test", "Run vcl-ut FFI tests"); test_step.dependOn(&run_tests.step); diff --git a/ffi/zig/src/lib.zig b/ffi/zig/src/lib.zig index f845bca..43a6519 100644 --- a/ffi/zig/src/lib.zig +++ b/ffi/zig/src/lib.zig @@ -41,6 +41,32 @@ fn clearLastError() void { last_error_len = 0; } +// ────────────────────────────────────────────────────────────────────── +// Tier-2 backend (P5d, vcl-ut#25) — the real `vclut_rs_verify`. +// +// Previously NAMED OWED ("declared in intent but not linked"). Now +// implemented by the Rust `vcltotal-attest` crate +// (`src/interface/attest`) and linked by build.zig. It decodes the +// wire `(Statement, OctadSchema)`, runs the conformance-pinned +// `vcltotal_parse::certified_level` (the same faithful image of the +// Idris corpus decision Tier-1 uses), and on a genuine level mints an +// Ed25519 attestation bound to `(sha256(stmt_wire), sha256(schema_wire), +// level)`. Fail-closed: a Reject / decode failure yields -1 and NO +// token. This is the Tier-2 *fallback* (trusted-certifier attestation) +// — explicitly weaker than Tier-1 recompute-PCC; see +// verification/proofs/VERIFICATION-STANCE.adoc. +// ────────────────────────────────────────────────────────────────────── + +extern fn vclut_rs_verify( + stmt_ptr: [*]const u8, + stmt_len: usize, + schema_ptr: [*]const u8, + schema_len: usize, + sk_ptr: [*]const u8, + out_ptr: [*]u8, + out_cap: usize, +) callconv(.c) i64; + // ────────────────────────────────────────────────────────────────────── // C-ABI exports // ────────────────────────────────────────────────────────────────────── @@ -91,6 +117,48 @@ pub export fn vclut_verify_query( /// Get the last error message. Returns an empty string when no error /// is pending. Caller does not own the pointer; copy before the next /// FFI call. +/// Tier-2 (P5d): verify a wire-marshalled `(Statement, OctadSchema)` +/// and, on a genuine certified level, emit a signed attestation. +/// +/// `stmt`/`schema` are the v1 wire bytes (the C-ABI marshalling, same +/// shape as the Tier-1 recompute module). `sk` is the certifier's +/// 32-byte Ed25519 seed (real provisioning is deployment, via the +/// estate token vault). On success returns the level `0..10` and +/// writes a 65-byte token `[level:1][sig:64]` into `out` (needs +/// `out_cap >= 65`). Returns -1 (Rejected) — writing nothing, +/// `vclut_last_error` set — on any decode failure, a Reject level, a +/// null pointer, or insufficient `out_cap`. **Fail-closed:** never a +/// token for a level the certifier did not establish. +pub export fn vclut_verify_wire( + stmt_ptr: [*]const u8, + stmt_len: usize, + schema_ptr: [*]const u8, + schema_len: usize, + sk_ptr: [*]const u8, + out_ptr: [*]u8, + out_cap: usize, +) callconv(.c) c_int { + clearLastError(); + const rc = vclut_rs_verify( + stmt_ptr, + stmt_len, + schema_ptr, + schema_len, + sk_ptr, + out_ptr, + out_cap, + ); + if (rc < 0) { + setLastError("Rejected (fail-closed): no genuine certified " ++ + "level — Tier-2 attestation NOT minted. The verification " ++ + "authority is the conformance-pinned certified_level; see " ++ + "verification/proofs/VERIFICATION-STANCE.adoc"); + return -1; + } + // 0..10 fits c_int; rc is bounded by the Rust backend. + return @intCast(rc); +} + pub export fn vclut_last_error() callconv(.c) [*:0]const u8 { if (last_error_len == 0) return ""; return @ptrCast(&last_error_buf[0]); @@ -123,3 +191,21 @@ test "verify is fail-closed: no fabricated level without a backend" { // and it never returns a "verified" (>=1) level here try std.testing.expect(rc < 1); } + +// P5d integration: the REAL Rust Tier-2 backend is linked +// (libvcltotal_attest.a via build.zig). Garbage wire bytes must +// decode-fail in the conformance-pinned decoder ⇒ no attestation ⇒ +// -1, end-to-end across the Zig↔Rust boundary. (A positive path needs +// a valid wire (Statement,OctadSchema), exhaustively covered by the +// Rust crate's own roundtrip/tamper suite; this asserts the +// fail-closed contract through the actual linked symbol.) +test "vclut_verify_wire fail-closed on garbage via the linked Rust backend" { + _ = vclut_init(); + var out: [65]u8 = [_]u8{0xAA} ** 65; + const sk = [_]u8{7} ** 32; + const bad = [_]u8{0xFF} ** 8; + const rc = vclut_verify_wire(&bad, bad.len, &bad, bad.len, &sk, &out, out.len); + try std.testing.expectEqual(@as(c_int, -1), rc); + // out untouched on the fail-closed path + for (out) |byte| try std.testing.expectEqual(@as(u8, 0xAA), byte); +} diff --git a/src/interface/attest/.gitignore b/src/interface/attest/.gitignore new file mode 100644 index 0000000..ea8c4bf --- /dev/null +++ b/src/interface/attest/.gitignore @@ -0,0 +1 @@ +/target diff --git a/src/interface/attest/ATTESTATION-FORMAT.adoc b/src/interface/attest/ATTESTATION-FORMAT.adoc new file mode 100644 index 0000000..5987272 --- /dev/null +++ b/src/interface/attest/ATTESTATION-FORMAT.adoc @@ -0,0 +1,93 @@ += VCL-total Tier-2 Attestation Format v1 (P5d, vcl-ut#25) +:toc: + +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +Normative format for the **Tier-2 (C-ABI trusted-certifier +attestation) FALLBACK**. See `verification/proofs/VERIFICATION-STANCE.adoc` +(authoritative) for the two-tier boundary model and ADR +`docs/decisions/0002-ffi-attestation-trust-boundary.adoc` for the +rationale. Tier-1 (recompute-PCC over `wasm32`) is the achieved tier; +this is the explicit *weaker* fallback for consumers that cannot run +the Tier-1 module. + +== Trust model (stated, not hidden) + +A C ABI erases types, so it cannot carry a re-checkable dependent +proof. The honest ceiling is *trusted-certifier attestation*: the +consumer **trusts** that (a) the Ed25519 private key is held only by a +genuine certifier and (b) that certifier ran the conformance-pinned +`vcltotal_parse::certified_level` (the same faithful image of the Idris +corpus decision Tier-1 uses) before signing. The token is *unforgeable* +and *bound*: it cannot be fabricated, transplanted onto a different +query/schema, or have its level escalated. This is strictly weaker than +Tier-1 (which trusts neither (a) nor (b) — it recomputes). It is **not** +a re-checkable proof and does not claim to be. + +== Signed message (81 bytes, fixed) + +[cols="1,3"] +|=== +| `DOMAIN` | 16 bytes — `"VCLT-ATTEST-v1\0\0"` (protocol/version domain separation; a signature here can never be replayed as any other protocol) +| `sha256(stmt_wire)` | 32 bytes — SHA-256 of the v1 `Statement` wire bytes (`VCLW…`, see `WIRE-FORMAT.adoc`) +| `sha256(schema_wire)` | 32 bytes — SHA-256 of the v1 `OctadSchema` wire bytes (`VCLS…`) +| `level` | 1 byte — the certified level `0..=10` +|=== + +`token = Ed25519_sign(certifier_sk, DOMAIN ‖ sha256(stmt_wire) ‖ +sha256(schema_wire) ‖ level)` — a detached 64-byte signature. + +`schema_id` is `sha256(schema_wire)` (content-addressed; no external +registry/trust). "query" in the issue-#25 phrasing +`(sha256(query), schema_id, level)` is the marshalled `Statement` +(`sha256(stmt_wire)`). + +== Wire token layout (C-ABI `out`) + +65 bytes: `[ level : u8 ][ sig : 64 bytes ]`. + +== Mint / verify + +* *Mint* (certifier side): decode `(stmt_wire, schema_wire)`; run + `certified_level`; **iff** `0 <= level <= 10`, sign and emit the + token. Any decode failure or Reject ⇒ **no token** (fail-closed — + never a token for an unestablished level). +* *Verify* (consumer side): recompute the 81-byte message from the + wire bytes the consumer holds + the attested `level`; Ed25519-verify + against the certifier's public key. Accept the level iff verification + succeeds. Verification does **not** re-run the decider — that is + Tier-1's role; Tier-2 trusts the certifier by construction of a C + ABI. + +A tampered `stmt_wire`, `schema_wire`, `level`, or `sig`, or a wrong +public key, all fail verification (machine-tested: +`src/interface/attest` — roundtrip + 5 tamper variants + fail-closed + +C-ABI). + +== C-ABI + +`vclut_rs_verify(stmt_ptr, stmt_len, schema_ptr, schema_len, sk_ptr, +out_ptr, out_cap) -> i64` (Rust, `src/interface/attest`), linked into +the Zig shim `ffi/zig/src/lib.zig` and exposed as +`vclut_verify_wire(...)`. Returns the level `0..10` (and writes the +65-byte token) or `-1` Rejected (writes nothing; `vclut_last_error` +set). `sk_ptr` is the certifier's 32-byte Ed25519 seed — **real key +provisioning is deployment**, via the estate token vault +(`hyperpolymath/reasonably-good-token-vault`); the test key +(`[7u8;32]`) is NOT a real certifier key. + +== Crypto + +Ed25519 via `ed25519-dalek` (de-facto standard, widely audited; +maintainer decision 2026-05-19), SHA-256 via `sha2`. Both are +*contained* in the separate `vcltotal-attest` crate (Tier-2 only) and +never touch the zero-dependency, `#![forbid(unsafe_code)]` +`vcltotal-parse` core. The only `unsafe` is one audited host/guest +C-ABI memory block. + +== Versioning + +Any change to the wire formats, message layout, or crypto bumps +`DOMAIN` (`VCLT-ATTEST-vN`) so old signatures cannot be +reinterpreted. Tracked: hyperpolymath/vcl-ut#25. diff --git a/src/interface/attest/Cargo.lock b/src/interface/attest/Cargo.lock new file mode 100644 index 0000000..de35178 --- /dev/null +++ b/src/interface/attest/Cargo.lock @@ -0,0 +1,324 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "base64ct" +version = "1.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06" + +[[package]] +name = "block-buffer" +version = "0.10.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3078c7629b62d3f0439517fa394996acacc5cbc91c5a20d8c658e77abd503a71" +dependencies = [ + "generic-array", +] + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "const-oid" +version = "0.9.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2459377285ad874054d797f3ccebf984978aa39129f6eafde5cdc8315b612f8" + +[[package]] +name = "cpufeatures" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "59ed5838eebb26a2bb2e58f6d5b5316989ae9d08bab10e0e6d103e656d1b0280" +dependencies = [ + "libc", +] + +[[package]] +name = "crypto-common" +version = "0.1.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "78c8292055d1c1df0cce5d180393dc8cce0abec0a7102adb6c7b1eef6016d60a" +dependencies = [ + "generic-array", + "typenum", +] + +[[package]] +name = "curve25519-dalek" +version = "4.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "97fb8b7c4503de7d6ae7b42ab72a5a59857b4c937ec27a3d4539dba95b5ab2be" +dependencies = [ + "cfg-if", + "cpufeatures", + "curve25519-dalek-derive", + "digest", + "fiat-crypto", + "rustc_version", + "subtle", + "zeroize", +] + +[[package]] +name = "curve25519-dalek-derive" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f46882e17999c6cc590af592290432be3bce0428cb0d5f8b6715e4dc7b383eb3" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "der" +version = "0.7.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e7c1832837b905bbfb5101e07cc24c8deddf52f93225eee6ead5f4d63d53ddcb" +dependencies = [ + "const-oid", + "zeroize", +] + +[[package]] +name = "digest" +version = "0.10.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292" +dependencies = [ + "block-buffer", + "crypto-common", +] + +[[package]] +name = "ed25519" +version = "2.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "115531babc129696a58c64a4fef0a8bf9e9698629fb97e9e40767d235cfbcd53" +dependencies = [ + "pkcs8", + "signature", +] + +[[package]] +name = "ed25519-dalek" +version = "2.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "70e796c081cee67dc755e1a36a0a172b897fab85fc3f6bc48307991f64e4eca9" +dependencies = [ + "curve25519-dalek", + "ed25519", + "serde", + "sha2", + "subtle", + "zeroize", +] + +[[package]] +name = "fiat-crypto" +version = "0.2.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "28dea519a9695b9977216879a3ebfddf92f1c08c05d984f8996aecd6ecdc811d" + +[[package]] +name = "generic-array" +version = "0.14.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85649ca51fd72272d7821adaf274ad91c288277713d9c18820d8499a7ff69e9a" +dependencies = [ + "typenum", + "version_check", +] + +[[package]] +name = "getrandom" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0" +dependencies = [ + "cfg-if", + "libc", + "wasi", +] + +[[package]] +name = "libc" +version = "0.2.186" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66" + +[[package]] +name = "pkcs8" +version = "0.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f950b2377845cebe5cf8b5165cb3cc1a5e0fa5cfa3e1f7f55707d8fd82e0a7b7" +dependencies = [ + "der", + "spki", +] + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "rand_core" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" +dependencies = [ + "getrandom", +] + +[[package]] +name = "rustc_version" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92" +dependencies = [ + "semver", +] + +[[package]] +name = "semver" +version = "1.0.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" + +[[package]] +name = "serde" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e" +dependencies = [ + "serde_core", +] + +[[package]] +name = "serde_core" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "sha2" +version = "0.10.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283" +dependencies = [ + "cfg-if", + "cpufeatures", + "digest", +] + +[[package]] +name = "signature" +version = "2.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77549399552de45a898a580c1b41d445bf730df867cc44e6c0233bbc4b8329de" +dependencies = [ + "rand_core", +] + +[[package]] +name = "spki" +version = "0.7.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d91ed6c858b01f942cd56b37a94b3e0a1798290327d1236e4d9cf4eaca44d29d" +dependencies = [ + "base64ct", + "der", +] + +[[package]] +name = "subtle" +version = "2.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "13c2bddecc57b384dee18652358fb23172facb8a2c51ccc10d74c157bdea3292" + +[[package]] +name = "syn" +version = "2.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "typenum" +version = "1.20.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "40ce102ab67701b8526c123c1bab5cbe42d7040ccfd0f64af1a385808d2f43de" + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "vcltotal-attest" +version = "0.1.0" +dependencies = [ + "ed25519-dalek", + "sha2", + "vcltotal-parse", +] + +[[package]] +name = "vcltotal-parse" +version = "0.1.0" + +[[package]] +name = "version_check" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" + +[[package]] +name = "wasi" +version = "0.11.1+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" + +[[package]] +name = "zeroize" +version = "1.8.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b97154e67e32c85465826e8bcc1c59429aaaf107c1e4a9e53c8d8ccd5eff88d0" diff --git a/src/interface/attest/Cargo.toml b/src/interface/attest/Cargo.toml new file mode 100644 index 0000000..25f9223 --- /dev/null +++ b/src/interface/attest/Cargo.toml @@ -0,0 +1,40 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later + +# Standalone workspace root (same rationale as ../parse, ../recompute-wasm): +# decoupled from the broken parent virtual workspace. This is the Tier-2 +# (C-ABI trusted-certifier attestation) FALLBACK crate — explicitly the +# weaker boundary tier (see VERIFICATION-STANCE.adoc's two-tier model). +# The crypto dependency is CONTAINED here and never touches the +# zero-dep, #![forbid(unsafe_code)] `vcltotal-parse` core. +[workspace] + +[package] +name = "vcltotal-attest" +version = "0.1.0" +edition = "2021" +license = "PMPL-1.0-or-later" +authors = ["Jonathan D.A. Jewell "] +repository = "https://github.com/hyperpolymath/vcl-ut" +description = "P5d (#25): Tier-2 C-ABI trusted-certifier attestation. Mints/verifies an Ed25519 signature binding (sha256(stmt_wire), sha256(schema_wire), level); the level comes from the conformance-pinned `vcltotal_parse::certified_level`. Fail-closed." + +[lib] +name = "vcltotal_attest" +crate-type = ["staticlib", "rlib"] +path = "src/lib.rs" + +[dependencies] +vcltotal-parse = { path = "../parse" } +# de-facto standard, widely audited (user decision 2026-05-19). +# default-features off keeps the tree minimal; `std` for the host +# staticlib; no rng feature (deterministic keys via from_bytes). +ed25519-dalek = { version = "2", default-features = false, features = ["std"] } +sha2 = { version = "0.10", default-features = false } + +[profile.release] +panic = "abort" +opt-level = "z" +lto = true +strip = true + +[profile.dev] +panic = "abort" diff --git a/src/interface/attest/README.adoc b/src/interface/attest/README.adoc new file mode 100644 index 0000000..32d912e --- /dev/null +++ b/src/interface/attest/README.adoc @@ -0,0 +1,54 @@ += vcltotal-attest +:toc: + +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +P5d of hyperpolymath/vcl-ut#25 — **Tier-2: C-ABI trusted-certifier +attestation (the FALLBACK tier).** Authoritative model: +`verification/proofs/VERIFICATION-STANCE.adoc`; rationale: ADR +`docs/decisions/0002-ffi-attestation-trust-boundary.adoc`; wire spec: +`ATTESTATION-FORMAT.adoc`. + +== Role + +For consumers that **cannot run the Tier-1 recompute `wasm32` module** +(`src/interface/recompute-wasm`). A C ABI cannot carry a re-checkable +proof, so this mints an Ed25519 attestation binding +`(sha256(stmt_wire), sha256(schema_wire), level)` — unforgeable and +bound, but *trusted* (the consumer trusts the certifier that signed +it). Strictly weaker than Tier-1, and labelled as such everywhere. + +== Fail-closed + +The level comes from the conformance-pinned +`vcltotal_parse::certified_level`. A token is minted **iff** the level +is `0..=10`; any decode failure or Reject ⇒ no token, `-1`. Never a +signed level the certifier did not establish. + +== Unsafe / deps + +Decode + decision logic stays in the `#![forbid(unsafe_code)]`, +zero-dependency `vcltotal-parse` core. Crypto (`ed25519-dalek`, +`sha2`) is contained here. The only `unsafe` is one audited host/guest +C-ABI memory block (`vclut_rs_verify`) — the declared trust boundary +the Zig shim links. + +== Build / test + +[source,sh] +---- +cargo test # 9 tests: roundtrip + 5 tamper + fail-closed + C-ABI +cargo build --release # → target/release/libvcltotal_attest.a +---- + +The Zig shim links the staticlib automatically: +`cd ffi/zig && zig build test` (cargo-builds + links + runs the +end-to-end fail-closed integration test). + +== Keys + +`sk` is the certifier's 32-byte Ed25519 seed. Real provisioning is +deployment via the estate token vault +(`hyperpolymath/reasonably-good-token-vault`). The test key is not a +real certifier key. diff --git a/src/interface/attest/src/lib.rs b/src/interface/attest/src/lib.rs new file mode 100644 index 0000000..1c3a511 --- /dev/null +++ b/src/interface/attest/src/lib.rs @@ -0,0 +1,386 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! P5d (#25) — **Tier-2: C-ABI trusted-certifier attestation +//! (FALLBACK).** +//! +//! See `verification/proofs/VERIFICATION-STANCE.adoc`'s canonical +//! two-tier boundary model. Tier-1 (recompute-PCC over `wasm32`, +//! `src/interface/recompute-wasm`) is the achieved tier: the consumer +//! re-validates. Tier-2 — *this crate* — is the explicit **weaker +//! fallback** for consumers that cannot run the Tier-1 wasm. A C ABI +//! erases types to machine words, so it cannot carry a re-checkable +//! dependent proof; the honest ceiling there is *trusted-certifier +//! attestation*: the consumer **trusts the certifier that minted the +//! token**, but the token is *unforgeable* and *bound* to the exact +//! `(query, schema, level)` it attests, so it cannot be forged, +//! transplanted onto a different query/schema, or have its level +//! escalated. +//! +//! TRUST MODEL (stated, not hidden). The consumer trusts: (a) the +//! certifier's Ed25519 private key is held only by a genuine +//! certifier; (b) that certifier ran the conformance-pinned +//! `vcltotal_parse::certified_level` (the same faithful image of the +//! corpus decision Tier-1 uses) before signing. This is strictly +//! weaker than Tier-1 (which needs neither (a) nor (b) — it +//! recomputes). It is *not* a re-checkable proof and does not pretend +//! to be one. +//! +//! TOKEN. Ed25519 signature over +//! `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level` +//! (`DOMAIN` is a fixed protocol/version tag — domain separation, so a +//! signature here can never be replayed as any other protocol's). The +//! level is `vcltotal_parse::certified_level` over the *decoded* wire; +//! it is signed iff it is `>= 0`. **Fail-closed:** a Reject (`-1`) or +//! any decode failure yields *no token* — never a signed level the +//! certifier did not establish. +//! +//! UNSAFE POLICY. All decode/decision logic is in the +//! `#![forbid(unsafe_code)]` `vcltotal-parse` crate; signing is the +//! audited `ed25519-dalek`. The only `unsafe` is one documented +//! host/guest C-ABI memory block in [`vclut_rs_verify`] — the declared +//! trust boundary the Zig shim links against. + +#![deny(clippy::undocumented_unsafe_blocks)] + +use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey}; +use sha2::{Digest, Sha256}; +use vcltotal_parse::{certified_level, from_wire, from_wire_schema}; + +/// Protocol + version domain-separation tag. Bump on any wire/format +/// change so old signatures cannot be reinterpreted. +pub const DOMAIN: &[u8; 16] = b"VCLT-ATTEST-v1\0\0"; + +/// A minted attestation: the certified level and the detached Ed25519 +/// signature over `DOMAIN ‖ sha256(stmt) ‖ sha256(schema) ‖ level`. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct Attestation { + pub level: u8, + pub sig: [u8; 64], +} + +fn sha256(bytes: &[u8]) -> [u8; 32] { + let mut h = Sha256::new(); + h.update(bytes); + h.finalize().into() +} + +/// The exact bytes signed/verified. `level` is `0..=10`. +fn signed_message(stmt_wire: &[u8], schema_wire: &[u8], level: u8) -> [u8; 81] { + let mut m = [0u8; 81]; + m[..16].copy_from_slice(DOMAIN); + m[16..48].copy_from_slice(&sha256(stmt_wire)); + m[48..80].copy_from_slice(&sha256(schema_wire)); + m[80] = level; + m +} + +/// Mint an attestation for a wire-encoded `(Statement, OctadSchema)`. +/// +/// Decodes both, runs the conformance-pinned +/// `vcltotal_parse::certified_level`, and signs **iff** the level is +/// `>= 0`. Returns `None` (fail-closed) on any decode failure or a +/// Reject — never a token for a level the certifier did not establish. +pub fn mint(stmt_wire: &[u8], schema_wire: &[u8], sk: &SigningKey) -> Option { + let stmt = from_wire(stmt_wire).ok()?; + let schema = from_wire_schema(schema_wire).ok()?; + let lvl = certified_level(&stmt, &schema); + if !(0..=10).contains(&lvl) { + return None; + } + let level = u8::try_from(lvl).ok()?; + let sig = sk.sign(&signed_message(stmt_wire, schema_wire, level)); + Some(Attestation { + level, + sig: sig.to_bytes(), + }) +} + +/// Verify an attestation against the certifier's public key. +/// +/// Recomputes the bound message from the wire bytes the consumer holds +/// together with the attested level, and checks the signature. Returns +/// `Some(level)` iff the token is a genuine certifier signature bound +/// to *these exact* `(stmt_wire, schema_wire, level)` — so a tampered +/// query, schema, level, or signature, or a wrong key, all reject. +/// Does **not** re-run the decider (that is Tier-1's job; Tier-2 trusts +/// the certifier — by construction of a C ABI). +pub fn verify( + stmt_wire: &[u8], + schema_wire: &[u8], + att: &Attestation, + vk: &VerifyingKey, +) -> Option { + if att.level > 10 { + return None; + } + let sig = Signature::from_bytes(&att.sig); + let msg = signed_message(stmt_wire, schema_wire, att.level); + vk.verify(&msg, &sig).ok().map(|()| att.level) +} + +// ── C-ABI: the `vclut_rs_verify` backend the Zig shim links ────────── + +/// `vclut_rs_verify` — the real backend declared (OWED) by +/// `ffi/zig/src/lib.zig`. Decodes the wire `(Statement, OctadSchema)`, +/// mints an attestation, and on success writes `[level:1][sig:64]` (65 +/// bytes) into `out` and returns the level (`0..=10`). Returns `-1` +/// (Reject) — writing nothing — on any decode failure, a Reject level, +/// a null pointer, or `out_cap < 65`. Fail-closed: never a token for an +/// unestablished level. +/// +/// # Safety +/// `stmt_ptr/stmt_len`, `schema_ptr/schema_len`, `sk_ptr` (32 bytes), +/// and `out_ptr/out_cap` must each describe valid, readable/writable +/// ranges. This is the declared host↔guest trust boundary the Zig shim +/// owns. +#[no_mangle] +pub unsafe extern "C" fn vclut_rs_verify( + stmt_ptr: *const u8, + stmt_len: usize, + schema_ptr: *const u8, + schema_len: usize, + sk_ptr: *const u8, + out_ptr: *mut u8, + out_cap: usize, +) -> i64 { + if stmt_ptr.is_null() + || schema_ptr.is_null() + || sk_ptr.is_null() + || out_ptr.is_null() + || out_cap < 65 + { + return -1; + } + // SAFETY: the only unsafe in the path. By this function's + // documented ABI contract the four ranges are valid; we narrow to + // slices immediately and hand the data to the + // `#![forbid(unsafe_code)]` decoder + audited ed25519-dalek. No raw + // pointer escapes; `out` is written only on the success path. + let (stmt_bytes, schema_bytes, sk_bytes) = unsafe { + ( + core::slice::from_raw_parts(stmt_ptr, stmt_len), + core::slice::from_raw_parts(schema_ptr, schema_len), + core::slice::from_raw_parts(sk_ptr, 32), + ) + }; + let sk_arr = match <[u8; 32]>::try_from(sk_bytes) { + Ok(a) => a, + Err(_) => return -1, + }; + let sk = SigningKey::from_bytes(&sk_arr); + match mint(stmt_bytes, schema_bytes, &sk) { + Some(att) => { + // SAFETY: out_cap >= 65 checked above; out_ptr non-null. + // Write exactly [level:1][sig:64]. + let out = unsafe { core::slice::from_raw_parts_mut(out_ptr, 65) }; + out[0] = att.level; + out[1..65].copy_from_slice(&att.sig); + i64::from(att.level) + } + None => -1, + } +} + +#[cfg(test)] +mod tests { + #![allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)] + use super::*; + use vcltotal_parse::ast::*; + use vcltotal_parse::schema::*; + use vcltotal_parse::{to_wire, to_wire_schema}; + + fn key() -> SigningKey { + // Deterministic test key (NOT a real certifier key — real key + // provisioning is deployment, via the estate token vault). + SigningKey::from_bytes(&[7u8; 32]) + } + + fn empty_schema() -> OctadSchema { + let m = |modality, fields| ModalitySchema { modality, fields }; + OctadSchema { + graph: m(Modality::Graph, vec![]), + vector: m(Modality::Vector, vec![]), + tensor: m(Modality::Tensor, vec![]), + semantic: m(Modality::Semantic, vec![]), + document: m(Modality::Document, vec![]), + temporal: m(Modality::Temporal, vec![]), + provenance: m(Modality::Provenance, vec![]), + spatial: m(Modality::Spatial, vec![]), + } + } + + fn parse_safe_stmt() -> Statement { + Statement { + select_items: vec![SelectItem::Star], + source: Source::Store("s".to_string()), + where_clause: None, + group_by: vec![], + having: None, + order_by: vec![], + limit: None, + offset: None, + proof_clause: None, + effect_decl: None, + version_const: None, + linear_annot: None, + epistemic_clause: None, + requested_level: SafetyLevel::ParseSafe, + } + } + + #[test] + fn roundtrip_mint_then_verify() { + let sk = key(); + let vk = sk.verifying_key(); + let sw = to_wire(&parse_safe_stmt()); + let cw = to_wire_schema(&empty_schema()); + let att = mint(&sw, &cw, &sk).expect("ParseSafe ⇒ level 0, mintable"); + assert_eq!(att.level, 0); + assert_eq!(verify(&sw, &cw, &att, &vk), Some(0)); + } + + #[test] + fn tampered_query_rejects() { + let sk = key(); + let vk = sk.verifying_key(); + let sw = to_wire(&parse_safe_stmt()); + let cw = to_wire_schema(&empty_schema()); + let att = mint(&sw, &cw, &sk).unwrap(); + let mut bad = sw.clone(); + *bad.last_mut().unwrap() ^= 0x01; // flip the requested-level byte + assert_eq!(verify(&bad, &cw, &att, &vk), None); + } + + #[test] + fn tampered_schema_rejects() { + let sk = key(); + let vk = sk.verifying_key(); + let sw = to_wire(&parse_safe_stmt()); + let cw = to_wire_schema(&empty_schema()); + let att = mint(&sw, &cw, &sk).unwrap(); + let mut badc = cw.clone(); + badc[6] ^= 0x01; + assert_eq!(verify(&sw, &badc, &att, &vk), None); + } + + #[test] + fn escalated_level_rejects() { + let sk = key(); + let vk = sk.verifying_key(); + let sw = to_wire(&parse_safe_stmt()); + let cw = to_wire_schema(&empty_schema()); + let mut att = mint(&sw, &cw, &sk).unwrap(); + att.level = 10; // attacker bumps the claimed level + assert_eq!(verify(&sw, &cw, &att, &vk), None); + } + + #[test] + fn wrong_key_rejects() { + let sk = key(); + let other = SigningKey::from_bytes(&[9u8; 32]).verifying_key(); + let sw = to_wire(&parse_safe_stmt()); + let cw = to_wire_schema(&empty_schema()); + let att = mint(&sw, &cw, &sk).unwrap(); + assert_eq!(verify(&sw, &cw, &att, &other), None); + } + + #[test] + fn flipped_signature_rejects() { + let sk = key(); + let vk = sk.verifying_key(); + let sw = to_wire(&parse_safe_stmt()); + let cw = to_wire_schema(&empty_schema()); + let mut att = mint(&sw, &cw, &sk).unwrap(); + att.sig[0] ^= 0x01; + assert_eq!(verify(&sw, &cw, &att, &vk), None); + } + + #[test] + fn fail_closed_on_garbage_no_token() { + let sk = key(); + assert!(mint(b"", b"", &sk).is_none()); + assert!(mint(b"not-vclw", b"not-vcls", &sk).is_none()); + assert!(mint(&[0xff; 64], &[0xff; 64], &sk).is_none()); + } + + #[test] + fn cabi_roundtrips_and_is_fail_closed() { + let sk = key(); + let vk = sk.verifying_key(); + let sw = to_wire(&parse_safe_stmt()); + let cw = to_wire_schema(&empty_schema()); + let skb = sk.to_bytes(); + let mut out = [0u8; 65]; + // SAFETY: valid owned slices (test). + let rc = unsafe { + vclut_rs_verify( + sw.as_ptr(), + sw.len(), + cw.as_ptr(), + cw.len(), + skb.as_ptr(), + out.as_mut_ptr(), + out.len(), + ) + }; + assert_eq!(rc, 0); + let att = Attestation { + level: out[0], + sig: <[u8; 64]>::try_from(&out[1..65]).unwrap(), + }; + assert_eq!(verify(&sw, &cw, &att, &vk), Some(0)); + + // Fail-closed: garbage ⇒ -1, out untouched. + let mut out2 = [0xAAu8; 65]; + // SAFETY: valid owned slices (test). + let rc2 = unsafe { + vclut_rs_verify( + [1u8, 2, 3].as_ptr(), + 3, + cw.as_ptr(), + cw.len(), + skb.as_ptr(), + out2.as_mut_ptr(), + out2.len(), + ) + }; + assert_eq!(rc2, -1); + assert!(out2.iter().all(|&b| b == 0xAA)); + } + + #[test] + fn cabi_rejects_small_out_and_nulls() { + let sk = key(); + let sw = to_wire(&parse_safe_stmt()); + let cw = to_wire_schema(&empty_schema()); + let skb = sk.to_bytes(); + let mut tiny = [0u8; 64]; + // SAFETY: valid slices; deliberately out_cap < 65. + let rc = unsafe { + vclut_rs_verify( + sw.as_ptr(), + sw.len(), + cw.as_ptr(), + cw.len(), + skb.as_ptr(), + tiny.as_mut_ptr(), + tiny.len(), + ) + }; + assert_eq!(rc, -1); + // SAFETY: deliberately null stmt pointer. + let rc2 = unsafe { + vclut_rs_verify( + core::ptr::null(), + 0, + cw.as_ptr(), + cw.len(), + skb.as_ptr(), + tiny.as_mut_ptr(), + tiny.len(), + ) + }; + assert_eq!(rc2, -1); + } +} diff --git a/verification/proofs/VERIFICATION-STANCE.adoc b/verification/proofs/VERIFICATION-STANCE.adoc index 918686e..cbacb90 100644 --- a/verification/proofs/VERIFICATION-STANCE.adoc +++ b/verification/proofs/VERIFICATION-STANCE.adoc @@ -40,15 +40,17 @@ typecheck. The concrete blockers were: `Composition` (forward refs, deleted `AllParameterised` still referenced, wrong `CertL6+` arities, non-reducing `rewrite`s). -*Phase 1–4 status (RESOLVED); Phase 5 boundary reinforcement — Tier-1 -RESOLVED, Tier-2/P5d OWED:* every blocker above is fixed *honestly* -and the corpus compiles (**12 modules**: Phase 4 = `LayoutProofs` + -L6–L10 `composeJoin` closure, PR #24; Phase 5 / vcl-ut#25 added +*Phase 1–4 status (RESOLVED); Phase 5 boundary reinforcement — BOTH +tiers RESOLVED:* every blocker above is fixed *honestly* and the +corpus compiles (**12 modules**: Phase 4 = `LayoutProofs` + L6–L10 +`composeJoin` closure, PR #24; Phase 5 / vcl-ut#25 added `Interface.{WireDecode,WireConformance}` — the certified wire/schema -decoder + cross-language `Refl` conformance, plus the faithful Rust -decision port and the recompute-`wasm32` artefact: **Tier-1 -recompute-PCC, RESOLVED**, PRs #26/#28/#29/#30/#31/#32; see the -canonical two-tier boundary model under "What is NOT proven"). +decoder + cross-language `Refl` conformance, the faithful Rust +decision port, the recompute-`wasm32` artefact (**Tier-1 +recompute-PCC**), and the Ed25519 C-ABI attestation fallback +(**Tier-2**, `src/interface/attest`, linked into the Zig shim) — both +**RESOLVED**, PRs #26/#28/#29/#30/#31/#32/#33 + P5d; see the canonical +two-tier boundary model under "What is NOT proven"). **Phase 2** de-vacuized L2/L3/L5 (new shared decider module `VclTotal.Core.Decide`, evidence-carrying predicates, `checkLevel2/3/5Sound`, genuine `composeJoin` closure). @@ -256,8 +258,9 @@ OWED section. `certifyRequested` (structurally — no proof-escape). + *Boundary model — two tiers, not one (canonical; other mentions - refer here). Tier-1 is RESOLVED (Phase 5 / vcl-ut#25, PRs - #29/#30/#31/#32); Tier-2 remains OWED (P5d).* + refer here). BOTH tiers RESOLVED (Phase 5 / vcl-ut#25, PRs + #26/#28/#29/#30/#31/#32/#33 + P5d): Tier-1 recompute-PCC over + `wasm32`, Tier-2 C-ABI signed-attestation fallback.* + ** *Tier-1 — recompute-PCC over `wasm32` (RESOLVED, the achieved tier).* The consumer is shipped the `wasm32` module @@ -295,15 +298,30 @@ OWED section. native verdict *by construction* (deterministic `cargo build` of the same pinned, pure, total source). ** *Tier-2 — C-ABI trusted-certifier attestation (FALLBACK, P5d — - still OWED).* A C ABI erases types to machine words, so it cannot + RESOLVED).* A C ABI erases types to machine words, so it cannot transport a re-checkable dependent `SafetyCertificate`; over a C - ABI the honest ceiling is *trusted-certifier attestation* (the - consumer trusts the checker that minted an unforgeable token - bound to `(sha256(query), schema_id, level)`). This tier exists - only for consumers that cannot run the Tier-1 wasm. The - fail-closed `ffi/zig` shim (Phase 3d) is its scaffolding; the - signed-attestation contract + `vclut_rs_verify` linkage are P5d, - OWED. + ABI the honest ceiling is *trusted-certifier attestation*, and + that ceiling is now reached. `src/interface/attest` + (`vcltotal-attest`) mints an Ed25519 signature over + `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level`, where + `level` is the conformance-pinned `vcltotal_parse::certified_level` + (the same faithful image of the corpus decision Tier-1 uses) and + is signed **iff** `0..=10` — fail-closed, never a token for an + unestablished level. The consumer Ed25519-verifies against the + certifier's public key: the token is *unforgeable* and *bound* + (a tampered query/schema/level/sig or wrong key all reject — + machine-tested: roundtrip + 5 tamper variants + fail-closed + + C-ABI). The previously-OWED `vclut_rs_verify` backend is this + crate, linked into the `ffi/zig` shim (`vclut_verify_wire`) by + `build.zig`; `zig build test` exercises the fail-closed path + end-to-end across the Zig↔Rust boundary. Trust model, stated: + the consumer trusts (a) the certifier's key is genuinely held and + (b) the certifier ran the pinned decider before signing — + strictly weaker than Tier-1 (which trusts neither; it + recomputes). Real key provisioning is deployment (estate token + vault). Spec: `src/interface/attest/ATTESTATION-FORMAT.adoc`; + crypto (`ed25519-dalek`/`sha2`) is contained to this Tier-2 crate + and never touches the zero-dep forbid-unsafe core. + So "a re-checkable proof is impossible by construction" is true *only of the C-ABI fallback tier*, **not of any FFI**: Tier-1 @@ -327,9 +345,11 @@ OWED section. the recompute tier — the producer encodes from Rust). (3) *RESOLVED:* the decision-transport tier is delivered as Tier-1 recompute-`wasm32` (P5c-5 #32) with the faithful Rust decision port machine-pinned to - the corpus (P5c-2/3/4 #31). (4) *OWED:* the P5d C-ABI - signed-attestation *fallback* contract + `vclut_rs_verify` linkage - (Tier-2). Until P5d, non-wasm consumers get the fail-closed shim. + the corpus (P5c-2/3/4 #31). (4) *RESOLVED:* the P5d C-ABI + signed-attestation *fallback* + `vclut_rs_verify` linkage (Tier-2, + `src/interface/attest`, linked into the Zig shim). **Nothing under + this issue's NAMED-OWED list remains** — what remains are the + precisely-scoped *disclosed limitations* below, not gaps. *Disclosed limitations, not hidden gaps:* (i) the certified decoder decodes any NaN bit-pattern to *a* NaN (Idris2 0.8.0 has no pure bit-exact `Bits64 -> Double`); finite + infinite values are @@ -378,10 +398,14 @@ OWED section. fail-closed (malformed/unmet → Reject, never a fabricated level). Recommended consumer posture: treat a Tier-1 recomputed level as a genuine machine basis (you verified it); still apply defence in - depth. The C-ABI level tag (Tier-2, P5d, *still OWED*) remains - advisory-only — a weaker fallback for consumers that cannot run the - wasm. See the canonical two-tier boundary model in "What is NOT - proven". + depth. If you cannot run the wasm, use **Tier-2** (P5d, RESOLVED): + `vclut_verify_wire` returns a level + an Ed25519 token bound to + `(sha256(stmt_wire), sha256(schema_wire), level)`; Ed25519-verify it + against the certifier's public key before trusting the level. Tier-2 + is *trusted-certifier* (you trust the certifier ran the pinned + decider and holds its key) — strictly weaker than Tier-1, and + fail-closed (no genuine level ⇒ no token). See the canonical + two-tier boundary model in "What is NOT proven". == Remediation roadmap (phased, tracked standards#124) @@ -456,8 +480,8 @@ OWED section. over a *C ABI*; over the estate's typed-wasm target it is the objective (PCC, TCB = checker kernel), with C-ABI attestation as the fallback tier — see the two-tier boundary model above. -. *Phase 5 (boundary reinforcement, hyperpolymath/vcl-ut#25 — Tier-1 - DONE; Tier-2/P5d OWED):* the Phase-4 residual is discharged in +. *Phase 5 (boundary reinforcement, hyperpolymath/vcl-ut#25 — BOTH + tiers RESOLVED):* the Phase-4 residual is fully discharged in precisely-scoped, merged steps. *P5a (#26):* the **trusted** Rust/SPARK-grade `src/interface/parse` parser (string → faithful Rust mirror of `Grammar.idr`; panic-free/total by static lints) — @@ -491,14 +515,21 @@ OWED section. disclosed in `AFFINESCRIPTISER-NA.adoc`, not faked) and plain `wasm32` is sufficient because the wasm type system is not load-bearing under recompute. - *Still OWED — P5d (Tier-2 fallback):* the C-ABI signed-attestation - contract over `(sha256(query), schema_id, level)` + the - `vclut_rs_verify` linkage, for consumers that cannot run the Tier-1 - wasm. The pre-existing `ffi/zig` fail-closed shim is its - scaffolding. Also still OWED: the *encode* direction (Idris→wire), - not required by recompute (the producer encodes from Rust). A - re-checkable proof remains impossible *only* over the C-ABI fallback - tier; Tier-1 sidesteps that by recomputation, not proof transport. + *P5d (Tier-2 fallback) — RESOLVED:* `src/interface/attest` + (`vcltotal-attest`) mints/verifies an Ed25519 attestation over + `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level` (level = + the pinned `certified_level`, signed iff `0..=10`, fail-closed); the + previously-OWED `vclut_rs_verify` is this crate, linked into the + `ffi/zig` shim (`vclut_verify_wire`) by `build.zig` with `zig build + test` exercising the boundary end-to-end. Spec + `src/interface/attest/ATTESTATION-FORMAT.adoc`; crypto contained, + core untouched. The only remaining disclosed item is the *encode* + direction (Idris→wire), which is **not a gap**: it is not required + by either tier (the producer encodes from the trusted Rust side; the + certified path only ever *decodes*). A re-checkable proof remains + impossible *only* over the C-ABI fallback tier; Tier-1 sidesteps + that by recomputation, Tier-2 is honestly the weaker trusted- + certifier ceiling. == Provenance @@ -520,10 +551,15 @@ decoder + `Refl` conformance (#29); P5c-1 certified `OctadSchema` codec (#30); P5c-2/3/4 `vcltotal_parse::decider` faithful Rust port of the corpus decision core, machine-pinned via `WireConformance` (#31); P5c-5 recompute `wasm32` artefact `src/interface/recompute-wasm` -(fail-closed, one audited host/guest unsafe block) (#32); P5c-6 this -PR — the `OWED→RESOLVED` stance flip + ADR -`docs/decisions/0002-ffi-attestation-trust-boundary.adoc`. Tier-2 -(P5d C-ABI signed-attestation fallback) remains OWED. +(fail-closed, one audited host/guest unsafe block) (#32); P5c-6 (#33) +the Tier-1 `OWED→RESOLVED` stance flip + ADR +`docs/decisions/0002-ffi-attestation-trust-boundary.adoc`. **P5d (this +PR):** Tier-2 — `src/interface/attest` (`vcltotal-attest`) Ed25519 +attestation mint/verify + the `vclut_rs_verify` backend linked into +the `ffi/zig` shim (`vclut_verify_wire`, `zig build test` green +end-to-end); ADR-0002 updated to Tier-2 RESOLVED. **Both tiers +RESOLVED; the vcl-ut#25 boundary-reinforcement workstream is +complete.** The corpus now builds clean as *12 modules* (`idris2 0.8.0 --build verification/proofs/vclut-core.ipkg`, exit 0, @@ -551,31 +587,35 @@ Notes for reproduction / honesty: reproduction only. The residual risk is now at the *boundary*, and the boundary no longer -lies. **Tier-1 (recompute-PCC over `wasm32`) is RESOLVED** (Phase 5 / -vcl-ut#25, PRs #26/#28/#29/#30/#31/#32): the previously-headline "no -parser" item is closed (trusted Rust `src/interface/parse`, P5a); the -`Statement` *and* `OctadSchema` *decode* side is **certified** -(`WireDecode`, total/zero-escape, `WireConformance` `Refl`-pinned to -the Rust encoder); the decision core is a faithful Rust port -machine-pinned to the corpus; and the consumer re-runs it from a -fail-closed `wasm32` module (`src/interface/recompute-wasm`) — *you -re-validate, you do not trust a tag*. The guarantee, TCB and -sufficiency of plain `wasm32` are stated in the canonical two-tier -model above. **Still OWED — Tier-2 / P5d:** the C-ABI -signed-attestation *fallback* contract + `vclut_rs_verify` linkage, -for consumers that cannot run the Tier-1 wasm (the `ffi/zig` -fail-closed shim is its scaffolding). Also still OWED / disclosed: the -*encode* direction (Idris→wire; not needed by recompute), the L6–L10 -*predicate* shallowness, the genuine `ABI.Layout` -alignment/no-padding theorems, `ABI.Foreign` plumbing, L3's disclosed -subquery/heuristic scoping, the NaN-payload reconstruction limit -(finite/infinite bit-exact; Rust proptest is the exhaustive witness), -and the cross-module `Refl` non-reduction of `find`/`elemBy` -(schema-resolution-dependent verdicts pinned Rust-side + input-value -conformance). A re-checkable proof remains impossible *only* over the -C-ABI fallback tier; Tier-1 sidesteps that by recomputation, not proof -transport — stated, not hidden. The former headline residuals -(*non-compiling corpus*, *vacuous L2/L3/L5 predicates*, *decorative -certificate*, *unsound `ABI.Layout`*, *lying FFI*, *no parser / -untransported certificate*) are all resolved; what remains is the P5d -fallback contract and the precisely-scoped disclosed limits above. +lies. **Both tiers are RESOLVED** (Phase 5 / vcl-ut#25, PRs +#26/#28/#29/#30/#31/#32/#33 + P5d). *Tier-1 (recompute-PCC over +`wasm32`):* the previously-headline "no parser" item is closed +(trusted Rust `src/interface/parse`, P5a); the `Statement` *and* +`OctadSchema` *decode* side is **certified** (`WireDecode`, +total/zero-escape, `WireConformance` `Refl`-pinned to the Rust +encoder); the decision core is a faithful Rust port machine-pinned to +the corpus; the consumer re-runs it from a fail-closed `wasm32` module +— *you re-validate, you do not trust a tag*. *Tier-2 (C-ABI +attestation fallback, P5d):* `src/interface/attest` mints/verifies an +Ed25519 token bound to `(sha256(stmt_wire), sha256(schema_wire), +level)` (level = the pinned `certified_level`, fail-closed), with +`vclut_rs_verify` linked into the Zig shim — for consumers that cannot +run the wasm; honestly the *weaker, trusted-certifier* tier. The +guarantees, TCBs and the sufficiency of plain `wasm32` are stated in +the canonical two-tier model above. What remains are **precisely-scoped +disclosed limitations, not gaps**: the *encode* direction (Idris→wire; +needed by neither tier), the L6–L10 *predicate* shallowness, the +genuine `ABI.Layout` alignment/no-padding theorems, `ABI.Foreign` +plumbing, L3's disclosed subquery/heuristic scoping, the NaN-payload +reconstruction limit (finite/infinite bit-exact; Rust proptest is the +exhaustive witness), and the cross-module `Refl` non-reduction of +`find`/`elemBy` (schema-resolution-dependent verdicts pinned Rust-side ++ input-value conformance). A re-checkable proof remains impossible +*only* over the C-ABI fallback tier; Tier-1 sidesteps that by +recomputation, Tier-2 is honestly its weaker ceiling — stated, not +hidden. The former headline residuals (*non-compiling corpus*, +*vacuous L2/L3/L5 predicates*, *decorative certificate*, *unsound +`ABI.Layout`*, *lying FFI*, *no parser / untransported certificate*, +*untransported attestation*) are all resolved; the vcl-ut#25 +boundary-reinforcement workstream is **complete**, with only the +precisely-scoped disclosed limits above remaining.