Broaden and harden PoC payload recovery; generate every quoted figure from the corpus

.gitignore

@@ -61,3 +61,6 @@ dev/tree-sitter/dist/
 
 dev/tree-sitter/src
 dev/tree-sitter/build
+
+# Lean artifacts
+lean/.lake/

doc/Makefile

@@ -1,14 +1,18 @@
-.PHONY: FORCE lenny all clean distclean
+.PHONY: FORCE all fast link clean open
 
 FILE=main
+BUILD=build
 
 all: $(FILE).pdf
 
-%.pdf: %.tex FORCE
-	latexmk -pdf $<
+$(FILE).pdf: $(FILE).tex FORCE
+	latexmk -pdf -outdir=$(BUILD) $(FILE).tex
+	cp $(BUILD)/$(FILE).pdf $@
 
 fast:
-	pdflatex $(FILE)
+	mkdir -p $(BUILD)
+	pdflatex -output-directory=$(BUILD) $(FILE)
+	cp $(BUILD)/$(FILE).pdf $(FILE).pdf
 
 link:
 	rm -f *.bib
@@ -17,15 +21,8 @@ link:
 	done
 
 clean:
-	for ext in aux log toc lof lot lol dlog bbl \
-		nav snm fls vrb blg out tpt fdb_latexmk; \
-	do \
-		$(RM) $(FILE).$$ext ; \
-	done
+	$(RM) -r $(BUILD)
 	$(RM) *.aux *.bak *~
 
-distclean: clean
-	$(RM) $(FILE).pdf
-	$(RM) $(FILE).ps
-	$(RM) $(FILE).dvi
-	$(RM) *.d
+open:
+	open $(FILE).pdf

doc/proof.tex → doc/always_embeddability.tex

@@ -1,8 +1,8 @@
-\section{Machine-checked Lean development}
+\section{Machine-checked: \textsc{Verify}}
 \label{app:lean}
 
 The declaration heads below summarize the Lean~4 development in
-\texttt{doc/proof.lean} that establishes \cref{thm:design:embed}
+\texttt{lean/always\_embeddability.lean} that establishes \cref{thm:design:embed}
 (there named \texttt{embedding\_closed\_under\_context}),
 faithful to the abstract definitions of \cref{sec:design:abstract}.
 The disjointness of openers and closers assumed there ($O \cap C = \emptyset$)

doc/eval.tex

@@ -329,8 +329,7 @@ \subsection{What embeddings are used for}
 The genuine embedded languages form the tail.
 Beyond the format strings, regular expressions, shell fragments,
 and HTML already visible in \cref{tab:eval:categories},
-the languages that motivate our injection discussion (\cref{sec:host:inject})
-appear only sparsely here:
+the languages that motivate our injection discussion appear only sparsely here:
 SQL accounts for 1,003,602 samples (0.79\%),
 CSS for 275,165 (0.22\%),
 JSON for 244,319 (0.19\%),
@@ -403,8 +402,7 @@ \subsection{Discussion and open questions}
 	such as synthesizing or editing HTTP or SQL queries?
 \item	How does matchertext affect the frequency of syntax-related,
 	and especially security-related, bugs in typical code?
-	The structural injection resistance of \cref{sec:host:inject}
-	bears directly on this,
+	The structural injection resistance bears directly on this,
 	but measuring its effect on real defect rates
 	is beyond what a static corpus analysis can capture.
 \end{itemize}

doc/main.tex

@@ -119,14 +119,14 @@
 
 \appendix
 \onecolumn
-\input{appendix}
+\input{always_embeddability}
 \twocolumn
 
 \bibliographystyle{plain}
 \arxiv{
-\bibliography{lang,net,sec,soc,new,thesis}
+\bibliography{lang,net,sec,soc,thesis}
 }{
-\bibliography{main,new,thesis}
+\bibliography{main,thesis}
 }
 
 \end{document}

injection-research/doc/Makefile

@@ -1,4 +1,4 @@
-.PHONY: FORCE lenny all clean distclean
+.PHONY: FORCE all fast link clean open
 
 FILE=main
 BUILD=build
@@ -24,8 +24,5 @@ clean:
 	$(RM) -r $(BUILD)
 	$(RM) *.aux *.bak *~
 
-distclean: clean
-	$(RM) $(FILE).pdf
-	$(RM) $(FILE).ps
-	$(RM) $(FILE).dvi
-	$(RM) *.d
+open:
+	open $(FILE).pdf

injection-research/doc/abs.tex

@@ -1,24 +1,25 @@
 \begin{abstract}
