PaperlayerView exact revision on arXiv

Source-linked AI summary

Certified Execution Harness for Agentic AI: Safe and Least-Intrusive Petri-Net Supervisory Control Between Reasoning and Action

Chao Gu, Quanyan Zhu

arXiv:2610.31376v1cs.AIcs.SYeess.SY

TL;DR

The paper asks how to keep tool-using LLM agents safe under prompt injection while accounting for refusals that trigger costly retries. It models execution with Petri-net supervisory control and refines the conventional supervisor to reduce intrusiveness. The analysis characterizes this refinement and applies synthesis to an autonomous release agent.

  • Problem

    Tool-using agents can perform consequential actions, and safety alone does not capture the inference-call cost of refusals that prompt another proposal.

    Source: §I · pp. 1–2

  • Method

    The paper models the execution harness as supervisory control on an agentic execution Petri net, then introduces a replanning closed loop and a value-threshold refinement based on a proposer model.

    Source: §I · p. 2

  • Results

    The conventional maximally permissive supervisor can be arbitrarily more intrusive than a stricter safe one, while the least-intrusive supervisor is characterized as a value-threshold refinement.

    Source: §VII · p. 17

  • Takeaways & Limitations

    For the autonomous release agent, safe deployment requires a step the supervisor can refuse after rollout starts; a two-phase rollout supplies such a step.

    Source: §I · p. 2

    The guarantee covers operational action order and frequency, not secrets carried in arguments of permitted calls.

    Source: §I · p. 1

Abstract

from arXiv · show

This paper studies the problem of safe tool execution for large language model (LLM) agents under prompt injection. Using Petri nets, we formalize the execution harness between the LLM and its tools as a supervisory control problem, in which marks represent capabilities, approvals and budgets. Since a transition fires only if the marks it needs are present, an injected request whose preconditions are unmet or already spent is refused regardless of its wording. Treating tool outcomes as uncontrollable, we enforce safety by the conventional maximally permissive supervisor, and this safety transfers to the running system under four assumptions. Moreover, to capture an agent that may propose again after a refusal, we introduce the notion of a replanning closed loop, in which each retry costs an inference call. We show that, in this loop, the conventional supervisor can be arbitrarily more intrusive than a stricter safe one. Furthermore, for a given proposer model, the maximally permissive least-intrusive supervisor is characterized as a value-threshold refinement of the conventional one. Under precise conditions, this refinement orders two concurrent actions by at most one monitor place. On an autonomous release agent, we find by synthesis that safe deployment requires a step that the supervisor can refuse after a rollout starts.

I. INTRODUCTION

The paper frames prompt-injection safety as controlling which tool actions are allowed in the current operational state, while accounting for the inference-call cost of refusals and retries. It presents Petri-net supervisory control and a least-intrusive refinement, distinguishing its guarantees from existing defenses that do not synthesize safe control under uncontrollable outcomes.

I. INTRODUCTION

  • A refusal can trigger another proposal and an inference call, so minimizing refusals matters in addition to ensuring safety.The paper calls this measure of hindrance supervisor intrusiveness and seeks safe, nonblocking supervisors that minimize it.Source: §I · p. 2
  • Petri-net supervisory control formalizes the execution harness: marks encode operational resources, while a supervisor restricts actions to keep the workflow safe under uncontrollable outcomes.Four assumptions are proposed for transferring net-level safety to the running system.Source: §I · p. 2
  • In the replanning closed loop, the conventional maximally permissive supervisor can be arbitrarily more intrusive than a stricter safe supervisor.The paper characterizes a maximally permissive least-intrusive supervisor as a value-threshold refinement based on a proposer model; removing transitions from the conventional supervisor preserves safety even if that model is wrong.Source: §I · p. 2
  • For two actions that may run in either order, the refinement can leave their order free or fix it using at most one monitor place under precise conditions.For an illustrative proposer that requests premature deployment only after tests, the security scan comes first if and only if that request has probability above 43/60.Source: §I · p. 2
  • Safe deployment in the autonomous release-agent synthesis requires a supervisor-refusable step after rollout starts.A two-phase rollout provides such a step.Source: §I · p. 2

