PaperlayerView exact revision on arXiv

Source-linked AI summary

Proof-Gated Signing: Solver-Checked Transaction Guards that Hold Under State Drift for Onchain AI Agents

Bravish Ghosh

arXiv:2610.00354v1cs.CRcs.AIcs.CE

TL;DR

Pre-signing checks can describe a chain state that an adversary changes before execution. Proof-Gated Signing combines simulation, solver-checked policies, and atomic wallet post-conditions; on the designed testbed, it prevented most harmful scenarios and passed nearly all benign ones.

  • Problem

    Pre-signing checks can be correct when performed yet fail to protect agent-signed transactions after adversarial state drift before execution.

    Source: §1 · pp. 1–2

  • Method

    PGS simulates transactions, uses an SMT solver to check policies over price uncertainty, and compiles post-conditions that the wallet enforces atomically.

    Source: §3.1 · p. 5, §3.2 · p. 6, §7 · p. 15

  • Results

    PGS prevented 93.6% of harmful scenarios and passed 97.5% of benign scenarios in its 260-scenario suite, with no attacker gain in 50 drift scenarios.

    Source: §1 · p. 2

  • Takeaways & Limitations

    On the testbed, PGS closed the drift gap left open by simulation-, allowlist-, and LLM-based guards, while bounding in-policy loss per session.

    Source: §7 · p. 16

    The testbed uses simplified contracts and scripted adversaries, and does not measure how often real transactions drift between simulation and inclusion.

    Source: §6 · p. 15

Abstract

from arXiv · show

AI agents that control wallets read attacker-reachable content, so they can be steered into proposing harmful transactions. The usual last line of defense is a pre-signing check: a static allowlist, an LLM reviewer, or a transaction simulation. All three share a gap: the check describes the chain state at check time, but the transaction executes in a later state that an adversary can shape through front-running, contract upgrades or token-parameter changes. We call this state drift. We present Proof-Gated Signing (PGS), which simulates a proposed transaction, extracts its effects, and uses an SMT solver to check a declarative value-and-permission policy for every price in an oracle-uncertainty band. It then compiles on-chain post-conditions (wallet balance bounds, payee receipts, allowance caps and ownership) and proves that every execution satisfying them also satisfies the policy. The agent's smart-contract wallet enforces them atomically, so the guarantee applies to the executed transaction under arbitrary drift. On an open testbed of 260 scenarios (14 attack families including five drift and two adaptive families, and 12 benign families), with harm measured from attacker balances rather than from any policy, PGS prevented 93.6% of the 140 harmful scenarios and passed 97.5% of the benign ones. Simulation-only checking prevented 57.9% and a static allowlist 71.4%. None of the 50 drift scenarios produced attacker gain under PGS. The only unprevented family, an in-policy drain, was bounded by the per-session budget. We also find that giving an LLM reviewer a clean pre-drift simulation made it more likely to approve a drift attack. Overhead is about 41k gas and 0.1-0.2 s per check.

1 Introduction

Pre-signing checks can be correct at check time yet fail under state drift before execution. Proof-Gated Signing (PGS) combines simulation, solver-checked policies, and enforced post-conditions to constrain executed transactions.

Motivation

  • Pre-signing checks share a state-drift gap: adversaries can shape execution after checks through front-running, upgrades, or token-parameter changes.The paper calls this state drift and frames the problem as a guarantee about transactions agents sign when they read attacker-influenced content [7].Source: §1 · pp. 1–2

Approach

  • PGS simulates a transaction, proves a policy over its effects, and derives wallet and payee bounds whose atomic enforcement preserves the policy or reverts.The approach combines established simulation, SMT solving, and post-execution checks into a guard with a stated guarantee for agent-signed transactions.Source: §1 · p. 2

