|
3 | 3 | All notable changes to sigil are documented here. The project follows |
4 | 4 | [Semantic Versioning](https://semver.org/spec/v2.0.0.html). |
5 | 5 |
|
| 6 | +## [0.8.2] — 2026-05-11 |
| 7 | + |
| 8 | +Audit-followup patch release. Clears three supply-chain advisories, |
| 9 | +repairs CI hygiene from the 2026-04-30 audit, discharges one previously- |
| 10 | +relabelled Verus admit, and repairs a broken fuzz target. No public-API |
| 11 | +changes. |
| 12 | + |
| 13 | +### Security |
| 14 | + |
| 15 | +- **Clear RUSTSEC-2026-0097 (`rand` 0.9.x line)** — bumped `rand` |
| 16 | + 0.9.2 → 0.9.4 via `cargo update`. The residual `rand 0.8.5` |
| 17 | + transitive (via `regorus`, the OPA / Rego policy engine) cannot be |
| 18 | + patched until upstream `regorus` releases with `rand = "0.9"+`; |
| 19 | + `wsc` does not use custom rand loggers so the unsoundness does not |
| 20 | + affect us. `deny.toml` already carried this justification; the |
| 21 | + `cargo audit` step in `supply-chain.yml` now matches. (PR #110, |
| 22 | + fixes #102.) |
| 23 | +- **Clear RUSTSEC-2026-0114 (`wasmtime` panic on table allocation)** — |
| 24 | + bumped `wasmtime` 43.0.1 → 43.0.2 via `cargo update`. (PR #110.) |
| 25 | +- **Clear RUSTSEC-2026-0104 (`rustls-webpki` CRL parsing panic)** — |
| 26 | + bumped `rustls-webpki` 0.103.12 → 0.103.13 via `cargo update`. |
| 27 | + (PR #110.) |
| 28 | + |
| 29 | +### Honesty |
| 30 | + |
| 31 | +- **Discharge first Verus `assume(false)`** — `lemma_le64_injective` |
| 32 | + in `src/lib/src/verus_proofs/dsse_proofs.rs` is now an actual proof, |
| 33 | + not a relabelled specification. The proof uses `assert ... by(bit_vector)` |
| 34 | + on the byte-mask equality and explicit unfolding of `spec_le64`'s |
| 35 | + indexed bytes. The other Verus admits remain marked SPECIFICATION |
| 36 | + ONLY per audit C-1; the Verus CI job keeps its `continue-on-error` |
| 37 | + mask until more admits are discharged. (PR #108, refs audit C-1.) |
| 38 | +- **Lift Kani `wasm_module` matrix mask** — the matrix entry was |
| 39 | + filtering on `wasm_module::tests`, which matched zero harnesses |
| 40 | + (Kani exits non-zero on no-match). The harness module is actually |
| 41 | + `wasm_module::component_proofs`. Updated the filter and lifted |
| 42 | + `continue-on-error` for that entry. The single harness |
| 43 | + (`proof_component_module_header_mutual_exclusivity`) runs cleanly. |
| 44 | + Kani `merkle` and `format` masks retained with per-harness |
| 45 | + diagnostic comments. (PR #112, refs audit C-7.) |
| 46 | + |
| 47 | +### CI hygiene |
| 48 | + |
| 49 | +- **Cargo Deny step hardening** — remove `|| true` that was |
| 50 | + silently swallowing install failures; add explicit step names; |
| 51 | + reword the rationale comment to reference `rust-toolchain.toml` |
| 52 | + and `rules_unprivileged_userns_clone` (the actual root cause that |
| 53 | + PR #106 addressed). (PR #107, fixes #103.) |
| 54 | + |
| 55 | +### Fixed |
| 56 | + |
| 57 | +- **Repair `fuzz_public_key.rs`** — the target referenced four APIs |
| 58 | + that had been removed from `SecretKey` / `PublicKey` |
| 59 | + (`from_openssh`, `from_any`). Rewritten against the current surface |
| 60 | + with round-trip preservation, PEM, and DER oracles. Module-level |
| 61 | + comment documents the dropped APIs to prevent reintroduction. |
| 62 | + (PR #109, original flag from audit PR #98.) |
| 63 | + |
| 64 | +### Deferred |
| 65 | + |
| 66 | +The following audit items remain open and are tracked separately: |
| 67 | + |
| 68 | +- **C-4 / #95** — enforce SPKI cert pinning at the TLS layer |
| 69 | + (ureq → rustls-direct migration). |
| 70 | +- **M-1 ff / #79 comment** — `no_std` verifier path for embedded / |
| 71 | + cFS targets. |
| 72 | +- **C-1 (partial)** — discharge the remaining Verus admits |
| 73 | + (`theorem_pae_injective_on_types`, `theorem_pae_injective_on_payloads`, |
| 74 | + `theorem_domain_separation`, `theorem_content_type_separation`, |
| 75 | + `lemma_leaf_node_domain_separation`). |
| 76 | +- **Kani `merkle` / `format` mask removal** — depends on harness |
| 77 | + rework (sha2 unwind > 4, SMT state-space blow-up). |
| 78 | +- **#88 follow-up** — extend Kani harness coverage to more parser |
| 79 | + paths beyond varint / DSSE. |
| 80 | +- **#89** — criterion benches CI integration (the bench harness lands |
| 81 | + in **PR #111**; CI gating deferred to a follow-up). |
| 82 | +- **#46** — post-quantum SLH-DSA signature backend. |
| 83 | +- **#91** — MIRAI abstract-interpretation prototype. |
| 84 | + |
| 85 | +### Contributors |
| 86 | + |
| 87 | +PRs in this release: #107 (cargo-deny), #108 (Verus discharge), #109 |
| 88 | +(fuzz repair), #110 (RUSTSEC bumps). Companion work landing on |
| 89 | +0.8.2+next: #111 (criterion benches, #89), #112 (Kani mask lift). |
| 90 | + |
| 91 | +[0.8.2]: https://github.com/pulseengine/sigil/compare/v0.8.1...v0.8.2 |
| 92 | + |
6 | 93 | ## [0.8.1] — 2026-04-30 |
7 | 94 |
|
8 | 95 | Audit-driven hardening release. Closes 26 of 33 findings from the |
|
0 commit comments