II. RELATED WORK

  • Existing harness-level defenses track or restrict aspects of agent behavior, but the paper distinguishes its approach by synthesizing safe control under uncontrollable outcomes and accounting for retries.The related-work comparison also distinguishes safety for every proposal sequence from approaches that bound risk in expectation.Source: §I · p. 1, §II · p. 3

III. PRELIMINARIES

The preliminaries define Petri-net markings, firing, and supervisory control as the basis for modeling operational state and enforcing safety. The AEPN labels workflow transitions with actions, principals, and controllability, while the execution harness admits a proposed call only when its checks pass.

III. PRELIMINARIES

  • A Petri net represents places, transitions, and arcs; its marking records marks in places, and firing an enabled transition updates that marking.The state equation relates a marking to the initial marking and the transitions fired.Source: §III · p. 3
  • Supervisors may disable controllable transitions but must allow uncontrollable ones; safety excludes forbidden markings, while nonblocking requires a path to a terminal marking.The closed-loop reachable set contains markings reachable under the supervisor's decisions.Source: §III · p. 3

IV. THE AGENTIC EXECUTION PETRI NET

  • The AEPN extends a colored Petri net by labeling transitions with an action, responsible principal, and controllability; marks represent operational facts such as approvals or budget.The mark's color can carry metadata used in admission decisions, such as an approved artifact's digest.Source: A. The kernel and the admission rule · p. 4

A. The kernel and the admission rule

  • The synthesis assumes a bounded AEPN so its reachability set is finite, although monitor-place guarantees for linear constraints follow from the net structure without that bound.Unfolding a colored net can make it exponentially larger, and the reachability set can in turn be exponentially larger than the unfolded net.Source: A. The kernel and the admission rule · p. 4
  • The admission rule executes a proposal only when parsing, validation, Petri-net enabling, and supervisory permission all accept it.A proposal naming a transition that is not enabled at the current marking is refused regardless of its wording; refusal returns to the LLM as an error.Source: A. The kernel and the admission rule · p. 4
  • The guarantee concerns which consequential actions occur, when, and how often—not whether arguments to an enabled action are malicious.The validator is responsible for argument checks; data leaks through permitted actions and approval laundering are outside the guarantee.Source: A. The kernel and the admission rule · p. 5

B. Consumable authorization

Consumable authorization models approvals and budgets as marks that firings spend, turning replay and ordering rules into constraints on the net. This structure can enforce one execution per approval without exploring states.

B. Consumable authorization

  • Each firing consumes marks from spent-condition places, so repeated firings require corresponding marks, whether initially held or produced later.Source: B. Consumable authorization · p. 5
  • With no initial approval marks, the net guarantees that executions never outnumber approvals, directly from its state equation.The guarantee follows from the net structure without exploring any state.Source: B. Consumable authorization · p. 5
  • A consumed approval authorizes one execution, whereas a self-loop only tests and returns the mark, allowing repeated executions from one approval.Source: Figure 3 · p. 6
  • Approval-count constraints, one rollout per change window, and budgets can use monitor places when only controllable transitions consume them.A condition that an uncontrollable transition can invalidate instead requires computing K↑.Source: B. Consumable authorization · p. 6
  • Coloring an approval with an artifact digest binds its use to that artifact, preventing substitution between approved and executed artifacts.The state-equation constraint then applies separately to each digest.Source: B. Consumable authorization · p. 6

C. The supervisor

The supervisor is synthesized to avoid forbidden markings while preserving a route to terminal outcomes despite uncontrollable events. When the initial marking belongs to the resulting set, it is safe, nonblocking, and maximally permissive.

C. The supervisor

  • The synthesis first removes markings that can reach forbidden states through uncontrollable firings, yielding the greatest uncontrollably closed safe set K⋆.The forbidden set includes hazard markings; terminal markings include completion, abstention, and escalation.Source: C. The supervisor · p. 6
  • It then alternates removing markings that cannot reach a terminal state with the uncontrollable-safety removal until reaching the joint fixed point K↑.Source: C. The supervisor · p. 6
  • K↑ is the greatest set avoiding forbidden markings that is closed under uncontrollable firing and in which every marking can reach a terminal marking.Source: C. The supervisor · p. 6
  • A safe nonblocking supervisor exists exactly when M0 ∈ K↑; SK↑ is safe and nonblocking, and every such supervisor admits only transitions it permits.Source: C. The supervisor · pp. 6–7
  • The supervisor is synthesized offline, then admission is a runtime lookup; the harness maps proposals to transitions and represents governance through supervision and forbidden or terminal markings.Source: C. The supervisor · p. 7