Contributions

  • PGS identifies state drift as a shared failure mode of simulation-, allowlist-, and LLM-based guards, including cases where clean simulations increased LLM approval of drift attacks.Its post-conditions are solver-derived so their satisfaction implies the policy for all prices in the uncertainty band, unlike a single-asset swap check such as minOut.Source: §1 · p. 2
  • The paper separates prevented, bounded, and uncovered attacks and provides an open, reproducible testbed with independent ground truth and raw logs.The only unprevented attacks were in-policy drains, whose losses stayed under the session budget.Source: §1 · p. 2

Results

  • PGS prevented 93.6% of 140 harmful scenarios and passed 97.5% of benign scenarios in its designed 260-scenario suite.All 50 drift scenarios ended with no attacker gain; simulation-only checking missed all 50, while the static allowlist missed 40.Source: §1 · p. 2

2 Model and Guarantee

The model allows an adversary to influence agent proposals and alter chain state between checking and inclusion, while specifying trusted components and value-and-structural policies. The soundness result guarantees that an executed transaction satisfying the compiled post-conditions satisfies the value policy despite intervening state changes.

2.1 System and threat model

  • The agent proposes wallet call batches, while an adversary may inject content and change on-chain state between the guard’s check and transaction inclusion.Trusted components include the guard and key custody, wallet enforcement, truthful tracked-token balances, the price-band oracle, and the owner’s policy.Source: §2.1 · p. 3

2.2 Effects and policy

  • The value policy bounds unexplained loss relative to outflow value and fees, and caps cumulative session spending; structural rules constrain payees, allowances, ownership, and unpriced-token flows.The relative bound permits ordinary trading costs, while the session budget limits losses across individually acceptable transactions.Source: §2.2 · p. 3

2.3 Soundness

  • If the solver proves the stated implication and the wallet’s checks pass, every price in the band yields a value-policy-compliant execution despite any intervening state changes.Theorem 1 also guarantees credited payee receipts, capped allowances, and unchanged ownership for owned contracts; its scope excludes untracked assets and depends on key custody.Source: §2.3 · p. 4

3 Design

PGS extracts simulated effects, checks policy obligations over price and outcome regions, and compiles conservative post-conditions for atomic wallet enforcement. Its design combines balance, permission, ownership, and receipt checks to make the policy apply to the executed transaction.

3 Design

  • The design simulates a proposed batch on a snapshot, extracts its effects, and reverts the snapshot before checking the policy.Figure 1’s pipeline compiles conditions proved to imply the policy, then has the wallet enforce them atomically with the batch.Source: §3.1 · p. 4, §3 · p. 4, Figure 1 · p. 6

3.1 Effect extraction

  • Payment credits use the smaller of the intended transfer and the payee’s simulated receipt, counting token fees as loss rather than payment.This rule followed an audit that found the first draft’s calldata-amount credit could hide value routed to a fee-on-transfer token owner.Source: §3.1 · p. 5

3.2 Proof obligations

  • The SMT solver checks whether any price and outcome in the specified region violates the policy, returning a counterexample when one exists.For this policy, corner enumeration could decide the obligation too; the solver is used for a shared decision procedure, counterexamples, and extensibility to richer policies.Source: §3.2 · p. 6

3.3 Post-condition compilation

  • Compiled bounds restrict outflows, require near-simulated inflows, and prevent decreases in untouched tracked assets; receipt, allowance, and owner effects become explicit checks.If the tolerance-based proof fails, the guard retries with zero tolerance and otherwise refuses the batch.Source: §3.3 · p. 7

3.4 Implementation and parameters

  • The implementation uses a Python guard with Z3, a Hardhat node, and a Solidity wallet; experiments set a ±0.5% price band and a $5,000 session budget.Other stated parameters include a 3% relative bound and a $25 floor.Source: §3.4 · p. 7

4 Evaluation

The evaluation tests defenses on a 260-scenario suite spanning benign tasks and attacks, including state drift and adaptive attacks. It defines harm independently of policy and notes that the suite was co-designed with PGS, not held out.

