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 376 papers

Memory Provenance Laundering in LLM Agents: A Non-Amplification Firewall for Persistent Memory
Jul 31, 2026Jinghan Xu, Yiyong Xiao, Wanru Shao +2Agent Memory Poisoning Tool Access Control for LLM Agents
MemTX: Transactional Belief Commit for Stateful Agent Memory
Jul 27, 2026Xiaoyang Li, Yiqi Wang, Haohui Lu +5Belief Revision LLM Agent Safety
University of Southern Queensland · 2Griffith University · 3The University of Sydney +2
Agent Memory Is a Surface for Endogenous Authorization Laundering
Sep 1, 2026Tommaso Cerruti, Mika Okamoto, Ansel Kaplan ErolLLM Agent Memory LLM Agent Security
ETH Zurich · Georgia Institute of Technology

Jul 31, 2026J/K move · Enter open · S save

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

Jinghan Xu, Yiyong Xiao, Wanru Shao, Hankai Liu+1

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

Open paper AskPDF arXiv

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.

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