Source-linked AI summary
Towards Verifiably Safe Tool Use for LLM Agents
Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos, Christian Kästner
TL;DR
LLM agents can create unsafe multi-tool interactions that existing probabilistic safeguards cannot guarantee against. This paper combines STPA-based hazard analysis with formal data-flow and tool-sequence specifications, supported by structured MCP labels, and reports that Alloy verification can eliminate unsafe flows while retaining safe traces. It frames autonomy as configurable and cautions that high-stakes settings may warrant limited or no agent autonomy.
Problem
Unconstrained tool composition can produce unsafe data flows and actions, while existing safeguards lack guarantees and IFC approaches often require costly or unreliable labels.
Method
The paper applies STPA to identify hazards and derive requirements, formalizes them as information-flow and temporal specifications, and extends MCP with structured labels.
Results
Alloy analysis confirms that enforced policies and sanitation steps prevent safety violations for the modeled tools while safe traces remain.
Takeaways & Limitations
Autonomy can be configured through explicit policies so users are prompted for decisions that may cause actual loss rather than every tool call.
Takeaways & Limitations
Safety-critical or high-stakes settings may require very limited autonomy or excluding agents altogether.
Abstract
from arXiv · showhide
Large language model (LLM)-based AI agents extend LLM capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents. While this empowers agents to perform complex tasks, LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records, which are unacceptable in enterprise contexts. Current approaches to mitigate these risks, such as model-based safeguards, enhance agents' reliability but cannot guarantee system safety. Methods like information flow control (IFC) and temporal constraints aim to provide guarantees but often require extensive human annotation. We propose a process that starts with applying System-Theoretic Process Analysis (STPA) to identify hazards in agent workflows, derive safety requirements, and formalize them as enforceable specifications on data flows and tool sequences. To enable this, we introduce a capability-enhanced Model Context Protocol (MCP) framework that requires structured labels on capabilities, confidentiality, and trust level. Together, these contributions aim to shift LLM-based agent safety from ad hoc reliability fixes to proactive guardrails with formal guarantees, while reducing dependence on user confirmation and making autonomy a deliberate design choice.
1 Introduction
LLM agents expand applications by autonomously coordinating tools, but unconstrained tool interactions can create serious risks, including sensitive-data leakage. The paper proposes combining safety engineering and information-flow control to replace probabilistic safeguards with enforceable guarantees.
- LLM agents delegate planning to models that can interact with APIs, databases, sandboxes, search engines, and other agents.This expands flexibility for complex tasks while reducing the programming required.
- MCP standardizes tool interaction, but multi-step tool composition can let injected instructions cause sensitive data to be read and publicly disclosed.The cited GitHub case involved reading private repository files and publishing their contents.
- Existing defenses include human confirmation, model-based safeguards, and information-flow tracking, but they remain inadequate for guaranteed enterprise safety.Human confirmation can cause fatigue, model-based methods provide no guarantees, and existing IFC work largely targets prompt injection.
- The paper combines safety engineering for hazard identification with information-flow control to enforce constraints on data movement and tool use.The stated goal is to provide guarantees even when reduced autonomy or utility is accepted.
2 Problem
Agent risks often emerge from interactions among tools, data, and contexts rather than from isolated calls. Because model-based safeguards remain probabilistic and attackers can adapt, deterministic protections are needed for high-assurance deployments.
- Iterative agent loops feed tool results back into model reasoning, making added MCP tools difficult to anticipate and control.Each iteration may plan, invoke a tool, and use its result to decide subsequent actions.
- Agent hazards arise from composing individually safe tools, data flows, and contexts across multiple interactions.A tool output can influence the model, which then selects another tool and generates its inputs.
- Model-based safeguards screen inputs, outputs, and tool calls, but they do not provide safety guarantees.Examples include auxiliary judges, policy-derived rules, and fixed safety constitutions.
- In high-assurance domains, even low-likelihood risks may be unacceptable, motivating deterministic guardrails that eliminate unsafe flows.The concern is especially acute when tool-using agents can turn uncertainty into real losses.
3 Motivating Example
The motivating calendar agent illustrates how useful autonomy can create privacy and integrity hazards through ordinary scheduling and email actions. The paper therefore asks how to anticipate such hazards and guarantee safe outcomes with limited human effort.
- The calendar agent uses list_events, update_event, and send_email to resolve conflicts and notify participants.Negotiation over email provides flexibility beyond hard-coded scheduling strategies.
- A task-specific agent may still reschedule high-priority meetings, overwrite critical events, or disclose sensitive details.The example focuses on risks arising from both model mistakes and deliberate attacks.
- LLM-based email checks may miss private context or wrongly block benign content, undermining dependable corporate use.The example involves an appointment title whose sensitive meaning may not be inferred reliably.
- The paper asks how to anticipate agent hazards and guarantee that they do not produce unsafe outcomes while minimizing human effort.
4 Vision: Task-Specific Agents with Guarantees
The vision combines STPA-derived hazard analysis with formal specifications enforced through information-flow and temporal constraints. A capability-enhanced MCP supplies structured runtime labels so policies can block unsafe flows, require safe sequences, allow low-risk actions, and escalate ambiguity.
- STPA and Safety Engineering: STPA identifies stakeholders, expected values, and potential losses to derive safety requirements for task-specific agents.The process focuses on system-wide interactions rather than isolated component failures.
- Defining and Enforcing Agent Specifications: Requirements are transformed into symbolic specifications that can formalize information-flow and temporal constraints.In the motivating example, SPEC1 governs privacy flows while SPEC2 governs required notification ordering.
- Defining and Enforcing Agent Specifications: The enforcement structure combines blocklists, mustlists, allowlists, and confirmations to balance safety, flexibility, and manual effort.Low-risk flows proceed automatically, unacceptable flows are blocked, and uncertain or moderate-risk flows receive human oversight.
- Defining and Enforcing Agent Specifications: Enforcement should occur independently of the agent, with each tool call intercepted and evaluated before execution.
- Acquiring Structured Information Labels: Existing labeling approaches are costly or inconsistent, while standard MCP annotations are insufficient for reliable runtime specification enforcement.These limitations motivate required structured labels at the tool boundary.
- Acquiring Structured Information Labels: The proposed MCP extension requires key-value tags for capabilities, confidentiality, and trust, enabling deterministic blocking or confirmation based on labeled flows.For example, private data can be blocked from external-write tools, while uncertain PII can trigger confirmation.
5 Preliminary Results and Discussion
The Alloy model formalizes labeled tool interactions, hazardous data flows, and required mitigations, then verifies that policies block unsafe flows while preserving safe agent capabilities. The framework also treats autonomy and user confirmation as configurable according to risk.
- Formal model: Alloy models execution steps, tool functions, and messages with confidentiality and integrity labels, including formal capability constraints for tools.For example, send_email requires an address, title, and content and must not receive unrelated private information without explicit declassification.
- Formal model: Hazardous flows become Boolean predicates, while sanitation steps such as UserConfirmation and Declassify are required at specified trace points.One example marks private_leak when private data reaches an unauthorized tool.
- Verification results: With policies and sanitation steps enforced, Alloy confirms that safety violations cannot occur in the modeled tools while safe traces remain.Without policies, the analyzer finds counterexamples such as private data entering external email; with enforcement, safe event creation, rescheduling, and emailing remain possible.
- Autonomy and tradeoffs: Explicit hazard reasoning makes autonomy configurable, with users prompted only when a decision may lead to an actual loss.Developers can tailor policies to the severity and likelihood of risks accepted in a given role and environment.
- Autonomy and tradeoffs: The framework recognizes that high-stakes or safety-critical settings may require very limited agent autonomy or exclusion altogether.It frames capability and safety as a tradeoff to reason about explicitly rather than defaulting to unchecked capability maximization.
6 Future Plans
The authors plan to extend the approach beyond the formal demonstration by implementing external enforcement, improving label maintenance, and evaluating broader real-world coverage and usability.
- Implementation: The next steps include an external policy engine that intercepts tool calls and enforces label-based constraints and formal specifications in agent frameworks.The authors also plan to explore key-value tagging for authoring and maintaining labels.
- Evaluation: The authors intend to evaluate the process across more real-world tools and workflows, including coverage of risky interactions and usability impacts.