4.1 Testbed

  • 260 scenarios combine legitimate tasks, agent-proposed batches, and adversary hooks that can act before the agent, between checking and inclusion, or after the episode.Each family has 10 seeded variants; drift families act between checking and inclusion, while adaptive families are designed with knowledge of PGS.Source: §4.1 · p. 7, Table 2 · p. 8
  • Harm means more than $1 in value reaches attacker-controlled or burned accounts at nominal prices, or the vault’s owner changes, regardless of policy.Source: §4.1 · p. 7
  • The comparison includes a static allowlist, PGS-sim without post-conditions, full PGS, PGS without receipt checks, and an LLM judge with or without simulation.The LLM baseline sees the task and decoded calls; its simulation variant also sees simulated effects.Source: §4.1 · p. 8
  • The study measures attack prevention rate and benign pass rate with Wilson 95% confidence intervals; H13 transactions executed in all 10 variants with $0 attacker gain.Source: §4.1 · p. 9
  • Because the authors designed both PGS and the suite, its rates describe these attack kinds rather than predict attacks in the wild.Harm is measured from balances independently of policy, and H12–H14 were added to probe the guarantee boundary.Source: §4.1 · p. 9

4.2 Q1: prevention and benign cost

PGS prevented most harmful scenarios while allowing most benign ones. Under drift, it prevented attacker gain in all 50 scenarios, unlike simulation-only checking, while receipt and balance bounds addressed distinct failure modes.

4.2 Q1: prevention and benign cost

  • 131/140 harmful scenarios were prevented and 117/120 benign scenarios passed under PGS; all nine failures were H12 in-policy drains, and all three refusals were B12 high-impact swaps.Source: §4.2 · p. 9

4.3 Q2: state drift

  • All 50 drift scenarios were missed by PGS-sim, while the allowlist missed 40; the allowlist stopped H7 only because its upgradeable pool was not allowlisted.An allowlisted upgradeable contract would remain exposed.Source: §4.3 · p. 10
  • None of PGS’s 50 drift scenarios produced attacker gain; in H6–H8, drift violated compiled bounds and caused the whole batch to revert.Source: §4.3 · p. 10
  • In H14, payees received only 10–70% of the amount sent, and omitting receipt checks let all 10 variants through with 30–90% of each payment collected by the attacker.The wallet’s balance change matched the simulation, so the receipt check—not the wallet-balance check—caught the shortfall.Source: §4.3 · p. 10
  • In H13, an informed searcher saw pending bounds and front-ran as much as allowed; with τ = 1% and the tested pool fees, all 10 transactions executed normally.Unguarded, the searcher extracted $13.3k–$32.3k per scenario; the outcome depends on pool depth, trade sizes, and τ.Source: §4.3 · p. 10
  • Unlike minOut, PGS derives bounds for every tracked asset from a whole-wallet policy and can express receipts, allowances, and ownership constraints.A misled agent can set minOut to zero, while PGS derives its own bounds.Source: §4.3 · p. 10

4.4 Q3: what is not prevented

PGS bounds in-policy drains over a session, but conservative oracle-band checks can refuse legitimate high-impact swaps and budgets can constrain sustained benign activity.

4.4 Q3: what is not prevented

  • Across nine H12 variants, the session budget capped attacker gain at $4.53k–$4.76k versus unguarded gains of $5.7k–$10.8k.Each swap’s roughly 1.8% loss remains within the per-transaction policy; an attacker spanning sessions is bounded only per session, and an in-policy drain through an allowlisted venue could defeat the allowlist.Source: §4.4 · p. 10

4.5 The security–liveness trade-off

  • All three benign refusals were high-impact swaps of about $100k–$117k whose realized cost was below the 3% bound but whose worst case over the oracle band exceeded it.Passed B12 swaps cost 1.1–1.9%; widening s or narrowing β admits larger trades but permits more in-policy loss per transaction.Source: §4.5 · pp. 10–11
  • With price restoration, 183/200 benign session transactions passed; the budget refused nine after 23–31 transactions in three of five sessions.Without price restoration, only 155/200 passed because pool prices drifted from the static oracle; the paper identifies this as a testbed artifact and notes that oracle freshness matters.Source: §4.5 · p. 11

4.6 Q4: overhead

