Skip to content

Fix four spec-conformance gaps (FW-ENV2, FW-TRA7, FW-INV5, FW-GW3) - #28

Open
brianv0 wants to merge 2 commits into
mainfrom
claude/spec-fix-clearcut
Open

Fix four spec-conformance gaps (FW-ENV2, FW-TRA7, FW-INV5, FW-GW3)#28
brianv0 wants to merge 2 commits into
mainfrom
claude/spec-fix-clearcut

Conversation

@brianv0

@brianv0 brianv0 commented Jul 30, 2026

Copy link
Copy Markdown
Owner

This PR addresses a spec-review finding of four verified spec-conformance gaps. Each fix ships with a test.

FW-ENV2 — default secret-shaped env scrub missed KEY and CERT

crates/formwork-blueprint/src/lib.rsNAME_MARKERS listed the narrower APIKEY/API_KEY/ACCESS_KEY/PRIVATE_KEY shapes but not the bare KEY the spec names normatively (TOKEN|SECRET|PASSWORD|KEY|AUTH|CREDENTIAL|CERT), and had no CERT. Replaced the *KEY entries with KEY (which subsumes them via the contains match) and added CERT. Test asserts SIGNING_KEY, DEPLOY_KEY, CLIENT_CERT, TLS_CERT are scrubbed by name while an allowlisted var survives.

FW-TRA7 — default write-subtract missed shell-rc files and .claude

profiles/default.toml — added **/.claude/** and the shell rc files (**/.bashrc, **/.zshrc, **/.zshenv, **/.bash_profile, **/.profile) to the write-subtract set. They are write-denied but stay readable (the FW-TRA7 point). Test asserts the resolved default profile's write-subtract set includes a shell-rc entry and .claude.

FW-INV5 / FW-XR1 — macOS fidelity over-claimed, ignoring host.seatbelt

crates/formwork-compile/src/lib.rscompile_macos inserted Enforced{Seatbelt} for FsRead/FsWrite/NetDefaultDeny/CrossDomainSocket unconditionally, unlike compile_linux which gates on host capabilities. Now gated on host.seatbelt; when false the caps report Unenforceable{reason}, mirroring the Linux no-Landlock branch. Test compiles with seatbelt=false and asserts the caps are Unenforceable, not Enforced.

FW-GW3 / FW-INV4 — gateway forwarded unshaded MCP methods

crates/formwork-gateway/src/lib.rsresources/subscribe, resources/unsubscribe, and completion/complete fell through to Frame::Passthrough and reached the backend unchecked. Added Frame::ResourceSubscribe and Frame::Completion variants: subscribe/unsubscribe gate on the resource axis by uri (oracle-free "resource not found", like resources/read); completion/complete gates on the referenced ref (ref/prompt by name on the prompt axis, ref/resource by uri on the resource axis), refusing oracle-free when ungranted. Fixture gained granted-path handlers. Test asserts an ungranted resource cannot be subscribed and an ungranted completion is refused, indistinguishable from a nonexistent one (FW-ADV-004), while granted paths round-trip.

Verification

cargo fmt --all, cargo clippy --workspace --all-targets --locked -- -D warnings, and cargo test --workspace --locked are all green; py suite (uv run pytest -q) passes (32 passed, 28 enforcement tests skipped on this Landlock-less host).

🤖 Generated with Claude Code

https://claude.ai/code/session_016Qk2hVoLeB2HCzukqCGKFB


Generated by Claude Code

claude added 2 commits July 30, 2026 16:06
Addresses a spec-review finding of four verified conformance gaps:

- FW-ENV2: the default env scrub's NAME_MARKERS omitted the bare `KEY`
  and `CERT` shapes the spec names normatively. Replace the narrower
  `APIKEY/API_KEY/ACCESS_KEY/PRIVATE_KEY` entries with `KEY` (which
  subsumes them via the `contains` match) and add `CERT`.

- FW-TRA7: the default profile's write-subtract set missed the
  shell-rc files and the `.claude` agent-config dir the spec names as
  tamper vectors. Add `**/.bashrc`, `**/.zshrc`, `**/.zshenv`,
  `**/.bash_profile`, `**/.profile`, and `**/.claude/**` (write-denied
  but readable).

- FW-INV5/FW-XR1: compile_macos claimed Enforced{Seatbelt} for
  FsRead/FsWrite/NetDefaultDeny/CrossDomainSocket unconditionally,
  unlike compile_linux. Gate them on host.seatbelt, reporting
  Unenforceable when absent, mirroring the Linux no-Landlock branch.

- FW-GW3/FW-INV4: the gateway let resources/subscribe,
  resources/unsubscribe, and completion/complete fall through to
  Passthrough and reach the backend unchecked. Classify and shade them:
  subscribe/unsubscribe gate on the resource axis by uri;
  completion/complete gates on the referenced ref (ref/prompt by name,
  ref/resource by uri). Refusals stay oracle-free (FW-ADV-004).

Each fix carries a unit/integration test; fmt, clippy, and the Rust and
Python suites are green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016Qk2hVoLeB2HCzukqCGKFB
compile_macos gated FsRead/FsWrite/NetDefaultDeny/CrossDomainSocket on
host.seatbelt via a fidelity(reason) helper, but still reported the
NetPortTier (NetPosture::Ports) and Exec (ExecPosture::Allowlist) caps
Enforced{Seatbelt} unconditionally through a leftover seatbelt() closure.
On a macOS host without Seatbelt that is a silent over-claim -- a
fail-open-silent violating FW-INV5 ("anything reported Enforced is
enforced") and FW-XR1 -- while compile_linux correctly gates both.

Route NetPortTier and Exec through the same has_seatbelt-gated fidelity()
helper and delete the now-unused seatbelt() closure. All six macOS caps
now degrade to Unenforceable when Seatbelt is absent.

Strengthen the report-soundness test to a paired allow/deny check over a
blueprint carrying both a direct port tier and an exec allowlist (plus
fs reads/writes), so all six Seatbelt-carried caps are asserted
Unenforceable when seatbelt == false and Enforced{Seatbelt} when true.

Tidy a comment: the FW-ENV2 NAME_MARKERS array also retains PASSWD, which
is not in the normative enumeration; note it accordingly (no behavior
change).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016Qk2hVoLeB2HCzukqCGKFB
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants