|
4 | 4 |
|
5 | 5 | ## [Unreleased] |
6 | 6 |
|
| 7 | +### Fixed — assail detector precision (false-positive reduction, 2026-06-24) |
| 8 | + |
| 9 | +Three `assail` analyzer fixes, all conservative (no new false negatives), found |
| 10 | +while triaging hyperpolymath/proven#68 and JoshuaJewell/paint-type#86: |
| 11 | + |
| 12 | +- **UncheckedAllocation (C) is now NULL-check aware.** The detector previously |
| 13 | + flagged *every* `malloc(...)` and emitted a line-less, file-level finding. It |
| 14 | + now scans per line, skips a malloc whose result is NULL-checked within a short |
| 15 | + window (`if (p == NULL)`, `if (!p)`, `nullptr`), and attaches a line number — |
| 16 | + which also lets an inline `// panic-attack: accepted` marker suppress a |
| 17 | + reviewed site (marker suppression is line-gated). A genuinely-unchecked malloc |
| 18 | + still fires. This is why a real null-check fix (proven `stubs.c`) previously |
| 19 | + failed to clear. |
| 20 | +- **DynamicCodeExecution (JS/Python) is word-boundary aware.** `contains("eval(")` |
| 21 | + matched FFI symbol names like `proven_calculator_eval(`. Now `\beval\s*\(` |
| 22 | + (and `\b(?:eval|exec)\s*\(` for Python); a genuine `eval(` still fires. |
| 23 | +- **CommandInjection (Shell) no longer matches the `--eval` CLI flag.** |
| 24 | + `contains("eval ")` matched `--eval`/`-eval`. Now the eval builtin is matched |
| 25 | + only in statement position (`(?m)(?:^|[\s;&|(])eval[ \t]`). |
| 26 | + |
| 27 | +Verified end-to-end: proven 1→0 active Critical/High (`stubs.c` clears), |
| 28 | +paint-type 36→35 (gossamer `--eval` benchmark FP clears; genuinely-unsafe |
| 29 | +vendored FFI + the irreducible `believe_me` axiom correctly remain). 4 new |
| 30 | +tests in `tests/analyzer_tests.rs`; full analyzer suite green; zero warnings. |
| 31 | +PR #134. Refs #32. |
| 32 | + |
7 | 33 | ### Added — attestation unforgeability proof (Idris2, PROOF-PROGRAMME §3.2) |
8 | 34 |
|
9 | 35 | - **`src/abi/AttestationUnforgeability.idr`**: Idris2 proof that the |
|
0 commit comments