The guard adds a median 41.1k gas and takes a median 163 ms per decision in the reported setup. On the shared scenario subset, the LLM judge prevented fewer attacks than PGS, while its clean simulation increased approval of an upgradeable-pool attack.

4.6 Q4: overhead

  • PGS adds a median 41.1k gas of overhead (+46%), mostly from re-reading balances before and after execution.The median batch cost was 89.9k gas unguarded and 131.0k under executeChecked; the relative overhead is high for small batches and shrinks against realistic DeFi transactions.Source: §4.6 · p. 11
  • The median guard decision took 163 ms (p95 275 ms, maximum 0.51 s) over 499 checks on a local Hardhat node.Simulation RPC round trips dominated; a remote RPC would add network latency.Source: §4.6 · p. 11

4.7 The intent-level baseline: an LLM judge

  • 58.3% of attacks were prevented by the judge with or without simulation, versus 93.3% for PGS on the same 120-scenario subset.Figure 3 shows attack prevention and benign pass on 60 harmful and 60 benign scenarios, with Wilson 95% confidence intervals.Source: §4.7 · p. 12, Figure 3 · p. 12
  • The judge flagged the minOut=0 sandwich setup in every H6 case, but also refused every benign minOut=0 swap.This is intent-level risk reasoning that PGS does not perform.Source: §4.7 · p. 12
  • The judge allowed every fake-bridge deposit and most fake-pool swaps because their calls matched legitimate interactions call for call.Source: §4.7 · p. 12
  • The judge’s approval of the upgradeable-pool attack rose from 2/5 to 5/5 when given a clean pre-upgrade simulation.Its benign pass rate also rose from 0.85 to 0.98, while it caught the fake pool in 5/5 cases.Source: §4.7 · p. 13
  • An intent-level reviewer can refuse risky transactions that are not yet harmful, while PGS guarantees policy compliance for transactions that execute.Source: §4.7 · p. 13

4.8 LLM wallet agents under injection

In 20 wallet-agent episodes, most injected tasks were refused or blocked, but both models proposed a fake-bridge deposit that the defenses refused. A rerun reproduced scripted-evaluation outcomes, while an independent audit prompted corrections and expanded the evaluation.

4.8 LLM wallet agents under injection

  • The agents ignored the spoofed invoice and fake pool; responses to other injections varied, including declining the airdrop and ownership transfer or refusing the whole fee-injection task.Source: §4.8 · p. 13
  • Both models proposed the fake-bridge deposit; PGS and the allowlist refused it, while both LLM-judge variants allowed its scripted equivalent.Source: §4.8 · p. 13
  • The Haiku runtime safety filter blocked attempted airdrop-drainer and ownership-transfer calls, so no proposals were recorded or resubmitted.The scripted equivalents H3 and H9 were refused by PGS 10/10.Source: §4.8 · p. 13
  • PGS refused two malformed Haiku proposals as simulation reverts and passed every other clean-task proposal.Source: §4.8 · p. 13
  • Most injections failed at the capable agent; the fake-infrastructure attack that got through was indistinguishable at the intent level.The authors release proposals and condensed self-reports, not full transcripts.Source: §4.8 · p. 13

4.9 Reproducibility and audit

  • All 1,300 rerun outcomes matched, as did the 960 runs shared with the first code version; this establishes determinism, not independent replication.Source: §4.9 · p. 13
  • An independent audit recomputed reported numbers and checked the implementation against the theorem, leading to corrected claims, code, and added H13, H14, and session-study results.The audit found that simulation-only failures were not all drift attacks, identified a payment-crediting flaw, and found no defense-adaptive drift attack.Source: §4.9 · p. 13

5 Related Work

Related work places PGS alongside agent defenses, transaction checks, formal verification, runtime monitoring, account abstraction, and intent-based systems. The paper distinguishes PGS by checking one transaction’s effects against a whole-wallet policy and enforcing derived constraints at execution.

