|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: MPL-2.0 |
| 3 | +Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
| 5 | + |
| 6 | +# Estate sweep campaign — 2026-05-26 |
| 7 | + |
| 8 | +**Owner**: @hyperpolymath |
| 9 | +**Tracker**: [hyperpolymath/panic-attack#32](https://github.com/hyperpolymath/panic-attack/issues/32) |
| 10 | +**Tool**: `panic-attack` v2.5.0 built 2026-05-26 |
| 11 | +**Scope**: 369-repo estate at `~/developer/repos/` |
| 12 | +**Outcome**: 16 narrow PRs + 1 real-bug fix PR + 35+ tracking issues + 3 upstream bug reports |
| 13 | + |
| 14 | +## Method |
| 15 | + |
| 16 | +Two-session campaign across 5 work tracks: |
| 17 | + |
| 18 | +1. **Track A — FFI / fixture classification PRs**: per-repo `audits/assail-classifications.a2ml` + `audits/audit-*.md` writing a narrow allow-list for legitimate `unsafe` / fixture-context findings. Each PR documents both the rationale and the anti-gameability mechanism (registry is a separate file from the source under scan; new unsafe inside a classified root requires a companion entry + doc edit, both visible in the diff). |
| 19 | +2. **Track B — real-bug remainder**: after Track A's classifications drained ~500 FFI-shaped findings, the genuine code-bug remainder was small. One critical fix landed (`svalinn` JWT signature verification). |
| 20 | +3. **Track C — per-repo tracking issues**: 35+ GitHub issues, one per repo, listing the Critical/High findings by category for human triage. Excludes Track A and Track D-coverage categories. |
| 21 | +4. **Track D / Phase 5 — proof-aware**: ProofDrift findings in 3 proof repos (`echidna`, `tropical-resource-typing`, `standards`) classified as legitimate axioms or detector false positives. **Zero findings required actual proof discharge.** |
| 22 | +5. **Track E — bridge CVE triage**: 24 per-repo CVE tracking issues from `panic-attack bridge triage` (RustSec advisory DB + reachability analysis) across 29 of 58 Rust repos with non-zero advisories. |
| 23 | + |
| 24 | +### Scan pipeline |
| 25 | + |
| 26 | +Initial attempt used `panic-attack assemblyline` (batch-scan a directory of repos) but stalled on a single 7-min repo with `--parallel` enabled. Pivoted to **per-repo `panic-attack assail --headless` with a 90s timeout** so no single repo can block the campaign. 349 of 368 repos scanned cleanly; 19 skipped (content-only, no source). Plus a nested-repo pass for 6 container directories (`a2ml`, `awesome-projects`, `idaptik`, `isers`, `julia-libraries`, `k9`) covering ~90 sub-repos. |
| 27 | + |
| 28 | +### Findings shape (post-scan, before any classification PRs) |
| 29 | + |
| 30 | +| Severity bucket | Count | |
| 31 | +|---|---| |
| 32 | +| Critical/High `UnsafeCode` / `UnsafeFFI` | 497 | |
| 33 | +| Critical/High `SupplyChain` | 398 | |
| 34 | +| Critical/High `UnboundedAllocation` | 516 | |
| 35 | +| Critical/High `DynamicCodeExecution` | 472 | |
| 36 | +| Critical/High `HardcodedSecret` | 122 | |
| 37 | +| Critical/High `CommandInjection` | 113 | |
| 38 | +| Critical/High `UnsafeDeserialization` | 73 | |
| 39 | +| Critical/High `UnsafeTypeCoercion` | 32 | |
| 40 | +| Critical/High `CryptoMisuse` | 28 | |
| 41 | +| Critical/High `ProofDrift` | 219 | |
| 42 | +| Other (Low/Medium) | 2,591 | |
| 43 | +| Already-suppressed | 961 | |
| 44 | +| Worktree-path artefacts (skipped) | 40 | |
| 45 | +| **Actionable this campaign** | **~2,477** | |
| 46 | + |
| 47 | +## Outputs |
| 48 | + |
| 49 | +### Pull requests (17 narrow PRs) |
| 50 | + |
| 51 | +Track A — FFI / fixture classifications: |
| 52 | + |
| 53 | +| Repo | PR | Findings | Pattern | |
| 54 | +|---|---|---|---| |
| 55 | +| `svalinn` | [#11](https://github.com/hyperpolymath/svalinn/pull/11) | 4 | test-context-fixture (JWT decode in bench/tests) | |
| 56 | +| `proven` | [#67](https://github.com/hyperpolymath/proven/pull/67) | 150 | legitimate-FFI (bindings/, ffi/) + protocol-type-identifier + binding-wrapper-naming | |
| 57 | +| `gossamer` | [#54](https://github.com/hyperpolymath/gossamer/pull/54) | 24 | Zig FFI (GTK WebKit) | |
| 58 | +| `docudactyl` | [#20](https://github.com/hyperpolymath/docudactyl/pull/20) | 15 | Zig FFI | |
| 59 | +| `proven-servers` | [#11](https://github.com/hyperpolymath/proven-servers/pull/11) | 10 | bindings/rust FFI | |
| 60 | +| `aerie` | [#35](https://github.com/hyperpolymath/aerie/pull/35) | 10 | Zig FFI | |
| 61 | +| `stapeln` | [#62](https://github.com/hyperpolymath/stapeln/pull/62) | 10 | eBPF + Zig FFI + Ada↔liboqs | |
| 62 | +| `ambientops` | [#102](https://github.com/hyperpolymath/ambientops/pull/102) | 10 | syscall + cross-subproject FFI | |
| 63 | +| `valence-shell` | [#32](https://github.com/hyperpolymath/valence-shell/pull/32) | 8 | POSIX shell job-control libc + Zig FFI | |
| 64 | +| `panll` | [#47](https://github.com/hyperpolymath/panll/pull/47) | 6 | Idris2 Zig FFI + src-gossamer OS-FFI | |
| 65 | +| `linguist` | [#3](https://github.com/hyperpolymath/linguist/pull/3) | 13 | sample-reference-fixture (PA001+PA022) + vendored PCRE | |
| 66 | +| `boj-server` | [#154](https://github.com/hyperpolymath/boj-server/pull/154) | 119 | 117 MCP cartridge_shim + 2 backend FFI (supersedes #153) | |
| 67 | +| `idaptik` | [#98](https://github.com/hyperpolymath/idaptik/pull/98) | 12 | in-game password fixtures (game-content) | |
| 68 | + |
| 69 | +Track D / Phase 5 — proof-aware: |
| 70 | + |
| 71 | +| Repo | PR | Findings | Status | |
| 72 | +|---|---|---|---| |
| 73 | +| `tropical-resource-typing` | [#4](https://github.com/hyperpolymath/tropical-resource-typing/pull/4) | 4 | merged — all PA021 detector false positives (comment-text matches in Isabelle `\<open>...\</close>`) | |
| 74 | +| `echidna` | [#107](https://github.com/hyperpolymath/echidna/pull/107) | 2 | merged — `funext` (HoTT standard axiom) + `Conflicts` (intentional design parameter) | |
| 75 | +| `standards` | [#184](https://github.com/hyperpolymath/standards/pull/184) | 1 file (4 postulates) | open — justified real-analysis postulates per file's own comment | |
| 76 | + |
| 77 | +Track B — real-bug fix: |
| 78 | + |
| 79 | +| Repo | PR / Issue | Type | |
| 80 | +|---|---|---| |
| 81 | +| `svalinn` | [#12](https://github.com/hyperpolymath/svalinn/issues/12), fix [#14](https://github.com/hyperpolymath/svalinn/pull/14) | `Jwt.verifyJwt` now actually verifies signatures via Web Crypto (was failing closed by accident on every call due to a chain of `%raw`-opacity bugs) | |
| 82 | + |
| 83 | +### GitHub issues (62+) |
| 84 | + |
| 85 | +Per-repo Track C tracking issues filed across 35+ repos aggregating ~1,300 Critical/High findings (excluding PA001/PA007 covered by Track A and ProofDrift covered by Track D). Full list in [panic-attack#32](https://github.com/hyperpolymath/panic-attack/issues/32) comment thread. |
| 86 | + |
| 87 | +Track E bridge-triage CVE tracking issues filed across 24 of 29 non-zero-CVE Rust repos. Full list in same tracker. |
| 88 | + |
| 89 | +Track D proof-aware tracking issues filed (then closed as superseded by Track D classification PRs): echidna#105, tropical-resource-typing#3, standards#181. |
| 90 | + |
| 91 | +### Upstream bugs filed against panic-attack itself |
| 92 | + |
| 93 | +- [#33](https://github.com/hyperpolymath/panic-attack/issues/33) — **design**: VeriSimDB hexad persistence (JSON output schema doesn't handle multi-axis well; would enable real `temporal diff` coverage) |
| 94 | +- [#43](https://github.com/hyperpolymath/panic-attack/issues/43) — **bug**: PA021 ProofDrift detector matches `sorry` / `oops` inside Isabelle `\<open>...\</close>` and `@{text ...}` comment antiquotations; Agda/Coq/Idris detectors likely have the same blind spot |
| 95 | +- [#47](https://github.com/hyperpolymath/panic-attack/issues/47) — **bug**: `bridge triage`'s `"Remove unused dependency from Cargo.toml"` action assumes direct dependency but fires on transitive deps (28/28 phantoms in a 6-repo sample were transitive) |
| 96 | + |
| 97 | +### Skipped / blocked |
| 98 | + |
| 99 | +| Repo / scope | Reason | |
| 100 | +|---|---| |
| 101 | +| `polystack` | Archived on GitHub (read-only) — 7 findings unclassified | |
| 102 | +| `hypatia` | Active working tree with 280+ untracked files at session start; deferred to avoid disturbing in-progress work | |
| 103 | +| `linguist` / `rescript` / `HOL` | Forks with issues disabled on GitHub — Track A PRs landed where possible, no Track C tracking issue | |
| 104 | +| `hyperpolymath-archive`, `standards-as-port` | Deleted on GitHub; local copies are orphans | |
| 105 | +| `julia-libraries/*.jl` | Julia chapter closed per project memory; covered only via container-level `julia-ecosystem#6` tracking issue | |
| 106 | +| `ephapax` preservation (`Semantics.v:3327`) | Parked debt per `ephapax-preservation-closure-plan` — not refiled | |
| 107 | +| `boj-server` `SafetyLemmas.idr` (5 `believe_me`) | Parked class-J primitive axioms (3-month dedicated harness) — not refiled | |
| 108 | +| `betlang` `substTop_preserves_typing` | Parked axiom with discharge recipe in betlang PR#27 — not refiled | |
| 109 | +| `agda-stdlib` | Upstream agda/agda-stdlib clone; no `hyperpolymath/` fork — out of scope | |
| 110 | + |
| 111 | +## Discoveries |
| 112 | + |
| 113 | +### `%raw` opacity in ReScript (svalinn) |
| 114 | + |
| 115 | +The most surprising find of the campaign: `svalinn`'s `Jwt.verifyJwt` was reported as a JWT-verify *bypass* on reading the ReScript source, but the compiled JS was actually compile-broken. ReScript's `%raw("decoded.payload")` block referenced a variable `decoded` that the compiler optimised away (it can't see references inside `%raw` strings), so every call threw `ReferenceError`. The catch-block in `AuthMiddleware.authenticateBearerToken` swallowed the error and returned `authenticated: false` — so JWT auth was **fail-closed by accident**, not by signature-skip. |
| 116 | + |
| 117 | +The same `%raw`-opacity pitfall was present in: |
| 118 | +- `base64UrlDecode` (bound `_i`, `%raw` referenced `i` — different variable name in compiled output) |
| 119 | +- `OAuth2.generateState` (`array` var elided across `%raw` boundaries) |
| 120 | +- `OAuth2` module named `URLSearchParams` (compiled to `let URLSearchParams = {}` which shadowed the global constructor → `getAuthorizationUrl` non-functional) |
| 121 | + |
| 122 | +All four bugs were in code that *looked* obviously correct on visual inspection. Lesson: never trust a `%raw` block whose only "use" of a binding is through the `%raw` string — ReScript will silently drop the binding. |
| 123 | + |
| 124 | +PR [`svalinn#14`](https://github.com/hyperpolymath/svalinn/pull/14) fixes all four with proper Web Crypto wiring (`importKey` + `verify` via JWK, signing input built from raw b64 segments via TextEncoder, algorithm allow-list rejecting `none`). 29/29 auth tests now pass (was 17/12 split). |
| 125 | + |
| 126 | +### Transitive-dep misclassification in `bridge triage` |
| 127 | + |
| 128 | +`bridge triage` reports `"Remove unused dependency from Cargo.toml"` as the recommended action for every phantom-classified CVE. Audit across 6 repos found **28/28 phantom packages were transitive** (pulled in by upstream crates, never declared in any local `Cargo.toml`). `cargo update` doesn't drop them because they're already at the latest crates.io version matching the upstream parent's constraint. |
| 129 | + |
| 130 | +Net: Lane 1 of the planned remediation (small no-behaviour-change PRs deleting unused deps) doesn't apply estate-wide. The underlying classification (`informational` + `phantom` = code unreachable) is correct; only the action string is misleading. Filed as panic-attack#47. |
| 131 | + |
| 132 | +### PA021 detector reads docstring text (tropical-resource-typing) |
| 133 | + |
| 134 | +Three of four PA021 ProofDrift findings on `tropical-resource-typing` were the detector counting the literal word `sorry` inside Isabelle `\<open>All proofs are complete — zero @{text sorry}.\</close>` header docstrings. The fourth (`Tropical_Ordinal.thy`) matched `oops` inside a docstring explaining echidna's evaluation handoff (`with \<open>oops\</close> are the ones we want ECHIDNA to evaluate`). |
| 135 | + |
| 136 | +Filed as panic-attack#43. Same blind spot probably affects PA021's Agda/Coq/Idris equivalents (counting `postulate` / `Admitted` / `believe_me` inside Haddock-style docstrings) and warrants a re-audit. |
| 137 | + |
| 138 | +### Mid-campaign correction: file-overwrite mistake |
| 139 | + |
| 140 | +The first `echidna` PR (#107) initially overwrote 14 pre-existing FFI-boundary classification entries on `audits/assail-classifications.a2ml`. The driver script (`file-ffi-pr-v2.sh`) did `cat > audits/assail-classifications.a2ml` without checking for an existing file. Fixed in a follow-up commit on the same branch (`fix: restore pre-existing FFI-boundary classifications`); the PR now sits at 16 entries (14 original + 2 new PA021). Future per-repo classification PRs should `git show origin/main:audits/assail-classifications.a2ml` before truncating. |
| 141 | + |
| 142 | +## Guardrails honoured throughout |
| 143 | + |
| 144 | +- All commits GPG-signed (key `4A03639C1EB1F86C7F0C97A91835A14A2867091E`). |
| 145 | +- Base = `main` for every PR — no stacked bases. |
| 146 | +- Auto-merge disabled on every PR (estate-wide auto-merge is banned per project memory). |
| 147 | +- Never `--no-verify` / `--no-gpg-sign`. |
| 148 | +- `features/panic-attacker/` stub dirs in other repos untouched (they reference the canonical tool, not divergent copies). |
| 149 | +- `vcl-ut/_wt-vclut*`, `hypatia/.claude/worktrees/agent-*`, ephapax `_wt-eph-*` worktrees — all untouched (parallel sessions). |
| 150 | +- Parked proof debts (`ephapax`, `betlang`, `boj-server` class-J) — not refiled. |
| 151 | +- Julia chapter closed — no per-`.jl` issues filed; container-level only. |
| 152 | +- `valence-shell`'s stray local `main` commit (workflow hardening, unpushed) preserved by branching from `origin/main` not local `main`. |
| 153 | +- Same defence applied to standards (foreign parallel session on `claude/governance-allowlist-foundation` branch left alone) and panic-attack itself (foreign session on `fix/idris-lang-chapel-not-c` left alone — this campaign-report branch was created from `origin/main`). |
| 154 | + |
| 155 | +## What remains |
| 156 | + |
| 157 | +Owner-side throughput now bounds the campaign: |
| 158 | + |
| 159 | +1. **Review/merge the 15 open PRs** — all narrow, signed, small surface area. |
| 160 | +2. **Triage the Track C tracking issues** (~1,300 findings) — separate real bugs from false-positive patterns per repo. |
| 161 | +3. **Decide on the 3 upstream panic-attack bugs** filed (#33 design, #43 detector, #47 bridge action). |
| 162 | + |
| 163 | +Deferred to follow-up sessions: |
| 164 | + |
| 165 | +- **hypatia** classification PR — re-attempt once the active session's untracked files have committed or cleared. |
| 166 | +- **polystack** — owner action to unarchive on GitHub before any work can land. |
| 167 | +- **Track E `assault`** — heavyweight per-target work (each binary needs build + manually-chosen long-running input). Not estate-wide automatable. Smoke-tested on `panic-attack` self-binary (light intensity, 5s/axis, cpu+memory): 0 crashes, 0 signatures, 100% robustness — as expected for a fast-exit CLI. |
| 168 | + |
| 169 | +## Campaign workspace |
| 170 | + |
| 171 | +Preserved at `/tmp/panic-attack-campaign-2026-05-26/`: |
| 172 | + |
| 173 | +- `per-repo/*.json` (349 assail reports, one per repo) |
| 174 | +- `bridge/*.json` (58 Rust-repo bridge reports) |
| 175 | +- `02-plan.json` (triage classification plan) |
| 176 | +- `assault/self-test.json` (Track E smoke test) |
| 177 | +- `00-per-repo.sh`, `00b-nested.sh`, `01-triage.ts`, `file-ffi-pr-v2.sh`, `file-track-c-issue.sh` (driver scripts) |
| 178 | +- `TRACKER-UPDATE.md` ... `TRACKER-UPDATE-V5.md` (intermediate session summaries posted on #32) |
0 commit comments