feat(security): invariant G7 — no unprivileged command weaker than the Bash tool

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "sudo-proxy"
-version = "1.1.0"
+version = "1.2.0"
 edition = "2021"
 license = "MIT"
 description = "Privileged command execution proxy with human approval via pkexec or sudo"

README.md

@@ -53,6 +53,16 @@ system files, manage services, or run any other command — with the human
 always in the loop, even when Claude Code is run with
 `--dangerously-skip-permissions`.
 
+It is deliberately **not** a way to run *un*privileged commands with less
+scrutiny than the Bash tool: an unprivileged command targeting the local
+machine is refused and delegated back to the Bash tool (which already applies
+your permission rules), and loopback aliases like `127.0.0.1` cannot dodge that.
+sudo-proxy handles privilege escalation and commands on remote hosts; there,
+unprivileged commands are gated the same way, and the per-command gate is only
+relaxed if you deliberately mark a host eligible in `hosts.json` *and* confirm
+once per session (a grant that is never persisted). See
+[REVIEWING.md](REVIEWING.md) invariant **G7**.
+
 For how this relates to mcp-firewall, sandboxing, polkit, doas, and other
 neighboring tools, see [docs/comparison.md](docs/comparison.md).
 

REVIEWING.md

@@ -9,15 +9,24 @@ code that has to hold it up, and — most importantly — here is where we have
 If you find a way to break any numbered claim below, that is a security finding;
 see [SECURITY.md](SECURITY.md) for where to send it.
 
-## The one claim
+## The claims
 
-Everything reduces to a single invariant:
+The privileged surface reduces to a single invariant (**G1**):
 
 > **Nothing privileged runs without a human deliberately approving the exact
 > command shown.**
 
-We would rather you try to falsify that than "review the project." Below it is
-broken into concrete, falsifiable sub-claims.
+A second invariant (**G7**) guards the *unprivileged* surface — the part that
+was historically weaker than the agent's own Bash tool:
+
+> **No unprivileged command runs with less human scrutiny than the agent's Bash
+> tool would apply: every unprivileged command faces a live human gate unless an
+> operator has *out-of-band* made its host eligible AND a human gave a
+> *session-scoped* confirmation; and a self/loopback target cannot route around
+> that gate by naming an alias of "localhost".**
+
+We would rather you try to falsify these than "review the project." Below they
+are broken into concrete, falsifiable sub-claims (C1–C7 for G1, C8–C10 for G7).
 
 ## Falsify one of these
 
@@ -39,10 +48,14 @@ finding.
   deduplicated and every request must carry a `time` within 60 s. *Attack:*
   cause the same approval to authorise two executions, or make a stale request
   pass. → `src/server.rs` (`check_freshness` `:58`, `try_insert` `:213`).
-- **C4 — Policy flips only on a keypress.** The `confirm_unprivileged` policy
-  flag can be changed *only* by an interactive keypress — never by a request
-  field, MCP tool flag, or replay. *Attack:* flip it from the wire. →
-  `src/tui.rs` (`classify_key`), `src/server.rs`.
+- **C4 — Unattended mode can't be enabled from the wire.** A daemon becomes
+  eligible for unattended unprivileged execution *only* via an out-of-band edit
+  of `hosts.json` (`policy.unattended_eligible`), which is read once at startup
+  and never mutated at runtime; and the session grant flips *only* on an
+  interactive `a` keypress, and *only* when eligible. No request field, MCP tool
+  flag, or replay can enable either barrier. *Attack:* enable unattended mode, or
+  flip the session grant, from the wire. → `src/hosts.rs` (`Policy`),
+  `src/tui.rs` (`classify_key`), `src/server.rs` (dispatch).
 - **C5 — No stored credential.** sudo-proxy never stores or caches a secret;
   authentication is owned entirely by `sudo`/`pkexec`. *Attack:* find any path
   where sudo-proxy holds, caches, or replays a credential. → `src/executor.rs`.
@@ -58,6 +71,34 @@ finding.
   without approval. → `src/server.rs` (`peer_uid`/`SO_PEERCRED` `:244`,
   `handle_connection`).
 
