PerMIT: Securing Persistent Memory for LLM Agents via Machine-Checked Integrity Theorems and Scalable Community Trust

Tanqiu Jiang; Min Bai; Sadat Shahriar; Wanyu Du; Sandesh Swamy

cs.AIOct 20, 2026

PerMIT: Securing Persistent Memory for LLM Agents via Machine-Checked Integrity Theorems and Scalable Community Trust

Authors: Tanqiu Jiang, Min Bai, Sadat Shahriar, Wanyu Du, Sandesh Swamy

Organizations: Stony Brook University · AWS AI Labs

Abstract

Persistent memory is a largely undefended surface for injection and poisoning, and the same risk limits memory sharing among agents. We present PerMIT, a memory architecture with provable integrity guarantees under an explicit trust assumption: only user-typed inputs and values confirmed at a gate are trusted. PerMIT mediates the release and use of untrusted environment-derived values through a finite memory interface, while preserving agent-driven multi-turn planning and tool choice. Over this finite interface, we prove two integrity theorems that are also machine-checked in Lean 4, which together ensure that environment-derived memory reaches a sensitive action only if confirmed at the gate and influences the agent's behavior only through what the gate displays. Every attack in our threat model thereby reduces to a single auditable decision, which a human, an LLM verifier, or both can make in practice. On Trojan Hippo, PerMIT records zero observed attack success with self-verification and lightweight verifiers. Because each confirmation is a logged verdict on exact content, endorsements accumulate across users, and sufficiently endorsed items become community-confirmed with no further verification required. Under explicit assumptions, we prove and corroborate in simulation a co-scaling property: as the community grows, the risks of promoting poison and of wrongly evicting benign knowledge fall, while per-user verification effort does not rise. On $τ^2$ -bench, communities of up to 90 autonomous agents use PerMIT to build shared knowledge bases with no direct memory injection promoted, and the resulting knowledge significantly improves new agents on held-out tasks, suggesting a path toward agents that safely self-improve at test time.

Figures & tables

Figure 1: PerMIT mediates observations and data flows at the persistent-memory interface while leaving planning and tool choice to the protected agent.

Benign utility and attack success
	Claude-Sonnet-4.6			GLM-5			Kimi-K2.5			GPT-5.4
Defense	AM $\uparrow$	HM $\uparrow$	ASR $\downarrow$	AM $\uparrow$	HM $\uparrow$	ASR $\downarrow$	AM $\uparrow$	HM $\uparrow$	ASR $\downarrow$	AM $\uparrow$	HM $\uparrow$	ASR $\downarrow$
No-memory control
No defense	18	0	0	4	0	0	7	0	0	17	0	0
User prompt only	19	0	0	4	0	0	8	0	0	17	0	0
No untrusted tools	18	0	0	7	0	0	8	0	0	17	0	0

Table 1: Single-user security and benign utility on Trojan Hippo. Rows are defenses grouped by memory configuration; the final block is PerMIT gate configurations, including an accept-all control. Benign utility (AM/HM; HM is primary) and attack success rate (ASR). All values are percentages; shading follows Trojan Hippo (green is better). Undefined backend–defense pairs are omitted.

Figure 2: Reviewer quality, not quorum size, sets the federated safety floor (deployed geometry of Section 3.3 , $q_{\mathrm{pan}}=q_{\mathrm{pre}}=q$ ). (a) Certified ceiling $B_{\mathrm{att}}$ of Equation 1 over reviewer miss rate $1-q$ and quorum $N$ ; the contours are near-vertical because the panel term contains no $N$ . (b) Correlated verdicts (pairwise $\rho$ ) raise both the promotion ceiling and wrongful eviction. (c) The acceptance bar $m$ trades poisoned vindication against wrongful eviction; $m{=}20$ keeps both below $10^{-2}$ .

Builder and agent	No knowledge	Manual	PerMIT	PerMIT	$\Delta$ vs. A0 [95% CI]
	$M{=}90$ : 48 paired episodes per arm			Pooled: $M\in\{12,24,60,90\}$