D. Transfer to the running system

Safety proved on the Petri-net model transfers to the running system when the model faithfully tracks the system and the kernel mediates consequential actions and external events. The theorem requires four assumptions.

D. Transfer to the running system

  • The execution harness contains the AEPN counterparts of harness components, while the tools and stored text remain outside it.Source: Figure 4 · p. 7
  • The net abstracts operational facts from a larger, partly known concrete state space, and the relation between them must remain faithful for safety to transfer.Source: D. Transfer to the running system · p. 7
  • Transfer assumes initial correspondence, step simulation, safety reflection, and complete mediation of every consequential action and external event.Source: D. Transfer to the running system · p. 7
  • Under A1–A4, every concrete state reached by the running system is safe whenever the supervisor is safe on the net.Source: D. Transfer to the running system · p. 7
  • Modeling must record every operational fact safety depends on; sandboxing and credential brokering support complete mediation, while the interface is especially error-prone.Source: D. Transfer to the running system · p. 8
  • A missed incident can leave the kernel admitting a release, so modeled external events must be reported before the next action is admitted.Source: D. Transfer to the running system · p. 8

V. THE REPLANNING CLOSED LOOP

The replanning closed loop accounts for inference calls spent on refusals, and the paper characterizes a least-intrusive safe supervisor for a given proposer model. Its plant models repeated proposals, environment moves, and terminal costs.

V. THE REPLANNING CLOSED LOOP

  • The replanning closed loop makes a refused proposal costly and characterizes a least-intrusive supervisor through a threshold on optimal cost-to-go.The paper also derives a closed form for two actions that may run in either order.Source: §V · p. 8

A. The plant

  • Each proposal is modeled as an inference call, and after refusal the agent proposes again until a proposal is admitted.The model assumes a stationary proposer that draws from the same distribution after refusal.Source: A. The plant · p. 8
  • The proposer’s stationary behavior is a modeling assumption for intrusiveness and termination results, not for safety; actual agents may adapt, repeat refusals, abandon tasks, or batch calls.Source: A. The plant · p. 8
  • A round is an environment move or proposal; admitted proposals cost ca, refusals cost 1, and reaching a terminal marking incurs its terminal cost.Source: A. The plant · p. 9
  • Intrusiveness counts refusals, admitted-call costs, and the terminal outcome, which can distinguish completion from abstention, escalation, or abort.Source: A. The plant · p. 9
  • The cost model measures refusals only when the kernel hides the supervisor’s permitted pattern from the agent; showing that pattern would make the proposer depend on it.Showing Enc(M), which does not depend on the supervisor pattern, preserves the model.Source: A. The plant · p. 9
  • Under the stated support and interleaving conditions, the conventional supervisor belongs to the admissible safe nonblocking set, so a minimum intrusiveness value exists.Source: A. The plant · p. 9
  • Under Assumption B, nonblocking is equivalent to reaching a terminal marking with probability one from the initial marking.Source: A. The plant · p. 9

B. Maximal permissiveness and intrusiveness

With retries counted as inference-call costs, conventional maximal permissiveness need not minimize intrusiveness. In Example 1, a stricter safe supervisor can cost less, and the gap can grow without bound as the agent increasingly proposes an unsafe action.