-Injection attacks remains one of the most persistent classes of software
-vulnerability, and the \emph{matchertext} discipline is being proposed as a
-structural defense: requiring the ASCII matcher pairs \verb|()|, \verb|[]|, and
-\verb|{}| to always match, so untrusted input in a matcher-delimited slot cannot
-break out without producing an unmatched matcher.
-This paper measures how much of the real injection landscape that proposal could
-structurally reach.
-We assemble a reproducible corpus unifying the MITRE CVE record with normalized
-enrichment and four proof-of-concept (PoC) databases, identify \textbf{91{,}760}
-injection CVEs among roughly 348k published records, and classify each by
-weakness family and by the embedded \emph{syntax} it targets.
-For the subset with an extractable PoC payload, we reduce each attack to a
-\emph{syntactic skeleton} and test whether a matchertext-aware host would contain
-it: whether the value sits in a matcher-delimited slot and is itself valid
-matchertext.
-We find that \textbf{82\%} of payload-backed injection CVEs are structurally
-contained, and, projected across all injection CVEs, at most \textbf{80\%} target
-a matcher-delimitable syntax; the residue is execution sinks and
-non-matcher-delimited contexts the discipline provably cannot address.
-These figures characterize the structure of recorded attack strings under a
-matchertext-aware host, not the behavior of a deployed defense: no such host is
-implemented or evaluated here.
+Injection remains one of the most persistent classes of software vulnerability.
+The escaping and sanitization meant to prevent it are per-language,
+per-context, and hand-applied at every use site.
+The \emph{matchertext} discipline proposes one rule instead: the ASCII matcher
+pairs \verb|()|, \verb|[]|, and \verb|{}| must always match.
+A host can then delimit an untrusted value with a matcher pair and read it to
+matcher balance, so escaping the slot would require an unmatched matcher, which
+is not valid matchertext.
+Whether that helps against injection depends on what it actually guarantees.
+We state the guarantee as an \emph{inertness} property, that the host's parse of
+a program is independent of the content placed in its holes, and reduce it to three
+premises: correct boundary location, a parser that does not re-enter the hole,
+and an interpreter that treats the hole as data.
+We then ask how much of the real landscape this could reach.
+From a reproducible corpus of \textbf{\dataInjectionCVEs} injection CVEs, classified by the
+embedded syntax each attack targets, and measuring the structure of recorded
+attack strings under a matchertext-aware host rather than a deployed one, we find
+that \textbf{\dataContainedShare} of those with a recoverable payload are structurally contained,
+and that at most \textbf{\dataHostableShare} of all injection CVEs target a matcher-delimitable
+syntax.
+The residue is execution sinks and non-matcher-delimited contexts, which no
+delimiting discipline can reach, so the boundary the measurement draws is a
+property of injection itself rather than of this design.
 \end{abstract}

injection-research/doc/classify.tex

@@ -1,10 +1,10 @@
-\section{Classification}
+\subsection{Classification}
 \label{sec:classify}
 
 We classify each injection CVE along two axes: the \emph{weakness family}
 (rooted in the CWE taxonomy) and the injection \emph{syntax type}: the
 embedded language the attack targets, such as SQL, HTML, shell, or LDAP.
-The syntax axis is the one that matters for matchertext, because prevention
+The syntax axis is the one that matters for matchertext, because containment
 depends on how the untrusted value is delimited in the target language, not on
 how the weakness is categorized.
 
@@ -13,8 +13,8 @@ \section{Classification}
 \mbox{CWE-74} (``Injection'') subtree (computed from the CWE ChildOf
 hierarchy across all enrichment sources) or if its description matches a
 phrase rule for a known injection class.
-This yields \textbf{91{,}760} injection CVEs, \textbf{26.4\%} of published
-records, spanning 351 distinct CWEs.
+This yields \textbf{\dataInjectionCVEs} injection CVEs, \textbf{\dataInjectionSharePrecise} of published
+records, spanning \dataInjectionCWEs distinct CWEs.
 
 \paragraph{Layered labeling.}
 Each CVE's syntax type is resolved by a fallback chain, ordered from most to
@@ -33,23 +33,23 @@ \section{Classification}
 
 (4) an explicit \texttt{unknown} bucket.
 
-\noindent Of the injection CVEs, 82{,}817 (90\%) are labeled deterministically from CWEs,
-7{,}657 from phrase rules, 1{,}160 from naive Bayes, and only 126 remain
+\noindent Of the injection CVEs, \dataMethodCwe (\dataMethodCweShare) are labeled deterministically from CWEs,
+\dataMethodRule from phrase rules, \dataMethodNb from naive Bayes, and only \dataMethodUnknown remain
 unknown, so the classification rests overwhelmingly on the deterministic
 layers.
 
 \paragraph{Label accuracy.}