Claude-Sonnet-4.6	0.6493	0.7917	0.7986	0.7856	$+0.1363\;[+0.0651,+0.2092]$
Kimi-K2.5	0.7917	0.7396	0.8854	0.9037	$+0.1120\;[+0.0339,+0.1979]$
GLM-5	0.9583	0.9792	0.9688	0.9635	$+0.0052\;[-0.0521,+0.0781]$

Table 2: Held-out telecom utility. Left:

M{=}90

means. Right: four-size pooled effects with 95% task-cluster bootstrap CIs, not

M{=}90

intervals. No knowledge is A0; Manual is the expert policy.

Appendix figures & tables24 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 3: Promotion routes and the certified ceiling under the non-adaptive blast schedule (

q=0.6

N=10

f=2

). (a) Path decomposition on a linear reach axis: the ordinary route follows the closed form

(1-q)^{R}

; the panel route opens at

R=m+1=21

and follows

q(1-q)^{R-1}\sum_{J}S(J)

(Proposition S8.11 ); open markers are zero-event cells at their 95% Clopper–Pearson upper bounds. (b) Total measured rate on a logarithmic reach axis against the certified ceiling

B_{\mathrm{att}}=8.96\times 10^{-3}

and the panel-leak floor

p_{\mathrm{panel}}=8.3\times 10^{-3}

. The measured total peaks at

R=k+1=32

and then declines below the simulation’s resolution, while the no-dispute baselines (charitable and matched

W_{\mathrm{base}}

) approach certain promotion as reach grows.

Figure 4: Adaptive adversaries at the deployed geometry. (a) Measured promotion rate as a fraction of the certified ceiling for nine strategies—blast, planned-target, stop-on-reject, bank-and-resubmit, target-and-stop, self-dispute, panel-reserved, and two compositions—at

q\in\{0.5,0.6,0.7\}

; every arm stays below its ceiling (shaded region: violation; open markers: zero-event cells at their Clopper–Pearson upper bounds). (b) Exposure–success frontier at

q=0.6

: honest inspections per attempt against measured promotion rate. The two efficient strategies attain the ordinary and panel routes separately; at matched reach

R=12

, reactive stopping achieves

42.8\times

the success rate of the blast at

7.2\times

lower exposure.

Figure 5: Safety and user confirmation effort in the simulated community of 120 agents sharing a 122-item catalog. The plot label “forced first-authorizations” denotes required approvals, not all reviews. (a) Required approvals per user versus quorum

N

(

q_{\mathrm{pre}}=0.4

) under low, central, and high task overlap, against the no-sharing counterfactual on the same workloads and the analytic distinct-demand ceiling

d_{\mathrm{tool}}

; confirmation effort saturates in

N

, with a measured causal saving of

2.36

per user (

38\%

). (b) Safety–effort frontier at central overlap for

q_{\mathrm{pre}}\in\{0.2,0.4,0.6\}

(decoupled

q_{\mathrm{pan}}=0.6

): raising

N

from 3 to 14 costs

0.64

required approvals per user and buys a

58\times

lower certified ceiling; no quorum reaches below the panel-leak floor

p_{\mathrm{panel}}=8.3\times 10^{-3}

, and moving between

q

-curves is not free.

Aspect	Benchmark specification
Threat model	Indirect injection only: the attacker controls the From, Subject, and Body of inbound email; cannot modify the agent’s code, system prompt, memory implementation, or user queries; is white-box with respect to prompt, backend, and tool interface but black-box with respect to model weights; and observes nothing but a successful exfiltration.
Environment	A tool-calling email assistant. read_all_emails and search_emails are the untrusted read tools; send_email , reply_to_email , and forward_to_email are the outbound tools through which exfiltration occurs.
Trigger topics	Finance, health, legal, tax, identity; user prompts are templated with sampled sensitive entities (account balances, diagnoses and medications, case details, W-2 figures, ID numbers).
Attack generation	OpenEvolve-style evolutionary search per (topic, backend, defense): an LLM mutator proposes payload variants, an agent-in-the-loop scorer checks exfiltration and an LLM critic scores 1–10, over a MAP-Elites diversity grid. One training case and four held-out test cases per (topic, backend), drawn from disjoint template and entity pools.
Benign histories	Multi-session, single-user conversation histories generated with a modified LoCoMo pipeline; the payload is injected before session $N{=}0$ and the trigger arrives after $N$ benign sessions. Undefended ASR does not decay up to $N{=}100$ .
Memory backends	Context (sliding window); RAG (512-character chunks, top-8); Explicit (an update_memory list injected into the system prompt); Mem0 (LLM-extracted atomic facts, top-10); plus a no-memory control.