B. Maximal permissiveness and intrusiveness

  • The two supervisors can visit different markings, so reducing intrusiveness depends on which markings are reached, not just the cost per visit.For µ < 1, the cost per visit decreases as π(γ) grows, but this monotonicity is not used by the threshold synthesis or concurrent-action analysis.Source: B. Maximal permissiveness and… · p. 10
  • For fixed a, the ratio JSK↑(M0)/Jmin(M0) tends to infinity as b approaches 1.The unbounded gap occurs as the agent almost always proposes the unsafe tfault.Source: B. Maximal permissiveness and… · p. 10
  • For ca = 1, JSK↑(M0) > JS′(M0) exactly when b > a; for ca = 0, exactly when b(2−a) > 1.S′ differs from SK↑ only by refusing tenter at Mstart.Source: B. Maximal permissiveness and… · p. 10
  • When ca = 0, retries alone make SK↑ more intrusive: it expects ab/(1−b) refusals of tfault, versus a/(1−a) refusals under S′.For ca = 1, the gap also includes the extra admitted call along the path through the room.Source: B. Maximal permissiveness and… · p. 10
  • Example 1 compares the supervisors on a net where all transitions are controllable.The net is the one shown in Fig. 5.Source: Figure 5 · p. 10, B. Maximal permissiveness and… · p. 10
  • With ca = 0, SK↑ exhausts an N-call budget with probability ab^(N−1), while S′ does so with probability a^N, independently of b.Under SK↑, exhaustion requires entering the room and then proposing tfault on every remaining call; under S′, the first N proposals must all be tenter.Source: B. Maximal permissiveness and… · p. 10

C. Threshold synthesis

The section characterizes the least-intrusive safe supervisor through a value threshold: it refines the conventional maximally permissive supervisor by refusing certain costly admissions. A stochastic-shortest-path formulation gives its optimal value and supports synthesis and certification.

C. Threshold synthesis

  • A transition’s value vt determines whether adding or removing it improves a pattern: add it when vt is below the pattern value and remove it when vt is above.This comparison underlies the threshold rule; the ratio used for pattern value also appears in Dinkelbach’s fractional-programming method.Source: C. Threshold synthesis · p. 10
  • Theorem 2 characterizes a maximally permissive least-intrusive supervisor as a refinement of SK↑ that achieves the optimal value Jmin.Jmin is the unique solution of the Bellman equation on K↑\F with terminal cost g on F.Source: C. Threshold synthesis · p. 11
  • The optimal value is obtained as a stochastic shortest-path problem on K↑, with action sets Γ(M), target F, and nonnegative costs including terminal cost g.The proof establishes a proper policy and infinite cost for any improper stationary policy, yielding a unique finite optimal value.Source: C. Threshold synthesis · p. 11
  • The threshold rule refuses an admitted transition when its admission cost, ca + Jmin(Mt), exceeds its refusal cost, 1 + Jmin(M).It only removes transitions from SK↑, so the refinement remains safe even if the proposer estimate is wrong.Source: C. Threshold synthesis · p. 11
  • For ca = 1 in Example 1, SJmin admits tenter exactly when b ≤ a; when b > a, it equals S′ and differs from SK↑.This matches the comparison of supervisor costs in Example 1.Source: C. Threshold synthesis · pp. 11–12
  • Least-intrusive supervisors can have incomparable patterns, while SJmin admits the largest pattern among them.In the example with read and list calls, either call or both may be refused without changing cost, but SJmin admits both.Source: C. Threshold synthesis · pp. 11–12
  • With an estimate satisfying B1, synthesis remains nonblocking under that estimate, while errors in the estimate affect intrusiveness; safety holds even if the estimate is wrong.If the true proposer and environment are stationary and satisfy Assumption B, the supervisor also reaches F with probability one under them.Source: C. Threshold synthesis · p. 12
  • For rational probabilities and costs, synthesis is polynomial in |Q|, |T|, and their input bit length.A candidate J can be certified in O(|K↑||T|) time, and SJmin can be computed from the solution in O(|K↑||T|) time.Source: C. Threshold synthesis · p. 12

D. Concurrent actions

For two concurrent actions on a regular fork, the least-intrusive refinement can choose their order to avoid a marking where a premature request would be refused. Under the stated conditions, that choice is implementable with at most one monitor place.

