From ef89c6cac4896325a3855599aa0ff704c265fc5f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 16 May 2026 17:13:55 +0200 Subject: [PATCH] =?UTF-8?q?release:=20v0.8.3=20=E2=80=94=20audit=20follow-?= =?UTF-8?q?up=20continuation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Patch release bundling four PRs: #112 — Kani matrix fix + per-job tolerate_failure pattern #114 — Cerisier formalization companion docs (mapping + scenarios) #115 — bump regorus 0.2.8 → 0.10, fully clears RUSTSEC-2026-0097 #116 — second Verus admit attempt (theorem_pae_injective_on_types) Notable: cargo audit ignore-list is down to one entry (rustls-pemfile, unmaintained-upstream). No actively-fixable RUSTSEC advisories remain. Audit-related fixes from this release are summarised in the "Audit follow-ups" sections of the CHANGELOG. Issue #117 (Sigstore Fulcio cert rotation invalidated our pinned fingerprints) was surfaced during this cycle and is tracked separately — not blocking because audit C-4 documents that pinning is currently warn-only. Trace: skip Co-Authored-By: Claude Opus 4.7 (1M context) --- CHANGELOG.md | 86 +++++++++++++++++++++++++++++++++++++++++++++ Cargo.lock | 8 ++--- Cargo.toml | 2 +- MODULE.bazel | 2 +- src/cli/BUILD.bazel | 2 +- 5 files changed, 93 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5fae9bd..f1a8da4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3,6 +3,92 @@ All notable changes to sigil are documented here. The project follows [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.8.3] — 2026-05-16 + +Audit-followup continuation. Closes the residual security-ignore-list +entry from v0.8.2, restructures the Kani matrix masking pattern, and +lands a second Verus proof attempt. No public-API changes; mostly +hygiene-and-honesty work. + +### Security + +- **Bump regorus 0.2.8 → 0.10 to fully clear RUSTSEC-2026-0097** + (PR #115). The audit fix in v0.8.2 bumped `rand` 0.9.x to 0.9.4 but + left the residual `rand 0.8.5` (transitive via regorus) under an + `--ignore RUSTSEC-2026-0097` flag in `supply-chain.yml` + `deny.toml`. + regorus 0.10 drops the rand 0.8.5 transitive entirely; both ignore + entries removed. Net effect: `cargo audit` returns 0 vulnerabilities + (the only remaining entry is `rustls-pemfile`, which is unmaintained + upstream and stays in the ignore list pending upstream deprecation). +- **Surfaced an out-of-band finding: Sigstore Fulcio cert rotation** + invalidated sigil's pinned fingerprints (filed as issue #117). The + pin set in `cert_pinning.rs::fulcio_production()` is stale as of + 2026-05-16; the keyless integration test catches this when run. + Resolution scope: update the pin set + add a monitoring job. Not + blocking this release because audit C-4 (issue #95) documented that + pinning is currently warn-only — the mismatch is logged, not + fail-closed. + +### Honesty + +- **Second Verus admit attempt: `theorem_pae_injective_on_types`** + (PR #116). Replaces `assume(false)` with an explicit ~70-line proof + using `Seq::add` indexing axioms and length-additive structural + reasoning, building on PR #108's discharge of `lemma_le64_injective`. + The proof has not yet been validated by Verus — CI's Bazel-side + toolchain dependency on Nix was unavailable on the run that would + have checked it, and the Verus job carries `continue-on-error: true` + per audit C-1. Even if Verus eventually rejects the attempt, the + structured `assert` chain is a substantive improvement on the bare + admit and gives the next attempt a concrete starting point. +- **Kani matrix mask is now per-job and documented** (PR #112). The + filter for `wasm_module` was renaming-bug — it pointed at a module + named `tests` that doesn't exist; the real module is `component_proofs`. + Filter fixed. The unwind-loop failures that came out once the filter + matched real harnesses (in `wasm_module`, `dsse`, `merkle`, `format`) + are now masked per-entry via a `tolerate_failure` matrix field, with + inline diagnostic comments explaining what the next attempt needs + (per-harness `#[kani::unwind(N)]` or rewriting equality checks). + +### Documentation + +- **Cerisier formalization companion docs** (PR #114) added to + `docs/security/`: + - `attestation-cerisier-mapping.md` — translates each sigil + attestation primitive into Cerisier's program-logic vocabulary, + identifies four extension gaps (G1 time-indexed predicates, + G2 cross-scheme transitions, G3 content-addressed store, + G4 key rotation). + - `attestation-trust-scenarios.md` — three concrete trust-evolution + scenarios (cross-scheme PQ migration, admits in proof chain, key + rotation) with proposed Cerisier-style judgements. + + Companion blog post on pulseengine.eu: + *"Reasoning about attestation chains: from TrustMee to Cerisier"* + (published 2026-05-11). + +### Deferred (still tracked) + +- **#117** — Sigstore Fulcio cert pin rotation (new this release). +- **#95** — enforce SPKI cert pinning at the TLS layer (audit C-4). +- **#79** — `no_std` verifier path for embedded / cFS targets. +- **#46** — post-quantum SLH-DSA backend. +- **#91** — MIRAI abstract-interpretation prototype. +- **#88 follow-up** — extend Kani harness coverage beyond varint; + needs per-harness `#[kani::unwind]` for the masked entries. +- **Audit C-1 (further)** — discharge the remaining Verus admits + (`theorem_pae_injective_on_payloads`, `theorem_domain_separation`, + `theorem_content_type_separation`, plus the merkle_proofs.rs admits). + +### Contributors + +PRs in this release: #112 (Kani matrix), #114 (Cerisier docs), +#115 (regorus bump), #116 (Verus proof attempt). #111 (criterion +benches, implements #89) also landed in this cycle but is not +release-coupled. + +[0.8.3]: https://github.com/pulseengine/sigil/compare/v0.8.2...v0.8.3 + ## [0.8.2] — 2026-05-11 Audit-followup patch release. Clears three supply-chain advisories, diff --git a/Cargo.lock b/Cargo.lock index 96ee84d..7663d9b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4721,7 +4721,7 @@ checksum = "9edde0db4769d2dc68579893f2306b26c6ecfbe0ef499b013d731b7b9247e0b9" [[package]] name = "wsc" -version = "0.8.2" +version = "0.8.3" dependencies = [ "anyhow", "base64 0.22.1", @@ -4771,7 +4771,7 @@ dependencies = [ [[package]] name = "wsc-attestation" -version = "0.8.2" +version = "0.8.3" dependencies = [ "base64 0.22.1", "chrono", @@ -4787,7 +4787,7 @@ dependencies = [ [[package]] name = "wsc-cli" -version = "0.8.2" +version = "0.8.3" dependencies = [ "clap", "env_logger", @@ -4800,7 +4800,7 @@ dependencies = [ [[package]] name = "wsc-component" -version = "0.8.2" +version = "0.8.3" dependencies = [ "wit-bindgen 0.47.0", "wsc", diff --git a/Cargo.toml b/Cargo.toml index 58c94c0..c58a9a0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -11,7 +11,7 @@ exclude = [ ] [workspace.package] -version = "0.8.2" +version = "0.8.3" edition = "2024" authors = ["Frank Denis ", "Ralf Anton Beier "] license = "MIT" diff --git a/MODULE.bazel b/MODULE.bazel index af50c82..6381eb2 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -3,7 +3,7 @@ module( name = "wsc", # Keep in sync with [workspace.package].version in Cargo.toml. - version = "0.8.2", + version = "0.8.3", ) # Dependencies diff --git a/src/cli/BUILD.bazel b/src/cli/BUILD.bazel index d7dd7df..59aa8dd 100644 --- a/src/cli/BUILD.bazel +++ b/src/cli/BUILD.bazel @@ -15,7 +15,7 @@ package(default_visibility = ["//visibility:public"]) # Version info - keep in sync with [workspace.package].version in Cargo.toml # and with the `version` field in MODULE.bazel. -VERSION = "0.8.2" +VERSION = "0.8.3" rust_binary( name = "wasmsign_cli",