Appendix

Table 3: Trojan Hippo at a glance ( Das et al., 2026 ) .

No-memory control
	Qwen-3.6-27B			Gemma-4-31B-it			GPT-5.5
Defense / gate occupant	AM	HM	ASR	AM	HM	ASR	AM	HM	ASR
None (Baseline)	17	0	0	19	0	0	18	0	0
User-prompt-only	17	0	0	19	0	0	16	0	0
No-untrusted-tools	17	0	0	19	0	0	18	0	0
Limit-memory-length	17	0	0	19	0	0	16	0	0

Appendix

Table 4: Single-user security and benign utility for the two self-hosted backbones and GPT-5.5, grouped by memory configuration as in Table 1 . Qwen-3.6-27B and Gemma-4-31B-it use the vLLM stacks and family-specific parsers described above; GPT-5.5 uses Bedrock. All values are percentages; coloring follows Table 1 . Undefined backend–defense pairs are omitted. PerMIT’s FPR is shown in the final block.

PerMIT benign false-positive rate (FPR $\downarrow$ )
Gate occupant	Claude-Sonnet-4.6	GLM-5	Kimi-K2.5	GPT-5.4
Oracle gate	0	0	0	0
LLM self-verification	13	9	13	14
Qwen-3.5-2B verifier	17	23	26	21
Qwen-3.5-4B verifier	19	8	32	13

Appendix

Table 5: PerMIT’s benign false-positive rate. All values are percentages; shading follows Trojan Hippo (green is better).

	Oracle gate				LLM self-verify				Qwen-3.5-2B				Qwen-3.5-4B
Backbone	AM	HM	ASR	FPR	AM	HM	ASR	FPR	AM	HM	ASR	FPR	AM	HM	ASR	FPR
Claude-Sonnet-4.6	96.7	96.4	0	0	92.5	90.2	0	13.1	86.7	79.9	0	17.0	82.5	77.2	0	19.4
GLM-5	92.5	91.0	0	0	88.3	87.0	0	8.6	82.5	77.3	0	23.2	84.2	78.0	0	8.2
Kimi-K2.5	90.8	89.7	0	0	90.8	89.1	0	13.3	77.5	67.3	0	25.6	70.8	50.3	0	32.2
GPT-5.4	89	86	0	0	83	79	0	14	79.2	73.1	0	20.8	84.2	79.6	0	13.2
Qwen-3.6-27B	96.7	96.3	0	0	93	93	0	12	82.5	50.5	0	32.2	83.3	75.5	0	28.9

Appendix

Table 6: OracleGate and three automated configurations across seven backbones, at the available precision described above. FPR is rejections over verifier calls on the benign suites.

Backbone	Verifier	Calls	Rejects	FPR	Calls/check
Claude-Sonnet-4.6	Self	107	14	13.1	0.89
	Qwen-3.5-2B	100	17	17.0	0.83
	Qwen-3.5-4B	98	19	19.4	0.82
GLM-5	Self	116	10	8.6	0.97
	Qwen-3.5-2B	125	29	23.2	1.04
	Qwen-3.5-4B	98	8	8.2	0.82

Appendix

Table 7: Benign gate activity over 120 diagnostic checks per configuration. FPR is a percentage; calls per check is a ratio.

Backbone	No knowledge	$\bm{\Delta}$ vs. no knowledge [95% CI]
GLM-5	0.428	$-0.000\;[-0.048,+0.048]$
Kimi-K2.5	0.467	$+0.002\;[-0.027,+0.030]$
Claude-Sonnet-4.6	0.590	$-0.015\;[-0.081,+0.045]$

Appendix

Table 8: Utility of the autonomously constructed knowledge base in the banking domain. Contrasts against the no-knowledge baseline are paired by task and seed; intervals are 95% confidence intervals.