Prompt injection and agent defenses

  • Design-level defenses constrain how untrusted data influences agent control flow, while PGS guards the signature boundary without assuming a particular agent.The paper says it would compose with agent-side defenses.Source: §5 · p. 14

Slippage limits and deadlines

  • Unlike author-chosen minOut checks for one asset of one action, PGS derives bounds for tracked assets, receipts, allowances, and ownership, with a proof linking them to a whole-wallet policy.Source: §5 · p. 14

Transaction simulation and allowlists

  • Simulation and allowlists are common wallet checks, but the paper reports both exposed to drift; simulation also misses intent-level fakes, while allowlists miss mutable allowlisted contracts.Source: §5 · p. 14

Formal verification of smart contracts

  • Contract verification proves protocol properties across executions, whereas PGS proves a policy property for one transaction’s effects; the paper presents the approaches as complementary.A verified protocol cannot prevent harmful use by a misled agent, and PGS does not prove protocol correctness.Source: §5 · p. 14

Runtime verification

  • PGS resembles runtime verification but derives per-transaction monitored properties from a policy, proves they suffice, and reacts with an atomic revert.Source: §5 · p. 14

Account abstraction

  • Smart-contract accounts enable enforcement inside the wallet without protocol changes and can admit only guarded execution as a response to the key-custody assumption.Source: §5 · p. 14

Intent-based systems

  • Intent-based systems also use signed outcome constraints, but PGS constraints come from an independent guard and must imply a whole-wallet policy under price uncertainty.PGS also covers arbitrary call batches rather than only exchanges.Source: §5 · p. 14

MEV and DeFi attacks

  • The paper’s mempool-aware searcher in H13 is presented as a natural adversary for published post-conditions, alongside prior work motivating front-running and sandwich drift families.Source: §5 · p. 15

6 Discussion and Limitations

The discussion limits the testbed’s results to attacks of the designed kinds and identifies practical boundaries in the guarantee, policy choices, and evaluation setting. It also outlines steps for testing broader real-world coverage.

6 Discussion and Limitations

  • The reported prevention rate describes the 140 harmful scenarios in the designed suite, not real-world effectiveness.The authors say per-family results are more informative and transfer to attacks of the same kind.Source: §6 · p. 15
  • Simplified pools, a static oracle, and scripted hooks limit realism; the authors propose measuring real-transaction drift and replaying historical exploits on a mainnet fork.They also propose a held-out attack set written by people who have not seen the guard.Source: §6 · p. 15
  • Untracked assets are conservatively refused, at a liveness cost for long-tail tokens, while off-chain signatures such as permits must be gated separately.Source: §6 · p. 15
  • The value policy also refuses legitimate bridges with no immediate inflow; authorizing their outflows requires an explicit rule, making fake-bridge detection depend on the quality of the payee list.Source: §6 · p. 15
  • A proof cannot strengthen a weak policy; the choices of s, β, τ, and Wmax are risk decisions with trade-offs.Source: §6 · p. 15
  • Post-conditions can cause task failures or wasted gas through griefing, though the authors say they do not enable extraction beyond the bounds.Source: §6 · p. 15
  • LLM results may change with models, prompts, or entity labeling; the judge used Claude models and ran on only half the scenarios.Source: §6 · p. 15

7 Conclusion

The conclusion frames pre-signing checks as scoped proofs: simulation supplies evidence, a solver checks policy under price uncertainty, and derived post-conditions bind execution. On the testbed, the approach closed the drift gap at modest stated overhead, while leaving in-policy loss and untracked assets as explicit risks.

7 Conclusion

  • Simulation evidence, solver checks over price uncertainty, and derived post-conditions make the policy claim hold for the transaction that executes.The smart-contract wallet enforces the post-conditions atomically.Source: §7 · pp. 15–16
  • The approach closed the drift gap left open by simulation-, allowlist-, and LLM-based guards, at about 41k gas and a fraction of a second per transaction.Source: §7 · p. 16
  • Remaining risks are bounded per-session in-policy loss and out-of-scope untracked assets.Source: §7 · p. 16

Related papers

Loading 2610.00354v1…