Flowproof Guard: runtime enforcement — design doc + P0 trust boundary

[AminChirazi]

Flowproof Guard: runtime policy enforcement for AI agents (design + P0)

Status: direction change — requires a charter amendment first

Flowproof's charter defines the mission as testing (record once, replay
forever). Guard extends that mission to runtime enforcement in production:

Test → Verify → Guard → Observe → production-derived regression → Test

Per CHARTER.md, changing direction is a human act done in the charter, and no
loop may take this work until an amendment lands. This issue is therefore:

1. the request for that amendment,
2. a design doc to be committed under docs/guard-design.md, and
3. one scoped P0 implementation issue (below).

Licensing (per resolved DECIDE 1): everything in this repo is Apache-2.0,
including Guard. The commercial boundary stays outside the repo (appliance,
hosted evidence archive, services). Building Guard here means open-sourcing it —
intended, and stated so it is a decision rather than a discovery.

Why Guard is a natural extension, not a pivot

Flowproof already enforces at runtime — in the test phase:

Exists today (test-time)	Guard makes it production-time
allow_egress + seccomp default-deny (kernel refuses undeclared destinations)	network policy enforcement
assert_no_tool_call (forbidden call fails the build)	tool policy: BLOCK before execution
controls + audit --since (a guarantee re-proved every commit)	policy decisions as signed evidence
cassette = ground truth, human-only mutation	tamper-evident decision records
"mechanism enforces, not instruction" (README)	an LLM is never the root of trust

The core principle carries over unchanged: authorization, deny rules, limits,
and destructive-action controls are enforced deterministically. LLMs may
classify, explain, and flag — never decide.

Design doc contents (docs/guard-design.md)

The full design from the original issue draft moves there, organized as:

1. Trust architecture — agent, its LLM, user input, retrieved content, tool
   output, and MCP output are untrusted by default. The agent under protection
   must not be able to modify its judge, its policies, or the evidence.
2. Policy model — allow / deny / constraints / limits / approval-required,
   governing tools, MCP servers, endpoints, methods, filesystem, browser, SAP
   operations, value thresholds, call counts. Expressed in flow-spec-style YAML
   (reuse existing configuration conventions; the spec's controls/
   allow_egress blocks are the seed, not a parallel system).
3. Enforcement flow — pre-action interception → deterministic evaluation →
   ALLOW / BLOCK / REVIEW, every verdict with a machine-readable decision
   record naming the rule, policy version, verifier version, and identity.
4. Verifier boundary — separate credentials for agent / capture / verifier /
   policy admin / approver; least privilege; the agent can never reach keys.
5. Evidence — append-only, hash-chained where appropriate, signed verdicts,
   policy-version references. Never claim tamper-proof where the deployment
   only provides tamper-evident.
6. Flywheel — verified test behavior proposes production policy (human
   promotes, never auto); blocked production behavior becomes a regression flow
   via flowproof convert (Production → test: side-effect capture, behavioral fingerprints, and run conversion #465). This is the differentiator.
7. LLM evaluator isolation & prompt-injection resilience — optional semantic
   evaluators: no write permissions, structured inputs, strict output schemas,
   recorded identity/version; a hard security failure cannot be overridden by an
   LLM PASS. Assume traces contain adversarial text targeting Guard itself
   (invariant 10 already takes this stance for cassettes).
8. Fail-safe semantics — explicit behavior per failure mode (Guard down,
   policy unavailable, signature invalid, timeout); risk tiers so read-only
   paths survive an outage while consequential ones fail closed.
9. Boundaries — integrate with SIEM/IAM/APM, never rebuild them. Guard owns
   exactly: can this agent safely perform this action, and can we prove why we
   allowed or blocked it?
10. Future — hardware-backed keys, attestation, the Guard appliance. Design
    interfaces so this is possible; require none of it. (Appliance branding uses
    canonical assets from automators-com/design-system; never redraw the mark.)

P0 — trust boundary (the implementable slice)

New crate flowproof-guard (versions move together, invariant 6):

• policy domain model + YAML deserialization (extending spec conventions)
• deterministic policy evaluator: (action, context, policy) → ALLOW/BLOCK/REVIEW
  — pure function, property-tested, no I/O
• decision record type: rule matched, policy@version, verifier@version,
  agent identity, timestamp — machine- and human-readable
• enforcement hook at the existing tool-call boundary in flowproof-agent
  (where assert_no_tool_call already observes) — BLOCK rejects before execution
• fail-safe: evaluator error on a protected action ⇒ BLOCK, recorded
• adversarial tests: agent attempts policy write, evidence write, fake
  Guard metadata in agent output, policy precedence conflicts, fail-open
  regression (these are integration tests; unit tests would give false
  confidence)

P0 definition of done — with a purchasing-agent example policy:
create_purchase_order(value=1200) → ALLOW with a decision record naming the
rule; modify_vendor_bank_account(...) → BLOCK before execution, decision
record emitted, and a regression flow is derivable from the blocked event.

Sequencing

• P0 (this issue): policy model, evaluator, decision records, tool-boundary
  enforcement, fail-safe, adversarial tests.
• P1: signed decision records, approval binding (approval tied to the exact
  action+input, not substitutable), REVIEW workflow, drift detection on
  fingerprints from Production → test: side-effect capture, behavioral fingerprints, and run conversion #465.
• P2: flywheel — test evidence → proposed policy (human-promoted); blocked
  production event → flowproof convert regression.
• P3: hardware-backed trust, attestation, appliance profile. No hardware
  work before P0–P2 are proven.

Depends on #465 (side effects, fingerprints, convert). P0 depends only on the
tool-call boundary, which ships today — it can start once the charter amendment
lands.

Constraints

• Deterministic evaluator; zero model calls on the enforcement path.
• Small PRs (~400 lines); every capability lands with the adversarial test
  that proves it holds.
• No weakening of existing gates; Guard adds boundaries, never relaxes one.
• Enforcement guarantees are documented per adapter — do not pretend every
  environment supports pre-execution blocking at the same layer.