|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | += panic-attack Audit 2026-03-30 |
| 3 | +:revdate: 2026-03-30 |
| 4 | + |
| 5 | +== Summary |
| 6 | + |
| 7 | +Status: `fail` (implementation strong, publication blocked) |
| 8 | + |
| 9 | +panic-attack is a mature security analysis suite: the README lists 196 passing |
| 10 | +tests, 47 supported languages, and multiple CLI modes. That makes it one of the |
| 11 | +headline wish-list tools for the estate, but the release gate still requires |
| 12 | +proof closure, green builds, and traceable invariants before any v1/stable |
| 13 | +claims get restored. |
| 14 | + |
| 15 | +== Evidence log |
| 16 | + |
| 17 | +* README claims: multi-language static analysis (47 langs), 20 weakness |
| 18 | + categories, attack simulation, system imaging, attestation, plus the |
| 19 | + event-chain export described in `panll-event-chain.json`. |
| 20 | +* `PROOF-NEEDS.md` records the current proof debt: analyzer soundness/completeness, |
| 21 | + SARIF correctness, CVE classification accuracy, reachability/taint invariants, |
| 22 | + attestation chain integrity, and lockfile parsing. Idris2 types exist only in |
| 23 | + `src/abi/Types.idr` and are minimal; large portions of the logic remain |
| 24 | + informal and would benefit from an Agda/Idris session. |
| 25 | +* `just test` runs `cargo test` but the build stops at `src/attestation/intent.rs:59` |
| 26 | + because `getrandom::getrandom` cannot be found in the version of the `getrandom` |
| 27 | + crate currently pulled in. The nightly compile log ends with `rustc` error |
| 28 | + E0425 (`cannot find function getrandom in crate getrandom`), so every test |
| 29 | + target fails before exercising anything beyond the first module. |
| 30 | +* `PROOF-NEEDS` also records 282 `unwrap()` calls scattered across the analyzer |
| 31 | + (already noted in the README as “dangerous patterns: 0 in our code but there |
| 32 | + are many `unwrap()`s because panic-attack hunts for them). |
| 33 | + |
| 34 | +== Confirmed blockers |
| 35 | + |
| 36 | +* `just test` fails immediately because `src/attestation/intent.rs` calls |
| 37 | + `getrandom::getrandom` but Rust cannot resolve that symbol in the dependency |
| 38 | + graph; until the crate dependency or feature set is corrected, there is no |
| 39 | + build/test evidence. |
| 40 | +* The proof debt is wide open: the analyzer’s detection/completeness invariants, |
| 41 | + the SARIF/attestation outputs, the miniKanren taint engine, and the bridge |
| 42 | + classification logic all have entries in `PROOF-NEEDS.md` and lack machine-checked |
| 43 | + scripts. |
| 44 | +* Template metadata such as `panic-attacker.toml.example`, `contractiles` |
| 45 | + scaffolding, and `docs/` narratives still expose TODOs about future |
| 46 | + system-level features, so the release gate sees residual preflight noise. |
| 47 | + |
| 48 | +== Containment actions taken |
| 49 | + |
| 50 | +* The README/ROADMAP/VISION files already insist the tool is for analysis and |
| 51 | + visibility, not for quiet operation; the gate now treats panic-attack as a |
| 52 | + research-grade scanner until the proofs and build-green status is restored. |
| 53 | +* `reports/` capture the latest assemblyline/adjudicate runs, so reviewers can |
| 54 | + see the operational output even though the upstream proofs remain untracked. |
| 55 | +* The `PROOF-NEEDS` document surfaced the high-priority invariants, so the next |
| 56 | + proof sessions have a defined backlog. |
| 57 | + |
| 58 | +== Immediate next actions |
| 59 | + |
| 60 | +* Fix the `getrandom` linkage: verify the `getrandom` dependency exposes `getrandom` |
| 61 | + or replace the call with a supported API (e.g., `rand::random`, `secrecy` |
| 62 | + wrappers, or a custom randomizer) so `cargo test`/`just test` can finish. |
| 63 | +* Schedule Claude-level proof sessions to mechanize analyzer soundness, |
| 64 | + taint propagation, SARIF validity, reachability accuracy, and the attestation |
| 65 | + chain described in `docs/assemblyline` outputs. Each theorem should produce a |
| 66 | + machine-checked Idris2/Agda file with zero `believe_me`. |
| 67 | +* Clean up the remaining template placeholders in the `contractiles`/`docs` |
| 68 | + directories so the release preflight does not flag `TODO` noise as proof debt. |
| 69 | +* Document the `self-*` reports (`self-a2ml.a2ml`, `self-roundtrip.json`) so |
| 70 | + reviewers can reproduce the scans and verify the attestation/assemblyline |
| 71 | + pipelines. |
| 72 | + |
| 73 | +== Invitation for review |
| 74 | + |
| 75 | +If you disagree with these blockers or can help close one, annotate this file |
| 76 | +or open an issue. We intentionally accept challenge; the goal is to make every |
| 77 | +release claim fact-based before we call it stable or publishable. |
0 commit comments