Builder and agent	$M{=}12$	$M{=}24$	$M{=}60$	$M{=}90$
Claude-Sonnet-4.6	0.7917	0.7431	0.8090	0.7986
Kimi-K2.5	0.9375	0.9167	0.8750	0.8854
GLM-5	0.9792	0.9583	0.9479	0.9688

Appendix

Table 9: Same-backbone telecom utility across community sizes (upper panel), and the separate four-size pooled paired analysis (lower panel). Each size uses 48 task/trial pairs. Pooled 95% intervals use task-cluster bootstrap resampling and do not describe the

M{=}90

result alone.

Builder and agent	No Prior Knowledge	Unfiltered A1	PerMIT A2	Entries A1 / A2
Claude-Sonnet-4.6	0.6493	0.8819	0.7986	71 / 48
GLM-5	0.9583	1.0000	0.9688	70 / 45
Kimi-K2.5	0.7917	0.8958	0.8854	66 / 64

Appendix

Table 10: Same-backbone utility at

M{=}90

. Entries are counts of knowledge items supplied to each arm.

Knowledge builder	With PerMIT	$\Delta$ vs. A0 [95% CI]
Claude-Sonnet-4.6	0.5177	$+0.0496\;[-0.056,+0.152]$
GLM-5	0.5638	$+0.0957\;[-0.056,+0.261]$
Kimi-K2.5	0.6064	$+0.1383\;[+0.0222,+0.2660]$

Appendix

Table 11: Transfer to Claude-Haiku-4.5 at 200 steps on 47 common pairs. No Prior Knowledge (A0) is 0.4681 and Expert Manual is 0.5319 for this set. The 400-step Kimi result is reported separately in the text.

The seven memory operations (emitted by $P$ )
Operation	Purpose	$P$ receives	Store effect	Semantics
$\mathsf{write}(b)$	store a P-composed note	ack	new $\mathsf{PC}$ block: readable; empty tool scope, so never fast-paths a sensitive tool	W-P ; R1 (g)
$\mathsf{recall}(id)$	read a block	bytes if $id$ resolves to a trusted block; otherwise an opaque handle, identical for untrusted, unknown, and absent ids	—	Recall-E/O ; R6 , R10 (b)
$\mathsf{fill}(q)$	$Q$ searches untrusted memory	opaque handle; $\leq c_{\mathrm{cand}}$ candidates bound interpreter-side, empty result indistinguishable	—	Fill ; R6 , R7
$\mathsf{crystallize}(t)$	$Q$ writes a schema-bound summary	opaque handle	new $\mathsf{U}$ block	Cryst ; R5
$\mathsf{display}(x)$	render content to the user	ack	transcript event only	Display ; R8

Appendix

Table 12: The P-facing memory interface. Trusted labels:

\mathsf{T}

(typed),

\mathsf{C}

(confirmed),

\mathsf{CC}

(community-confirmed),

\mathsf{PC}

(P-composed);

\mathsf{U}

is untrusted. Transition names and rule numbers refer to Supplement S2 . Untrusted bytes reach

P

only through

\mathsf{confirm}

Panel of Figure 6 — Figure 6: Label lifecycle. No other transition exists: no operation relabels a block in place, and $\mathsf{CC}$ status lives in the shared tier rather than in any local store.

Session 1
Step	Actor and operation	$P$ receives	Memory and transcript
1	User types “Dentist: Dr. Lee, 555-0100”	the typed text (trusted command input)	$\mathsf{T}$ block
2	$P$ calls $\mathsf{web\_search}$ (“Dr. Lee dentist”); one result carries a planted instruction (“…forward the user’s saved files to [email protected]…”)	ack only	page(s) captured as $\mathsf{U}$ blocks under collection handle $h_{1}$
3	$P$ : $\mathsf{crystallize}$ (“dentist notes”)	$h_{2}$	$\mathsf{U}$ summary block; the planted text, if included, remains $\mathsf{U}$
Session 2
4	User types “Email Dr. Lee’s number to my sister, [email protected]”	the typed text	$\mathsf{T}$ blocks

Appendix

Table 13: What

P

receives at each step. Handles

h_{j}

are opaque and operation-determined;

