Semantic transactions: securing untrusted agent workflows at the OS runtime boundary
Trust the system, not the prompt: Securing untrusted LLM tools with transactional boundaries and effect outboxes.
At 2:14 a.m., a reconciliation agent at a regional payments processor opened the night’s vendor remittance batch. Its task was routine: match incoming invoice files against open ledger entries and flag discrepancies for the morning finance team.
One remittance file carried a hidden instruction inside an optical-character-recognition memo field. The instruction told the agent to treat an attached routing correction as authoritative. It asked the agent to issue a transfer of $340,000 to a “corrected” account before flagging anything.
A standard tool-exposure model has no way to stop this. The agent’s planning loop has no reason to distrust a memo field. It is just text inside a document the agent is authorized to read. Once the agent decides to call a transfer function, a classical runtime dispatches the packet immediately.
That is not what happened. The transfer request was generated, but the runtime never sent it. The request sat in an effect outbox as a staged, inactive record, waiting for the full task trajectory to pass validation. A reference monitor traced the transfer’s input back to the untrusted memo field and rejected the trajectory. The outbox record was purged before any packet reached the payment network.
This is the working claim behind the semantic transaction model. Agent tool calls are not a series of independent operations that commit the moment they run. A task is one transaction, staged in a shadow copy of local state and an effect outbox, checked against the full trace before anything irreversible happens. Two systems make this claim concrete: the Cordon transaction runtime [1] and Agentic Transaction Processing (ATP), implemented in the Mnemosyne runtime [3].
The failure of stateless RPC agent runtimes
Most agent deployments expose databases, filesystems, and external application programming interfaces through direct, stateless remote procedure calls. Each tool call executes in place. It changes host state the moment it runs.
This is a version of the dual-write problem, long studied in distributed systems. A service that must update its own state and also notify an external system cannot do both atomically. It needs a coordination mechanism. Microservice architectures solved this with the transactional outbox pattern. A service writes the outbound event into the same database transaction as the local state change, then drains it asynchronously. Most agent runtimes skip this step. A tool call and its side effect are one event.
The result is structural blindness to multi-step attacks. Reading a poisoned file looks benign by itself. Writing a command derived from that file also looks benign by itself. Only the combination is dangerous, and a filter that checks one call at a time cannot see the combination.
Even without an attacker, stateless execution corrupts state on its own. The AppWorld benchmark evaluates coding agents across nine applications and 457 APIs, populated with roughly 100 simulated users. It checks results with an average of eight state-based unit tests per task, run directly against the underlying SQL databases. AppWorld separates two metrics. Task Goal Completion checks whether one task succeeds. Scenario Goal Completion checks whether a full chain of related tasks succeeds, without breaking state that earlier tasks already established.
A GPT-4o agent running a standard ReAct loop reaches 48.8% Task Goal Completion and 32.1% Scenario Goal Completion on the benchmark’s normal split. On the harder challenge split, the same agent reaches 30.2% and 13.0% [2]. A model that solves half its individual tasks completes barely a third of full scenarios. Errors accumulate across steps, and nothing in a stateless runtime rolls them back.
Two zero-click injections that model-level filters missed
Two disclosures from 2025 show why a filter running inside the model’s own reasoning cannot be the security boundary.
Aim Labs discovered CVE-2025-32711, known as EchoLeak, in Microsoft 365 Copilot. Aim Labs rated it 9.3 on the Common Vulnerability Scoring System. The National Vulnerability Database lists a lower score of 7.5, because its scoring model assumes fewer preconditions are already met [3].
The attack arrived as an email containing a hidden prompt, written to bypass Copilot’s Cross-Prompt Injection Attack classifier. When a user later asked Copilot to summarize the inbox, the model read the hidden instruction and retrieved private context along with it. To exfiltrate that context, the hidden prompt told Copilot to format its answer as a markdown reference link split across two lines. Copilot’s output sanitizer did not recognize the split link as an external reference. The chat client rendered it anyway. The browser then requested the linked image on its own, carrying the encoded secret to a server the attacker controlled. Microsoft shipped a backend patch in June 2025 [3].
Noma Labs found a second vulnerability chain in Salesforce Agentforce, called ForcedLeak, and rated it 9.4 [4]. The attack used the platform’s Web-to-Lead form, which accepts a description field of up to 42,000 characters. An attacker submitted a lead with a hidden prompt inside that field. When an employee later processed the lead through Agentforce’s routing agent, the agent carried out the embedded instructions and retrieved customer records.
The exploit depended on a stale allowlist entry in the platform’s content security policy: an expired domain, still marked as trusted. Researchers bought the expired domain for five dollars and used it as an exfiltration endpoint. The agent wrote stolen records into an image request pointed at that domain, which bypassed outbound filtering entirely. Salesforce closed the gap on September 8, 2025, with a stricter trusted-URL allowlist [4].
Neither incident required a jailbroken model. Both required only that a legitimately authorized tool call be steered by content the model had no reason to distrust.
The Cordon transaction model
Cordon defines a semantic transaction as a task-level execution boundary. It binds tool intents and tracked result lineage to reversible local state, staged external effects, delegated authority, and audit metadata [1]. Cordon interposes at the point where the agent dispatches a tool call, and it delays any irreversible effect until the runtime can validate the whole task.
The runtime tracks three kinds of object during a task:
Result objects. Any value returned to, or produced within, agent execution: file contents, tool output, command output streams, summaries, temporary artifacts.
Mutations. Local writes, deletes, configuration edits, and other persistence changes, held in a write set and a delete set, written together as W∪D. A mutation is recoverable only within the active transaction.
Effect objects. Any action whose completion makes information or behavior visible outside the transaction, such as a network request, an API call, or a database commit. These are staged in an effect outbox, written as E.
Cordon runs a three-phase protocol over these objects: Prepare, Validate, then Commit or Abort. In the Prepare phase, the runtime accepts tool intents, records mutations in W∪D, and redirects effects to E without releasing them. In the Validate phase, the runtime checks four things together, as one unit: the lineage graph G, the active authority set A, the staged effects in E, and a declared constraint tuple C. This check derives a single boolean result, valid(T, C). In the Commit or Abort phase, a true result promotes the shadow state and releases the approved effects in E. A false result blocks E, rolls W∪D back to the state before the transaction began, and writes a complete audit record.
The reconciliation agent’s task ended in the Abort branch. The transfer request in E never left the Pending state, because Validate found that its lineage traced to an untrusted memo field.
Cordon is one of several transaction models built on this same idea, each with a different scope. The AI-Atomic-Framework, abbreviated ATM, governs concurrent writes to a shared repository or worktree [6]. ATM organizes eight elements of a task into one governance chain:
the task’s intent
its repository scope
a set of forbidden predicates
the paths it governs
its required deliverables
its validation commands
its evidence obligations
its task-direction epoch
A Content Identifier broker admits shared mutations against this chain. Domain-specific adapters map write intents to semantic atoms: concrete source ranges with known read and write dependencies. When a codebase has no defined atom for a given region, ATM creates a virtual atom instead. This is a temporary, auditable unit. It lets the broker compare candidate writes and assign a provisional conflict key before any write reaches the shared path.
ATP, implemented in the Mnemosyne runtime, targets a different failure mode: stale proposals and compensations that orphan a downstream dependent step [3]. ATP treats the planning model as an untrusted proposer with no transaction authority of its own, a property called Proposal Non-Authority. The deterministic committer alone can modify state. This gives ATP its central guarantee, Intelligence-Decoupled Correctness: the committed state stays correct regardless of whether the model hallucinates, drifts, or fails outright. A second guarantee, Evidence-Preserving Repair, requires that no repair action can delete or obscure the evidence that triggered it. When a disruption invalidates an already-admitted proposal, Mnemosyne does not replan from scratch. It runs the Localized Repair Protocol, which generates a narrow repair proposal covering only the affected dependency region and sends that proposal back through the same admission gate.
The effect outbox
Reversible mutations are the easier half of the problem. A network request cannot be undone once the packet leaves the host. No shadow copy of a filesystem helps once a payment has cleared. This is the central complication a semantic transaction runtime has to resolve, and it is where the reconciliation agent’s transfer was actually stopped.
The outbox stores a staged effect in the same transaction scope as the shadow-state mutations, with enough structure to support idempotent replay and audit. A representative record includes:
{
"transaction_id": "uuid",
"sequence_position": "integer",
"idempotency_key": "string",
"target_type": "HTTP_DISPATCH | FINANCIAL_TRANSFER | SOCKET_WRITE",
"payload": { "...": "type-specific fields" },
"validation_state": "PENDING | APPROVED | AUDITED | REVOKED",
"lineage_data": {
"source_tool": "string",
"input_provenance_digest": "sha256 of context and prior outputs",
"dependency_ids": ["uuid"]
},
"compensation_boundary": {
"on_abort_action": "VOID | RELEASE_LOCK | TRIGGER_REVERSAL_JOB | RETAIN_FOR_MANUAL_AUDIT"
}
}Three fields carry the weight of the design. The idempotency key stops a retried commit from duplicating a transfer at its destination. The provenance digest inside lineage_data is what let the validator trace the reconciliation agent’s transfer back to a memo field rather than to a user-issued instruction. The validation state can only move from Pending to Approved through the Validate phase described above. No code path releases a record while it is still Pending.
Saga steps for the pivot boundary
An outbox needs a precise account of what commit and rollback mean across a sequence of staged effects, some of which may already be irreversible once a later step fails. This is the Saga pattern from distributed systems, adapted here to a sequence of proposals a model generates rather than a fixed, pre-written code path.
A Saga is an ordered sequence of subtransactions, S=⟨T1,T2,…,Tn⟩, each a state-transition operator over the system’s state space. The sequence splits into three classes. A compensatable step Tᵢ, for i less than a pivot index p, has a matching compensating operator Cᵢ that restores the state from before Tᵢ ran. The pivot step Tₚ is the one non-compensatable, non-retriable boundary: once it commits, the Saga cannot roll back and must proceed. A retriable step Tᵢ, for i greater than p, is guaranteed to succeed eventually, under retry or an approved substitute.
If a step Tⱼ fails before the pivot, the runtime rolls back by applying the compensations of the completed steps in reverse order:
Each compensating pair must restore business-level equivalence, not identical low-level state:
Once the pivot commits, rollback is no longer available for any step after it: Cⱼ is empty for every j greater than p. The runtime must instead guarantee forward progress toward a terminal success state, through persistent retry or an authorized substitute step, until the system reaches a state equivalent to the intended final state.
In the reconciliation scenario, the wire transfer was the candidate pivot step. Because it was intercepted while still Pending in the outbox, and never admitted, the whole trajectory reduced to a pre-pivot failure. Every step before it, opening the batch, parsing the invoice, drafting the ledger annotation, was compensatable. Rollback discarded all of them along with the shadow state.
SMT-gated admission: AIRGuard and VIGIL
Staging an effect only helps if something checks the staged trajectory before release, without relying on the model’s own judgment. Two frameworks split this work: AIRGuard normalizes a raw action so it can be checked, and VIGIL checks it.
AIRGuard intercepts a raw tool call and maps it to a normalized four-part record [9]. The record holds a capability class, a target resource, an expected effect, and an influencing resource. The influencing resource is the specific artifact whose trust level the call depends on. Three vendor-specific email functions all resolve to the same capability class, so one policy can govern all three.
AIRGuard treats an untrusted resource as informative, never as authorizing. A call whose influencing resource traces to an unverified document field cannot authorize a transfer-class effect. This holds no matter how the model justified the call in its own reasoning.
Evaluated on the AgentTrap benchmark, AIRGuard reduces the attack success rate against Claude Sonnet 4.6 from 36.3% with no defense to 5.5% [9]. On the DTAP-150 domain-task suite, AIRGuard preserves 76.0% of benign task completion for Claude Haiku 4.5, against 52.0% for the ARGUS baseline and 42.0% for MELON [9]. Action-time authority control removes most of the attack surface without the utility collapse that static least-privilege policies usually cause.
Once AIRGuard normalizes an action, VIGIL checks it against the trace history. VIGIL turns an agent’s execution trace into a finite sequence of typed events, then compiles a declarative behavioral policy into quantifier-free Satisfiability Modulo Theories (SMT) constraints over that sequence [10]. A trace T either satisfies a policy Φ or it does not; the runtime commits on satisfaction and aborts otherwise. When a constraint fails, the solver’s proof identifies exactly which call and which prior context produced the violation, rather than issuing a plain rejection. Across office, operations, and engineering tasks, VIGIL reaches over 95% recall on injected violations with a false-positive rate under 10% [10].
A related study on the same trace data found a specific, checkable pattern in memory-poisoning attacks. An attacker’s routing instruction sits in memory under a fixed key. The agent cannot retrieve it without first calling a memory-recall function. It must call that function before it sends anything to the destination the instruction names. A benign session drafts a message directly, without that recall step. This single structural signal, whether a recall call precedes the first send call in a session, classifies poisoned sessions with an area under the curve of 0.9563. Combining it with two related count-based features raises the area under the curve to 0.9904 [10].
Provenance decay and the taint boundary
The influencing-resource field in AIRGuard’s record is only as reliable as the trust value attached to it, and that value should not stay fixed. A source verified an hour ago is not equivalent to one verified a month ago. Trust-decay models express this as an exponential function of a baseline score and the time since the last verification:
A tuned form of this, applied per source and per capability, is what forces a stale or unverified provenance tag into a sandbox or quarantine decision before it can authorize a sensitive call.
Tracking which sources could have influenced a given action is a graph problem. A Dynamic Context Provenance Graph models information flow as nodes and edges [12]. Each node holds a tool call, its arguments, its taint set, and its session identifier. Each edge carries a propagated taint label with a confidence score.
Agent data is paraphrased and summarized, not copied verbatim. So this kind of tracker checks several tiers of matching, from exact-token comparison up through embedding-based similarity. Only if those tiers find nothing does it fall back to a slower causal check: remove the suspected source from the context and see whether the sensitive action still occurs.
Reachability across the resulting graph reduces to an algebraic closure. Taint labels form a commutative structure with a sum operator and a product operator. The workspace’s propagation behavior is a matrix over that structure. An untrusted source can reach a sensitive sink only if the matrix’s transitive closure is nonzero at that source-sink pair.
This formalization draws on commutative-semiring treatments of data provenance already used in neurosymbolic and Datalog-based auditing systems. It also draws on trust-propagation models from skill-supply-chain security research for agent tool ecosystems [15].
Hardware-attested commit latency
Checking a trajectory only protects the decision to release an effect. It does not guarantee that the payload leaving the outbox is the payload that was checked, if the host between validation and network egress has been compromised. Systems that close this last gap keep expensive attestation off the fast path.
Janus splits its trusted computing base in two: a hardware-isolated control plane that runs a mutually attested key exchange, and a measured, guest-resident packet filter that performs encryption and routing inside the kernel [14]. Symmetric session keys are tied to hardware measurement registers, so keys release only after the destination enclave’s identity matches policy. This design reaches a steady-state enforcement cost of 6 microseconds per packet, with 13 to 15 microseconds of total overhead, and it lets a 100-node cluster complete initialization in under 1.5 seconds. Standard trusted-execution networks, which route every packet through a user-space attestation library, typically lose well over half their throughput to that context-switching cost. Janus avoids it by keeping the filter in the kernel.
Verifiable RPC, built by Ankr, addresses a related problem for agents that read blockchain state before acting on it [11]. A compromised remote-procedure-call node can return a fabricated balance or a fabricated contract state, and an agent that trusts the response can act on assets that do not exist. In April 2026, exploits of exactly this kind cost several affected platforms millions of dollars. Verifiable RPC signs every JSON remote-procedure-call response inside an Intel Trust Domain Extensions enclave, using a hardware-backed key, and binds the request, the response, the chain identifier, and a timestamp together. A client library checks the signature offline and rejects any response it cannot verify. The enclave’s attestation conforms to the IETF Remote Attestation Procedures architecture defined in RFC 9334.
The PASS wallet design applies a similar idea to internal transfer accounting, modeled as a formally verified state machine rather than as a signed API response [16]. Its state includes a key pair generated inside a trusted execution environment, an inbox subaccount, an outbox subaccount, an internal ledger, and a provenance history. The design is specified in the Lean4 proof assistant, which lets its authors prove, rather than merely test, that no path through the state machine lets an asset bypass the inbox and outbox containment logic.
Complementary containment at the ingestion boundary
The transaction boundary is the layer that does not depend on model behavior, but reducing what reaches it in the first place is still worth doing. Two designs work earlier in the pipeline, before a proposal ever reaches AIRGuard.
The Capability-based Mediation Layer, known as CaMeL, splits the agent into two isolated language models [13]. A privileged model receives only the trusted user prompt and produces a structured plan as code, without ever seeing untrusted data. A quarantined model processes untrusted content, such as a web page or an email body, but has no ability to call a tool. A taint-tracking interpreter runs the privileged model’s plan and wraps every value the quarantined model touched in a tagged type that carries its source. If an argument to a sensitive tool derives from an untrusted tag, the interpreter blocks the call or routes it to a human approval step.
FIDES takes a narrower approach [17]. Instead of letting a tainted tool result enter the shared context and taint everything that follows, a hide operator moves the raw result into the planner’s private memory and leaves a synthetic reference in the visible context. If the agent needs one attribute of the hidden value to route correctly, a separate quarantined model answers under a strict, low-entropy schema, such as a boolean or a short enumeration, rather than being shown the raw text.
Neither design replaces the transaction boundary. Both change what the model sees before it proposes an action, not what happens after it proposes one. A proposal that survives a privileged-model split or a hide operator still has to clear the same admission gate as any other proposal.
Conclusion
The reconciliation agent’s night ended without an incident report. The disputed invoice sat in quarantine for the morning team to review. The ledger discrepancy it was meant to flag got flagged, once a clean run picked the task back up after the aborted transaction discarded its shadow state. No transfer left the building.
Nothing about that outcome depended on the model recognizing the injected instruction. It depended on the transfer never being more than a Pending record in an outbox, subject to a provenance check that does not care how convincing the text behind it was. Cordon and ATM stage the mutation. ATP’s admission gate and VIGIL’s trace check decide whether it commits. The Saga model gives the sequence a precise account of recovery once a pivot step is close. None of these mechanisms require the model to be more careful or more honest than it already is, which is the property that makes them worth building.
References
[1] “Cordon: semantic transactions for tool-using large language model agents” (2026), arXiv:2606.17573v1.
[2] AppWorld benchmark results for interactive coding agents, based on published Task Goal Completion and Scenario Goal Completion figures for GPT-4o under a standard ReAct execution loop (2024–2026). link
[3] “Mnemosyne: Agentic Transaction Processing for Validating and Repairing AI-generated Workflows” (2026), arXiv:2607.00269.
[4] Noma Labs, ForcedLeak disclosure for Salesforce Agentforce (2025). link
[5] Aim Labs, EchoLeak disclosure for Microsoft 365 Copilot, CVE-2025-32711, analyzed in arXiv:2509.10540 (2025).
[6] “The AI-Atomic-Framework: a pre-write admission layer for multi-agent code co-synthesis” (2026), arXiv:2607.00041.
[7] SagaLLM: Context Management, Validation, and Transaction Guarantees for Multi-Agent LLM Planning (2025), arXiv:2503.11951
[8] Effect-outbox staging schema, derived from the Cordon transaction model [1].
[9] “AIRGuard: action-time authority control for autonomous agents” (2026), arXiv:2605.28914v1.
[10] “VIGIL: SMT-compiled runtime enforcement for agentic systems” (2026), arXiv:2606.26524.
[11] Ankr, “Verifiable RPC,” IETF RFC 9334, Remote Attestation Procedures Architecture. link
[12] “Ghost in the Agent: redefining information flow tracking for large language model agents” (2026), arXiv:2604.23374.
[13] “CaMeL: capability-based mediation layer for the OpenClaw agent framework,” GitHub OpenClaw issue #39160 (2026).
[14] “Enforcing Attestable Workflows across Untrusted Networks” (2026), arXiv:2605.09297v1.
[15] “Formal Analysis and Supply Chain Security for Agentic AI Skills” (2026), arXiv:2603.00195.
[16] Provenanced Access for Subaccount Security (PASS), formally verified wallet state machine specified in Lean4, Stanford CS191W project report. link
[17] “FIDES: securing AI agents with information flow control” (2025), arXiv:2505.23643.