|
| 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 | +# Audit: panic-attack assail Critical/High residuals (valence-shell) |
| 7 | + |
| 8 | +**Auditor**: Jonathan D.A. Jewell |
| 9 | +**Date**: 2026-06-01 |
| 10 | +**Scope**: panic-attack assail Critical/High findings that remained after Track A (PR #32, UnsafeCode/UnsafeFFI under impl/rust-cli/src/, impl/zig/, ffi/rust/src/). Tracking issue: [hyperpolymath/valence-shell#33](https://github.com/hyperpolymath/valence-shell/issues/33). |
| 11 | +**Registry**: `audits/assail-classifications.a2ml` (entries 9–17). |
| 12 | +**Cross-reference**: campaign tracker [hyperpolymath/panic-attack#32](https://github.com/hyperpolymath/panic-attack/issues/32). |
| 13 | + |
| 14 | +## Findings audited |
| 15 | + |
| 16 | +| # | Category | Location | Verdict | |
| 17 | +|---|----------|----------|---------| |
| 18 | +| 1.a | UnboundedAllocation | `impl/rust-cli/src/audit_log.rs` | bounded-by-fs-size | |
| 19 | +| 1.b | UnboundedAllocation | `impl/rust-cli/src/redirection.rs` | bounded-by-process-output | |
| 20 | +| 1.c | UnboundedAllocation | `impl/rust-cli/src/main.rs` | bounded-by-fs-size | |
| 21 | +| 1.d | UnboundedAllocation | `impl/rust-cli/src/secure_erase.rs` | false-positive | |
| 22 | +| 1.e | UnboundedAllocation | `impl/rust-cli/src/executable.rs` | bounded-by-fs-size | |
| 23 | +| 2 | CommandInjection | `scripts/verify-proofs.sh` | false-positive | |
| 24 | +| 3 | UnsafeDeserialization | `impl/mcp/src/Server.res` | false-positive | |
| 25 | +| 4 | ProofDrift | `proofs/coq/filesystem_composition.v` | declared-model-gap | |
| 26 | +| 5 | UnsafeCode | `impl/rust-cli/tests/security_tests.rs` | legitimate-ffi | |
| 27 | +| — | SupplyChain | `flake.nix` | fixed-at-source (this PR) | |
| 28 | + |
| 29 | +The pre-existing audit `audits/audit-ffi-2026-05-26.md` covers Wave 1 (eight UnsafeCode classifications under impl/rust-cli/src/, impl/zig/, ffi/rust/src/). |
| 30 | + |
| 31 | +## §1 UnboundedAllocation (5 sites) |
| 32 | + |
| 33 | +panic-attack flags `fs::read_to_string` and large `.collect()` patterns as PA024 (InputBoundary / UnboundedAllocation). All five firings in valence-shell are local-FS reads driven by the shell operator, not network ingress. |
| 34 | + |
| 35 | +### 1.a `audit_log.rs:189` |
| 36 | + |
| 37 | +```rust |
| 38 | +pub fn read_all(&self) -> Result<Vec<AuditEntry>> { |
| 39 | + let content = std::fs::read_to_string(&self.log_path) |
| 40 | + .context("Failed to read audit log")?; |
| 41 | + // ... split + parse line-by-line |
| 42 | +} |
| 43 | +``` |
| 44 | + |
| 45 | +The audit log is the shell's own append-only operations log. Its growth is bounded by: |
| 46 | + |
| 47 | +1. Operator-controlled log path (`AuditLog::new(log_path, ...)`). |
| 48 | +2. Operator-controlled log rotation (out-of-band; the shell does not auto-rotate). |
| 49 | + |
| 50 | +Threat surface: local FS DoS, mitigated by rotation. **No untrusted-network ingress.** A future hardening could stream entries with `BufReader::lines()` (no behaviour change visible to consumers), but the present DoS budget equals "operator decided to keep N MB of audit log on disk". |
| 51 | + |
| 52 | +### 1.b `redirection.rs:68` |
| 53 | + |
| 54 | +```rust |
| 55 | +let mut buffer = gag::BufferRedirect::stdout()?; |
| 56 | +f(state)?; |
| 57 | +let mut output = String::new(); |
| 58 | +buffer.read_to_string(&mut output)?; |
| 59 | +``` |
| 60 | + |
| 61 | +`gag::BufferRedirect` captures the in-process stdout of a closure the shell just executed in response to an operator command. The output is generated by code the operator chose to run; the memory budget is identical to letting that closure write directly to `/dev/stdout`. |
| 62 | + |
| 63 | +### 1.c `main.rs:162` |
| 64 | + |
| 65 | +```rust |
| 66 | +if let Some(ref script_path) = cli.script { |
| 67 | + let script_content = std::fs::read_to_string(script_path) |
| 68 | + .context(format!("Cannot read script: {}", script_path))?; |
| 69 | + // ... shebang strip + execute |
| 70 | +} |
| 71 | +``` |
| 72 | + |
| 73 | +The shell is being invoked as `vsh script.sh`. Same threat model as `bash script.sh`. Reading the script in full before parsing is standard for any POSIX shell (incremental parsing of compound constructs across newlines requires lookahead anyway). |
| 74 | + |
| 75 | +### 1.d `secure_erase.rs:53` |
| 76 | + |
| 77 | +```rust |
| 78 | +let rotational_path = format!("/sys/block/{}/queue/rotational", dev_name); |
| 79 | +if let Ok(content) = fs::read_to_string(&rotational_path) { |
| 80 | + match content.trim() { |
| 81 | + "0" => return Ok(DriveType::SataSSD), |
| 82 | + "1" => return Ok(DriveType::HDD), |
| 83 | + _ => {} |
| 84 | + } |
| 85 | +} |
| 86 | +``` |
| 87 | + |
| 88 | +`/sys/block/<dev>/queue/rotational` is a Linux kernel sysfs node whose content is always `0\n` or `1\n` (2 bytes). No DoS surface; classified as PA024 false-positive. |
| 89 | + |
| 90 | +### 1.e `executable.rs:743` |
| 91 | + |
| 92 | +```rust |
| 93 | +let content = std::fs::read_to_string(&path) |
| 94 | + .map_err(|e| anyhow::anyhow!("source: {}: {}", path.display(), e))?; |
| 95 | +``` |
| 96 | + |
| 97 | +This is the `source` builtin: the operator explicitly types `source foo.sh`. Same threat model as 1.c. |
| 98 | + |
| 99 | +## §2 CommandInjection — `scripts/verify-proofs.sh` |
| 100 | + |
| 101 | +The single `eval` use: |
| 102 | + |
| 103 | +```bash |
| 104 | +run_test() { |
| 105 | + local name="$1" |
| 106 | + local cmd="$2" |
| 107 | + # ... |
| 108 | + if eval "$cmd"; then |
| 109 | +``` |
| 110 | +
|
| 111 | +is called with literal string arguments from the same file: |
| 112 | +
|
| 113 | +```bash |
| 114 | +run_test "Coq: filesystem_model.v" \ |
| 115 | + "cd proofs/coq && coqc filesystem_model.v" |
| 116 | +``` |
| 117 | +
|
| 118 | +The script's own argv parsing only inspects `$1 == --verbose`; no external command string ever flows into `$cmd`. The `eval` exists because each test command embeds `cd ... && tool ...` and the test harness wants to run those in a single subshell. |
| 119 | +
|
| 120 | +A future refactor to a bash array of argv tokens would silence the heuristic without changing behaviour, but **no real injection surface exists**. Classified as false-positive. |
| 121 | +
|
| 122 | +## §3 UnsafeDeserialization — `impl/mcp/src/Server.res` |
| 123 | +
|
| 124 | +The single `JSON.parseExn` at `Server.res:508`: |
| 125 | +
|
| 126 | +```rescript |
| 127 | +let request = try { |
| 128 | + JSON.parseExn(body) |
| 129 | +} catch { |
| 130 | +| _ => |
| 131 | + let error = Dict.make() |
| 132 | + // ... build JSON-RPC -32700 "Parse error" envelope ... |
| 133 | + return JSON.Encode.object(error) |
| 134 | +} |
| 135 | +``` |
| 136 | +
|
| 137 | +Wrapping `JSON.parseExn` in `try/catch` and converting failure to a JSON-RPC parse-error response is **functionally equivalent** to `JSON.parse + Result match`. The PA025 heuristic fires on the API name; the safety property (parse failure does not throw out of this function) is upheld by the surrounding `try/catch`. |
| 138 | +
|
| 139 | +A stylistic migration to `JSON.parse` is fine but not security-relevant. Classified as false-positive. |
| 140 | +
|
| 141 | +## §4 ProofDrift — `proofs/coq/filesystem_composition.v` |
| 142 | +
|
| 143 | +The Admitted at line 238 (and the two `admit.` tactics it relies on at 232/237) were **deliberately introduced** in PR [#48](https://github.com/hyperpolymath/valence-shell/pull/48) ("proofs(coq): assert single_op_reversible model gap (Qed → Admitted)") and documented in `docs/PROOF-NARRATIVE.adoc` § Assumption. |
| 144 | +
|
| 145 | +The original `Qed.` was a soundness defect: it closed a proof that contained an `admit.` tactic mid-body. Switching to `Admitted.` makes the model gap honest. The classification records that the Admitted is an **audited, intentional model gap**, not proof drift accumulating silently. |
| 146 | +
|
| 147 | +Closing this would require closing `single_op_reversible` as a Coq theorem, which is currently blocked by the open-frontier work tracked in `docs/PROOF-NARRATIVE.adoc`. |
| 148 | +
|
| 149 | +## §5 UnsafeCode — `impl/rust-cli/tests/security_tests.rs` |
| 150 | +
|
| 151 | +```rust |
| 152 | +let euid = unsafe { libc::geteuid() }; |
| 153 | +if euid == 0 { /* skip destructive tests unless VSH_ALLOW_ROOT_TESTS=1 */ } |
| 154 | +``` |
| 155 | +
|
| 156 | +`libc::geteuid()` is a one-shot POSIX syscall identical in pattern to the impl/rust-cli/src/* libc usage classified in `audit-ffi-2026-05-26.md`. The test guard exists so the suite stays portable when the operator runs `cargo test` as root (e.g. inside a container). Classified `legitimate-ffi` for consistency with Wave 1. |
| 157 | +
|
| 158 | +## §6 SupplyChain — `flake.nix` (fixed at source) |
| 159 | +
|
| 160 | +Not classified — addressed directly in this PR by committing a `flake.lock` with pinned `nixpkgs` (revision `e9a7635a57597d9754eccebdfc7045e6c8600e6b`, `nixos-unstable`) and `flake-utils` (revision `11707dc2f618dd54ca8739b309ec4fc024de578b`). The lock matches the format and pinning cadence used elsewhere in the estate (e.g. `hyperpolymath/boj-server/flake.lock`). |
| 161 | +
|
| 162 | +## Anti-gameability |
| 163 | +
|
| 164 | +Each classification names a specific `(file, category)` pair. Adding a new finding under one of these files **does** flip to `suppressed: true` automatically; preventing that requires moving the new finding outside the classified file (the registry is per-file, not glob). |
| 165 | +
|
| 166 | +For the cross-cutting rationale ("all UnboundedAllocation reads are bounded-by-FS or bounded-by-process-output"), the audit doc must be re-read whenever a new `read_to_string` is added — the diff makes the new call site visible against the rationale. |
| 167 | +
|
| 168 | +## Verification |
| 169 | +
|
| 170 | +On the PR branch, against the fresh-clone tree: |
| 171 | +
|
| 172 | +```bash |
| 173 | +panic-attack assail . --headless --output-format json --output /tmp/post.json |
| 174 | +jq '[.weak_points[] | select((.severity == "Critical" or .severity == "High") and (.suppressed | not))] | length' /tmp/post.json |
| 175 | +``` |
| 176 | +
|
| 177 | +should report `0` after this PR lands (all 18 Critical/High findings either fixed-at-source or audited as classified). |
| 178 | +
|
| 179 | +## Closes |
| 180 | +
|
| 181 | +Closes [hyperpolymath/valence-shell#33](https://github.com/hyperpolymath/valence-shell/issues/33). Cross-references [hyperpolymath/panic-attack#32](https://github.com/hyperpolymath/panic-attack/issues/32). |
0 commit comments