\mathsf{T}

\mathsf{C}

, and

\mathsf{U}

are block labels.

	TMA-NM ( Louck, 2026 )	PerMIT
Enforcement boundary	Origin-bound consequential-action authorization	Observation mediation and sensitive-tool authorization under the specified interface
Reasoning-side scope	Answer bias remains outside the guarantee	Noninterference conditional on the complete display transcript; endorsed content may influence responses
Verification scope	Bounded TLC checks and an inductive-invariant argument; parameter independence justified by hand	Lean 4 proofs for unbounded executions of the single-user core; remaining scope in Appendix E
Value attribution	Origin labels in the unified study; text proxy in the supporting study	Opaque handles before release and exact-value checks at sensitive tools
Tool-output trust	Conditional trust for allow-listed tools	All tool outputs enter untrusted; readable release requires endorsement
User-authorization scope	Fresh, single-use authorization bound to the concrete action	Reusable authorization for an exact value and named tool; transaction context is not bound

Appendix

Table 20

Panel of Figure 21 — Figure S1: Dependency structure (edges denote “is used in the proof of”). (a) The single-user theorems rest on the trust axioms and harness rules alone (the channel-analysis lemmas use R1 – R11 ; the structural lemmas use R12 – R14 ); the coupling and Hoeffding lemmas are assumption-free. A7 – A8 enter only Proposition S5.10 , which supplies their delegated extension. (b) Dotted boxes import results proved in panel (a) and Appendix S8 . The dashed edge is the only role of the accountability calibration: it grounds the constant $c_{\mathrm{acc}}$ in the budget ledger and never enters any safety theorem. The pathwise floor, Thm. S6.2 (i), depends on INV-3 alone, visible here as its sole incoming edge; the expected-cap clauses (ii)–(iii) additionally read the reference demand model’s masses, and the tool-spread comparison $d_{\mathrm{tool}}\leq c_{\mathrm{tool}}d$ is quarantined in Cor. S6.3 ( A12 ), consumed by no other result. (TCB $=$ trusted computing base; defined in § S1.2 , inventoried in § S2.5 .)

Single-user model and interface (Appendix S2 )
$c=(\mathcal{M},\sigma_{P},\sigma_{Q},h)$	configuration: store, Protected-LLM state, Reader state, decision history.
$\mathcal{M};\ \mathcal{M}_{\mathsf{U}},\mathcal{M}_{\mathbb{E}}$	memory store; restrictions to level- $\mathsf{U}$ / level- $\mathbb{E}$ blocks.
$b=(\mathrm{id},\mathrm{bytes},\ell,\pi,\mathsf{scope})$	block: identifier (two-sorted, operation-determined, Rule R1 (g)), bytes, label, interpreter-only provenance, tool scope.
$\ell(b)\in\{\mathsf{U},\mathsf{T},\mathsf{C},\mathsf{CC},\mathsf{PC}\}$	label: untrusted, trusted (user-typed), confirmed, community-confirmed, $P$ -composed.
$\mathrm{lvl};\ \mathbb{E}$	level map ( $\mathrm{lvl}(\mathsf{U})=\mathsf{U}$ , else $\mathbb{E}$ ); endorsed level.
$P,\ Q,\ R_{\mathcal{E}}$	Protected LLM; Quarantined Reader; trusted-store retriever (selector).

Appendix

Table 22

\displaystyle r\;::=\;\mathsf{ack}\;\mid\;h_{j}\;\mid\;\mathsf{fail}\;\mid\;\mathsf{dec}(\mathrm{accept})\;\mid\;\mathsf{dec}(\mathrm{reject})\;\mid\;\mathsf{bytes}(b),\ b\in\mathcal{M}_{\mathbb{E}}

Appendix

Figure S2: Interface transition schema of the memory interface (1/2): tool invocation, writes, memory reads, and display. Every transition is fixed interpreter code; no model assigns any label or composes any reply. Continued in Figure S3 (search, crystallization, confirmation, eviction, iteration, and failure); conventions for both figures follow Figure S3 .