-Only the naive-Bayes layer is statistical, and it is both the smallest (1.3\% of
-labels) and the only one we can score directly: on a held-out set of 8{,}948
-CVEs it reaches a weighted precision of \textbf{0.885} and recall of
-\textbf{0.853} at 97\% coverage, and it is strongest exactly where the
-prevention analysis is most sensitive (HTML/DOM 0.98/0.89, SQL 0.85/0.90),
+Only the naive-Bayes layer is statistical, and it is both the smallest (\dataMethodNbShare of
+labels) and the only one we can score directly: on a held-out set of \dataNbTestDocs
+CVEs it reaches a weighted precision of \textbf{\dataNbPrecision} and recall of
+\textbf{\dataNbRecall} at \dataNbCoverage coverage, and it is strongest exactly where the
+containment analysis is most sensitive (HTML/DOM \dataNbPrecisionHtmlDom/\dataNbRecallHtmlDom, SQL \dataNbPrecisionSql/\dataNbRecallSql),
 weakest on the small execution-sink classes it labels least often
-(code/eval 0.56/0.74).
-The deterministic layers carry the remaining 98\% of labels and rest on the
+(code/eval \dataNbPrecisionCodeEval/\dataNbRecallCodeEval).
+The deterministic layers carry the remaining \dataMethodDeterministicShare of labels and rest on the
 CWE-to-syntax map, whose accuracy we do not independently validate.
 Since that map dominates the syntax labels the projection of \cref{sec:prevent}
-is computed from, we export an audit sample of 75 CVEs from each labeling layer,
+is computed from, we export an audit sample of \dataAuditPerMethod CVEs from each labeling layer,
 over-sampling the rare and least reliable ones.
 
 \paragraph{Weakness families.}
@@ -58,4 +58,4 @@ \section{Classification}
 followed by command injection and code/expression injection.
 Because family and syntax are distinct axes (CRLF header injection and XSS
 share the rendering family but differ sharply in matchertext-hostability), the
-prevention analysis works from the finer syntax axis throughout.
+containment analysis works from the finer syntax axis throughout.

injection-research/doc/concl.tex

@@ -1,18 +1,32 @@
 \section{Conclusion}
 \label{sec:concl}
 
-Measured against a reproducible corpus of 91{,}760 injection vulnerabilities,
-the matchertext discipline is structurally applicable to a large and
-concentrated majority of the injection landscape: the recorded payloads of 82\%
-of attacks for which we could recover one are contained by a matcher-delimited
-slot under a matchertext-aware host, and at most 80\% of all injection CVEs
-target a syntax such a host can delimit.
+Injection is defended today one host at a time, and each defense knows the syntax
+it protects.
+This paper argues that a single host-independent check can stand in for that
+collection, and measures how far it would reach.
+The guarantee is \emph{inertness}, that a host's parse does not depend on what its
+holes contain, which is strictly stronger than the closure property the discipline
+inherits and does not follow from it without assumptions about the host.
+Naming those assumptions reduces inertness to three premises, of which the
+load-bearing one, that reading to matcher balance ends an embedded value where it
+should, is discharged here by a machine-checked proof
+(\cref{sec:appendix:lean}); the two that remain are properties of a host parser
+and its interpreter, and are per-host rather than per-context.
+Adoption is correspondingly bounded: where a format already delimits with
+matchers, as LDAP filters and PDF strings do, the discipline costs nothing at all.
+
+Measured against a reproducible corpus of \dataInjectionCVEs injection vulnerabilities,
+that reach is a large and concentrated majority of the landscape: the recorded
+payloads of \dataContainedShare of attacks for which we could recover one are contained by a
+matcher-delimited slot under a matchertext-aware host, and at most \dataHostableShare of all
+injection CVEs target a syntax such a host can delimit.
 The corpus also shows the shape of the containment, not only its size: it
 divides into inert embedding and outright rejection along the host language's
 native delimiter, the division \cref{sec:resist} derives, though the ratio
 between the two is a property of these recorded payloads rather than of an
 adaptive attacker.
-The residue falls along the two conditions of \cref{sec:threat}: execution sinks,
+The residue falls along the two premises of \cref{sec:threat}: execution sinks,
 where the host runs the value by design, and contexts whose delimiters are not
 matchers, neither of which any delimiting discipline can reach.
 The pipeline, corpus manifest, and per-skeleton rewrites are the concrete basis