diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 0f81b4c..21491f0 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -5,7 +5,7 @@ [metadata] project = "panic-attack" version = "2.5.5" -last-updated = "2026-06-02" +last-updated = "2026-06-24" status = "active" [project-context] @@ -89,6 +89,16 @@ test-count = "897 passing (cargo test --release; 4 ignored; 901 runnable per --l truthfulness-fix = "tests/ WeakPoint constructions sed-updated for test_context field (was silently broken on main post-#102)" blocker = "none" +[session-2026-06-24] +description = "assail detector precision fixes (false-positive reduction) — PR #134" +unchecked-alloc = "UncheckedAllocation (C) now NULL-check aware: per-line scan, skips malloc whose result is guarded (if (p==NULL)/if(!p)/nullptr) within a 7-line window, attaches line number (enables inline // panic-attack: accepted markers). Genuinely-unchecked malloc still fires. New helper c_alloc_result_is_null_checked() in analyzer.rs." +dyn-code-exec = "DynamicCodeExecution (JS/Python) word-boundary aware: \\beval\\s*\\( (and \\b(?:eval|exec)\\s*\\( for Python) so FFI symbols like proven_calculator_eval( are not flagged; genuine eval( still fires." +command-injection = "CommandInjection (Shell) no longer matches --eval/-eval CLI flag: eval builtin matched only in statement position via (?m)(?:^|[\\s;&|(])eval[ \\t]." +conservative = "All three are precision-only (no new false negatives): a site is treated benign only on a clear signal. 4 new tests in tests/analyzer_tests.rs; full analyzer suite 17/17 green; zero warnings." +verified = "End-to-end re-scan: proven 1->0 active Critical/High (stubs.c clears, the genuine fix now registers); paint-type 36->35 (gossamer --eval benchmark FP clears; vendored unsafe FFI + irreducible believe_me axiom correctly remain)." +origin = "Surfaced triaging proven#68 / paint-type#86; refs panic-attack#32." +blocker = "none" + [next-priorities] hexad-patch-bridge = "Migrate Patch Bridge mitigation registry from JSON to hexad persistence (ROADMAP v2.2.0 / v2.4.0)" multi-lockfile = "Extend Patch Bridge beyond Cargo.lock to package-lock.json, mix.lock, etc. (ROADMAP v2.4.0)" diff --git a/CHANGELOG.md b/CHANGELOG.md index 6c62896..60d450f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,32 @@ ## [Unreleased] +### Fixed — assail detector precision (false-positive reduction, 2026-06-24) + +Three `assail` analyzer fixes, all conservative (no new false negatives), found +while triaging hyperpolymath/proven#68 and JoshuaJewell/paint-type#86: + +- **UncheckedAllocation (C) is now NULL-check aware.** The detector previously + flagged *every* `malloc(...)` and emitted a line-less, file-level finding. It + now scans per line, skips a malloc whose result is NULL-checked within a short + window (`if (p == NULL)`, `if (!p)`, `nullptr`), and attaches a line number — + which also lets an inline `// panic-attack: accepted` marker suppress a + reviewed site (marker suppression is line-gated). A genuinely-unchecked malloc + still fires. This is why a real null-check fix (proven `stubs.c`) previously + failed to clear. +- **DynamicCodeExecution (JS/Python) is word-boundary aware.** `contains("eval(")` + matched FFI symbol names like `proven_calculator_eval(`. Now `\beval\s*\(` + (and `\b(?:eval|exec)\s*\(` for Python); a genuine `eval(` still fires. +- **CommandInjection (Shell) no longer matches the `--eval` CLI flag.** + `contains("eval ")` matched `--eval`/`-eval`. Now the eval builtin is matched + only in statement position (`(?m)(?:^|[\s;&|(])eval[ \t]`). + +Verified end-to-end: proven 1→0 active Critical/High (`stubs.c` clears), +paint-type 36→35 (gossamer `--eval` benchmark FP clears; genuinely-unsafe +vendored FFI + the irreducible `believe_me` axiom correctly remain). 4 new +tests in `tests/analyzer_tests.rs`; full analyzer suite green; zero warnings. +PR #134. Refs #32. + ### Added — attestation unforgeability proof (Idris2, PROOF-PROGRAMME §3.2) - **`src/abi/AttestationUnforgeability.idr`**: Idris2 proof that the