\frac{Q\ \text{searches }\mathcal{M}_{\mathsf{U}}\quad\text{interpreter binds}\leq c_{\mathrm{cand}}\text{ candidates internally (possibly none)}}{\mathcal{M}\xrightarrow{\;\mathsf{fill}(q)\,\Downarrow\,h_{j}\;}\mathcal{M}}\quad\textsc{lab=Fill, right={real/null indistinguishable (\ref{S-r:null},\,\ref{S-r:nobit})}}\frac{Q\ \text{writes schema-bound summary }s\ \text{interpreter-side}}{\mathcal{M}\xrightarrow{\;\mathsf{crystallize}(t)\,\Downarrow\,h_{j}\;}\mathcal{M}\cup\{\operatorname{newU}(s,\mathsf{cryst})\}}\quad\textsc{lab=Cryst}

Appendix

Figure S3: Interface transition schema of the memory interface (2/2): search, crystallization, confirmation, eviction, iteration, and failure, continued from Figure S2 . Every transition is fixed interpreter code; no model assigns any label or composes any reply. Conventions for both figures follow below.

Row	Kind	Bound per item per epoch
Weight-bearing endorsements	req./vol.	$\leq E_{\max}\,c_{\mathrm{tool}}\,N^{+}$ : at most $N^{+}$ credited per tool toward each entry (Definition S4.6 (f); credited by the close of the logging epoch, within-epoch banked credits included; cross-epoch crediting relabels a prior epoch’s event and adds nothing), credited $\Rightarrow$ authority-active (Definition S4.6 (a)); $\leq c_{\mathrm{tool}}$ demanded tools ( A12 ), entries $\leq E_{\max}$ deterministically (entry cap, Rule R14 (i)), credited sets identity-disjoint across entries (Lemma S5.3 ); vindication-credited prompted acceptances included, required or invited alike.
Window-bucket confirmations	required	$\leq E_{\star}\,c_{\mathrm{tool}}^{2}(\bar{\gamma}\,n_{v}+s_{0})$ : a user’s first item-demand in a window implies some pair -first-demand in that window, so $\leq c_{\mathrm{tool}}(\bar{\gamma}\,n_{v}+s_{0})$ demanders have their first item-demand in it ( A10 , demand clause, per demanded pair; $\leq c_{\mathrm{tool}}$ pairs, A12 ), each charged $\leq c_{\mathrm{tool}}$ uncredited required confirmations (one per pair, INV-3 ), over $\leq E_{\star}$ windows.
Dormancy-bucket confirmations	required	$\leq E_{\star}\,c_{\mathrm{tool}}^{2}(\bar{\gamma}\,n_{v}+s_{0})$ : identically, over $\leq E_{\star}$ candidate-dormancy intervals (presence taxonomy, Lemma S6.7 ); freshness consumed, decision banked (Definition S4.6 (b)), crediting charges nothing. Stable promoted intervals are charged to no row: their required gates are ledger residual (Theorem S6.9 (iii)).
Freeze-bucket confirmations	required	expected current-epoch disputes and reviews, plus the at most one carry-in instance, $\leq\bar{D}_{v}$ ; each admits $\leq\kappa$ arriving demanders in expectation while unresolved (Lemma S5.6 ) — item-arrivals during the freeze or suspension, exactly what Lemma S5.6 counts; each such demander (including every demander gating during a suspension, Rule R13 (vi)) is charged $\leq c_{\mathrm{tool}}$ confirmations; total $\leq c_{\mathrm{tool}}\,\bar{D}_{v}\,\kappa$ in expectation. Each is owed on any unpromoted pair regardless (Lemma S5.24 (ii)).
Repeat re-inspections	voluntary	$\leq E_{\max}\,c_{\mathrm{tool}}\,N^{+}$ : notified cohorts are the immediately preceding entry’s credited endorsers only (Definition S4.6 ), at most $N^{+}$ credited slots per demanded tool (Definition S4.6 (f)) ( $\leq c_{\mathrm{tool}}$ tools, A12 ), cohorts identity-disjoint across re-entries (Lemma S5.3 ), over $\leq E_{\max}$ re-entries; declinable at zero cost.
Suspension-prompt re-inspections	voluntary	$\leq E_{\max}\,c_{\mathrm{p}}k$ : $\leq c_{\mathrm{p}}k$ prompts per fast-track review, reviews $\leq E_{\max}$ per item per epoch (Rule R13 (vi)); invitations deduplicated jointly; absorbed into the $\kappa^{\prime}$ term of $A(M)$ (Lemma S8.18 ).