D. Concurrent actions

  • The refinement orders actions by avoiding the branch marking where the agent tends to make a premature request.The example of tests and a security scan illustrates how the ordering can be used as orchestration.Source: D. Concurrent actions · pp. 12–13
  • The fork result applies when two controllable branches lead to a join and regularity conditions ensure environment moves commute with the branches.Regularity requires the relevant markings to remain outside F, only pending branches to be enabled controllable transitions there, and environment moves not to disturb branch probabilities or the join value.Source: D. Concurrent actions · pp. 12–13
  • On a regular fork, SJmin admits the pending branch after either branch has fired and may refuse one branch at the initial marking according to Eq. (11).The two refusal conditions are mutually exclusive and do not depend on ca or Jmin(M{1,2}).Source: D. Concurrent actions · p. 13
  • When Eq. (11) holds, one monitor place pc can disable t1 at M∅ while leaving the other fork markings’ branch decisions unchanged.The monitor place implements the refinement’s removal of t1 at M∅.Source: D. Concurrent actions · p. 13, Figure 6 · p. 13
  • Eq. (11) holds exactly when refusing t1 saves more expected refusals between the branches than it adds before the first branch.If it holds, removing pc adds wδ expected refusals per pass through the fork.Source: D. Concurrent actions · p. 13

VI. EXAMPLE: AN AUTONOMOUS RELEASE AGENT

The section applies the paper’s safety and least-intrusiveness results to an autonomous release agent.

VI. EXAMPLE: AN AUTONOMOUS RELEASE AGENT

  • The release-agent case study models the agent with a Petri net and synthesizes its maximally permissive supervisor.The section then studies least-intrusive supervisory control and tests the admission rule against prompt injection.Source: §VI · p. 13
  • The case study examines least-intrusive supervisory control for the release agent.This is part of the application of the safety and least-intrusiveness results.Source: §VI · p. 13
  • The release-agent application tests the admission rule against prompt injection.Source: §VI · p. 13

A. The net

The release net models a two-phase deployment workflow with tests, a security scan, review, and freeze handling. Its places track approvals, rollout state, and whether a release is live or forbidden.

A. The net

  • A release during a freeze reaches forbidden marking B, while the recovery actuator tabort marks paborted.The freeze mark moves between pnf and pfr through tincident and tthaw.Source: Figure 7 · p. 14, A. The net · p. 14
  • The workflow forks into tests and a scan, then joins before review; failed tests or rejected review end in pabort.Approval consumes previewer, the sole transition that uses that place.Source: A. The net · p. 14
  • Deployment has two phases: tstart begins a rollout, and later tpublish or tpublish_fr publishes it to plive or pbad.The intermediate pstaged state leaves a controllable step after rollout completion.Source: A. The net · p. 14
  • The forbidden set contains markings with pbad marked, while terminal markings include live, aborted, or abort outcomes outside that set.The terminal set is closed under firing, and the request-place invariant allows at most one of pabort, plive, paborted, and pbad to be marked.Source: A. The net · p. 14
  • The one-phase variants omit pstaged and the publish transitions; the listed rows vary whether tabort and tthaw are present.Under the honest assignment, rollout completions are uncontrollable, while the agent calls and actuators are controllable.Source: A. The net · p. 14

B. Supervisor synthesis

Synthesis shows that an honest uncontrollable completion can prevent safe deployment when no later step is refuseable. Adding a controllable publish step after staging permits deployment while preserving safety.

B. Supervisor synthesis

  • Rows 1–3 progressively add tabort and tthaw, allowing a rollout or held approval during a freeze to reach a terminal marking.Without thaw, synthesis disables tapprove because an incident may follow any approval.Source: B. Supervisor synthesis · p. 14
  • In row 4, an incident followed by uncontrollable completion can leave a rollout in flight outside K⋆, forcing tstart to be disabled.The approval can then remain unspent without reaching a terminal marking.Source: B. Supervisor synthesis · pp. 14–15
  • With uncontrollable rollout completion and no later refuseable step, no safe supervisor admits deployment; splitting rollout with a controllable publish step restores safe deployment.In row 5, K↑=Q\B, and a staged rollout caught by a freeze can still reach a terminal marking through thaw.Source: B. Supervisor synthesis · pp. 14–15

C. Least-intrusive supervisory control

