From 5b7fd70124013eeb09f210115384658927d635ae Mon Sep 17 00:00:00 2001 From: Hong Jiarong Date: Wed, 8 Jul 2026 12:37:37 +0800 Subject: [PATCH] =?UTF-8?q?spec:=20=E9=92=89=E6=AD=BB=20agent=20=E6=89=A7?= =?UTF-8?q?=E8=A1=8C=E9=9D=A2=E8=BE=B9=E7=95=8C(ADR-0018)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ADR-0001/0002/0004 覆盖协作治理到 triggerAgent,但触发后 agent 在执行层 能干什么——读哪些文件、跑什么命令——无 ADR / spec 覆盖。ADR-0017 落地时 采用 bypassPermissions + 全量内置工具,agent 文件/shell 面对宿主无界; workspace.ts 的 confine() 沙箱意图存在但被 ADR-0017 静默覆盖成死代码。 新增 ADR-0018 + Spec.System.AgentSurface 模块补这一层: - AgentFileOp(run × path)+ Authorized 谓词(路径必须落在 run 工作区内) - 与 Lock 正交:Lock 限定并发,Surface 限定波及面,都按 run × project 作用域 - 机制 OPEN(工具包装 / OS 沙箱 / SDK 钩子),契约只钉不变式 - ADR-0017 的 bypassPermissions + workspace.ts 死代码标为偏离契约,对齐为 follow-up --- ...-execution-surface-bounded-by-workspace.md | 136 ++++++++++++++++++ spec/Spec/System.lean | 6 +- spec/Spec/System/AgentSurface.lean | 44 ++++++ 3 files changed, 184 insertions(+), 2 deletions(-) create mode 100644 docs/adr/0018-agent-execution-surface-bounded-by-workspace.md create mode 100644 spec/Spec/System/AgentSurface.lean diff --git a/docs/adr/0018-agent-execution-surface-bounded-by-workspace.md b/docs/adr/0018-agent-execution-surface-bounded-by-workspace.md new file mode 100644 index 0000000..462c272 --- /dev/null +++ b/docs/adr/0018-agent-execution-surface-bounded-by-workspace.md @@ -0,0 +1,136 @@ +# ADR 0018: The Agent Execution Surface Is Bounded By The Project Workspace + +## Status + +Accepted. The decision is pinned; alignment of the current Hub +implementation to it is a follow-up surfaced below (constitution rule 4: +implementation diverging from contract must be surfaced, not silently kept). + +Builds on **ADR-0001** (project group as collaboration space), **ADR-0002** +(project lock scoped to `run_id`), **ADR-0004** (permission grants govern +`triggerAgent`), **ADR-0007** (the engineering file is a directory tree on +disk), and **ADR-0017** (Claude Code SDK as the agent runtime). + +## Context + +ADR-0001/0002/0004 together cover *collaboration governance* up to the +moment a teacher `@Claude`s: who may trigger an `AgentRun`, that the run +holds a project-scoped lock, that the group is a long-lived space. They stop +at `triggerAgent`. What the agent may do *after* the trigger — which files it +may read or write, what commands it may run — is not named in any ADR, not +modeled in `spec/`, and not enforced by any contract-level invariant. + +The gap is not theoretical. ADR-0017 adopted the Claude Code SDK with +`allowedTools: ["Read", "Write", "Bash", "Glob", "Grep"]` and +`permissionMode: "bypassPermissions"`. Under that configuration the SDK's +built-in tools operate over the whole host filesystem with no confinement, and +`Bash` executes arbitrary shell with no approval gate. The Hub's +`hub/src/agent/workspace.ts` was *intended* to be "the agent's only file +surface" (its module doc says so) and ships a `confine()` path validator that +rejects `..` and absolute escapes. But ADR-0017's cutover left those custom +tools unwired — the SDK's built-in tools replaced them — so `confine()` is +dead code and the boundary it was meant to enforce does not exist at runtime. +Compounding this, the systemd unit's default `SERVICE_USER` is `root` +(`hub/deploy/install_service.sh`), so the unbounded agent runs as root. + +This is a real divergence point by the constitution's test: "if unwritten, +will the developer and the agent make different assumptions?" They already +have. ADR-0017 assumed the boundary was an implementation concern; the +`workspace.ts` author assumed it was a contract. The next person to touch the +runner has nothing telling them the boundary must be enforced, and ADR-0017 +silently overrode the one that existed. + +## Decision + +### The agent execution surface is bounded by the run's project workspace + +During an `AgentRun`, every file operation the agent performs — read, write, +glob, grep target — must fall **within the run's project workspace directory** +(the on-disk engineering-file tree of ADR-0007). Operations whose target path +escapes that tree are refused. This is a platform core invariant, pinned in +`Spec.System.AgentSurface`. + +The boundary is **per-run, anchored to the run's project**, the same scope as +the Lock (ADR-0002). This keeps the two invariants composable: + +- `Lock` (ADR-0002) bounds **concurrency** — who may be modifying the project. +- `AgentSurface` (this ADR) bounds **blast radius** — what the agent may touch. + +Both scope to `run × project`. Acquiring the lock and entering the surface +happen together at run start; releasing the lock and leaving the surface +happen together at run termination. + +### Shell execution is subject to the same boundary, by effect + +A shell command the agent runs executes with the workspace as its working +directory (already true for the `cph` subprocess, ADR-0016) and its **file +effects** — files read, written, created, or deleted — are subject to the same +workspace boundary. The agent may invoke **named external tools** whose +binaries live outside the workspace (notably `cph` via `CPH_BIN`); the +boundary governs *file effects*, not *binary location*. Arbitrary +`cat /etc/shadow` or `curl … > /etc/...` is out of bounds regardless of how it +is invoked. + +### The Hub process runs as a non-privileged service user + +The systemd unit must not run as `root`. The default in +`hub/deploy/install_service.sh` changes from `root` to a dedicated unprivileged +user. This is a deployment invariant, recorded here because the unbounded-agent +risk is compounded by root; it is enforced in the unit, not in `spec/` (it is +not a semantic divergence between developer and agent — it is operational +discipline). + +### The mechanism is deliberately left open + +How the boundary is *enforced* — path validation inside tool wrappers (the +`workspace.ts` `confine()` shape), an OS-level sandbox (bubblewrap / container +/ chroot), the SDK's own permission hooks, or some combination — is `OPEN`. +The contract pins the **invariant** (operations stay in the workspace), not +the **mechanism**. Any mechanism that upholds the invariant satisfies the +contract; switching mechanisms is not a spec change. + +## Consequences + +- `Spec.System.AgentSurface` gains an `AgentFileOp` structure and an + `Authorized` predicate mirroring `Memory.McpReadRequest.Authorized`: the op + carries a `run` and a `path`; `Authorized` holds iff the path falls within + the run's workspace, via platform-provided `runWorkspace` and `pathWithin` + (representations `OPEN`). +- `hub/src/agent/workspace.ts`'s `confine()` intent is now contract-backed. + Re-wiring it (or replacing it with an OS sandbox) is **mandatory**, not a + preference. Its current dead-code status under ADR-0017 is a divergence to + be addressed, not silently retained. +- ADR-0017's `bypassPermissions` + unrestricted built-in tools is a + **divergence from this ADR** and is surfaced as such (constitution rule 4). + The reconciliation — restrict the SDK tool set, wrap Bash, or sandbox at the + OS level — is the open mechanism question above. Whichever is chosen must + uphold the `AgentSurface` invariant. +- Inbound file/image delivery (`hub/src/feishu/trigger.ts`) lands files under + `${workspaceDir}/.cph/inbox/`, which is inside the boundary — consistent, no + change to the delivery path. +- The `cph` subprocess (ADR-0016) already runs with `cwd = workspaceDir` + (`hub/src/agent/cph.ts`), so it is inside the boundary by construction. +- Force-release of a stuck lock (ADR-0002 admin override) does not cross the + surface boundary — it is a lock-table operation, not an agent operation. + +## Open Questions / Deferred + +- **Enforcement mechanism.** Tool-wrapper path validation vs OS-level sandbox + (bubblewrap/container) vs SDK permission hooks vs a combination. The + contract pins the invariant; this picks the mechanism. Must be resolved + before production, since the current mechanism is "none". +- **`bypassPermissions` reconciliation.** Whether the Claude Code SDK can be + configured to confine its built-in Read/Write/Glob/Grep to a subtree and to + gate Bash, or whether the Hub must re-introduce custom tools wrapping + `confine()`, is the concrete implementation question ADR-0017 left open and + this ADR now forces. +- **Shell command vocabulary.** Whether the agent's Bash is restricted to a + whitelist (e.g. `cph`, `ls`, `grep`) or allowed arbitrary commands whose + *effects* are then confined, is a policy choice left to implementation. The + invariant governs effects either way. +- **Per-user rate limiting and token budgets.** Orthogonal to the surface + boundary (this ADR is about *what* the agent may touch, not *how often* it + may run). Deferred to a separate concern. +- **Inbound file size / MIME limits.** The inbox lives inside the boundary, + but unbounded file size is a DoS vector distinct from the boundary + invariant. Deferred. diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean index f400a98..1b7f6bc 100644 --- a/spec/Spec/System.lean +++ b/spec/Spec/System.lean @@ -2,10 +2,10 @@ import Spec.System.ProjectGroup import Spec.System.Run import Spec.System.Lock import Spec.System.Memory +import Spec.System.AgentSurface import Spec.System.Permission import Spec.System.PermissionGrant import Spec.System.Audit - /-! # System —— Hub 平台层契约 @@ -17,10 +17,12 @@ import Spec.System.Audit - `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。 - `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。 - `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。 +- `AgentSurface` —— agent 执行面被 run 的工作区所界定(ADR-0018);与 Lock 正交—— + Lock 限定并发,Surface 限定波及面。机制 OPEN。 - `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。 - `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构 (ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。 - `Audit` —— 有意从简(内容多为 plumbing,OPEN)。 -标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004。 +标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018。 -/ diff --git a/spec/Spec/System/AgentSurface.lean b/spec/Spec/System/AgentSurface.lean new file mode 100644 index 0000000..64c215f --- /dev/null +++ b/spec/Spec/System/AgentSurface.lean @@ -0,0 +1,44 @@ +import Spec.Prelude +import Spec.System.Run + +/-! +# AgentSurface —— Agent 执行面边界(ADR-0018) + +ADR-0001/0002/0004 覆盖"协作治理"直到 `triggerAgent`:谁能触发一次 run。但触发之后 +agent 在执行层面能干什么——读哪些文件、跑什么命令——任何 ADR / 散文都未定。ADR-0017 +落地时采用 Claude Code SDK 的 `bypassPermissions` + 全量 Read/Write/Bash/Glob/Grep, +agent 的文件与 shell 面对宿主**无界**:spec 与 ADR 均未钉死边界。本模块补这一层。 + +钉死的不变式:agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project +的工作区目录内(ADR-0007:工程文件是目录树;此 ADR 固定"agent 操作落在该树内")。 +逃逸即越权,拒绝。与 `Lock`(ADR-0002)正交:Lock 限定**并发**(谁在改),Surface +限定**波及面**(能改到哪)。二者都按 run × project 作用域。 + +shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论,但**机制** +——路径校验工具包装、OS 级沙箱(bubblewrap/容器)、SDK 权限钩子,或其组合——`OPEN` +(ADR-0018)。契约钉死不变式,不钉死机制。 +-/ + +namespace Spec.System + +variable (I : Identifiers) (Path : Type) + +/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、 +指向某路径;是否越权由下方 `Authorized` 钉死。 -/ +structure AgentFileOp where + /-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/ + run : I.RunId + /-- 操作目标路径(`PINNED` 字段, ADR-0018)。 -/ + path : Path + +/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内 +(`PINNED` 平台核心安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 均由平台提供 +(表示 `OPEN`——路径如何表示、"在内"如何判定是纯 plumbing,非本层分歧点);本谓词只 +钉死"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写宿主任意文件。 -/ +def AgentFileOp.Authorized + (op : AgentFileOp I Path) + (runWorkspace : I.RunId → Option Path) + (pathWithin : Path → Path → Prop) : Prop := + ∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w + +end Spec.System