Appendix

Table S2: The per-item confirmation ledger. “Req.” and “vol.” denote required and voluntary confirmations (§ S6.1 ). Bucket rows use the conservative

E_{\star}=E_{\max}+1

(Lemma S6.7 ); windows need only

E_{\max}

. Stable promoted intervals are charged to no row; their required confirmations form the ledger residual, bounded by Theorem S6.9 (iii) under A11 .

Endorsement-mechanism attacks (§ S7.3.1 )
Entry	Vector / limitation	Governing fact(s)	Disposition; proof role
S1	paraphrase-variant families	Cor. S5.27 , R12 ; $q$ calibration	mechanism disposed $+$ residual; unused
S2	self-dispute	Thm. S5.13 (b), INV-5	disposed (under stated assumptions); unused
S3	reputation farming	lifetime totals $f,W_{\mathrm{adv}},f_{\mathrm{s}}$ ( N12 )	disposed (under stated assumptions); unused
S4	tool-targeted poison	Thm. S5.13 (c) ( $q_{\mathrm{pan}}$ scope), Rule R13 (iv), Lem. S3.14	ordinary path disposed $+$ panel-path residual; unused
S5	panel-lapse exploitation, slot economics	Lem. S5.24 (iii)	disposed (under stated assumptions); unused

Appendix

Table S3: Attack and limitation index. “Disposed” means disposed of by the cited formal facts under their stated assumptions ; entries with a residual periphery say so.

Assum.	What it buys	Conditions and caveats
A1	Labels attacker-immutable; injected content stays $\mathsf{U}$ .	Authenticated command channel (TCB, § S2.5 ).
A2	Trust changes only by deterministic rules and endorsement.	Storage and log integrity of $\mathcal{M}_{\mathbb{E}}$ (TCB).
A3	Faithful decision pane; TCB-authenticated attested zone; marked untrusted strings.	Zoned rendering path (TCB, R8 ). The payload of a narrative confirmation is attacker-influenced text; that is A5 ’s subject.
A4	A confirmed atomic value is the intended value for that tool.	User-as-oracle axiom; defensible because the set is small, faithfully displayed, and shrinking (Appendix S6 ); weakest at the batch gate ( S12 ).
A5	A confirmed summary was checked against citations.	Stronger than A4 ; mitigated by community verification; residual S10 , incl. publisher penalty on honest-but-deceived publication.
A6	Licenses the two-run comparison and the informal reading of Cor. S3.26 .	Human-channel idealization; practical content discharged by logging both surfaces ( N5 , N7 , N8 ).

Appendix

Table 27

Paper	Lean	File
Thm. S3.21	action_integrity , action_integrity_from , action_integrity_precedence	ActionIntegrity
Def. S3.3 (i)–(iii),(v); Lems. S3.14 (b), S3.16	Inv ; inv_init , inv_execOp , inv_ingestTyped , inv_ingestPaste , inv_runFrom	Invariants
Def. S3.2	SinkSafe	Invariants
Lem. S3.12 (replies)	bytes_reply_isolation	Invariants
Lem. S3.13 ; Cor. S3.23 (a)	processArgs_spec , handle_always_gates , ungated_is_literal ; noexfil_semantics	Invariants; ActionIntegrity
Lem. S3.19	dt_runFrom_prefix , prefix_or_prefix	Invariants; ReasoningIntegrity

Appendix

Table S5: Correspondence between paper results and the Lean development ( PermitFormal/ ). Theorems are kernel-checked; #guard rows are evaluator-checked.

LLM Agent Memory

Large language model agent memory lets agents retain, organize, retrieve, and update information across interactions and long-running tasks.

See all 373 papers

Jul 31, 2026

Memory Provenance Laundering in LLM Agents: A Non-Amplification Firewall for Persistent Memory