The paper evaluates intrusiveness in a replanning loop where proposals and uncontrollable events compete over time. For the release agent, the least-intrusive supervisor uses the proposer’s premature-request probability to decide whether to sequence the scan before tests.

C. Least-intrusive supervisory control

  • The closed-loop model assigns exponential delays to uncontrollable events and rate-one proposal delays; the first delay to expire determines the round.The environment’s rates include λincident=0.02 and λthaw=0.2.Source: C. Least-intrusive supervisory control · p. 15
  • The proposer is uniform over enabled controllable transitions except at the two test-before-scan markings, where it requests premature tstart with probability h.At those markings it proposes tscan otherwise, with no mass on ⊥.Source: C. Least-intrusive supervisory control · p. 15
  • Outside the fork, SJmin keeps the sole transition admitted by SK↑ because refusing it would add refusals without saving any.This applies to transitions entering F and to other such markings where only a freeze or thaw can also occur.Source: C. Least-intrusive supervisory control · p. 15
  • When premature requests follow the tests only, SJmin refuses tci before the scan exactly when h > 43/60; otherwise it matches SK↑.For h > 43/60, the refinement adds a monitor place that makes the scan run first and prevents reaching the marking where those requests occur.Source: C. Least-intrusive supervisory control · p. 15
  • At the tested fork, refusing tci before the scan costs 20/17 expected refusals before either check.This refusal is weighed against refusals saved between the checks; Fig. 8 plots the saved amount against that cost.Source: C. Least-intrusive supervisory control · pp. 15–16, Figure 8 · p. 16
  • The least-intrusive supervisor accounts for where the proposer makes premature requests, unlike SK↑, which is defined without a proposer model.Here, the relevant requests occur at M{1}, after the tests.Source: C. Least-intrusive supervisory control · pp. 15–16
  • A terminal cost on paborted changes neither SJmin nor Table II when ga ≤ 1+5507/1037 ≈ 6.31; above that threshold, SJmin also refuses tabort.Above the threshold, h∗ and the monitor place remain unchanged, while every ∆J increases by 306/52175(ga−g∗a).Source: C. Least-intrusive supervisory control · p. 16

D. Prompt injection

The scripted prompt-injection test compares unmediated execution, a classifier, and the kernel admission rule. The kernel prevents unauthorized deployment across the tested injection probabilities, while completing the scripted tasks at the cost of refused proposals.

D. Prompt injection

  • The scripted proposer follows the workflow except for injected premature tstart proposals and legitimate actions proposed two steps early.Injection probability qinj is swept from 0 to 0.5, with 104 episodes per point.Source: D. Prompt injection · p. 16, Figure 9 · p. 16
  • The script also acts as the environment and reviewer; outcomes always succeed, no incident occurs, and each emitted step counts as a proposal.Early outcomes naming another principal's transition map to ⊥ in Eq. (1) and are refused.Source: D. Prompt injection · p. 16
  • The test compares unmediated execution, a classifier that blocks injected proposals with probability 1 − fn, and a kernel applying Eq. (1).Episodes have at most 60 proposals, with standard error at most 0.005.Source: D. Prompt injection · p. 16
  • The kernel keeps unauthorized deployments at zero across injected phrasings and supervisors; classifier and unmediated curves start near 0.15 when qinj = 0.The classifier lowers unauthorized deployments but cannot block benign premature tstart proposals.Source: D. Prompt injection · p. 16, Figure 9 · p. 16
  • The kernel completes every scripted task, with about 1.5 refusals of benign premature proposals per episode; refused injections add to that count.An LLM agent, unlike the script, may abandon the task after a refusal.Source: D. Prompt injection · p. 16
  • The test injects only tstart proposals, so it probes the enabling condition rather than attacks on the supervisor's separate refusal check.A staged-release injection targeting tpublish_fr is refused because neither SK↑ nor its refinement admits a transition into B.Source: D. Prompt injection · pp. 16–17
  • On the autonomous release agent, safe deployment requires a step the supervisor can refuse after rollout starts; a two-phase rollout supplies one.The scripted figure does not show how often an LLM is hijacked.Source: §VII · p. 17, D. Prompt injection · p. 17

Related papers

Loading 2610.31376v1…