Agent-assistance disclosure: this work was prepared with AI-agent assistance (drafting, code, experiments) under human direction. The authors, writing as Third Projection Collective, take responsibility for its content. Open proofs are marked [OPEN] in the text.
Abstract
Abela and Vella cast exploit analysis as reconstructing a weird machine (WM): a map $f:\Sigma\to L^*$ sending script fragments to strings of exploit-primitive labels, where each label $l$ denotes a memory-state transition $\delta_l$ [1]. We give this a denotational semantics. (1) The definitions as stated do not compose: each $\delta_l$ has its own state abstraction $W\to W'$ and is called a function while being defined by constraints. Reading primitives as relations on a single product state space makes labels a monoid homomorphism $L^*\to\mathrm{Rel}(W,W)$, i.e. a functor into the Kleisli category of the powerset monad. (2) The explanations $\mathrm{Ex}(w,w')=\{s\in L^*:(w,w')\in\delta_s\}$ make $W$ a category enriched in the quantale $\mathcal P(L^*)$ of languages, and reconstruction is computing its hom-objects. For finite abstractions each hom-object is regular. (3) For the paper's own allocation and free primitives on heap size we compute $\mathrm{Ex}$ exactly (checked by brute force on 12{,}495 cases). Every hom-object is infinite, and the string alloc$\cdot$free explains every observation, so a label $f(p)$ is never determined by observed states; minimal explanations carry only the sign of the heap change. Open problems: a 2-categorical presentation of the equations between explanations, completeness of the stack-based compound-statement algorithm, and any re-validation of the original prototype, which we did not run.
1. The definitions, repaired
In [1], Definition 1 types a primitive's behaviour as $\delta_l:\mathcal P(W)\times\Sigma\to\mathcal P(W')$ over a primitive-specific abstraction, and § IV defines each $\delta_l$ by a constraint, e.g. $\delta_{\mathrm{memalloc}}(\{w_0\},p)=\{w_0'\}$ for all $p$ with $w_0'>w_0$. That constraint admits many $w_0'$, so $\delta_l$ is a relation, not a function; and since $W\neq W'$ in general and each primitive uses a different $W$, the composite semantics of a label string $l^*$ promised by Definition 2 is not defined. We fix both.
Definition 1
Let $W$ be a set of abstract states (the product of all components used by any primitive). A primitive theory is a set $L$ of labels with relations $\delta_l\subseteq W\times W$. Extend to strings by $\delta_\varepsilon=\mathrm{id}_W$ and $\delta_{st}=\delta_s;\delta_t$ (relational composition). Given an observation $(w,w')$, its explanations are $\mathrm{Ex}(w,w')=\{s\in L^*:(w,w')\in\delta_s\}$.
Components a primitive does not mention are unconstrained unless a frame condition is stated; [1] states one only for the code/stack region component ($w_1'=w_1$). Dependence on the fragment $p$ is dropped: no $\delta_l$ in [1] uses it.
Proposition 2
$s\mapsto\delta_s$ is the unique monoid homomorphism $L^*\to(\mathrm{Rel}(W,W),;,\mathrm{id})$ extending $l\mapsto\delta_l$; equivalently a functor from the one-object free category on $L$ into $\mathrm{Kl}(\mathcal P)$.
Proof. $L^*$ is the free monoid on $L$ and relational composition is associative with unit $\mathrm{id}_W$; $\mathrm{Rel}=\mathrm{Kl}(\mathcal P)$. ∎
2. Explanations as an enriched category
$\mathcal P(L^*)$ with union and concatenation is a unital quantale (unit $\{\varepsilon\}$).
Theorem 3
$\mathrm{Ex}$ makes $W$ a $\mathcal P(L^*)$-enriched category: $\{\varepsilon\}\subseteq\mathrm{Ex}(w,w)$ and $\mathrm{Ex}(w,m)\cdot\mathrm{Ex}(m,w')\subseteq\mathrm{Ex}(w,w')$. Conversely, for any factorization $u=st$, $u\in\mathrm{Ex}(w,w')$ iff $s\in\mathrm{Ex}(w,m)$ and $t\in\mathrm{Ex}(m,w')$ for some $m$.
Proof. $\delta_\varepsilon=\mathrm{id}$ gives identities. If $(w,m)\in\delta_s$ and $(m,w')\in\delta_t$ then $(w,w')\in\delta_s;\delta_t=\delta_{st}$. Conversely if $(w,w')\in\delta_{st}$, by definition of relational composition some $m$ has $(w,m)\in\delta_s$, $(m,w')\in\delta_t$. ∎
Thus composition along observed intermediate states is sound for the compound-statement case of WMRecon (Algorithm 1 in [1]): labels found for consecutive sub-fragments concatenate to an explanation of the block. The converse direction, that WMRecon's stack discipline finds every explanation of a block, depends on which intermediate states the tool observes and is OPEN.
Proposition 4
If $W$ is finite, every $\mathrm{Ex}(w,w')$ is a regular language, recognized by the NFA with states $W$, transitions $x\xrightarrow{l}y$ for $(x,y)\in\delta_l$, start $w$, accept $w'$. The matrix $M=\sum_l \delta_l\, l$ over the Kleene algebra of languages has $\mathrm{Ex}=M^*$.
Proof. A run of that NFA on $s$ from $w$ to $w'$ is exactly a chain witnessing $(w,w')\in\delta_s$. $M^*$ is the standard Kleene-algebra closure of a matrix [2]. ∎
The NFA is the reconstructed WM read as an automaton; this matches Dullien's finite-state view of weird machines [3], which models the machine but not the analyst's explanation problem.
3. The allocation primitives, computed
Take the heap component $W=\mathbb N$ (allocated size) and $L=\{a,f\}$ with $\delta_a=\{(x,y):y>x\}$, $\delta_f=\{(x,y):y<x\}$, exactly as in [1], § IV-A.
Theorem 5
For $s\in\{a,f\}^*$ let $k_f(s)$ be the length of its leading run of $f$ and $k_a(s)$ the length of its trailing run of $a$. Then $s\in\mathrm{Ex}(w,w')$ iff: $s=\varepsilon$ and $w=w'$; or $s=a^k$, $k\ge1$, $w'-w\ge k$; or $s=f^k$, $k\ge1$, $w-w'\ge k$; or $s$ contains both letters, $k_f(s)\le w$ and $k_a(s)\le w'$.
Proof. An $a$-run of length $q$ from $x$ can end at exactly the values $y\ge x+q$; an $f$-run of length $r$ from $x$ at exactly $0\le y\le x-r$. Pure strings follow. Suppose both letters occur. Necessity: the leading $f$-run starts at $w$, so $w\ge k_f$; the trailing $a$-run starts at a value $\ge0$, so $w'\ge k_a$. Sufficiency: send every $f$-run to $0$ except a final $f$-run, which we send to $w'$; send every $a$-run that is followed by an $f$-run of length $r$ to $\max(x+q,\,r+w')$, which is legal and leaves room for that $f$-run. The leading $f$-run (if any) reaches $0$ since $w\ge k_f$. If $s$ ends in an $a$-run, it starts at $0$ and reaches $w'$ since $w'\ge k_a$. ∎
code/check.py compares the theorem with brute-force relational composition for all $|s|\le7$ and $w,w'\le6$ (12{,}495 cases, intermediates bounded by 60): zero mismatches.
Corollary 6
(i) $af\in\mathrm{Ex}(w,w')$ for all $w,w'$; every hom-object is infinite. (ii) $\delta_{aa}\subsetneq\delta_a$, so labels are not idempotent and $\{a^k\}$ distinguishes counts only as lower bounds. (iii) The shortest explanation of $(w,w')$ is $\varepsilon$, $a$ or $f$ according to the sign of $w'-w$.
Proof. (i) $k_f(af)=k_a(af)=0$; and $a f^n\in\mathrm{Ex}(w,w)$ for all $n$. (ii) $(0,1)\in\delta_a\setminus\delta_{aa}$. (iii) From Theorem 5. ∎
So, for these primitives, the label $f(p)$ that WMRecon assigns is a choice and not a consequence of observations: the observation pair determines only a sign, and the five-allocation loop in [1], Fig. 2 is labelled “AllocPrimitive” consistently with this. Explanation counts grow quickly; for $(0,3)$ the numbers of explanations of length $0,\dots,7$ are $0,1,2,4,7,15,30,60$ (computed). This is the WM analogue of proof multiplicity in e-graphs [4]. For the execute-crafted-code primitive with frame $w_1'=w_1$, $\delta_e=\{((pc,C),(pc',C)):pc'\notin C\}$ satisfies $\delta_e;\delta_e=\delta_e$ whenever some address lies outside $C$, so $e^n$ for all $n\ge1$ explain the same observations: an idempotent label.
4. Open problems
OPEN 1. Equations such as $\delta_e^2=\delta_e$ and $\delta_{aa}\subseteq\delta_a$ are 2-cells between explanations. A presentation of the 2-category (or Kleene algebra with hypotheses) they generate, and a canonical-form theorem selecting one label string per observation, is not proved here. OPEN 2. Completeness of WMRecon's stack algorithm relative to Theorem 3. OPEN 3. We did not run the original DynamoRIO prototype and make no claim about its empirical results. A WM is an interpreter without a specification; relating reconstruction to the specializer semantics of [5] is left as a remark.
References
[1] Robert Abela and Mark Vella. Casting exploit analysis as a Weird Machine reconstruction problem. 2021, arXiv:2109.13100 [cs.CR]; arXiv metadata gives DOI 10.2053/WorldCIS.2017.0012 (WorldCIS 2017).
[2] Dexter Kozen. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Information and Computation, 110, 2, 1994. DOI: 10.1006/inco.1994.1037.
[3] Thomas Dullien. Weird Machines, Exploitability, and Provable Unexploitability. IEEE Transactions on Emerging Topics in Computing, 8, 2, 2020. DOI: 10.1109/TETC.2017.2785299.
[4] Third Projection Collective. The Homotopy Type of E-Graph Explanations: Measuring Proof Multiplicity in Equality Saturation. 2026, Source.
[5] Third Projection Collective. Computing the Futamura Diamond. 2026, Source.
Web presentation: document structure, notation, theorem references, and citations were converted from the attached LaTeX source. The original source bundle, PDF, and computational artifacts remain available below.