+The G7 sub-claims (unprivileged surface):
+
+- **C8 — No unattended unprivileged exec except behind two human acts; the grant
+  never persists.** No unprivileged command reaches `exec_direct` without a
+  per-command keypress *unless* (a) its daemon is `unattended_eligible` (barrier
+  1, config-only) *and* (b) a human answered `a` this session (barrier 2). The
+  grant lives only in memory, is never written to `hosts.json`, and dies with the
+  daemon/tunnel. *Attack:* reach `exec_direct` unattended on a non-eligible
+  daemon; make an `a` press grant a session without eligibility; make the grant
+  survive a session/tunnel boundary or a restart; or make a stale
+  `confirm_unprivileged` key re-enable it. → `src/server.rs` (dispatch),
+  `src/hosts.rs` (`Policy`, migration), `tests/approval.rs`.
+- **C9 — Self/loopback can't dodge local policy.** A request naming any loopback
+  alias of the daemon's own machine (`localhost`, `127.0.0.0/8`, `::1`,
+  `localhost.`, the machine's own hostname) routes to the *local* path, not an
+  SSH tunnel, and a local unprivileged command is refused (delegated to the Bash
+  tool). *Attack:* make `execute(host="127.0.0.1")` (or `::1`, or the own
+  hostname) open an SSH-to-self tunnel, or slip a local unprivileged command past
+  the Bash-delegation refusal. → `src/server.rs` (`is_local_host`), `src/mcp.rs`
+  (`normalize_host`, `execute`).
+- **C10 — Backstop composition (soundness).** `is_local_host` is best-effort, so
+  an *undetectable* self-alias (ssh-config alias, NAT hairpin) may still route
+  SSH-to-self. That cannot yield unattended exec, because C8 holds on *every*
+  daemon: the tunnel lands on a daemon whose only unattended path is the
+  eligible + session-confirmed grant. *Attack:* find a host string that is really
+  the local box, escapes C9, *and* runs unprivileged unattended. → composition of
+  `src/mcp.rs` routing and `src/server.rs` dispatch.
+
 ## The trust boundary (what to actually read)
 
 The security-critical path is four files; almost everything else (the MCP
@@ -104,9 +145,17 @@ what carries **no proof**, roughly in order of how much it worries us:
 5. **`base64` / `serde_json` decoding.** Panic-freedom of the decode paths rests
    on the upstream crates' `Result`-returning APIs and our `.unwrap()`-free call
    sites — an assumption, not a proof.
-6. **Auto-approve, if ever enabled.** The "remember this command" surface (audit
-   finding F2) is off by design; the moment it exists, prefix-matching escapes
-   become live. → `docs/architecture.md` allowlisting note.
+6. **The unattended window on an eligible daemon.** The old persisted, global
+   auto-approve (finding F2) is gone. What remains is bounded: on a daemon an
+   operator has *deliberately* made `unattended_eligible`, one `a` keypress opens
+   a session-scoped, non-persistent window in which unprivileged commands run
+   with only an audit-log line. Inside that window the gate is the operator's
+   two prior decisions (the config edit and the `a` press) plus the audit log —
+   there is no per-command human check. We judge this at Bash parity (a Bash
+   allow-rule is a similar, and less bounded, operator opt-in), but the window is
+   real: an operator who enables eligibility and presses `a` on a hostile-looking
+   command is not protected by the code. → `src/server.rs` dispatch, finding F2
+   in `docs/security-audit.md`.
 
 ## Run it in a container
 

docs/architecture.md

@@ -30,11 +30,14 @@ Functional but minimal.
 - TUI approval prompt + sudo for privilege escalation (local and remote)
 - Non-privileged mode (direct execution, no escalation) — also TUI-gated by default
 - `--verbose` / `-v` on server: prints startup info, logs each request
-- Per-host policy in `hosts.json`: pressing `a` at an unprivileged prompt
-  writes `policy.confirm_unprivileged=false` so the daemon skips the gate
-  on this host from then on
-- `--no-confirm-unprivileged` / `--confirm-unprivileged` on server:
-  explicit overrides of the persisted policy
+- Per-daemon policy in `hosts.json` (`policy.unattended_eligible`, default
+  false): whether the daemon may offer the session-scoped `a` answer. Read once
+  at startup, immutable at runtime — an out-of-band operator opt-in (invariant
+  G7, barrier 1). Pressing `a` on an eligible daemon flips an in-memory,
+  never-persisted session grant (barrier 2); on a non-eligible daemon `a`
+  approves just the one command
+- `--unattended-eligible` on server: makes the daemon eligible without editing
+  the file (the session grant still needs the `a` keypress and is never persisted)
 - `--no-privilege` on client: sends request with `privileged: false`
 - `--host` flag on server: SSHs into remote, starts sudo-proxy, tunnels socket (used by MCP `start_server`)
 - `--print` mode for human-readable output on stdout

docs/assurance-case.md

@@ -37,6 +37,10 @@ asserted, evidence not yet produced).
 > **G1 — Nothing privileged runs without a human deliberately approving the
 > exact command shown.**
 