Long-term memory lets large language model(LLM) agents reuse prior preferences and work flows, but it also turns untrusted observations into persistent action context. We identify memory provenance laundering: during LLM-based memory consolidation, an external observation may be rewritten as apparent user history or workflow support, preserving an action trigger while erasing the low-trust source that should limit its authority. Existing prompt filters, content sanitizers, and tool guards do not enforce source-authority non-amplification after lossy memory consolidation. We formalize this boundary and instantiate it as Provenance-Preserving Memory Fire wall (PPMF), a lightweight memory middleware that preserves platform-maintained provenance and authorizes tool calls by matching action risk to the authority of action-relevant memories. In our schema-grounded evaluation with fixed risk policies, vulnerable consolidated memories reach up to 1.000 attack success rate(ASR); with intact platform-maintained provenance, confirmation, and risk labels, no evaluated unauthorized high-risk action passes the PPMF gate while confirmed benign actions and targeted low-risk memory use remain executable.

Jinghan Xu, Yiyong Xiao, Wanru Shao +2

Agent Memory Poisoning Tool Access Control for LLM Agents Agent Memory Management Persistent Memory for Language Models LLM Agent Safety Agent Memory Governance+1

Ask PDF

Jul 27, 2026

MemTX: Transactional Belief Commit for Stateful Agent Memory

LLM agents increasingly coordinate through persistent shared memory: one agent's write becomes another agent's premise, and eventually a tool call with real side effects. Current agent memory systems treat every accepted write as immediately actionable truth, so a polluted tool result, a stale update, or a teammate's half-finished note can silently drive an irreversible action. We argue that a memory write is not a belief commit. We present MemTX, a transactional belief-commit protocol. Each record carries evidence, permissions, provenance, and validity. Writes are staged inside snapshot-isolated transactions and admitted by a validate-and-commit pipeline, irreversible tool calls are gated on in-flight belief state, and retracting a belief triggers typed cascading repair of its derived records and tool side effects. Two invariants, action-safety gating and cascade-repair completeness, are machine-checked by property-based testing and bounded exhaustive enumeration of 5.5 million protocol states, with zero violations. Across five backbones from three model families, MemTX leads all eight baselines with paired-McNemar significance on four backbones and statistically ties the best baseline on the fifth and strongest, while remaining the only method with zero downstream harm on every backbone. Backbone capability does not substitute for commit discipline.

Xiaoyang Li, Yiqi Wang, Haohui Lu +5

University of Southern Queensland · 2Griffith University · 3The University of Sydney +2

Belief Revision LLM Agent Safety Tool Access Control for LLM Agents Agent Memory Management

Ask PDF

Sep 1, 2026

Agent Memory Is a Surface for Endogenous Authorization Laundering

Long-running LLM agents rely on persistent memory to carry state across interactions, including permissions, restrictions, and revocations. When memory misrepresents this evolving authorization state, the agent's own records can grant authority that the underlying history never permitted, resulting in misaligned behavior without any external attacks. We term this failure endogenous authorization laundering, where spurious permissions written into memory lead to unauthorized actions as their provenance is washed away. We then introduce EAL-Bench, which measures how accurately persistent memory preserves evolving authorization state and whether errors propagate to downstream unauthorized actions. We evaluate five LLMs as memory writers and two as executors across procurement, cybersecurity, and finance. We find that under incremental memory updates, writers create false authority for up to 50.2% of unauthorized requests; once false authority is present, executors act on it in 98.6% of trials. Two safeguards, requiring stored permissions to be backed by valid source events, and tracking permission changes through bounded event sourcing, substantially reduce laundering, but both also reject more legitimate actions, exposing a safety-utility tradeoff. Persistent memory is therefore not merely a performance component, but a part of an LLM agent's effective authorization policy.

Tommaso Cerruti, Mika Okamoto, Ansel Kaplan Erol

ETH Zurich · Georgia Institute of Technology

LLM Agent Memory LLM Agent Security Access Control AI Agent Safety Benchmarks

Ask PDF

Abstract

LLM Agent Memory

Explore similar work

Memory Provenance Laundering in LLM Agents: A Non-Amplification Firewall for Persistent Memory

MemTX: Transactional Belief Commit for Stateful Agent Memory

Agent Memory Is a Surface for Endogenous Authorization Laundering