Progent enforces symbolic restrictions on tool calls and checks whether policy updates narrow or expand an agent's executable permissions.
Tool-using agents need enough authority to complete a legitimate task, but instructions inside retrieved content can redirect that authority toward an attacker's objective. A policy inferred only at the start may lack values learned later, while unrestricted policy updates can let untrusted observations expand the agent's permissions.
Progent addresses this tension by separating language-model policy generation from deterministic enforcement. Its protected interface is the tool call and its arguments; attacks confined to textual answers or actions that bypass the instrumented tool interface are outside that enforcement boundary.
A policy language with allow and forbid rules over tool identifiers and argument conditions, plus explicit handling of blocked calls.
An SMT-based comparison that determines whether a proposed policy permits any call previously forbidden.
An execution architecture supporting task-derived initialization, contextual updates, configurable expansion approval, and library or MCP-proxy integration.
A policy model receives the trusted user request and tool definitions and constructs the initial rule set. At runtime, a deterministic checker evaluates every proposed call against rules for its tool, including restrictions on argument values and structured fields. A denied call can terminate execution, request user involvement, or return feedback that lets the agent try another approach.
Updates are proposed in two stages. The system first decides whether an update may be useful without exposing that decision to the new tool result. If needed, the policy model then receives the fuller context and proposes revised rules. The model's proposal is not itself the enforcement decision.
The SMT check compares the sets of calls allowed before and after the update. A subset is applied automatically; an expansion goes to an approver. Approvers can deny, automatically accept, apply tool-specific rules, or involve a human. Thus, the formal confinement property describes narrowing between approved expansions, and does not certify the initial policy's interpretation of intent.
AgentDojo and Agent-SafetyBench supply tool-using tasks and adversarial settings. Comparisons include an unprotected agent and prior defenses, measuring legitimate utility without attack, utility during attack, and attacker-objective completion as distinct quantities.
Ablations fix the initial policy or vary expansion handling to isolate the role of updates and approval. Version 3 uses Auto-Approve by default, while human review is a separate condition. Model sweeps distinguish the policy generator from the acting agent. Integration studies examine existing agents, and runtime measurements assess policy generation, checking, and updates.
Open this note in the interactive notebook (comments, hooks) → · All notes