+> A second, parallel top-level invariant **G7** (below) guards the *unprivileged*
+> surface: no unprivileged command runs with less scrutiny than the agent's Bash
+> tool. G2–G6 decompose G1; G7 stands beside it with its own sub-goals.
+
 ```
                                   ┌──────────────────────────────────────┐
    C1 TOE: daemon + MCP server    │  G1  No privileged execution without  │
@@ -124,8 +128,8 @@ keypress binds to the command shown.*
 | **Sn5.1** | TLC-checked: the `PolicyFlipsOnlyOnKeypress` invariant of [`proofs/tla/`](../proofs/tla/) proves the policy flag flips only via an interactive `a` keypress on an unprivileged request — never a request field, replay, MCP flag, or timeout — over all attacker forgeries/replays and operator choices. `src/server.rs`. | 4 | [discharged] (model-checked) |
 | **G5.2** | The prompt reads a single keypress in non-canonical mode and times out after 60 s (default **deny**). | — | |
 | **Sn5.2** | `src/tui.rs` prompt; timeout test. | 1 | [discharged] |
-| **G5.3** | The `confirm_unprivileged=false` policy relaxes only the **non-privileged** gate, never the privileged one, and only via an interactive `a` keypress. | — | |
-| **Sn5.3** | TLC-checked: `NoExecWithoutApproval` + `PrivilegedGateIndependentOfPolicy` ([`proofs/tla/`](../proofs/tla/)) prove the privileged gate requires a `y` keypress for *any* value the policy flag took, so `confirm_unprivileged` relaxes only the non-privileged gate. Audit finding **F2** by-design trade-off still documented; `display_banner` reliability is a separate backlog item. | 4 | [discharged] (model-checked) |
+| **G5.3** | No policy value relaxes the **privileged** gate: `privileged:true` requires a `y` keypress regardless of `unattended_eligible` or the session grant. | — | |
+| **Sn5.3** | TLC-checked: `PrivilegedGateIndependentOfPolicy` ([`proofs/tla/`](../proofs/tla/)) proves the privileged gate requires a `y` keypress for *any* eligibility/grant state. The *unprivileged* side (eligibility + session grant) is the second invariant **G7** below. | 4 | [discharged] (model-checked) |
 
 ### G6 — Adversary cannot bypass the gate
 
@@ -142,6 +146,21 @@ keypress binds to the command shown.*
 | **G6.4** | Resource exhaustion cannot force-open the gate: 1 MiB request cap, 64 in-flight, 16 MiB output cap. | — | |
 | **Sn6.4** | `src/server.rs`, `src/executor.rs`; cap test (flaky **S2**, control sound). | 1–2 | [partial] |
 
+### G7 — No unprivileged command runs with less scrutiny than the Bash tool
+
+*Every unprivileged command faces a live human gate unless an operator made its
+host eligible out-of-band AND a human confirmed the session; and a self/loopback
+target cannot route around that gate.*
+
+| Node | Claim / Evidence | Rung | Status |
+|------|------------------|------|--------|
+| **G7.1** | No unprivileged command runs unattended except behind two barriers — `unattended_eligible` (config-only, immutable at runtime) AND an in-session `a` keypress — and the grant is never persisted. | — | |
+| **Sn7.1** | `tests/approval.rs` (`every_unprivileged_request_is_prompted_when_not_eligible`, `non_eligible_approved_always_grants_nothing`, `eligible_approved_always_grants_session_but_never_persists`); `src/hosts.rs` (`stale_confirm_unprivileged_key_is_inert`). TLC: `NoUnattendedUnprivilegedExec` ([`proofs/tla/`](../proofs/tla/)). Closes audit **F2**. | 2, 4 | [discharged] |
+| **G7.2** | No persisted policy value enables unattended execution on load (fail-closed default; stale `confirm_unprivileged` inert). | — | |
+| **Sn7.2** | `src/hosts.rs` serde tests; `Policy::default` is `unattended_eligible=false`. | 2 | [discharged] |
+| **G7.3** | A self/loopback target is classified local and cannot route SSH-to-self around local policy; local unprivileged is delegated to the Bash tool. Soundness of undetected aliases rests on G7.1 holding on every daemon (C10). | — | |
+| **Sn7.3** | `src/server.rs` (`is_local_host_classifies_self_and_loopback`), `src/mcp.rs` (`normalize_host_folds_loopback_to_local`). Closes audit **F5**. | 2 | [discharged] |
+
 ## Open items tracked against the case
 
 These are the leaves where the argument is currently weakest, drawn from
@@ -158,9 +177,12 @@ These are the leaves where the argument is currently weakest, drawn from
   authenticity to client auth.
 - **Sn6.4 / S2** — stabilise the flaky resource-cap test so the cap stays
   covered in CI.
-- **Sn4.4 / Sn5.3** — accepted residual risks (look-alike `reason`, the
-  `confirm_unprivileged` trade-off); revisit if an auto-approve surface is ever
-  added (see the [allowlisting note](architecture.md#design-note-allowlisting-when-it-lands)).
+- **Sn4.4** — accepted residual risk (look-alike `reason`).
+- **G7.1 residual** — the bounded unattended window on an eligible daemon after an
+  `a` keypress (audit **F2**, now closed but with a characterised residual);
+  judged at Bash-allow-rule parity. Revisit if a command allowlist / auto-approve
+  surface is ever added (see the
+  [allowlisting note](architecture.md#design-note-allowlisting-when-it-lands)).
 
 ## How to use this document
 

docs/formalisation-roadmap.md

@@ -126,8 +126,11 @@ specification:
 - `shell_escape` round-trips through `/bin/sh` byte-for-byte;
 - every field displayed at the approval prompt is dangerous-char-free;
 - `privileged:true` ⇒ an interactive keypress occurred before exec;
-- the `confirm_unprivileged` policy flag is flippable *only* by an interactive
-  keypress, never by a request field.
+- unattended unprivileged execution requires both `unattended_eligible` (config-
+  only, never set from the wire) and an in-session `a` keypress, and the grant is
+  never persisted (invariant G7 / C8); a stale `confirm_unprivileged` key is inert;
+- self/loopback host targets are classified local and cannot route SSH-to-self
+  (G7 / C9), tested by `is_local_host`'s truth table.
 
 This is the cheap bridge to formal methods: these properties become the proof
 obligations for the higher rungs.
@@ -209,10 +212,12 @@ half with a stable-Rust typestate (rationale below).
 The most interesting properties are temporal and relational, not per-function:
 
 - Model the **approval state machine** — request → freshness check → dedup →
-  prompt → keypress → exec, plus the `confirm_unprivileged` policy transition
-  (finding F2) — in **TLA+/PlusCal** or **Alloy**, and model-check: replay is
-  impossible; no exec without approval; the policy flag transitions *only* on an
-  interactive keypress (never via a request field, replay, or MCP tool flag).
+  prompt → keypress → exec, plus the unprivileged eligibility + session-grant
+  transitions (invariant G7, finding F2) — in **TLA+/PlusCal** or **Alloy**, and
+  model-check: replay is impossible; no exec without approval; eligibility is a
+  runtime-immutable input; and `NoUnattendedUnprivilegedExec` — an unprivileged
+  command runs unattended only when eligible AND a prior in-session `a` keypress
+  occurred, with the grant reset at the session boundary (never persisted).
 - For the A3 / SSH-tunnel path, model freshness + replay + channel assumptions
   in the symbolic-protocol provers **Tamarin** or **ProVerif**. These are the
   standard instruments for "what does the tunnel actually guarantee," and they

docs/mcp.md

@@ -26,6 +26,13 @@ sudo-proxy as tools over stdio JSON-RPC. Any MCP-capable AI client
 - `privileged`: whether to escalate privileges (default `true`).
 - `env`: environment variables to pass.
 
+> **Local unprivileged commands are refused.** A request with `privileged: false`
+> that targets the local machine (including loopback aliases such as `127.0.0.1`,
+> `::1`, or this host's own name) is declined with a message pointing the agent
+> back to its Bash tool, which already applies the client's permission rules
+> (invariant G7). sudo-proxy runs privileged commands (local and remote) and
+> unprivileged commands on remote hosts.
+
 **`update_host`** — record metadata about a known host.
 - `host` (required): hostname to update.
 - `description`: human-readable description (e.g. "CI server").