diff --git a/.gitignore b/.gitignore index be53a50..15911f4 100644 --- a/.gitignore +++ b/.gitignore @@ -61,3 +61,6 @@ dev/tree-sitter/dist/ dev/tree-sitter/src dev/tree-sitter/build + +# Lean artifacts +lean/.lake/ diff --git a/doc/Makefile b/doc/Makefile index 1d5dbde..39deba5 100644 --- a/doc/Makefile +++ b/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 diff --git a/doc/proof.tex b/doc/always_embeddability.tex similarity index 95% rename from doc/proof.tex rename to doc/always_embeddability.tex index 49600ce..68fec08 100644 --- a/doc/proof.tex +++ b/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$) diff --git a/doc/eval.tex b/doc/eval.tex index 58e6869..da96b99 100644 --- a/doc/eval.tex +++ b/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} diff --git a/doc/main.tex b/doc/main.tex index c8fe31a..e1dfeff 100644 --- a/doc/main.tex +++ b/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} diff --git a/injection-research/doc/Makefile b/injection-research/doc/Makefile index 24aa833..39deba5 100644 --- a/injection-research/doc/Makefile +++ b/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 \ No newline at end of file +open: + open $(FILE).pdf diff --git a/injection-research/doc/abs.tex b/injection-research/doc/abs.tex index 87344cf..2ace122 100644 --- a/injection-research/doc/abs.tex +++ b/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} diff --git a/injection-research/doc/classify.tex b/injection-research/doc/classify.tex index 4186aad..d076825 100644 --- a/injection-research/doc/classify.tex +++ b/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. diff --git a/injection-research/doc/concl.tex b/injection-research/doc/concl.tex index 30a6fee..d2ea6de 100644 --- a/injection-research/doc/concl.tex +++ b/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 diff --git a/injection-research/doc/containment.tex b/injection-research/doc/containment.tex new file mode 100644 index 0000000..652aac2 --- /dev/null +++ b/injection-research/doc/containment.tex @@ -0,0 +1,143 @@ +\section{Measuring matchertext containment} +\label{sec:prevent} + +Matchertext contains an injection under mainly two conditions: the untrusted value lands in a slot +a matchertext-aware host delimits with a matcher pair, and the value is itself +valid matchertext, checked by the passive \textsc{Verify} scan rather than by +escaping. +An attack then fails one of two ways, by \emph{inert embedding} or by +\emph{rejection}, and which route a real attack takes is a property of the +payload, and so measurable against the corpus. + +\begin{figure*}[t] +\footnotesize +\input{generated/fig-tree} +\caption{Containment outcome as two decisions. The context condition is tested +first, so the \dataOutsideCVEs outside are never candidates rather than escapes; the value +condition then separates inert embedding from rejection. The leaves reconcile +with \cref{tab:mech}.} +\label{fig:prevent:tree} +\end{figure*} + +\paragraph{Method.} +For each of the \dataPayloadBackedCVEs payload-backed CVEs we reuse its syntactic skeleton and decide two things: +whether the target syntax is one a matchertext host can delimit with a matcher +pair, and, if so, whether the skeleton passes \textsc{Verify}. +A passing skeleton is contained by \emph{inert embedding}; a failing one is +stopped by \emph{rejection}. +This test characterizes the structure of each recorded payload under a +matchertext-aware host; it does not exercise a deployed host parser, which we +leave to future implementation work. + +\begin{table}[t] +\centering +\small +\input{generated/tbl-mech} +\caption{Containment outcome by syntax over all \dataPayloadBackedCVEs payload-backed CVEs. +Contexts a matchertext host can delimit (upper block) are contained by inert +embedding or by rejection; the \emph{Outside} column counts CVEs failing a +premise of \cref{sec:threat}, either an execution sink (the HTML/DOM entries +are \texttt{javascript:} URLs) or a context whose delimiters are not matchers.} +\label{tab:mech} +\end{table} + +\paragraph{Results.} +Of the \dataPayloadBackedCVEs payload-backed injection CVEs, the recorded payloads of +\textbf{\dataContained} (\textbf{\dataContainedShare}) are contained by a matcher-delimited slot that a +matchertext-aware host reads to matcher balance, assuming no intervening +decoding; the split turns on the host's native delimiter. +The per-syntax mechanisms of \cref{sec:resist} appear directly in the corpus. +LDAP is the pure rejection case: every real LDAP payload fails \textsc{Verify} +(\dataLdapInert inert, \dataLdapRejected rejected), its parenthesis breakout carrying an unmatched \verb|)|. +SQL and XSS, breaking out on nonmatchers, are overwhelmingly valid matchertext +and embed inertly; the \dataSqlRejected SQL rejections additionally carry an unbalanced +function or subquery parenthesis. +The ratio between the two mechanisms is descriptive, not predictive. +These payloads were written against quote and tag-delimited hosts; an attacker +aware of a matcher-delimited slot would balance the matchers, shifting cases +from rejection to inert embedding. +Containment is unaffected, since both routes hold the value, but the split +itself is a property of the recorded corpus rather than of an adaptive attacker. + +\paragraph{Where matchertext cannot help.} +The remaining \dataOutsideCVEs payload-backed CVEs are outside both conditions, and divide +by the premise of \cref{sec:threat} they fail. +\dataOutsideSemantic target execution/semantic sinks (server-side templates, expression +languages, code evaluation, spreadsheet formulas, and \verb|javascript:| URLs) +where the host runs the contained value by design, so delimiting cannot stop +it: the template payload \verb|{{7*7}}| is already valid matchertext yet is +still executed. +The other \dataOutsideNonmatcher target contexts delimited by non-matchers with no matcher hosting: +shell command separators (\verb|;|~\verb-|-~\verb|&|), CR/LF header breaks, and +the angle brackets of XML/XXE, none of which are matcher characters. + +\paragraph{Projection.} +A payload is required to classify the mechanism, but the \emph{context} +condition can be read from the syntax label alone. +Projecting it onto the full corpus, at most \textbf{\dataHostableCVEs} of the +\textbf{\dataInjectionCVEs} injection CVEs (\textbf{\dataHostableShare}) target a matcher-delimitable +syntax. +This is an upper bound, since a fraction of HTML/DOM cases are the +\verb|javascript:| semantic sinks above: \dataHtmlDomJsSinks of the +\dataHtmlDomBacked HTML/DOM CVEs carrying a payload are such sinks, a rate of +\textbf{\dataJsSinkRate}. + +Turning the measured rate into a corpus estimate needs care, because +payload-backed CVEs are not a random sample. +A SQL injection payload is a literal string a write-up can quote, whereas +code-eval and argument payloads are usually built at run time and never appear +verbatim, so payload availability correlates with syntax and specifically with +matcher-hostable syntax. +Applying the pooled \dataContainedShare to the whole corpus inherits that skew +and yields \dataNaiveEstimate (\dataNaiveShare), too high by \dataSkewCost CVEs. +We therefore estimate a containment rate per syntax and weight by the corpus +counts (\cref{tab:strata}), the standard post-stratification correction, giving +a central estimate of \textbf{\dataCentralEstimate} +(\textbf{\dataCentralShare}) against the \dataHostableShare ceiling. +Within a syntax the estimate still assumes payload-backed CVEs carry semantic sinks at +the same rate as the rest, which their skew toward exploitable web bugs may not +warrant. + +\begin{table}[t] +\centering +\small +\input{generated/tbl-strata} +\caption{Post-stratification strata. The containment rate is measured on the +payload-backed CVEs of each syntax and applied to that syntax's share of the +corpus, so the estimate does not inherit the sampling skew of the subset. +A dagger would mark a syntax with no payload-backed CVE, whose rate falls back +to the structural rule of \cref{sec:threat}.} +\label{tab:strata} +\end{table} +Read against a single denominator, the full \dataInjectionCVEs injection CVEs, +the reach of the discipline runs from a floor of \textbf{\dataFloorShare} to a +ceiling of \textbf{\dataHostableShare}, with \dataCentralShare as the central +estimate. +The floor counts only the \dataContained CVEs whose recorded payload we verified +as contained, and treats every CVE without a recoverable payload as uncontained; +it is therefore a hard lower bound rather than an estimate. +The \dataContainedShare reported above is a different quantity, the contained +share \emph{within} the payload-backed subset, and does not sit on this scale: +it answers what happens once a payload is known, not how much of the corpus that +covers. +The gap between \dataPayloadBackedCVEs and \dataInjectionCVEs is payload +availability, not a containment failure. + +\paragraph{What payload availability bounds.} +That gap is a property of the disclosure ecosystem rather than of our +extraction. +Most CVEs never receive a public proof of concept at all: Mandiant finds that +\textbf{51\%} of vulnerabilities disclosed in 2021 and 2022 eventually acquired +public exploit or proof-of-concept code~\cite{mandiant23tte}, and VulnCheck +reports \textbf{26\%} of CVEs carrying 2025 identifiers had such code by the end +of that year, a share that grows as a vulnerability +ages~\cite{vulncheck26exploit}. +Our corpus agrees from the other direction: \dataInjectionWithPoc injection CVEs +(\dataInjectionWithPocShare) carry any proof-of-concept reference whatsoever, so +for the remainder there is no artifact to recover, from this pipeline or any +other. +A literal attack string is a stricter requirement still, since a proof of +concept that constructs its payload at run time exposes none. +The measurable population is therefore roughly half the corpus rather than all +of it, and the fragment-level bound should be read against that population, not +against \dataInjectionCVEs. diff --git a/injection-research/doc/corpus.tex b/injection-research/doc/corpus.tex new file mode 100644 index 0000000..095fd07 --- /dev/null +++ b/injection-research/doc/corpus.tex @@ -0,0 +1,5 @@ +\section{Corpus and classification} +\label{sec:corpus} + +\input{data} +\input{classify} diff --git a/injection-research/doc/data.tex b/injection-research/doc/data.tex index c262d03..c4945fe 100644 --- a/injection-research/doc/data.tex +++ b/injection-research/doc/data.tex @@ -1,4 +1,4 @@ -\section{Data sources} +\subsection{Data sources} \label{sec:data} Every source is keyed on the CVE identifier, so no vulnerability is duplicated; @@ -28,25 +28,31 @@ \section{Data sources} measure cross-source disagreement. \paragraph{Proof-of-concept payloads.} -Four PoC databases supply real attack strings: +Six PoC databases supply real attack strings: \href{https://gitlab.com/exploit-database/exploitdb}{Exploit-DB}, the \href{https://github.com/projectdiscovery/nuclei-templates}{Nuclei detection templates}, the \href{https://github.com/rapid7/metasploit-framework}{Metasploit Framework} -modules, and the -\href{https://github.com/nomi-sec/PoC-in-GitHub}{nomi-sec PoC-in-GitHub} index. -The first three are cloned locally so that a payload can be extracted from the -exploit file; the last contributes links only. +modules, the +\href{https://github.com/nomi-sec/PoC-in-GitHub}{nomi-sec PoC-in-GitHub} index, +the \href{https://github.com/trickest/cve}{trickest/cve} exploit index, and +\href{https://github.com/vulhub/vulhub}{Vulhub}'s reproduction environments. +The first three, and Vulhub's worked exploit requests, are cloned locally so +that a payload can be extracted; PoC-in-GitHub and trickest contribute links +only. +A trickest entry separates candidate exploit repositories from advisory +write-ups, and only the former are counted as PoC evidence. PoC references are unified in a single table, with a local path where a payload is extractable. Because exploit code is dual-use, the corpus stores only links, identifiers, and locally-extracted payload fragments; no exploit files are redistributed. \paragraph{Scale.} -The pinned snapshot comprises \textbf{365{,}310} CVE records -(\textbf{347{,}651} in the \texttt{PUBLISHED} state). -Across all categories the PoC databases link to 25{,}041 CVEs (Exploit-DB), -8{,}975 (PoC-in-GitHub), 4{,}256 (Nuclei), and 3{,}106 (Metasploit); their +The pinned snapshot comprises \textbf{\dataCVERecords} CVE records +(\textbf{\dataPublishedCVEs} in the \texttt{PUBLISHED} state). +Across all categories the PoC databases link to \dataPocTrickestCVEs CVEs (trickest), +\dataPocExploitdbCVEs (Exploit-DB), \dataPocGithubCVEs (PoC-in-GitHub), \dataPocNucleiCVEs (Nuclei), +\dataPocMetasploitCVEs (Metasploit), and \dataPocVulhubCVEs (Vulhub); their coverage of the injection subset is reported with the results in \cref{sec:results}. A key methodological caveat is that these sources have different, sometimes diff --git a/injection-research/doc/appendix.tex b/injection-research/doc/embeded_boundary.tex similarity index 71% rename from injection-research/doc/appendix.tex rename to injection-research/doc/embeded_boundary.tex index 32e1cc8..a1230b2 100644 --- a/injection-research/doc/appendix.tex +++ b/injection-research/doc/embeded_boundary.tex @@ -1,37 +1,21 @@ -\section{Machine-checked Lean development} +\section{Machine-checked: \textsc{FindEmbedEnd}} \label{sec:appendix:lean} The declaration heads below summarize the Lean~4 development in -\texttt{injection-research/doc/proof.lean} that establishes premise~L1 of \cref{sec:threat} (there +\texttt{lean/embed\_boundary.lean} that establishes premise~L1 of \cref{sec:threat} (there named \texttt{embed\_boundary}), extending the machine-checked closure development of~\cite{matchertext} with the boundary characterization that closure alone does not supply. Tactic proof bodies are elided here and given in full in the source file. \begin{lstlisting} -import Mathlib +import core + open Classical variable {α : Type*} -- the alphabet Σ, kept abstract variable (Pi : Set (α × α)) -- the set of pairs Π -def Opener (x : α) : Prop := ∃ y, (x, y) ∈ Pi -def Closer (x : α) : Prop := ∃ y, (y, x) ∈ Pi -def Matcher (x : α) : Prop := Opener Pi x ∨ Closer Pi x -def Nonmatcher (x : α) : Prop := ¬ Matcher Pi x - --- Lemma: no opener can be a closer, and vice versa. -theorem disjoint - (h : ∀ x y z, (x, y) ∈ Pi → (z, x) ∈ Pi → False) - (x : α) : ¬ (Opener Pi x ∧ Closer Pi x) := by ... - --- The inductive definition of matchertext. -inductive MT (Pi : Set (α × α)) : List α → Prop where - | flat (n : List α) (h : ∀ x ∈ n, Nonmatcher Pi x) : MT Pi n - | nest (m₁ m₂ m₃ : List α) (o c : α) (hp : (o, c) ∈ Pi) - (h₁ : MT Pi m₁) (h₂ : MT Pi m₂) (h₃ : MT Pi m₃) : - MT Pi (m₁ ++ [o] ++ m₂ ++ [c] ++ m₃) - -- Net matcher depth: +1 per opener, -1 per closer, 0 per nonmatcher. Noncomputable since only -- a host implementation would need a computable version. noncomputable def delta (x : α) : Int := if Opener Pi x then 1 else if Closer Pi x then -1 else 0 diff --git a/injection-research/doc/generated/fig-tree.tex b/injection-research/doc/generated/fig-tree.tex new file mode 100644 index 0000000..20e00c6 --- /dev/null +++ b/injection-research/doc/generated/fig-tree.tex @@ -0,0 +1,15 @@ +%% GENERATED by pipeline/latex.py -- do not edit. +%% Regenerate with: python3 pipeline/latex.py +\begin{verbatim} + 11,265 payload-backed CVEs + ┌──────────────┴──────────────┐ + yes no + matcher-delimitable context? OUTSIDE + 9,275 (82%) 1,990 (18%) + ┌───────────┴───────────┐ ┌──────────┴──────────┐ + pass fail 807 1183 + VERIFY(v) VERIFY(v) execution sinks non-matcher delimiters + ▼ ▼ templates, eval, shell ; | & + INERT EMBED REJECTED javascript: CR/LF, XML <> + 8,761 (94%) 514 (6%) (A4) +\end{verbatim} diff --git a/injection-research/doc/generated/numbers.tex b/injection-research/doc/generated/numbers.tex new file mode 100644 index 0000000..22452f4 --- /dev/null +++ b/injection-research/doc/generated/numbers.tex @@ -0,0 +1,116 @@ +%% GENERATED by pipeline/latex.py -- do not edit. +%% Regenerate with: python3 pipeline/latex.py +\newcommand{\dataPublishedCVEs}{347{,}651\xspace} +\newcommand{\dataCVERecords}{365{,}310\xspace} +\newcommand{\dataInjectionCVEs}{91{,}760\xspace} +\newcommand{\dataInjectionShare}{26\%\xspace} +\newcommand{\dataInjectionSharePrecise}{26.4\%\xspace} +\newcommand{\dataInjectionCWEs}{351\xspace} +\newcommand{\dataInjectionKev}{345\xspace} +\newcommand{\dataMethodCwe}{82{,}817\xspace} +\newcommand{\dataMethodCweShare}{90\%\xspace} +\newcommand{\dataMethodRule}{7{,}657\xspace} +\newcommand{\dataMethodNb}{1{,}160\xspace} +\newcommand{\dataMethodNbShare}{1.3\%\xspace} +\newcommand{\dataMethodUnknown}{126\xspace} +\newcommand{\dataNbTestDocs}{8{,}948\xspace} +\newcommand{\dataNbPrecision}{0.885\xspace} +\newcommand{\dataNbRecall}{0.853\xspace} +\newcommand{\dataNbCoverage}{97\%\xspace} +\newcommand{\dataNbPrecisionHtmlDom}{0.98\xspace} +\newcommand{\dataNbRecallHtmlDom}{0.89\xspace} +\newcommand{\dataNbPrecisionSql}{0.85\xspace} +\newcommand{\dataNbRecallSql}{0.90\xspace} +\newcommand{\dataNbPrecisionCodeEval}{0.56\xspace} +\newcommand{\dataNbRecallCodeEval}{0.74\xspace} +\newcommand{\dataMethodDeterministicShare}{98.6\%\xspace} +\newcommand{\dataAuditPerMethod}{75\xspace} +\newcommand{\dataInjectionWithPoc}{52{,}684\xspace} +\newcommand{\dataInjectionWithPocShare}{57\%\xspace} +\newcommand{\dataPocRows}{481{,}880\xspace} +\newcommand{\dataPocTrickestCVEs}{164{,}200\xspace} +\newcommand{\dataPocExploitdbCVEs}{27{,}934\xspace} +\newcommand{\dataPocGithubCVEs}{8{,}975\xspace} +\newcommand{\dataPocNucleiCVEs}{4{,}256\xspace} +\newcommand{\dataPocMetasploitCVEs}{3{,}106\xspace} +\newcommand{\dataPocVulhubCVEs}{245\xspace} +\newcommand{\dataKevRows}{1{,}638\xspace} +\newcommand{\dataVedasScored}{306{,}029\xspace} +\newcommand{\dataPayloadBackedCVEs}{11{,}265\xspace} +\newcommand{\dataDistinctSkeletons}{4{,}858\xspace} +\newcommand{\dataSingletonGroups}{3{,}972\xspace} +\newcommand{\dataSingletonGroupShare}{82\%\xspace} +\newcommand{\dataSingletonCVEShare}{35\%\xspace} +\newcommand{\dataSingletonVerdicts}{16\xspace} +\newcommand{\dataTopTwoShare}{80\%\xspace} +\newcommand{\dataGroupAlertDocId}{507\xspace} +\newcommand{\dataGroupAlertCookie}{327\xspace} +\newcommand{\dataGroupPhpOpen}{0\xspace} +\newcommand{\dataSubPrivilegeAuthenticated}{1{,}591\xspace} +\newcommand{\dataSubPrivilegeHighPriv}{11{,}085\xspace} +\newcommand{\dataSubPrivilegeLowPriv}{28{,}471\xspace} +\newcommand{\dataSubPrivilegePreAuth}{50{,}607\xspace} +\newcommand{\dataSubTechniqueArgument}{496\xspace} +\newcommand{\dataSubTechniqueAuthBypass}{341\xspace} +\newcommand{\dataSubTechniqueBlind}{16\xspace} +\newcommand{\dataSubTechniqueBlindBoolean}{944\xspace} +\newcommand{\dataSubTechniqueBlindTime}{905\xspace} +\newcommand{\dataSubTechniqueDde}{16\xspace} +\newcommand{\dataSubTechniqueDeserialization}{63\xspace} +\newcommand{\dataSubTechniqueDomBased}{1{,}853\xspace} +\newcommand{\dataSubTechniqueEl}{245\xspace} +\newcommand{\dataSubTechniqueErrorBased}{127\xspace} +\newcommand{\dataSubTechniqueEval}{321\xspace} +\newcommand{\dataSubTechniqueFileAccess}{20\xspace} +\newcommand{\dataSubTechniqueFileInclusion}{773\xspace} +\newcommand{\dataSubTechniqueFilterBreakout}{2\xspace} +\newcommand{\dataSubTechniqueHeaderInjection}{476\xspace} +\newcommand{\dataSubTechniqueHyperlink}{4\xspace} +\newcommand{\dataSubTechniqueJsInjection}{9\xspace} +\newcommand{\dataSubTechniqueMacro}{301\xspace} +\newcommand{\dataSubTechniqueMutation}{21\xspace} +\newcommand{\dataSubTechniqueOgnlSpel}{28\xspace} +\newcommand{\dataSubTechniqueOperator}{3\xspace} +\newcommand{\dataSubTechniqueReflected}{6{,}318\xspace} +\newcommand{\dataSubTechniqueResponseSplitting}{180\xspace} +\newcommand{\dataSubTechniqueSandboxEscape}{19\xspace} +\newcommand{\dataSubTechniqueSeparator}{697\xspace} +\newcommand{\dataSubTechniqueSsti}{192\xspace} +\newcommand{\dataSubTechniqueStacked}{6\xspace} +\newcommand{\dataSubTechniqueStored}{15{,}485\xspace} +\newcommand{\dataSubTechniqueSubstitution}{954\xspace} +\newcommand{\dataSubTechniqueUnionBased}{2{,}802\xspace} +\newcommand{\dataSubTechniqueXmlInjection}{150\xspace} +\newcommand{\dataSubTechniqueXxe}{9\xspace} +\newcommand{\dataContained}{9{,}275\xspace} +\newcommand{\dataContainedShare}{82\%\xspace} +\newcommand{\dataFloorShare}{10.1\%\xspace} +\newcommand{\dataInertCVEs}{8{,}761\xspace} +\newcommand{\dataRejectedCVEs}{514\xspace} +\newcommand{\dataOutsideCVEs}{1{,}990\xspace} +\newcommand{\dataOutsideSemantic}{807\xspace} +\newcommand{\dataOutsideNonmatcher}{1{,}183\xspace} +\newcommand{\dataSqlRejected}{477\xspace} +\newcommand{\dataLdapInert}{0\xspace} +\newcommand{\dataLdapRejected}{1\xspace} +\newcommand{\dataHostableCVEs}{73{,}246\xspace} +\newcommand{\dataHostableShare}{80\%\xspace} +\newcommand{\dataHtmlDomCVEs}{50{,}884\xspace} +\newcommand{\dataHtmlDomBacked}{4{,}862\xspace} +\newcommand{\dataHtmlDomJsSinks}{284\xspace} +\newcommand{\dataJsSinkRate}{5.8\%\xspace} +\newcommand{\dataJsSinkRemoved}{2{,}972\xspace} +\newcommand{\dataCentralEstimate}{70{,}274\xspace} +\newcommand{\dataNaiveEstimate}{75{,}550\xspace} +\newcommand{\dataNaiveShare}{82\%\xspace} +\newcommand{\dataSkewCost}{5{,}276\xspace} +\newcommand{\dataCentralShare}{77\%\xspace} +\newcommand{\dataCorpusPayloads}{25{,}369\xspace} +\newcommand{\dataCorpusHostable}{14{,}670\xspace} +\newcommand{\dataCorpusInert}{12{,}938\xspace} +\newcommand{\dataCorpusRejected}{713\xspace} +\newcommand{\dataCorpusInertShare}{94.8\%\xspace} +\newcommand{\dataCorpusRejectedShare}{5.2\%\xspace} +\newcommand{\dataGroundTruthCases}{149{,}811\xspace} +\newcommand{\dataGroundTruthPairs}{241\xspace} +\newcommand{\dataGroundTruthResolved}{15\xspace} diff --git a/injection-research/doc/generated/tbl-anchors.tex b/injection-research/doc/generated/tbl-anchors.tex new file mode 100644 index 0000000..0bfa1e6 --- /dev/null +++ b/injection-research/doc/generated/tbl-anchors.tex @@ -0,0 +1,23 @@ +%% GENERATED by pipeline/latex.py -- do not edit. +%% Regenerate with: python3 pipeline/latex.py +\begin{tabular}{llrll} +\toprule +Suite & CWE & Cases & Family & Syntax \\ +\midrule +\texttt{juliet-c} & 78 & 7{,}800 & command injection & Shell command \\ +\texttt{juliet-c} & 90 & 780 & query injection & LDAP \\ +\texttt{juliet-java} & 89 & 3{,}660 & query injection & SQL \\ +\texttt{juliet-java} & 113 & 2{,}196 & rendering injection & CRLF / header \\ +\texttt{juliet-java} & 80 & 1{,}080 & rendering injection & HTML / DOM (XSS) \\ +\texttt{juliet-java} & 643 & 732 & query injection & XPath / XQuery \\ +\texttt{juliet-java} & 78 & 720 & command injection & Shell command \\ +\texttt{juliet-java} & 90 & 720 & query injection & LDAP \\ +\texttt{juliet-java} & 81 & 540 & rendering injection & HTML / DOM (XSS) \\ +\texttt{juliet-java} & 83 & 540 & rendering injection & HTML / DOM (XSS) \\ +\texttt{owasp-benchmark} & 89 & 504 & query injection & SQL \\ +\texttt{owasp-benchmark} & 79 & 455 & rendering injection & HTML / DOM (XSS) \\ +\texttt{owasp-benchmark} & 78 & 251 & command injection & Shell command \\ +\texttt{owasp-benchmark} & 90 & 59 & query injection & LDAP \\ +\texttt{owasp-benchmark} & 643 & 35 & query injection & XPath / XQuery \\ +\bottomrule +\end{tabular} diff --git a/injection-research/doc/generated/tbl-mech.tex b/injection-research/doc/generated/tbl-mech.tex new file mode 100644 index 0000000..8f0a40d --- /dev/null +++ b/injection-research/doc/generated/tbl-mech.tex @@ -0,0 +1,24 @@ +%% GENERATED by pipeline/latex.py -- do not edit. +%% Regenerate with: python3 pipeline/latex.py +\begin{tabular}{lrrr} +\toprule +Syntax & Inert embed & Rejected & Outside \\ +\midrule +HTML / DOM (XSS) & 4{,}542 & 36 & 284 \\ +SQL & 4{,}217 & 477 & 0 \\ +LDAP & 0 & 1 & 0 \\ +NoSQL & 1 & 0 & 0 \\ +XPath / XQuery & 1 & 0 & 0 \\ +\midrule +Shell command & --- & --- & 1{,}103 \\ +Code / eval & --- & --- & 445 \\ +CRLF / header & --- & --- & 55 \\ +Formula (CSV) & --- & --- & 37 \\ +Template & --- & --- & 29 \\ +Argument & --- & --- & 15 \\ +Expression language & --- & --- & 12 \\ +XML & --- & --- & 10 \\ +\midrule +Total & 8{,}761 & 514 & 1{,}990 \\ +\bottomrule +\end{tabular} diff --git a/injection-research/doc/generated/tbl-payload-corpus.tex b/injection-research/doc/generated/tbl-payload-corpus.tex new file mode 100644 index 0000000..48fa26f --- /dev/null +++ b/injection-research/doc/generated/tbl-payload-corpus.tex @@ -0,0 +1,16 @@ +%% GENERATED by pipeline/latex.py -- do not edit. +%% Regenerate with: python3 pipeline/latex.py +\begin{tabular}{lrrrr} +\toprule +Syntax & Payloads & Inert & Rejected & Outside \\ +\midrule +HTML / DOM (XSS) & 11{,}534 & 10{,}367 & 148 & 1{,}019 \\ +Shell command & 10{,}312 & 0 & 0 & 10{,}312 \\ +SQL & 3{,}002 & 2{,}456 & 546 & 0 \\ +Template & 252 & 0 & 0 & 252 \\ +XML & 135 & 0 & 0 & 135 \\ +LDAP & 81 & 68 & 13 & 0 \\ +NoSQL & 43 & 37 & 6 & 0 \\ +XPath / XQuery & 10 & 10 & 0 & 0 \\ +\bottomrule +\end{tabular} diff --git a/injection-research/doc/generated/tbl-poc-sources.tex b/injection-research/doc/generated/tbl-poc-sources.tex new file mode 100644 index 0000000..8c5bc4f --- /dev/null +++ b/injection-research/doc/generated/tbl-poc-sources.tex @@ -0,0 +1,14 @@ +%% GENERATED by pipeline/latex.py -- do not edit. +%% Regenerate with: python3 pipeline/latex.py +\begin{tabular}{lrrr} +\toprule +Source & PoC rows & CVEs & Injection CVEs \\ +\midrule +\texttt{trickest} & 422{,}605 & 164{,}200 & 49{,}381 \\ +\texttt{exploitdb} & 33{,}425 & 27{,}934 & 11{,}297 \\ +\texttt{github} & 17{,}904 & 8{,}975 & 2{,}533 \\ +\texttt{nuclei} & 4{,}261 & 4{,}256 & 1{,}980 \\ +\texttt{metasploit} & 3{,}440 & 3{,}106 & 726 \\ +\texttt{vulhub} & 245 & 245 & 91 \\ +\bottomrule +\end{tabular} diff --git a/injection-research/doc/generated/tbl-strata.tex b/injection-research/doc/generated/tbl-strata.tex new file mode 100644 index 0000000..ef175ad --- /dev/null +++ b/injection-research/doc/generated/tbl-strata.tex @@ -0,0 +1,16 @@ +%% GENERATED by pipeline/latex.py -- do not edit. +%% Regenerate with: python3 pipeline/latex.py +\begin{tabular}{lrrr} +\toprule +Syntax & CVEs & Payload-backed & Contained \\ +\midrule +HTML / DOM (XSS) & 50{,}884 & 4{,}862 & 94.2\% \\ +SQL & 22{,}225 & 4{,}694 & 100.0\% \\ +Shell command & 9{,}672 & 1{,}103 & 0.0\% \\ +Code / eval & 6{,}666 & 445 & 0.0\% \\ +CRLF / header & 656 & 55 & 0.0\% \\ +Argument & 430 & 15 & 0.0\% \\ +Formula (CSV) & 321 & 37 & 0.0\% \\ +Expression language & 273 & 12 & 0.0\% \\ +\bottomrule +\end{tabular} diff --git a/injection-research/doc/generated/tbl-syntax.tex b/injection-research/doc/generated/tbl-syntax.tex new file mode 100644 index 0000000..4ee1ace --- /dev/null +++ b/injection-research/doc/generated/tbl-syntax.tex @@ -0,0 +1,14 @@ +%% GENERATED by pipeline/latex.py -- do not edit. +%% Regenerate with: python3 pipeline/latex.py +\begin{tabular}{lrr} +\toprule +Injection syntax & CVEs & with PoC \\ +\midrule +HTML / DOM (XSS) & 50{,}884 & 27{,}265 \\ +SQL & 22{,}225 & 14{,}961 \\ +Shell command & 9{,}672 & 5{,}298 \\ +Code / eval & 6{,}666 & 3{,}962 \\ +CRLF / header & 656 & 331 \\ +Argument & 430 & 216 \\ +\bottomrule +\end{tabular} diff --git a/injection-research/doc/intro.tex b/injection-research/doc/intro.tex index 36d80c5..b8ce9bf 100644 --- a/injection-research/doc/intro.tex +++ b/injection-research/doc/intro.tex @@ -26,27 +26,30 @@ \section{Introduction} assumptions, and how much of the real injection landscape it could reach. We make four contributions: \begin{itemize} -\item A reproducible, snapshot-pinned corpus (\cref{sec:data}) that unifies - the official CVE record with normalized enrichment and four - proof-of-concept databases, so that classification, exploitation - signals, and real attack payloads can be joined on a common key. -\item A two-axis, multi-source classifier (\cref{sec:classify}) that labels - each injection CVE by weakness family and by the embedded - \emph{syntax} it targets, and a syntactic-skeleton grouping that - clusters attacks by structural shape (\cref{sec:results}). +\item A security reading of the matchertext discipline + (\cref{sec:relevance}), which develops what the rule is, why a + discipline designed for verbatim embedding bears on injection at all, + and what would have to hold for it to help. \item A precise threat model and security property (\cref{sec:threat}) that - states the guarantee as an \emph{inertness} invariant, distinguishes it - from the weaker closure theorem it is easily conflated with, and reduces - it to three named premises; the load-bearing boundary premise we - discharge with a machine-checked Lean proof (\cref{sec:appendix:lean}). -\item An empirical measurement of matchertext's structural reach (\cref{sec:prevent}): - each skeleton is rewritten to its matchertext-equivalent and checked - for breakout, yielding both a measured figure over payload-backed CVEs - and a projection over the full injection corpus. + states the guarantee as an \emph{inertness} invariant, distinguishes it + from the weaker closure theorem it is easily conflated with, and reduces + it to three named premises; the load-bearing boundary premise we + discharge with a machine-checked Lean proof (\cref{sec:appendix:lean}). +\item A structural argument (\cref{sec:resist}) that matcher-delimiting + untrusted input resists injection across SQL, HTML, LDAP, and PDF, with + the options for fitting the discipline into existing languages and how + it compares with the defenses already deployed. +\item An empirical measurement of its structural reach + (\cref{sec:prevent}), over a reproducible, snapshot-pinned corpus + (\cref{sec:corpus}) that unifies the official CVE record with normalized + enrichment and four proof-of-concept databases, classified by weakness + family and by the embedded \emph{syntax} each attack targets + (\cref{sec:results}). \end{itemize} -A vulnerability is tallied as structurally containable only where the mechanism -holds structurally, and the payload-backed and projected figures are reported -separately, each over its own subset. -Both figures assume a matchertext-aware host and characterize attack structure, -not a deployed defense. +Together these answer whether one uniform check could replace the collection of +per-host defenses injection is fought with today, and how much of the recorded +landscape such a check would reach. +Both figures below assume a matchertext-aware host and characterize attack +structure rather than a deployed defense, and the payload-backed and projected +figures are reported separately, each over its own subset. diff --git a/injection-research/doc/main.tex b/injection-research/doc/main.tex index 332930a..b360fbb 100644 --- a/injection-research/doc/main.tex +++ b/injection-research/doc/main.tex @@ -8,6 +8,21 @@ linkcolor=blue,citecolor=blue,urlcolor=black]{hyperref} \usepackage{cleveref} \usepackage{graphicx} +\usepackage{tikz} +\usepackage{pmboxdraw} % box-drawing glyphs for the ASCII figures under pdflatex +\usepackage{amssymb} +% Glyphs the ASCII figures use that pmboxdraw does not cover. Each is set in a +% box exactly one character cell wide, as pmboxdraw itself does, so that they sit +% on the monospace grid and do not shift the rest of their line. +\newlength{\pmbdcell} +\newcommand{\pmbdglyph}[1]{% + \settowidth{\pmbdcell}{0}% + \makebox[\pmbdcell][c]{\ensuremath{#1}}% +} +\DeclareUnicodeCharacter{25BC}{\pmbdglyph{\blacktriangledown}} +\DeclareUnicodeCharacter{25BA}{\pmbdglyph{\blacktriangleright}} +\DeclareUnicodeCharacter{2208}{\pmbdglyph{\in}} +\DeclareUnicodeCharacter{00B7}{\pmbdglyph{\cdot}} \usepackage{booktabs} \usepackage{xurl} % allow long URLs in the bibliography to break anywhere \usepackage[T1]{fontenc} @@ -60,6 +75,10 @@ \newcommand{\ie}{{\em i.e.},\xspace} \newcommand{\eg}{{\em e.g.},\xspace} +% Every corpus figure quoted in the text, generated from data/cve.db by +% pipeline/latex.py. Regenerate with: python3 pipeline/latex.py +\input{generated/numbers} + %%%%%%%%%%%%%%%%%%%%%% \begin{document} @@ -79,17 +98,24 @@ \input{intro} \input{motivation} -\input{data} -\input{classify} -\input{results} + +\input{relevance} \input{threat} \input{resist} -\input{prevent} + +\input{corpus} +\input{results} +\input{containment} + +\input{related} + \input{concl} \appendix \onecolumn -\input{appendix} +\input{embeded_boundary} +\newpage +\input{to_matchertext} \twocolumn \bibliographystyle{plain} diff --git a/injection-research/doc/motivation.tex b/injection-research/doc/motivation.tex index c1de8f6..81f269b 100644 --- a/injection-research/doc/motivation.tex +++ b/injection-research/doc/motivation.tex @@ -5,7 +5,7 @@ \section{Background and motivation} vulnerability. This section surveys the breadth of the problem beyond its most familiar members, its measured prevalence and cost, and why the very machinery built to contain it has itself become a recurring source of vulnerabilities: -the motivation for the structural approach this thesis evaluates. +the motivation for the structural approach this paper evaluates. \subsection{A wider family of embedding hazards} \label{sec:bg:hazards} @@ -64,7 +64,7 @@ \subsection{A wider family of embedding hazards} That is exactly the failure a matcher-balance discipline is built to resist, and because it recurs across the injection and markup attacks above rather than in any single language pair, -one structural discipline can address the breakout-based members at once---as +one structural discipline can address the breakout-based members at once, as distinct from the execution and algorithmic members (template evaluation, ReDoS, entity expansion) it cannot. @@ -181,3 +181,80 @@ \subsection{The sanitizer as attack surface} check, and what remains per host is a bounded change to a parser the host already owns, not a new artifact shadowing one it does not. + +\subsection{The narrow waist} +\label{sec:bg:waist} + +\begin{figure*}[t] +\centering +\begin{tikzpicture}[ + lang/.style={font=\small}, + link/.style={draw=black!45, line width=0.4pt}, + waist/.style={draw, fill=black!8, minimum width=5.4cm, + minimum height=0.9cm, font=\small}, + note/.style={font=\small}, +] +\begin{scope}[xshift=-4.3cm] + \node[note] at (0,2.6) {\textbf{Today}}; + \node[lang] (t1) at (-1.8,1.7) {Java}; + \node[lang] (t2) at (-0.6,1.7) {PHP}; + \node[lang] (t3) at ( 0.6,1.7) {$\cdots$}; + \node[lang] (t4) at ( 1.8,1.7) {Go}; + \node[lang] (s1) at (-1.8,-1.7) {SQL}; + \node[lang] (s2) at (-0.6,-1.7) {HTML}; + \node[lang] (s3) at ( 0.6,-1.7) {$\cdots$}; + \node[lang] (s4) at ( 1.8,-1.7) {shell}; + \foreach \a in {t1,t2,t3,t4} + \foreach \b in {s1,s2,s3,s4} + \draw[link] (\a) -- (\b); + \node[note] at (0,-2.6) {$N \times M$ escapers, one per pair}; +\end{scope} +\begin{scope}[xshift=4.3cm] + \node[note] at (0,2.6) {\textbf{With matchertext}}; + \node[lang] (u1) at (-2.4,1.7) {C}; + \node[lang] (u2) at (-1.2,1.7) {Java}; + \node[lang] (u3) at ( 0.0,1.7) {PHP}; + \node[lang] (u4) at ( 1.2,1.7) {$\cdots$}; + \node[lang] (u5) at ( 2.4,1.7) {Go}; + \node[waist] (w) at (0,0) {matchers must match}; + \node[lang] (v1) at (-2.4,-1.7) {SQL}; + \node[lang] (v2) at (-1.2,-1.7) {HTML}; + \node[lang] (v3) at ( 0.0,-1.7) {LDAP}; + \node[lang] (v4) at ( 1.2,-1.7) {$\cdots$}; + \node[lang] (v5) at ( 2.4,-1.7) {URI}; + \foreach \a in {u1,u2,u3,u4,u5} \draw[link] (\a) -- (w.north); + \foreach \b in {v1,v2,v3,v4,v5} \draw[link] (w.south) -- (\b); + \node[note] at (0,-2.6) {$N + M$ implementations, one rule each}; +\end{scope} +\end{tikzpicture} +\caption{The narrow waist. Each escaper today is written for one composing +language and one host, and must model that host's syntax and track it as it +changes. A rule both sides implement once decouples them, since the rule mentions +neither: any language emitting valid matchertext is compatible with any host +reading to matcher balance. Not everything passes through the waist, however: +contexts delimited by non-matchers, such as shell separators and CR/LF header +breaks, and execution sinks, which run their contents by design, lie outside it, and +\cref{sec:prevent} measures how much of the recorded landscape that leaves.} +\label{fig:bg:waist} +\end{figure*} + +The defenses of \cref{sec:bg:sanitizer} share a shape. +Each is written for one composing language and one host, and works by knowing the +host well enough to transform values for it: a Java-to-SQL escaper knows SQL, and +an HTML sanitizer knows the browser's parser closely enough to predict it. +Neither transfers to the other's problem, so the number of defenses to write, +audit, and re-synchronize grows with the product of the two populations. + +\Cref{fig:bg:waist} shows the alternative. +A rule that both sides implement once decouples them, because the rule mentions +neither: a language that emits valid matchertext is compatible with every host +that reads to matcher balance, and such a host accepts values from every such +language, without either knowing what the other is. +The count falls from $N \times M$ relationships to $N + M$ implementations, which +is the shape the Internet protocol stack takes for the same reason, a waist thin +enough that what sits above and below it can vary independently. + +Whether that shape is worth adopting is a security question rather than an +aesthetic one, and it turns on what the shared rule actually guarantees when the +value in the hole is chosen by an attacker. +\Cref{sec:relevance} takes it up. diff --git a/injection-research/doc/prevent.tex b/injection-research/doc/prevent.tex deleted file mode 100644 index 6a51655..0000000 --- a/injection-research/doc/prevent.tex +++ /dev/null @@ -1,100 +0,0 @@ -\section{Measuring matchertext containment} -\label{sec:prevent} - -Matchertext contains an injection under mainly two conditions: the untrusted value lands in a slot -a matchertext-aware host delimits with a matcher pair, and the value is itself -valid matchertext, checked by the passive \textsc{Verify} scan rather than by -escaping. -An attack then fails one of two ways, by \emph{inert embedding} or by -\emph{rejection}, and which route a real attack takes is a property of the -payload, and so measurable against the corpus. - -\paragraph{Method.} -For each of the 5{,}025 payload-backed CVEs we reuse its syntactic skeleton and decide two things: -whether the target syntax is one a matchertext host can delimit with a matcher -pair, and, if so, whether the skeleton passes \textsc{Verify}. -A passing skeleton is contained by \emph{inert embedding}; a failing one is -stopped by \emph{rejection}. -This test characterizes the structure of each recorded payload under a -matchertext-aware host; it does not exercise a deployed host parser, which we -leave to future implementation work. - -\begin{table}[t] -\centering -\small -\begin{tabular}{lrrr} -\toprule -Syntax & Inert embed & Rejected & Outside \\ -\midrule -HTML / DOM (XSS) & 2{,}772 & 13 & 219 \\ -SQL & 1{,}000 & 322 & 0 \\ -LDAP & 0 & 3 & 0 \\ -NoSQL & 1 & 0 & 0 \\ -\midrule -Shell command & --- & --- & 333 \\ -Code / eval & --- & --- & 301 \\ -CRLF / header & --- & --- & 29 \\ -Formula (CSV) & --- & --- & 17 \\ -Template & --- & --- & 5 \\ -XML & --- & --- & 4 \\ -Argument & --- & --- & 3 \\ -Expression language & --- & --- & 3 \\ -\midrule -Total & 3{,}773 & 338 & 914 \\ -\bottomrule -\end{tabular} -\caption{Containment outcome by syntax over all \(5{,}025\) payload-backed CVEs. -Contexts a matchertext host can delimit (upper block) are contained by inert -embedding or by rejection; the \emph{Outside} column counts CVEs failing a -condition of \cref{sec:threat}, either an execution sink (the HTML/DOM entries -are \texttt{javascript:} URLs) or a context whose delimiters are not matchers.} -\label{tab:mech} -\end{table} - -\paragraph{Results.} -Of the 5{,}025 payload-backed injection CVEs, the recorded payloads of -\textbf{4{,}111} (\textbf{82\%}) are contained by a matcher-delimited slot that a -matchertext-aware host reads to matcher balance, assuming no intervening -decoding; the split turns on the host's native delimiter. -The per-syntax mechanisms of \cref{sec:resist} appear directly in the corpus. -LDAP is the pure rejection case: every real LDAP payload fails \textsc{Verify} -(0 inert, 3 rejected), its parenthesis breakout carrying an unmatched \verb|)|. -SQL and XSS, breaking out on nonmatchers, are overwhelmingly valid matchertext -and embed inertly; the 322 SQL rejections additionally carry an unbalanced -function or subquery parenthesis. -The ratio between the two mechanisms is descriptive, not predictive. -These payloads were written against quote and tag-delimited sinks; an attacker -aware of a matcher-delimited slot would balance the matchers, shifting cases -from rejection to inert embedding. -Containment is unaffected, since both routes hold the value, but the split -itself is a property of the recorded corpus rather than of an adaptive attacker. - -\paragraph{Where matchertext cannot help.} -The remaining 914 payload-backed CVEs are outside both conditions, and divide -along the two conditions they fail. -545 target execution/semantic sinks (server-side templates, expression -languages, code evaluation, spreadsheet formulas, and \verb|javascript:| URLs) -where the host runs the contained value by design, so delimiting cannot stop -it: the template payload \verb|{{7*7}}| is already valid matchertext yet is -still executed. -The other 369 target contexts delimited by non-matchers with no matcher hosting: -shell command separators (\verb|;|~\verb-|-~\verb|&|), CR/LF header breaks, and -the angle brackets of XML/XXE, none of which are matcher characters. - -\paragraph{Projection.} -A payload is required to classify the mechanism, but the \emph{context} -condition can be read from the syntax label alone. -Projecting it onto the full corpus, at most \textbf{73{,}246} of the -\textbf{91{,}760} injection CVEs (\textbf{80\%}) target a matcher-delimitable -syntax. -This is an upper bound, since a fraction of HTML/DOM cases are the -\verb|javascript:| semantic sinks above, and the payload-backed subset puts a -number on that fraction: 219 of the 3{,}004 HTML/DOM CVEs carrying a payload are -such sinks, a rate of \textbf{7.3\%}. -Applying it to the 50{,}884 HTML/DOM CVEs removes an estimated 3{,}710, for a -central estimate of \textbf{69{,}536} (\textbf{76\%}) against the 80\% ceiling. -The estimate assumes payload-backed CVEs carry sinks at the same rate as the -rest, which their skew toward exploitable web bugs may not warrant. -The reach of the discipline is thus bounded from below at the fragment level and -from above at the syntax level, and the gap between 5{,}025 and 91{,}760 is -payload availability, not a containment failure. diff --git a/injection-research/doc/refs.bib b/injection-research/doc/refs.bib index a1adb91..498a048 100644 --- a/injection-research/doc/refs.bib +++ b/injection-research/doc/refs.bib @@ -294,3 +294,317 @@ @misc{wijayarathna18esapi howpublished = {arXiv:1810.01017, \url{https://arxiv.org/abs/1810.01017}}, year = {2018}, } + +% ---- Related work: language-based construction ---- + +@inproceedings{mcclure05sqldom, + author = {Russell A. McClure and Ingolf H. Kr\"uger}, + title = {{SQL} {DOM}: Compile Time Checking of Dynamic {SQL} Statements}, + booktitle = {International Conference on Software Engineering (ICSE)}, + year = {2005}, +} + +@inproceedings{cook05safequery, + author = {William R. Cook and Siddhartha Rai}, + title = {Safe Query Objects: Statically Typed Objects as Remotely + Executable Queries}, + booktitle = {International Conference on Software Engineering (ICSE)}, + year = {2005}, +} + +@inproceedings{cheney13liq, + author = {James Cheney and Sam Lindley and Philip Wadler}, + title = {A Practical Theory of Language-Integrated Query}, + booktitle = {International Conference on Functional Programming (ICFP)}, + year = {2013}, +} + +@inproceedings{chlipala15urweb, + author = {Adam Chlipala}, + title = {Ur/{Web}: A Simple Model for Programming the Web}, + booktitle = {Principles of Programming Languages (POPL)}, + year = {2015}, +} + +@article{kern14securing, + author = {Christoph Kern}, + title = {Securing the Tangled Web}, + journal = {Communications of the ACM}, + volume = {57}, + number = {9}, + year = {2014}, +} + +@misc{trustedtypes, + author = {{W3C}}, + title = {Trusted Types}, + howpublished = {W3C Working Draft, \url{https://www.w3.org/TR/trusted-types/}}, + year = {2024}, +} + +% ---- Related work: syntax embedding and safe quotation ---- + +@article{bravenboer10stringborg, + author = {Martin Bravenboer and Eelco Dolstra and Eelco Visser}, + title = {Preventing Injection Attacks with Syntax Embeddings}, + journal = {Science of Computer Programming}, + volume = {75}, + number = {7}, + year = {2010}, + note = {Earlier version in GPCE 2007}, +} + +@inproceedings{kohlbecker86hygienic, + author = {Eugene Kohlbecker and Daniel P. Friedman and Matthias Felleisen + and Bruce Duba}, + title = {Hygienic Macro Expansion}, + booktitle = {LISP and Functional Programming (LFP)}, + year = {1986}, +} + +@article{dybvig92syntactic, + author = {R. Kent Dybvig and Robert Hieb and Carl Bruggeman}, + title = {Syntactic Abstraction in {Scheme}}, + journal = {LISP and Symbolic Computation}, + volume = {5}, + number = {4}, + year = {1993}, +} + +@article{taha00metaml, + author = {Walid Taha and Tim Sheard}, + title = {{MetaML} and Multi-Stage Programming with Explicit Annotations}, + journal = {Theoretical Computer Science}, + volume = {248}, + number = {1--2}, + year = {2000}, +} + +@inproceedings{sheard02template, + author = {Tim Sheard and Simon Peyton Jones}, + title = {Template Meta-programming for {Haskell}}, + booktitle = {Haskell Workshop}, + year = {2002}, +} + +@inproceedings{mainland07quoted, + author = {Geoffrey Mainland}, + title = {Why It's Nice to Be Quoted: Quasiquoting for {Haskell}}, + booktitle = {Haskell Workshop}, + year = {2007}, +} + +@article{carette09tagless, + author = {Jacques Carette and Oleg Kiselyov and Chung-chieh Shan}, + title = {Finally Tagless, Partially Evaluated: Tagless Staged Interpreters + for Simpler Typed Languages}, + journal = {Journal of Functional Programming}, + volume = {19}, + number = {5}, + year = {2009}, +} + +@inproceedings{renggli10embedding, + author = {Lukas Renggli and Tudor G\^irba and Oscar Nierstrasz}, + title = {Embedding Languages Without Breaking Tools}, + booktitle = {European Conference on Object-Oriented Programming (ECOOP)}, + year = {2010}, +} + +% ---- Related work: static analysis and detection ---- + +@inproceedings{huang04webssari, + author = {Yao-Wen Huang and Fang Yu and Christian Hang and Chung-Hung Tsai + and Der-Tsai Lee and Sy-Yen Kuo}, + title = {Securing Web Application Code by Static Analysis and + Runtime Protection}, + booktitle = {International World Wide Web Conference (WWW)}, + year = {2004}, +} + +@inproceedings{livshits05finding, + author = {V. Benjamin Livshits and Monica S. Lam}, + title = {Finding Security Vulnerabilities in {Java} Applications with + Static Analysis}, + booktitle = {USENIX Security Symposium}, + year = {2005}, +} + +@inproceedings{jovanovic06pixy, + author = {Nenad Jovanovic and Christopher Kruegel and Engin Kirda}, + title = {{Pixy}: A Static Analysis Tool for Detecting Web Application + Vulnerabilities}, + booktitle = {IEEE Symposium on Security and Privacy (S\&P)}, + year = {2006}, +} + +@inproceedings{xie06static, + author = {Yichen Xie and Alex Aiken}, + title = {Static Detection of Security Vulnerabilities in Scripting + Languages}, + booktitle = {USENIX Security Symposium}, + year = {2006}, +} + +@inproceedings{wassermann07sound, + author = {Gary Wassermann and Zhendong Su}, + title = {Sound and Precise Analysis of Web Applications for Injection + Vulnerabilities}, + booktitle = {Programming Language Design and Implementation (PLDI)}, + year = {2007}, +} + +@inproceedings{tripp09taj, + author = {Omer Tripp and Marco Pistoia and Stephen J. Fink and Manu Sridharan + and Omri Weisman}, + title = {{TAJ}: Effective Taint Analysis of Web Applications}, + booktitle = {Programming Language Design and Implementation (PLDI)}, + year = {2009}, +} + +@inproceedings{tripp13andromeda, + author = {Omer Tripp and Marco Pistoia and Patrick Cousot and Radhia Cousot + and Salvatore Guarnieri}, + title = {{Andromeda}: Accurate and Scalable Security Analysis of Web + Applications}, + booktitle = {Fundamental Approaches to Software Engineering (FASE)}, + year = {2013}, +} + +@inproceedings{arzt14flowdroid, + author = {Steven Arzt and Siegfried Rasthofer and Christian Fritz and + Eric Bodden and Alexandre Bartel and Jacques Klein and + Yves Le Traon and Damien Octeau and Patrick McDaniel}, + title = {{FlowDroid}: Precise Context, Flow, Field, Object-Sensitive and + Lifecycle-Aware Taint Analysis for {Android} Apps}, + booktitle = {Programming Language Design and Implementation (PLDI)}, + year = {2014}, +} + +@inproceedings{dahse14simulation, + author = {Johannes Dahse and Thorsten Holz}, + title = {Simulation of Built-in {PHP} Features for Precise Static Code + Analysis}, + booktitle = {Network and Distributed System Security Symposium (NDSS)}, + year = {2014}, +} + +% ---- Related work: cross-cutting structural defenses ---- + +@inproceedings{pietraszek05csse, + author = {Tadeusz Pietraszek and Chris Vanden Berghe}, + title = {Defending Against Injection Attacks Through Context-Sensitive + String Evaluation}, + booktitle = {Recent Advances in Intrusion Detection (RAID)}, + year = {2005}, +} + +@inproceedings{nadji09dsi, + author = {Yacin Nadji and Prateek Saxena and Dawn Song}, + title = {Document Structure Integrity: A Robust Basis for Cross-Site + Scripting Defense}, + booktitle = {Network and Distributed System Security Symposium (NDSS)}, + year = {2009}, +} + +@inproceedings{terlouw09blueprint, + author = {Mike Ter Louw and V. N. Venkatakrishnan}, + title = {{BLUEPRINT}: Robust Prevention of Cross-Site Scripting Attacks + for Existing Browsers}, + booktitle = {IEEE Symposium on Security and Privacy (S\&P)}, + year = {2009}, +} + +@article{vangundy12noncespaces, + author = {Matthew Van Gundy and Hao Chen}, + title = {{Noncespaces}: Using Randomization to Defeat Cross-Site Scripting + Attacks}, + journal = {Computers \& Security}, + volume = {31}, + number = {4}, + year = {2012}, +} + +@misc{w3c_csp, + author = {{W3C}}, + title = {Content Security Policy Level 3}, + howpublished = {W3C Working Draft, \url{https://www.w3.org/TR/CSP3/}}, + year = {2024}, +} + +@inproceedings{boyd04sqlrand, + author = {Stephen W. Boyd and Angelos D. Keromytis}, + title = {{SQLrand}: Preventing {SQL} Injection Attacks}, + booktitle = {Applied Cryptography and Network Security (ACNS)}, + year = {2004}, +} + +@inproceedings{barrantes03isr, + author = {Elena Gabriela Barrantes and David H. Ackley and Trek S. Palmer + and Darko Stefanovic and Dino Dai Zovi}, + title = {Randomized Instruction Set Emulation to Disrupt Binary Code + Injection Attacks}, + booktitle = {Computer and Communications Security (CCS)}, + year = {2003}, +} + +@misc{owasp_xss, + author = {{OWASP}}, + title = {Cross Site Scripting Prevention Cheat Sheet}, + howpublished = {\url{https://cheatsheetseries.owasp.org/cheatsheets/Cross_Site_Scripting_Prevention_Cheat_Sheet.html}}, +} + +% ---- Related work: definitions and measurement ---- + +@inproceedings{su06essence, + author = {Zhendong Su and Gary Wassermann}, + title = {The Essence of Command Injection Attacks in Web Applications}, + booktitle = {Principles of Programming Languages (POPL)}, + year = {2006}, +} + +@inproceedings{ray12defining, + author = {Donald Ray and Jay Ligatti}, + title = {Defining Code-Injection Attacks}, + booktitle = {Principles of Programming Languages (POPL)}, + year = {2012}, +} + +@inproceedings{halfond06classification, + author = {William G. J. Halfond and Jeremy Viegas and Alessandro Orso}, + title = {A Classification of {SQL}-Injection Attacks and Countermeasures}, + booktitle = {International Symposium on Secure Software Engineering (ISSSE)}, + year = {2006}, +} + +@article{hannousse22xss, + author = {Abdelhakim Hannousse and Salima Yahiouche}, + title = {Twenty-Two Years Since Revealing Cross-Site Scripting Attacks: + A Systematic Mapping and a Comprehensive Survey}, + journal = {Computer Science Review}, + volume = {43}, + year = {2022}, +} + +@inproceedings{lekies13dom, + author = {Sebastian Lekies and Ben Stock and Martin Johns}, + title = {25 Million Flows Later: Large-Scale Detection of {DOM}-based {XSS}}, + booktitle = {Computer and Communications Security (CCS)}, + year = {2013}, +} + +@misc{mandiant23tte, + author = {{Mandiant}}, + title = {Analysis of Time-to-Exploit Trends: 2021--2022}, + howpublished = {Google Cloud Threat Intelligence blog}, + year = {2023}, + note = {\url{https://cloud.google.com/blog/topics/threat-intelligence/time-to-exploit-trends-2021-2022/}}, +} + +@misc{vulncheck26exploit, + author = {{VulnCheck}}, + title = {2026 Exploit Intelligence Report}, + howpublished = {VulnCheck}, + year = {2026}, + note = {\url{https://www.vulncheck.com/blog/2026-vulncheck-exploit-intelligence-report}}, +} diff --git a/injection-research/doc/related.tex b/injection-research/doc/related.tex new file mode 100644 index 0000000..21a2489 --- /dev/null +++ b/injection-research/doc/related.tex @@ -0,0 +1,100 @@ +\section{Related work} +\label{sec:related} + +Matchertext treats injection as a structural problem: keep untrusted input from +altering the syntax around it, rather than filter what it may contain. +\Cref{sec:resist:baselines} sets it head-to-head against the defenses deployed +today; here we place it in the broader literature, grouped by how each line +attacks the embedding boundary. + +\subsection{Language-based construction} +The strongest host-specific defenses fix the embedded language's structure +before any value is bound. +Parameterized queries do this for SQL~\cite{owasp_parameterization}, and a +programming-languages tradition hardens the same idea into types: SQL~DOM~\cite{mcclure05sqldom} +and Safe Query Objects~\cite{cook05safequery} replace string building with typed +query values; language-integrated query gives the host-to-SQL translation a +formal, meaning-preserving account~\cite{cheney13liq}; and Ur/Web~\cite{chlipala15urweb} +collapses web multi-language composition into one statically typed language. +For markup, contextual auto-escaping selects the escaper from each hole's +inferred syntactic context~\cite{samuel11csas}, and typed-value schemes such as +SafeHtml and Trusted Types gate dangerous sinks so they accept only +non-spoofable objects rather than arbitrary strings~\cite{kern14securing,trustedtypes}. +Each buys a strong guarantee by knowing the language it protects: a fixed +language, a dedicated sink API, or an owning compiler. +Matchertext keeps values as plain text and fixes only the \emph{boundary}, so one +rule serves hosts it was never specialized to (\cref{sec:resist:baselines}). + +\subsection{Syntax embedding and safe quotation} +The closest work makes embedding safe by construction in the language itself. +StringBorg~\cite{bravenboer10stringborg} embeds the embedded language's grammar +into the composing one, adds quotation and antiquotation forms, and assimilates +the result into API calls in that embedded language, rendering programs +impervious to injection by construction. +It is the nearest neighbor to matchertext, and the sharpest contrast: it needs an +explicit grammar and a combined-syntax toolchain per language pair, where +matchertext asks only that unrelated languages share one lexical invariant. +The metaprogramming machinery this draws on has the same shape and the same +assumption of a known embedded language: hygienic macros embed code in code without +capture~\cite{kohlbecker86hygienic,dybvig92syntactic}, staged and +quotation-based programming generate well-typed embedded fragments~\cite{taha00metaml,sheard02template,mainland07quoted}, +tagless-final embeddings make ill-typed embedded terms unrepresentable~\cite{carette09tagless}, +and language workbenches sidestep parser composition through projectional +editing~\cite{renggli10embedding}. +All own the embedded language's parser or type system; matchertext targets the case where the +surrounding ecosystem shares no grammar or AST at all. + +\subsection{Static analysis and detection} +A large body of work finds injection flaws in existing code rather than +preventing them. +Information-flow and taint analyses trace untrusted data to sensitive sinks: +WebSSARI~\cite{huang04webssari}, Livshits and Lam~\cite{livshits05finding}, +Pixy~\cite{jovanovic06pixy}, Xie and Aiken~\cite{xie06static}, and the +industrial-scale successors TAJ~\cite{tripp09taj} and Andromeda~\cite{tripp13andromeda}, +with FlowDroid~\cite{arzt14flowdroid} the mobile analogue. +String analysis reasons about the generated query itself~\cite{wassermann07sound}, and +modern SAST productizes both for continuous integration~\cite{dahse14simulation}. +These detect variants of a bad construction after the fact and trade soundness +against precision and analyst noise. +Matchertext instead makes the boundary-breaking construction unrepresentable, and +is complementary to analysis for the errors (wrong sink, logic faults, misuse +outside the discipline) that a boundary rule does not touch. + +\subsection{Cross-cutting structural defenses} +Closer in ambition are defenses that enforce a global invariant separating +trusted structure from untrusted data. +CSSE tags input and evaluates it in context across SQL, XSS, and shell +injection~\cite{pietraszek05csse}; Document Structure Integrity~\cite{nadji09dsi}, +BLUEPRINT~\cite{terlouw09blueprint}, and Noncespaces~\cite{vangundy12noncespaces} +protect HTML structure through browser cooperation and randomized or +nonce-marked namespaces; Content Security Policy mitigates content injection at +execution time~\cite{w3c_csp}; and SQLrand~\cite{boyd04sqlrand} and +instruction-set randomization~\cite{barrantes03isr} randomize the accepted +language so injected code cannot speak it. +All mark trusted structure \emph{out of band}, with propagated metadata, +browser state, or a secret, whereas matchertext makes the boundary +self-delimiting \emph{in band} and public, with no tag to carry and no secret to +keep. +The web's lack of a universal escaper, precisely because parse context is +per-language and non-composable~\cite{owasp_xss}, is what forces these +per-context schemes; matchertext offers not one encoder for all contexts but one +rule for locating the hole before any context-specific encoder runs. + +\subsection{Definitions and measurement} +Formal framings of injection ground the inertness property of \cref{sec:threat}. +The language-theoretic security program frames the root cause as processing rich +input without first recognizing it~\cite{momot16langsec}; Su and Wassermann +define command injection as untrusted input altering the intended syntactic +structure of the generated command, with a grammar-based prevention +algorithm~\cite{su06essence}; and Ray and Ligatti define code injection by +whether input is used as a normal-form value rather than as code~\cite{ray12defining}, +the vocabulary matchertext's guarantee targets. +Taxonomies and measurements bound the problem: the SQL-injection countermeasure +taxonomy of Halfond et al.~\cite{halfond06classification}, systematic XSS +surveys~\cite{hannousse22xss}, and large-scale studies of DOM-based +XSS~\cite{lekies13dom} show defenses clustering around sink-specific filtering +and detection, with no cross-language boundary convention among the standard +categories. +The weakness labels reviewers and CVE pipelines use group these failures by +effect~\cite{cwe,owasp_top10_2021}; matchertext addresses the subset that shares +a single lexical boundary mechanism. diff --git a/injection-research/doc/relevance.tex b/injection-research/doc/relevance.tex new file mode 100644 index 0000000..12ebefd --- /dev/null +++ b/injection-research/doc/relevance.tex @@ -0,0 +1,114 @@ +\section{Matchertext and its security relevance} +\label{sec:relevance} + +The narrow waist of \cref{sec:bg:waist} is a claim about \emph{embedding}, +not about security. +Matchertext was designed so that a string in one language can be placed in another +verbatim, without escaping; its stated benefit is that the writer of embedded text +need reason about only one language's rules at a time~\cite{matchertext}. +That is a usability argument. +This section states the discipline precisely enough to reason about, explains why +a property invented for embedding bears on injection at all, and sets out the +questions the rest of the paper answers. + +\subsection{The discipline} +\label{sec:relevance:discipline} + +Matchertext is a purely syntactic rule over an alphabet $\Sigma$ and a set $\Pi$ +of open/close character pairs: the \emph{matchers} must match. +Writing $O$ and $C$ for the openers and closers of $\Pi$, and \emph{nonmatchers} +for every other character, the language $L$ of matchertext strings is defined +inductively: any string of nonmatchers is in $L$, and if $m_1,m_2,m_3\in L$ and +$(o,c)\in\Pi$ then $m_1\,o\,m_2\,c\,m_3\in L$. +The concrete configuration takes $\Sigma$ to be Unicode and $\Pi$ to be the three +ASCII pairs \verb|()|, \verb|[]|, and \verb|{}|; the angle brackets are excluded +because they are used unmatched as inequality operators far too often to +constrain~\cite{matchertext}. +Nothing else is fixed: the discipline assigns no meaning to any character and is +deliberately oblivious to the syntax of any particular language. + +Three results carry over from the original development, and the rest of this paper +uses only these. +First, \emph{closure}, also called always-embeddability: if $m\in L$ and +$(s_o,s_c)$ is a matched delimiter pair, then $s_o\,m\,s_c\in L$. +A valid matchertext string placed inside matched delimiters therefore yields a +valid matchertext string, at any nesting depth and with no escaping or expansion. +Second, membership in $L$ is decided by a single linear scan, the \textsc{Verify} +recognizer, which maintains a stack of unclosed openers and accepts exactly when +every closer matches its opener and the stack ends empty. +Third, a total encoder \textsc{ToMatchertext} maps \emph{any} string into $L$ by +escaping only its unmatched matchers, so free-form input that legitimately +contains an unmatched bracket need not be rejected. +Closure and the correctness of \textsc{Verify} are machine-checked; so is +\textsc{ToMatchertext}'s landing in $L$ on every input +(\cref{sec:appendix:tomatchertext}), leaving only its decoder round-trip informal. +For the rationale behind $\Pi$, the hosting syntaxes, and the empirical +compliance study, see~\cite{matchertext}. + +\subsection{From embedding to security} +\label{sec:relevance:security} + +Verbatim embedding and injection resistance are not the same property, and the +paper's claim turns on the difference between them. + +Injection, as \cref{sec:motivation} describes it, is a boundary failure: a value +meant to occupy one syntactic region escapes it, because a delimiter inside the +value collides with the delimiter that was supposed to contain it. +Conventional defenses attack the \emph{collision}, transforming the value so that +its dangerous characters can no longer be confused with the host's, which is why +they must know the host's syntax and why there is a different one for every +host and context. +Matchertext attacks the \emph{boundary} instead. +If a host delimits an untrusted value with a matcher pair and finds the end of +that value by counting matchers rather than by scanning for a terminator, then +escaping the region requires emitting an unmatched matcher, and by closure no +valid matchertext string contains one. +The characters that drive the classic breakouts, the quote in SQL and the angle +bracket in HTML, are nonmatchers: the discipline leaves them entirely +unconstrained, and they become ordinary data inside a matched region, which +closure keeps balanced whatever nonmatchers the value carries. + +Two consequences follow, and they are the reason this is a security question +rather than a syntactic one. +The check is \emph{host-independent}: \textsc{Verify} inspects only the six +matcher characters and knows nothing about SQL, HTML, or LDAP, so the same +recognizer serves every host, which is exactly what a sanitizer cannot do. +And the check is a \emph{verification} rather than a transformation, so its failure +mode is benign: a rejected value is data that does not embed, whereas a missed case +in an escaping routine \emph{is} the injection. +Together these are the narrow waist applied to security: one uniform obligation on +the value, in place of one bespoke transformation per host-context pair. + +\subsection{What must hold, and what we ask} +\label{sec:relevance:questions} + +Closure constrains \emph{strings}, whereas security is a claim about +\emph{parsers}, and the second does not follow from the first without assumptions +about the host. +\Cref{sec:threat} states those assumptions; three questions organize the rest of +the paper. + +\paragraph{Q1: what is actually guaranteed, and under what assumptions?} +Delimiting a value is not by itself a security property, and ``cannot break out'' +is not a specification. +\Cref{sec:threat} states the guarantee as an \emph{inertness} invariant on the +host's parse, separates it from the weaker closure property it is easily +conflated with, and reduces it to a small set of named premises about the host +parser, the interpreter, and the pipeline that reaches them. + +\paragraph{Q2: can a real language adopt this, and at what cost?} +The guarantee assumes a matchertext-aware host, and no mainstream language is one +today. +\Cref{sec:resist} develops the argument for the syntaxes where injection actually +occurs, then asks what adopting it costs: which hosting options deliver the +property, what each adds to the trusted computing base, and how the result +compares with the defenses already deployed for these hosts. + +\paragraph{Q3: how much of the real injection landscape could this reach?} +Even granting the property and its adoption, the discipline addresses only +injections that are structural breakouts from matcher-delimitable contexts, and +that is a proper subset of what the term covers. +\Cref{sec:corpus,sec:results,sec:prevent} measure the subset against a corpus of +recorded vulnerabilities, and \cref{sec:prevent} reports both what fraction of +attacks with a recoverable payload would be contained and what fraction of the +landscape is out of reach in principle. diff --git a/injection-research/doc/resist.tex b/injection-research/doc/resist.tex index 7beeccd..b7bc6f9 100644 --- a/injection-research/doc/resist.tex +++ b/injection-research/doc/resist.tex @@ -15,8 +15,8 @@ \section{Injection resistance by matcher-delimiting untrusted input} \subsection{Preventing SQL injection} \label{sec:resist:sql} -The discipline is worth making concrete in the setting that most sharply -motivates it, untrusted input embedded into a query language such as SQL. +Take the setting that most sharply motivates the discipline: untrusted input +embedded into a query language such as SQL. Recall the classic vulnerability of \cref{sec:intro}: a server composes a clause like \verb|"WHERE name = '"+userName+"'"|, and a \verb|userName| containing a quote closes the literal early and appends attacker-controlled @@ -50,12 +50,35 @@ \subsection{Preventing SQL injection} on read. Defined on every input, it never rejects, and because its escapes are themselves balanced its output is always valid matchertext, its sole and host-independent -obligation, checkable in isolation by the \textsc{Verify} scan and saying nothing -about SQL. +obligation (\cref{sec:appendix:tomatchertext}), checkable in isolation by the +\textsc{Verify} scan and saying nothing about SQL. The failure mode is therefore benign: an encoder bug yields mis-encoded \emph{data}, never a breakout, where in conventional escaping one missed case \emph{is} the injection. +Reading inverts the encoder. +Assume \textsc{esc} is uniquely decodable: injective, with a reserved introducer +so that its outputs are recognizable in the surrounding text, as any +backslash-style escape is. +Then \textsc{FromMatchertext} scans the balance-delimited region once, mapping +each \textsc{esc}$(c)$ back to its matcher $c$ and copying every other character, +so that $\textsc{FromMatchertext}(\textsc{ToMatchertext}(v)) = v$ for every $v$: +\begin{verbatim} +FromMatchertext(m): + out = []; i = 0 + while i < |m|: + if m[i..] begins with esc(c): + out += c; i += |esc(c)| + else: + out += m[i]; i += 1 + return out +\end{verbatim} +This round-trip is a data-fidelity property, argued here rather than proved: it is +no part of the inertness claim, which rests only on output $\in L$ +(\cref{sec:appendix:tomatchertext}). +A decoder bug corrupts a value; it cannot manufacture a breakout, since the region +is already inertly delimited before decoding begins. + Under a matchertext-aware host that ends each value by matcher balance, matchertext offers a \emph{structural} property: no valid-matchertext value, in any position, can escape its delimiters or alter the surrounding query structure, @@ -162,3 +185,136 @@ \subsection{Preventing PDF object injection} design: data an application deliberately routes into a \verb|/JS| action still runs, though it can no longer escape its string to \emph{introduce} one, which is where the reported attacks overwhelmingly live. + +\subsection{Fitting matchertext into existing languages} +\label{sec:resist:fitting} + +\begin{table*}[t] +\centering +\small +\begin{tabular}{llllll} +\hline +Route & Example & Changes & New syntax & Compatibility & Trusted delta \\ +\hline +Reuse native matchers & \verb|(uid=|$v$\verb|)|, \verb|/URI (|$v$\verb|)| & nothing & none & full & none \\ +Extend the host grammar & \verb|WHERE name = [|$v$\verb|]| & host parser & hole form & per host & boundary reader \\ +Replace the host language & MinML for markup & host parser & wholly new & none & whole parser \\ +\hline +\end{tabular} +\caption{Routes to premise A1, an aware host. \emph{Trusted delta} is what each +adds to the trusted computing base of \cref{sec:threat} beyond the parser the +host already has.} +\label{tab:resist:a1} +\end{table*} + +\begin{table*}[t] +\centering +\small +\begin{tabular}{llll} +\hline +Route & Example & Guarantees A2? & Cost \\ +\hline +String concatenation & \verb|"... = [" + v + "]"| & no, by inspection only & none \\ +Matchertext literal & \verb|M"(WHERE name = [|$v$\verb|])"| & lexer reads to balance & literal form \\ +Structural interpolation & \verb|M{}"(WHERE name = [{v}])"| & holes fixed before binding & literal + interpolation \\ +\hline +\end{tabular} +\caption{Routes to premise A2, the value reaching a hole. Only the interpolating +form makes the template's structure independent of $v$ at composition time.} +\label{tab:resist:a2} +\end{table*} + +Adoption is two problems, not one, and the hosting syntaxes +of~\cite{matchertext} answer only the second. +Premise A1 of \cref{sec:threat} constrains the \emph{host}: the SQL engine, HTML +parser, or directory server that interprets the composed text must end the +embedded value by matcher balance. +Premise A2 constrains the \emph{application} that composes it: the untrusted value +must reach a matcher-delimited hole rather than be concatenated in beside one. +The two are discharged by changes to different languages, by different people, +and are worth separating. + +\paragraph{Making the host aware (A1).} +\Cref{tab:resist:a1} compares the routes. +Reusing a construct the format \emph{already} delimits with matchers is free: +LDAP search filters and PDF literal strings +(\cref{sec:resist:ldap,sec:resist:pdf}) are parenthesis-delimited by definition, +so the discipline coincides with the format, and A1 costs no new syntax and no +new trusted code. +It also reaches only the formats built that way. +Extending a host's grammar with a hole form reaches the syntaxes where injection +actually concentrates, at the price of a change inside the host's parser, and the +change is not always conservative: T-SQL already gives \verb|[|$\dots$\verb|]| a +meaning as a delimited identifier, so a hole form for SQL must either pick +different delimiters or accept that it is not backward-compatible in the way +\cite{matchertext}'s \verb|M"|$\dots$\verb|"| literal is for C. +Replacing the host language obtains A1 by construction and reaches everything it +covers, but only for new deployments, since nothing previously written parses. + + +\paragraph{Making the composition safe (A2).} +A1 is worth nothing if the value never reaches the hole, and today that is left to +developer discipline: nothing stops a programmer from concatenating into the query +around a hole rather than into it. +This is where the source-level syntaxes of~\cite{matchertext} earn their place in +a security argument, and \cref{tab:resist:a2} sets them against the status quo. +A matchertext literal with structural interpolation makes the template's holes +explicit and its structure fixed, so an interpolated value cannot alter the +surrounding query no matter what it contains, an application of the discipline +that~\cite{matchertext} identifies as its security-relevant use of interpolation. +The literal form is a conservative extension for mainstream C-like languages, +since a marker abutting a quote is input their grammars already reject, so it can +ship behind a flag without endangering existing code. + + +Together the two premises replace an obligation on the programmer at every use +site with an obligation on two parsers: A1 relocates a bounded part of the host's +parser, and A2 adds a lexical form to the application language. +Neither removes a parser from the trusted base, and neither is meant to +(\cref{sec:bg:sanitizer}). + +\subsection{Comparison with existing defenses} +\label{sec:resist:baselines} + +\Cref{sec:bg:sanitizer} contrasts matchertext with hand-escaping and sanitizers. +The strongest defenses for these hosts are not sanitizers, however, and +matchertext should be measured against those instead. + +\emph{Parameterized queries} are the strongest of them. +A prepared statement fixes the query structure before any value is bound, so no +value can alter it, and it holds today with no change to the language. +It binds \emph{values}, however, and only values: a table or column name cannot +be a placeholder, so identifier positions fall back to ad-hoc allow-listing, +which is the construction \cref{sec:resist:sql} covers directly with +\verb|FROM [|\textit{table}\verb|]|. +\emph{Contextual auto-escaping} and typed template contexts do the same work for +markup, selecting the escaper from the syntactic context rather than leaving the +choice to the programmer, and browser-side mechanisms such as Trusted Types +enforce a related discipline at the host. +\emph{Taint tracking} is orthogonal to all of these: it decides \emph{which} +values are untrusted, not what happens when one reaches a hole. + +Matchertext differs from all of them in what it is a defense \emph{of}. +Each baseline is a mechanism for one host: prepared statements know SQL, +auto-escapers know markup, and neither transfers to LDAP filters, PDF strings, or +URIs, each of which needs a defense written and maintained separately. +Inertness is stated over a hole rather than over a value, and \textsc{Verify} +inspects six characters and knows nothing about the language around them, so one +check serves every host and covers identifier positions as readily as values. +That is the narrow waist of \cref{sec:bg:waist} claimed as a security property: +$N$ hosts need $N$ defenses today, and one discipline instead of $N$ is the +distinctive claim. +Two consequences follow. +Correctness stops depending on a per-context choice, removing the failure mode +that defeated every participant in the study of \cref{sec:bg:prevalence}; and +because the obligation is a check rather than a transformation, a bug in it +rejects data instead of admitting a breakout. + +The cost is where the obligation lands. +The baselines ask for a library; matchertext asks the host to read to matcher +balance, which \cref{tab:resist:a1} shows is free where the format already +delimits with matchers, as in LDAP and PDF, and a parser change where it does +not. +The two also compose: nothing in \cref{sec:threat} prevents a parameterized query +from carrying a matcher-delimited identifier, which is the combination neither +mechanism reaches alone. diff --git a/injection-research/doc/results.tex b/injection-research/doc/results.tex index 61300f0..2ce3fd1 100644 --- a/injection-research/doc/results.tex +++ b/injection-research/doc/results.tex @@ -4,70 +4,59 @@ \section{Results} \begin{table}[t] \centering \small -\begin{tabular}{lrr} -\toprule -Injection syntax & CVEs & with PoC \\ -\midrule -HTML / DOM (XSS) & 50{,}884 & 5{,}207 \\ -SQL & 22{,}225 & 5{,}545 \\ -Shell command & 9{,}672 & 1{,}013 \\ -Code / eval & 6{,}666 & 1{,}699 \\ -CRLF / header & 656 & 73 \\ -Argument & 430 & 39 \\ -\bottomrule -\end{tabular} -\caption{Largest injection syntax types, of \(91{,}760\) injection CVEs, with +\input{generated/tbl-syntax} +\caption{Largest injection syntax types, of \dataInjectionCVEs injection CVEs, with the count carrying at least one linked proof-of-concept.} \label{tab:syntax} \end{table} \paragraph{Syntax distribution.} \Cref{tab:syntax} shows that injection is overwhelmingly concentrated in two -syntaxes (HTML/DOM and SQL together account for four in five injection CVEs) +syntaxes (HTML/DOM and SQL together account for \dataTopTwoShare of injection CVEs) with a long tail of shell, code-eval, header, template, LDAP, XML, and formula contexts. This concentration matters directly for \cref{sec:prevent}: the two dominant syntaxes are exactly the ones a matchertext host can delimit with a matcher pair. -Exploitation signals are sparse but consistent with severity: 345 injection CVEs +Exploitation signals are sparse but consistent with severity: \dataInjectionKev injection CVEs appear in the CISA Known-Exploited catalog, and command injection, though only a tenth of the corpus, carries a disproportionate share of them. \paragraph{Proof-of-concept coverage.} -\textbf{13{,}691} injection CVEs (15\%) carry at least one linked PoC. -The four PoC databases overlap, so unifying them raises payload coverage well -above any single source. Of these, \textbf{5{,}025} yield an extractable payload; the remainder +\textbf{\dataInjectionWithPoc} injection CVEs (\dataInjectionWithPocShare) carry at least one linked PoC. +The PoC databases overlap, so unifying them raises payload coverage well +above any single source. Of these, \textbf{\dataPayloadBackedCVEs} yield an extractable payload; the remainder are links only or exploits from which no literal attack string can be recovered, such as modules -that construct their payload programmatically. This linkage is what makes the prevention analysis +that construct their payload programmatically. This linkage is what makes the containment analysis of \cref{sec:prevent} possible, since it supplies the real attack strings. \paragraph{Sub-classification.} Beyond the two primary axes, each injection CVE is labelled on orthogonal facets, each from its strongest available signal, and stored in long form so a CVE can carry one label per dimension at once. -The CVSS vector yields reachability for free: \textbf{50{,}607} injection CVEs -are exploitable pre-authentication, 28{,}471 require low privilege, and 11{,}085 +The CVSS vector yields reachability for free: \textbf{\dataSubPrivilegePreAuth} injection CVEs +are exploitable pre-authentication, \dataSubPrivilegeLowPriv require low privilege, and \dataSubPrivilegeHighPriv high privilege. Finer \emph{technique} labels come from PoC payloads and descriptions where -present: SQL injections resolve into blind-boolean (866), union-based (621), -blind-time (372), and authentication-bypass (201) attacks, while XSS resolves -into stored (15{,}559), reflected (6{,}337), and DOM-based (1{,}610). +present: SQL injections resolve into blind-boolean (\dataSubTechniqueBlindBoolean), union-based (\dataSubTechniqueUnionBased), +blind-time (\dataSubTechniqueBlindTime), and authentication-bypass (\dataSubTechniqueAuthBypass) attacks, while XSS resolves +into stored (\dataSubTechniqueStored), reflected (\dataSubTechniqueReflected), and DOM-based (\dataSubTechniqueDomBased). \paragraph{Syntactic groups.} -For the \textbf{5{,}025} injection CVEs with an extractable PoC payload, we +For the \textbf{\dataPayloadBackedCVEs} injection CVEs with an extractable PoC payload, we reduce each payload to a \emph{syntactic skeleton}: string literals, numbers, and identifiers are abstracted to placeholders (\verb||, \verb||, \verb||) while the structural grammar (matchers, operators, tags, and a curated set of injection keywords) is preserved. -Grouping by identical skeleton yields \textbf{2{,}143} distinct groups -(1{,}817 of them singletons), so specific values never split a group but a +Grouping by identical skeleton yields \textbf{\dataDistinctSkeletons} distinct groups +(\dataSingletonGroups of them singletons), so specific values never split a group but a different breakout structure always does. The largest groups are recognizable attack families: the XSS skeletons -\verb|ALERT(DOCUMENT.)| (453 CVEs) and its -\verb|DOCUMENT.COOKIE| variant (231), and the code-eval fragment -\verb|| (110). -The tail is long: the singletons are 85\% of groups but only 36\% of CVEs, and -they collapse to fifteen distinct verdicts, since the skeleton preserves tags and +\verb|ALERT(DOCUMENT.)| (\dataGroupAlertDocId CVEs) and its +\verb|DOCUMENT.COOKIE| variant (\dataGroupAlertCookie), and the code-eval fragment +\verb|| (\dataGroupPhpOpen). +The tail is long: the singletons are \dataSingletonGroupShare of groups but only \dataSingletonCVEShare of CVEs, and +they collapse to \dataSingletonVerdicts distinct verdicts, since the skeleton preserves tags and operators that the containment test does not depend on. Because the skeleton preserves exactly the matcher structure while discarding -values, it is the natural unit on which to test matchertext prevention next: the +values, it is the natural unit on which to test matchertext containment next: the verdict depends only on that structure, so it is shared by every CVE in a group. diff --git a/injection-research/doc/threat.tex b/injection-research/doc/threat.tex index 32dbe1c..2687e80 100644 --- a/injection-research/doc/threat.tex +++ b/injection-research/doc/threat.tex @@ -5,6 +5,37 @@ \section{Threat model and security property} makes the conditions explicit: what is trusted, what the attacker controls, the property that is meant to hold, and the deployment premises it requires. The property is stated below as an invariant on the host's parse. +\Cref{fig:threat:pipeline} shows the path an untrusted value takes and where each +premise binds. + +\begin{figure*}[t] +\footnotesize +\begin{verbatim} + UNTRUSTED │ TRUSTED COMPUTING BASE +─────────────┼────────────────────────────────────────────────────────────────────────────────── + │ + attacker │ canon(v) ──► VERIFY ──► s_o[ v ]s_c ──► host parser ──► interpreter + │ │ decode & v ∈ L ? value placed ends value binds the + └─ v ───┼─► normalize │ in the hole by matcher terminal + │ fail balance as data + arbitrary │ │ + bytes, │ ▼ + encodings, │ ToMatchertext(v) + may be │ escape unmatched + invalid │ matchers, re-embed + │ +─────────────┼────────────────────────────────────────────────────────────────────────────────── + binds: │ A3 (TCB ii) A2 A1 · L1 · L2 L3 · A4 +\end{verbatim} +\caption{Where each premise binds. The attacker chooses $v$ and nothing else; +everything right of the boundary must be correct for inertness to hold. A value +failing \textsc{Verify} is not embedded, but is escaped by \textsc{ToMatchertext} +and re-enters at the hole. Note that A3 binds at the first stage while its +violation surfaces at the last: a value that is still encoded when checked, such +as \texttt{\%5D}, passes \textsc{Verify} and only becomes an unmatched matcher +once the parser reads it.} +\label{fig:threat:pipeline} +\end{figure*} \paragraph{Protected asset.} For a host program with a hole $P[\cdot]$ @@ -17,7 +48,9 @@ \section{Threat model and security property} with a matcher pair and ends the embedded value by matcher balance rather than by scanning for its native closer; (ii) the \textsc{Verify} recognizer that decides membership in the matchertext language $L$; and (iii) the total encoder -\textsc{ToMatchertext} and its inverse, used on free-form fields. +\textsc{ToMatchertext} and its inverse, used on free-form fields; its +output-in-$L$ obligation is discharged in \cref{sec:appendix:tomatchertext}, +narrowing~(iii) to the decoder round-trip. The boundary-locating step of (i) is the operationally load-bearing part; we discharge it below as premise L1 (machine checked), so what the host must still be trusted for is the \emph{implementation} of that step rather than its principle. @@ -28,7 +61,7 @@ \section{Threat model and security property} that are \emph{not} valid matchertext. Following Kerckhoffs, the attacker knows the discipline, which delimiter kind guards the hole, and where the hole boundaries lie, and crafts $v$ \emph{against} -the matcher-delimited slot, not the legacy quote or tag-delimited sink that the +the matcher-delimited slot, not the legacy quote or tag-delimited host that the recorded corpus payloads (\cref{sec:results}) target. The attacker does not control the host source, the configuration $(\Sigma,\Pi)$, or the trusted components above. @@ -48,10 +81,11 @@ \section{Threat model and security property} \emph{string}, not the host \emph{parser}. \paragraph{Deployment premises.} -Inertness holds under four assumptions, each necessary: +Inertness holds under four premises, each necessary: \begin{itemize} -\item[\textbf{A1}] \emph{Aware host.} The sink is a matchertext-aware host that - ends the value by matcher balance rather than at its native closer. +\item[\textbf{A1}] \emph{Aware host.} The host that interprets the composed text + is matchertext-aware: it ends the value by matcher balance rather + than at its native closer. \item[\textbf{A2}] \emph{Delimited context.} Every untrusted value is routed into a matcher-delimited hole; a value concatenated into host syntax outside a hole is unprotected, exactly as with any point-of-use defense. @@ -133,4 +167,4 @@ \section{Threat model and security property} access-control question; algorithmic denial of service (regular-expression backtracking, entity expansion), which is not a breakout; and second-order injection in which stored input is reinterpreted later in a different context, -unless it is re-checked under A3 at that later sink. \ No newline at end of file +unless it is re-checked under A3 at that later host. \ No newline at end of file diff --git a/injection-research/doc/to_matchertext.tex b/injection-research/doc/to_matchertext.tex new file mode 100644 index 0000000..9f22073 --- /dev/null +++ b/injection-research/doc/to_matchertext.tex @@ -0,0 +1,83 @@ +\section{Machine-checked: \textsc{ToMatchertext}} +\label{sec:appendix:tomatchertext} + +The declaration heads below summarize the Lean~4 development in +\texttt{lean/to\_matchertext.lean} that discharges the write-path obligation of +\cref{sec:threat} (TCB item~iii): the total encoder's output is \emph{always} +matchertext. It reuses the base definitions of \cref{sec:appendix:lean} +(\texttt{Opener}, \texttt{Closer}, \texttt{Nonmatcher}, \texttt{MT}, and the +\texttt{depth}/\texttt{embed\_boundary} results) and the closure lemmas +\texttt{mt\_append}/\texttt{mt\_wrap} of~\cite{matchertext}. +Definition bodies are shown in full; tactic proof bodies are elided and given in +the source file. + +\begin{lstlisting} +import Core +import embed_boundary +import always_embeddable +open Classical + +variable {α : Type*} -- the alphabet Σ, kept abstract +variable (Pi : Set (α × α)) -- the set of pairs Π + +-- A pending scan context: an opener awaiting its closer, with the output at its level. +abbrev Ctx (α : Type*) := α × List α + +-- End of input: every opener still pending is unmatched, so it is escaped. +noncomputable def unwind (esc : α → List α) : List (Ctx α) → List α → List α + | [], out => out + | (o, b) :: st, out => unwind esc st (b ++ esc o ++ out) + +-- One left-to-right pass. `st` holds the pending openers, `out` the output at the current +-- level. A closer is matched only if it pairs with the top; else it is unmatched and escaped. +noncomputable def encAux (esc : α → List α) : + List (Ctx α) → List α → List α → List α + | st, out, [] => unwind esc st out + | st, out, x :: xs => + if Opener Pi x then encAux esc ((x, out) :: st) [] xs + else if Closer Pi x then + match st with + | (o, b) :: st' => + if (o, x) ∈ Pi then encAux esc st' (b ++ [o] ++ out ++ [x]) xs + else encAux esc st (out ++ esc x) xs + | [] => encAux esc st (out ++ esc x) xs + else encAux esc st (out ++ [x]) xs + +noncomputable def toMatchertext (esc : α → List α) (v : List α) : List α := + encAux Pi esc [] [] v + +-- Lemma: an escape contains no matchers, hence is matchertext. +theorem esc_mt (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) (c : α) : + MT Pi (esc c) := ... + +-- Lemma: unwinding the pending stack preserves matchertext. +theorem unwind_mt (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) + (st : List (Ctx α)) (hst : ∀ p ∈ st, MT Pi p.2) + (out : List α) (hout : MT Pi out) : + MT Pi (unwind esc st out) := by ... + +-- Invariant (the crux): every accumulated segment stays matchertext. +theorem encAux_mt (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) + (st : List (Ctx α)) (hst : ∀ p ∈ st, MT Pi p.2) + (out : List α) (hout : MT Pi out) (v : List α) : + MT Pi (encAux Pi esc st out v) := by ... + +-- Theorem (output ∈ L): any string at all, once encoded, is matchertext. +theorem toMatchertext_mt (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) (v : List α) : + MT Pi (toMatchertext Pi esc v) := ... + +-- Corollary (write-path payoff): reading to matcher balance recovers exactly the encoded +-- value, for a freely chosen v. embed_boundary assumes MT Pi m, which toMatchertext_mt supplies. +theorem embed_boundary_encoded + (hdisj : ∀ x y z, (x, y) ∈ Pi → (z, x) ∈ Pi → False) + (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) + (v : List α) {c : α} (hc : Closer Pi c) : + (∀ p, p <+: toMatchertext Pi esc v → 0 ≤ depth Pi p) + ∧ depth Pi (toMatchertext Pi esc v) = 0 + ∧ depth Pi (toMatchertext Pi esc v ++ [c]) = -1 := ... +\end{lstlisting} diff --git a/injection-research/manifest.json b/injection-research/manifest.json index 50431fd..adad3f2 100644 --- a/injection-research/manifest.json +++ b/injection-research/manifest.json @@ -1,14 +1,34 @@ { + "BenchmarkJava": { + "commit": "79b9bd6177e07991a9c11dc19e457c840e229931", + "fetched": "2026-07-28", + "url": "https://github.com/OWASP-Benchmark/BenchmarkJava.git" + }, + "PayloadsAllTheThings": { + "commit": "434cc897f9b1e561f3804631e40643e6c82c3d14", + "fetched": "2026-07-28", + "url": "https://github.com/swisskyrepo/PayloadsAllTheThings.git" + }, "PoC-in-GitHub": { "commit": "c27b1516f2f40af43ae8114264f8330e84ce4a6f", "fetched": "2026-07-13", "url": "https://github.com/nomi-sec/PoC-in-GitHub.git" }, + "SecLists": { + "commit": "aeb36e9df937d1b77042e5667780e8156cd419f7", + "fetched": "2026-07-28", + "url": "https://github.com/danielmiessler/SecLists.git" + }, "advisory-database": { "commit": "79c2cf4630fcc44f2632735de08432a07cfaf204", "fetched": "2026-07-13", "url": "https://github.com/github/advisory-database.git" }, + "cve-scores": { + "commit": "eef9ab5b2a334e83b23dc90f1d12fd280866e1d8", + "fetched": "2026-07-28", + "url": "https://github.com/ARPSyndicate/cve-scores.git" + }, "cvelistV5": { "commit": "92d64b4c9b3c5a0ce1fd1e5f8c017b9772e0139b", "fetched": "2026-07-13", @@ -35,6 +55,21 @@ "fetched": "2026-07-13", "url": "https://gitlab.com/exploit-database/exploitdb.git" }, + "fuzzdb": { + "commit": "5656ab25dc6bb43bae32236fab775658a90d7380", + "fetched": "2026-07-28", + "url": "https://github.com/fuzzdb-project/fuzzdb.git" + }, + "juliet-c": { + "fetched": "2026-07-28", + "sha256": "ada9d7e1c323d283446df3f55bdee0d00bda1fed786785fe98764d58688f38eb", + "url": "https://samate.nist.gov/SARD/downloads/test-suites/2017-10-01-juliet-test-suite-for-c-cplusplus-v1-3.zip" + }, + "juliet-java": { + "fetched": "2026-07-28", + "sha256": "d985f4177c2bcd7b03455a05c1c8f2e755f55c9eb250accd052f05f877347e60", + "url": "https://samate.nist.gov/SARD/downloads/test-suites/2017-10-01-juliet-test-suite-for-java-v1-3.zip" + }, "kev": { "fetched": "2026-07-13", "sha256": "c62c660cb9612925ce5910f313c8a09d1cf58f9b7bf677c785c44e20f2451b2c", @@ -180,6 +215,16 @@ "sha256": "a96a85a365ea3ada08220bd748bc5921f60f4b63feb8e33c27da73c8d65c2084", "url": "https://access.redhat.com/hydra/rest/securitydata/cve.json" }, + "trickest-cve": { + "commit": "b3a270a001a31742516eaea5c494f365de9d3c80", + "fetched": "2026-07-28", + "url": "https://github.com/trickest/cve.git" + }, + "vulhub": { + "commit": "aeaf65793f147f29bd50841ef77f4e9cad07ecc7", + "fetched": "2026-07-28", + "url": "https://github.com/vulhub/vulhub.git" + }, "vulnrichment": { "commit": "3d48581d1262450948913da31a996c293c65dc6d", "fetched": "2026-07-13", diff --git a/injection-research/pipeline/build_db.py b/injection-research/pipeline/build_db.py index def142e..8903462 100644 --- a/injection-research/pipeline/build_db.py +++ b/injection-research/pipeline/build_db.py @@ -33,6 +33,9 @@ DROP TABLE IF EXISTS cwe_hierarchy; DROP TABLE IF EXISTS poc; DROP TABLE IF EXISTS advisory; +DROP TABLE IF EXISTS payload; +DROP TABLE IF EXISTS ground_truth; +DROP TABLE IF EXISTS exploit_score; CREATE TABLE cve(cve_id TEXT PRIMARY KEY, state TEXT, published_at TEXT, updated_at TEXT, assigner TEXT, description TEXT); CREATE TABLE cwe_assignment(cve_id TEXT, cwe_id INTEGER, source TEXT, @@ -52,8 +55,53 @@ -- Per-source advisory metadata (severity / fix status) for breadth. CREATE TABLE advisory(cve_id TEXT, source TEXT, severity TEXT, status TEXT, ref TEXT, UNIQUE(cve_id, source, ref)); +-- Attack payloads by sink type, from the curated corpora. Independent of the CVE +-- record: these are the strings themselves, which is what matchertext is +-- assessed against. +CREATE TABLE payload(corpus TEXT, path TEXT, syntax_type TEXT, payload TEXT, + UNIQUE(corpus, syntax_type, payload)); +-- CWE-labeled cases from synthetic suites. is_vulnerable is 1/0 where the suite +-- states a verdict (OWASP Benchmark) and NULL where it does not (Juliet files +-- carry both a good and a bad variant in one file). +CREATE TABLE ground_truth(suite TEXT, case_id TEXT, category TEXT, cwe_id INTEGER, + is_vulnerable INTEGER, UNIQUE(suite, case_id)); +-- VEDAS exploit-availability score, an alternative signal to EPSS. +CREATE TABLE exploit_score(cve_id TEXT PRIMARY KEY, epss REAL, vedas REAL); """ +# (corpus, path under data/raw, syntax_type). Line-oriented .txt only: markdown +# payload tables carry prose and shell transcripts that pollute the measurement. +PAYLOAD_SOURCES = [ + ("fuzzdb", "fuzzdb/attack/sql-injection", "sql"), + ("fuzzdb", "fuzzdb/attack/no-sql-injection", "nosql"), + ("fuzzdb", "fuzzdb/attack/os-cmd-execution", "shell_command"), + ("fuzzdb", "fuzzdb/attack/ldap", "ldap"), + ("fuzzdb", "fuzzdb/attack/xpath", "xpath_xquery"), + ("fuzzdb", "fuzzdb/attack/xss", "html_dom"), + ("fuzzdb", "fuzzdb/attack/html_js_fuzz", "html_dom"), + ("fuzzdb", "fuzzdb/attack/xml", "xml"), + ("fuzzdb", "fuzzdb/attack/server-side-include", "template"), + ("patt", "PayloadsAllTheThings/SQL Injection/Intruder", "sql"), + ("patt", "PayloadsAllTheThings/NoSQL Injection/Intruder", "nosql"), + ("patt", "PayloadsAllTheThings/LDAP Injection/Intruder", "ldap"), + ("patt", "PayloadsAllTheThings/Command Injection/Intruder", "shell_command"), + ("patt", "PayloadsAllTheThings/Server Side Template Injection/Intruder", "template"), + ("seclists", "SecLists/Fuzzing/XSS", "html_dom"), + ("seclists", "SecLists/Fuzzing/Databases", "sql"), + ("seclists", "SecLists/Fuzzing/LDAP.Fuzzing.txt", "ldap"), + ("seclists", "SecLists/Fuzzing/XML-FUZZ.txt", "xml"), + ("seclists", "SecLists/Fuzzing/XXE-Fuzzing.txt", "xml"), + ("seclists", "SecLists/Fuzzing/command-injection-commix.txt", "shell_command"), + ("seclists", "SecLists/Fuzzing/UnixAttacks.fuzzdb.txt", "shell_command"), + ("seclists", "SecLists/Fuzzing/Windows-Attacks.fuzzdb.txt", "shell_command"), + ("seclists", "SecLists/Fuzzing/SSI-Injection-Jhaddix.txt", "template"), + ("seclists", "SecLists/Fuzzing/HTML5sec-Injections-Jhaddix.txt", "html_dom"), + ("seclists", "SecLists/Fuzzing/URI-XSS.fuzzdb.txt", "html_dom"), +] +# Same bounds as report.extract_payload, so corpus and PoC-derived payloads are +# measured on comparable strings. +PAYLOAD_MIN, PAYLOAD_MAX = 3, 200 + CVSS_KEYS = ("cvssV4_0", "cvssV3_1", "cvssV3_0", "cvssV2_0") @@ -355,6 +403,166 @@ def load_debian(con): con.commit() +EDB_ID_RE = re.compile(r"(?:exploits?|/)(\d{3,6})") + + +def link_exploitdb_ids(con): + """Join Exploit-DB *links* to the exploit files already cloned locally. + + load_exploitdb maps CVEs through the `codes` column of files_exploits.csv. + Where that column is blank the mapping is lost, even though other sources + link the CVE to the very same EDB entry and the file is already on disk. + Recovering those costs no network at all. Must run after the link-only + sources, since it reads their refs. + """ + csv_path = RAW / "exploitdb" / "files_exploits.csv" + if not csv_path.exists(): + return + files = {} + with open(csv_path, encoding="utf-8", errors="replace", newline="") as f: + for r in csv.DictReader(f): + files[r["id"]] = (r["file"], r.get("type")) + rows = [] + for cve, ref in con.execute( + "SELECT cve_id, ref FROM poc WHERE ref LIKE '%exploit-db.com%'"): + m = EDB_ID_RE.search(ref) + if m and m.group(1) in files: + path, kind = files[m.group(1)] + rows.append((cve, "exploitdb", m.group(1), "exploitdb/" + path, kind)) + _poc(con, rows) + + +def load_trickest(con): + """trickest/cve: per-CVE markdown whose POC section lists exploit links. + + The section has two subsections and they are not equivalent: "Github" holds + candidate PoC repositories, "Reference" holds advisory and write-up URLs that + are usually not exploits. Tag them apart so a PoC count can exclude the + latter rather than inflating on advisory links. + """ + base = RAW / "trickest-cve" + if not base.exists(): + print("trickest: not fetched, skipping") + return + rows = [] + for f in base.rglob("CVE-*.md"): + cid = f.stem + _, sep, tail = f.read_text(encoding="utf-8", errors="replace").partition("### POC") + if not sep: + continue + kind = None + for line in tail.splitlines(): + line = line.strip() + if line.startswith("####"): + kind = line.lstrip("# ").strip().lower() + elif line.startswith("- http") and kind: + rows.append((cid, "trickest", line[2:].strip(), None, kind)) + _poc(con, rows) + + +def load_vulhub(con): + """vulhub: reproducible per-CVE container environments. + + local_path points at the environment's README, not the directory, because it + is the README that carries the worked exploit request; that is what + extract_payload can read. + """ + base = RAW / "vulhub" + if not base.exists(): + print("vulhub: not fetched, skipping") + return + rows = [] + for d in base.glob("*/CVE-*"): + if not (d.is_dir() and CVE_RE.fullmatch(d.name)): + continue + readme = d / "README.md" + rows.append((d.name, "vulhub", str(d.relative_to(base)), + str(readme.relative_to(RAW)) if readme.exists() else None, + "environment")) + _poc(con, rows) + + +def load_vedas(con): + path = RAW / "cve-scores" / "cve-scores.csv" + if not path.exists(): + print("cve-scores: not fetched, skipping") + return + with open(path, encoding="utf-8", errors="replace", newline="") as f: + rows = [(r["CVE"], _num(r.get("EPSS")), _num(r.get("VEDAS"))) + for r in csv.DictReader(f) if (r.get("CVE") or "").startswith("CVE-")] + con.executemany("INSERT OR REPLACE INTO exploit_score VALUES(?,?,?)", rows) + con.commit() + + +def _num(v): + try: + return float(v) + except (TypeError, ValueError): + return None + + +def _payload_files(rel): + p = RAW / rel + if p.is_file(): + return [p] + if not p.is_dir(): + return [] + return sorted(f for f in p.rglob("*") if f.suffix in (".txt", ".fuzz")) + + +def load_payloads(con): + rows = set() + for corpus, rel, syn in PAYLOAD_SOURCES: + files = _payload_files(rel) + if not files: + print(f"payloads: {rel} missing, skipping") + continue + for f in files: + path = str(f.relative_to(RAW)) + for line in f.read_text(encoding="utf-8", errors="replace").splitlines(): + s = line.strip() + if PAYLOAD_MIN <= len(s) <= PAYLOAD_MAX and not s.startswith("#"): + rows.add((corpus, path, syn, s)) + con.executemany("INSERT OR IGNORE INTO payload VALUES(?,?,?,?)", rows) + con.commit() + + +def load_ground_truth(con): + """OWASP Benchmark (explicit verdict) and NIST SARD Juliet (CWE-labeled paths).""" + rows = [] + bench = RAW / "BenchmarkJava" / "expectedresults-1.2.csv" + if bench.exists(): + with open(bench, encoding="utf-8", errors="replace", newline="") as f: + for line in f: + parts = [p.strip() for p in line.split(",")] + if len(parts) >= 4 and parts[0].startswith("BenchmarkTest"): + rows.append(("owasp-benchmark", parts[0], parts[1], + int(parts[3]) if parts[3].isdigit() else None, + 1 if parts[2].lower() == "true" else 0)) + else: + print("benchmark: not fetched, skipping") + for suite in ("juliet-java", "juliet-c"): + z = RAW / "sard" / f"{suite}.zip" + if not z.exists(): + print(f"{suite}: not fetched, skipping") + continue + seen = set() + with zipfile.ZipFile(z) as zf: + for name in zf.namelist(): + if not name.endswith((".java", ".c", ".cpp")): + continue + m = re.search(r"CWE(\d+)_([^/]*)", name) + if not m: + continue + case = name.rsplit("/", 1)[-1] + if case in seen: + continue + seen.add(case) + rows.append((suite, case, m.group(2).split("__")[0], int(m.group(1)), None)) + con.executemany("INSERT OR IGNORE INTO ground_truth VALUES(?,?,?,?,?)", rows) + con.commit() + + def run(args): years = set(getattr(args, "years", None) or ()) DB.parent.mkdir(parents=True, exist_ok=True) @@ -371,16 +579,22 @@ def run(args): load_cwe(con) for name, fn in (("exploitdb", load_exploitdb), ("nuclei", load_nuclei), ("metasploit", load_metasploit), ("poc_github", load_poc_github), - ("ghsa", load_ghsa), ("redhat", load_redhat), ("debian", load_debian)): + ("trickest", load_trickest), ("vulhub", load_vulhub), + ("ghsa", load_ghsa), ("redhat", load_redhat), ("debian", load_debian), + ("edb_links", link_exploitdb_ids), + ("vedas", load_vedas), ("payloads", load_payloads), + ("ground_truth", load_ground_truth)): print(name, flush=True) fn(con) con.execute("CREATE INDEX idx_cwe_cve ON cwe_assignment(cve_id)") con.execute("CREATE INDEX idx_cvss_cve ON cvss(cve_id)") con.execute("CREATE INDEX idx_poc_cve ON poc(cve_id)") con.execute("CREATE INDEX idx_advisory_cve ON advisory(cve_id)") + con.execute("CREATE INDEX idx_payload_syn ON payload(syntax_type)") con.commit() for table in ("cve", "cwe_assignment", "cvss", "kev", "epss", "nvd_status", - "cwe_hierarchy", "poc", "advisory"): + "cwe_hierarchy", "poc", "advisory", "payload", "ground_truth", + "exploit_score"): print(f"{table}: {con.execute(f'SELECT COUNT(*) FROM {table}').fetchone()[0]} rows") print("poc by source:", dict(con.execute("SELECT source, COUNT(*) FROM poc GROUP BY 1"))) con.close() diff --git a/injection-research/pipeline/export.py b/injection-research/pipeline/export.py index 09ba3eb..80a18fa 100644 --- a/injection-research/pipeline/export.py +++ b/injection-research/pipeline/export.py @@ -14,6 +14,10 @@ DB = ROOT / "data" / "cve.db" EXPORTS = ROOT / "data" / "exports" +# Quoted in classify.tex, so latex.py reads it from here rather than +# repeating the value. +AUDIT_PER_METHOD = 75 + YEAR = "COALESCE(NULLIF(substr(v.published_at,1,4),''), substr(v.cve_id,5,4))" @@ -92,7 +96,7 @@ def cwe_disagreement(con): ["cve_id", "cna_family", "adp_family", "nvd_family"], sorted(rows)) -def audit_sample(con, per_method=75): +def audit_sample(con, per_method=AUDIT_PER_METHOD): rows = [] for (method,) in con.execute("SELECT DISTINCT method FROM classification ORDER BY method"): sample = sorted( @@ -120,6 +124,12 @@ def coverage(con): WHERE cve_id IN (SELECT cve_id FROM classification)""")], ["sanity_xss_n", q("SELECT COUNT(*) FROM classification WHERE syntax_type='html_dom'")], ["sanity_sqli_n", q("SELECT COUNT(*) FROM classification WHERE syntax_type='sql'")], + ["corpus_payloads", q("SELECT COUNT(*) FROM payload")], + ["corpus_payloads_hostable", q( + "SELECT COUNT(*) FROM payload_assessment WHERE preventable=1")], + ["ground_truth_cases", q("SELECT COUNT(*) FROM ground_truth")], + ["published_with_vedas", q("""SELECT COUNT(*) FROM cve v JOIN exploit_score USING(cve_id) + WHERE v.state='PUBLISHED'""")], ] write("coverage.csv", ["metric", "value"], rows) diff --git a/injection-research/pipeline/fetch.py b/injection-research/pipeline/fetch.py index 038a9db..7173084 100644 --- a/injection-research/pipeline/fetch.py +++ b/injection-research/pipeline/fetch.py @@ -27,9 +27,30 @@ "metasploit-framework": "https://github.com/rapid7/metasploit-framework.git", "advisory-database": "https://github.com/github/advisory-database.git", "PoC-in-GitHub": "https://github.com/nomi-sec/PoC-in-GitHub.git", + # PoC linkage and exploit-availability scoring + "trickest-cve": "https://github.com/trickest/cve.git", + "cve-scores": "https://github.com/ARPSyndicate/cve-scores.git", + "vulhub": "https://github.com/vulhub/vulhub.git", + # Payload corpora: the attack strings themselves, per sink type. These drive + # the matchertext-prevention measurement, which needs payloads rather than + # CVE metadata. + "PayloadsAllTheThings": "https://github.com/swisskyrepo/PayloadsAllTheThings.git", + "fuzzdb": "https://github.com/fuzzdb-project/fuzzdb.git", + "SecLists": "https://github.com/danielmiessler/SecLists.git", + # Labeled ground truth: injection cases with known CWE and known verdict. + "BenchmarkJava": "https://github.com/OWASP-Benchmark/BenchmarkJava.git", } REDHAT_URL = "https://access.redhat.com/hydra/rest/securitydata/cve.json" DEBIAN_URL = "https://security-tracker.debian.org/tracker/data/json" +# NIST SARD Juliet suites: synthetic cases whose paths encode the CWE, giving a +# CWE-labeled corpus independent of the CVE record. +SARD_SUITES = { + "juliet-java": "https://samate.nist.gov/SARD/downloads/test-suites/" + "2017-10-01-juliet-test-suite-for-java-v1-3.zip", + "juliet-c": "https://samate.nist.gov/SARD/downloads/test-suites/" + "2017-10-01-juliet-test-suite-for-c-cplusplus-v1-3.zip", +} +FREEZE = False def sha256(path): @@ -52,6 +73,11 @@ def download(url, dest): def pin(manifest, key, url, dest, today, **extra): prev = manifest.get(key, {}).get("sha256") + # --freeze keeps an already-pinned rolling feed at its recorded revision, so a + # corpus change can be attributed to newly added sources rather than to + # upstream drift in the old ones. + if FREEZE and dest.exists() and prev: + return # These HTTP endpoints serve mutable "latest"/rolling feeds (NVD re-scores # CVEs, CWE/Debian/Red Hat track head), so a drifted local copy means the # upstream moved: re-fetch and re-pin rather than aborting. @@ -66,6 +92,8 @@ def pin(manifest, key, url, dest, today, **extra): def run(args): + global FREEZE + FREEZE = getattr(args, "freeze", False) manifest = json.loads(MANIFEST.read_text()) if MANIFEST.exists() else {} today = datetime.datetime.now(datetime.UTC).date() @@ -96,6 +124,9 @@ def run(args): pin(manifest, "cwe", CWE_URL, RAW / "cwe" / "cwec_latest.xml.zip", today) + for name, url in SARD_SUITES.items(): + pin(manifest, name, url, RAW / "sard" / f"{name}.zip", today) + fetch_redhat(manifest, today) pin(manifest, "debian", DEBIAN_URL, RAW / "debian" / "debian_security.json", today) @@ -130,4 +161,6 @@ def fetch_redhat(manifest, today): ap = argparse.ArgumentParser(description=__doc__) ap.add_argument("--years", type=int, nargs="*", help="restrict NVD feeds to these years") ap.add_argument("--epss-date", help="EPSS snapshot date YYYY-MM-DD (default: yesterday)") + ap.add_argument("--freeze", action="store_true", + help="keep already-pinned rolling feeds at their recorded revision") run(ap.parse_args()) diff --git a/injection-research/pipeline/fetch_github.py b/injection-research/pipeline/fetch_github.py new file mode 100644 index 0000000..2fdd3f1 --- /dev/null +++ b/injection-research/pipeline/fetch_github.py @@ -0,0 +1,436 @@ +"""Stage 1b: recover payloads from linked GitHub PoC repositories. + +Most injection CVEs with a PoC link have no local file, so no payload can be +extracted from them. This resolves each CVE's most specific linked repo to a +commit SHA, fetches that exact commit, and keeps only the extracted payload. + +Reproducibility is the reason for the SHA. A quarter of these repos are already +gone and HEAD moves under the rest, so a corpus fetched by branch name cannot be +replayed. `git ls-remote` resolves the SHA without spending API quota, and +codeload serves that commit directly -- the archive's root directory is +`repo-`, so the pin is self-evidencing. Pins land in data/github_pins.json. + +Only the payload is stored, never the repo: archives are parsed in memory and +dropped, so no exploit code is written to disk (see the dual-use note in +doc/data.tex). + +Aggregators are excluded. trickest's Github section lists any repo mentioning a +CVE, which sweeps in bulk mirrors -- one nuclei-templates fork is linked from +11,758 CVEs -- and they are large, payload-free, and would dominate the fetch. + +Usage: + python3 pipeline/fetch_github.py # full run, resumable + python3 pipeline/fetch_github.py -n 500 # sample, for measurement +""" +import argparse +import io +import json +import queue +import random +import re +import sqlite3 +import subprocess +import sys +import tarfile +import threading +import time +import urllib.error +import urllib.request +from concurrent.futures import ThreadPoolExecutor +from pathlib import Path + +from report import extract_payload + +ROOT = Path(__file__).resolve().parents[1] +DB = ROOT / "data" / "cve.db" +PINS = ROOT / "data" / "github_pins.json" + +CODELOAD = "https://codeload.github.com/{owner}/{repo}/tar.gz/{ref}" +REPO_RE = re.compile(r"https?://(?:www\.)?github\.com/([\w.-]+)/([\w.-]+)", re.I) +# A linked repo is often the vulnerable application itself, not a proof of +# concept, and its own source is full of benign script tags, jQuery includes and +# CLI flags that read as payloads. Documentation is always searched, because that +# is where a PoC is written up; code is searched only when its path says the file +# is the exploit. Everything else is skipped, which costs a few genuine payloads +# and removes a much larger amount of application source. +DOC_EXT = {".md", ".txt", ".rst", ""} +CODE_EXT = {".py", ".php", ".rb", ".sh", ".js", ".go", ".java", ".pl", ".html", + ".json", ".yaml", ".yml", ".xml"} +POC_HINT = re.compile(r"(?:poc|exploit|payload|vuln|attack|cve-\d)", re.I) +MAX_MEMBER = 256 << 10 +MAX_ARCHIVE = 25 << 20 +TIMEOUT = 25 + +DDL = """ +CREATE TABLE IF NOT EXISTS remote_payload( + cve_id TEXT PRIMARY KEY, source TEXT, repo TEXT, sha TEXT, + file TEXT, payload TEXT, status TEXT); +""" + + +def repo_of(url): + m = REPO_RE.match(url.strip()) + if not m: + return None + return m.group(1), m.group(2).removesuffix(".git") + + +def candidates(con, max_fanout, done): + """CVEs with a specific (non-aggregator) GitHub repo and no payload yet.""" + rows = con.execute(""" + SELECT cl.cve_id, cl.syntax_type, p.ref + FROM classification cl JOIN poc p USING(cve_id) + WHERE p.local_path IS NULL AND p.ref LIKE '%github.com%' + AND cl.cve_id NOT IN (SELECT cve_id FROM poc WHERE local_path IS NOT NULL) + AND cl.cve_id NOT IN (SELECT cve_id FROM syntactic_group) + ORDER BY cl.cve_id, p.ref""").fetchall() + pairs, fan = set(), {} + for cve, syn, ref in rows: + r = repo_of(ref) + if r: + pairs.add((cve, syn, r)) + fan[r] = fan.get(r, 0) + 1 + by_cve = {} + for cve, syn, r in sorted(pairs): + if fan[r] > max_fanout or cve in done: + continue + if cve not in by_cve or fan[r] < fan[by_cve[cve][1]]: + by_cve[cve] = (syn, r) + return [(k, *by_cve[k]) for k in sorted(by_cve)] + + +def resolve_sha(owner, repo): + """Resolve HEAD to a commit SHA over the git protocol, not the REST API. + + Fallback for when the batched GraphQL path is unavailable. + """ + try: + out = subprocess.run( + ["git", "ls-remote", f"https://github.com/{owner}/{repo}", "HEAD"], + capture_output=True, text=True, timeout=TIMEOUT, + env={"GIT_TERMINAL_PROMPT": "0", "PATH": "/usr/bin:/bin:/usr/local/bin"}) + except subprocess.TimeoutExpired: + return None, "timeout" + if out.returncode != 0 or not out.stdout.strip(): + return None, "gone" + return out.stdout.split()[0], None + + +def _gql(query): + """Run one GraphQL query. gh exits non-zero when any alias 404s, but the + surviving aliases are still in `data`, so parse regardless of exit code.""" + try: + out = subprocess.run(["gh", "api", "graphql", "-f", "query=" + query], + capture_output=True, text=True, timeout=180) + return (json.loads(out.stdout) or {}).get("data") or {} + except Exception: # noqa: BLE001 + return {} + + +def resolve_batch(repos): + """SHA, root file listing and README text for many repos in one request. + + Downloading whole archives turned out to be bandwidth-bound: 24 concurrent + codeload fetches saturated the link at ~283 KB/s, which no amount of + threading or cores can fix. The tree gives the filenames for a few KB, so + only the handful of documents worth reading are ever transferred. + + Returns {(owner, name): (sha_or_None, [entry names], readme_text_or_None)}. + A deleted repo yields (None, [], None) without failing the batch. + """ + q = ["query {"] + for i, (o, n) in enumerate(repos): + q.append(f" r{i}: repository(owner:{json.dumps(o)}, name:{json.dumps(n)}) {{" + f" defaultBranchRef {{ target {{ ... on Commit {{ oid }} }} }}" + f" tree: object(expression:\"HEAD:\") {{ ... on Tree {{ entries {{ name type }} }} }}" + f" readme: object(expression:\"HEAD:README.md\") {{ ... on Blob {{ text }} }} }}") + q.append("}") + data = _gql("\n".join(q)) + result = {} + for i, key in enumerate(repos): + node = data.get(f"r{i}") + if not node: + result[key] = (None, [], None) + continue + target = (node.get("defaultBranchRef") or {}).get("target") or {} + tree = node.get("tree") or {} + entries = [(e.get("name"), e.get("type")) for e in (tree.get("entries") or ())] + result[key] = (target.get("oid"), entries, + (node.get("readme") or {}).get("text")) + return result + + +def fetch_blobs(items): + """Fetch specific file contents in one request. + + items: [((owner, name), path), ...]. Returns {(key, path): text_or_None}. + """ + if not items: + return {} + q = ["query {"] + for i, ((o, n), path) in enumerate(items): + q.append(f" b{i}: repository(owner:{json.dumps(o)}, name:{json.dumps(n)}) {{" + f" object(expression:{json.dumps('HEAD:' + path)})" + f" {{ ... on Blob {{ text }} }} }}") + q.append("}") + data = _gql("\n".join(q)) + out = {} + for i, key_path in enumerate(items): + node = data.get(f"b{i}") or {} + out[key_path] = ((node.get("object") or {}).get("text")) + return out + + +def subdir_paths(repos_dirs): + """List one level down, for repos whose root documents yielded nothing. + + items: [((owner, name), dirname), ...] -> {(key, dirname): [file names]} + """ + if not repos_dirs: + return {} + q = ["query {"] + for i, ((o, n), d) in enumerate(repos_dirs): + q.append(f" d{i}: repository(owner:{json.dumps(o)}, name:{json.dumps(n)}) {{" + f" object(expression:{json.dumps('HEAD:' + d)})" + f" {{ ... on Tree {{ entries {{ name type }} }} }} }}") + q.append("}") + data = _gql("\n".join(q)) + out = {} + for i, key_dir in enumerate(repos_dirs): + node = (data.get(f"d{i}") or {}).get("object") or {} + out[key_dir] = [e.get("name") for e in (node.get("entries") or ()) + if e.get("type") == "blob"] + return out + + +# Directories worth descending into when the root turned up nothing. Anchored on +# name segments: an unanchored "doc" matches docker and an unanchored "report" +# matches aj-report, neither of which holds a write-up. +DIR_HINT = re.compile( + r"(?:^|[-_.])(?:pocs?|exploits?|payloads?|vulns?|attacks?|docs?|" + r"writeups?|reports?|cve)(?:$|[-_.])", re.I) + + +def doc_paths(entries, limit): + """Root-level files worth reading, READMEs first. + + Dotfiles are skipped: they are extensionless, so they satisfy DOC_EXT and + would otherwise spend the per-repo budget on .gitattributes rather than the + write-up. + """ + names = [n for n, t in entries + if t == "blob" and n and not n.startswith(".") and eligible(n)] + names.sort(key=lambda n: (0 if "readme" in n.lower() else 1, n)) + return names[:limit] + + +def fetch(owner, repo, sha): + url = CODELOAD.format(owner=owner, repo=repo, ref=sha) + req = urllib.request.Request(url, headers={"User-Agent": "matchertext-research"}) + for attempt in range(3): + try: + with urllib.request.urlopen(req, timeout=TIMEOUT) as r: + if int(r.headers.get("Content-Length") or 0) > MAX_ARCHIVE: + return None, "oversize" + blob = r.read(MAX_ARCHIVE + 1) + # Never return a truncated archive: a cut-off gzip cannot be + # listed, so an oversized repo is skipped rather than half-read. + return (None, "oversize") if len(blob) > MAX_ARCHIVE else (blob, None) + except urllib.error.HTTPError as e: + if e.code in (429, 503) and attempt < 2: + time.sleep(2 ** attempt * 5) + continue + return None, f"http_{e.code}" + except Exception as e: # noqa: BLE001 + if attempt < 2: + time.sleep(2) + continue + return None, type(e).__name__ + return None, "retries" + + +def eligible(name): + """Documentation always; code only when the path claims to be the exploit.""" + suffix = Path(name).suffix.lower() + if suffix in DOC_EXT: + return True + return suffix in CODE_EXT and bool(POC_HINT.search(name)) + + +def scan(blob, syn): + try: + tf = tarfile.open(fileobj=io.BytesIO(blob), mode="r:gz") + members = [m for m in tf.getmembers() + if m.isfile() and m.size <= MAX_MEMBER and eligible(m.name)] + except Exception: # noqa: BLE001 + return None, "bad_archive" + # READMEs first: prose carries the worked payload far more often than the + # exploit script, which usually builds it at runtime. + members.sort(key=lambda m: (0 if "readme" in Path(m.name).name.lower() else 1, + m.name)) + for m in members: + try: + text = tf.extractfile(m).read().decode("utf-8", "replace") + except Exception: # noqa: BLE001 + continue + payload = extract_payload(text, syn) + if payload: + return payload, m.name + return None, None + + +def one(item, sha=None): + cve, syn, (owner, repo) = item + slug = f"{owner}/{repo}" + if sha is None: + sha, err = resolve_sha(owner, repo) + if sha is None: + return {"cve_id": cve, "repo": slug, "sha": None, + "file": None, "payload": None, "status": "gone"} + blob, err = fetch(owner, repo, sha) + if blob is None: + return {"cve_id": cve, "repo": slug, "sha": sha, + "file": None, "payload": None, "status": err} + payload, where = scan(blob, syn) + return {"cve_id": cve, "repo": slug, "sha": sha, + "file": where if payload else None, "payload": payload, + "status": "payload" if payload else "no_payload"} + + +def run(args): + con = sqlite3.connect(DB) + con.executescript(DDL) + keep = "" if args.retry else "" + done = {c for (c,) in con.execute( + "SELECT cve_id FROM remote_payload" if not args.retry else + "SELECT cve_id FROM remote_payload WHERE payload IS NOT NULL OR status='gone'")} + todo = candidates(con, args.max_fanout, done) + if args.n: + random.Random(args.seed).shuffle(todo) + todo = sorted(todo[:args.n]) + print(f"{len(done)} already fetched; {len(todo)} to go", file=sys.stderr, flush=True) + + pins = json.loads(PINS.read_text()) if PINS.exists() else {} + batch, t0 = [], time.time() + + def flush(): + con.executemany( + """INSERT OR REPLACE INTO remote_payload + VALUES(:cve_id, 'github', :repo, :sha, :file, :payload, :status)""", + batch) + con.commit() + PINS.write_text(json.dumps(pins, indent=1, sort_keys=True)) + batch.clear() + + def do_chunk(chunk): + """Two requests per chunk: listing, then the documents worth reading.""" + resolved = resolve_batch([r for _, _, r in chunk]) + rows, wanted = [], [] + for cve, syn, key in chunk: + sha, entries, readme = resolved.get(key, (None, [], None)) + if sha is None: + rows.append({"cve_id": cve, "repo": "/".join(key), "sha": None, + "file": None, "payload": None, "status": "gone"}) + continue + payload = extract_payload(readme, syn) if readme else None + if payload: + rows.append({"cve_id": cve, "repo": "/".join(key), "sha": sha, + "file": "README.md", "payload": payload, + "status": "payload"}) + continue + paths = [p for p in doc_paths(entries, args.docs) if p != "README.md"] + wanted.append((cve, syn, key, sha, paths, entries)) + blobs = fetch_blobs([(key, p) for _, _, key, _, ps, _ in wanted for p in ps]) + deep, resolved_rows = [], [] + for cve, syn, key, sha, paths, entries in wanted: + hit = hitfile = None + for p in paths: + text = blobs.get((key, p)) + hit = extract_payload(text, syn) if text else None + if hit: + hitfile = p + break + if hit or not args.deep: + resolved_rows.append({"cve_id": cve, "repo": "/".join(key), "sha": sha, + "file": hitfile, "payload": hit, + "status": "payload" if hit else "no_payload"}) + else: + dirs = [n for n, t in entries + if t == "tree" and n and not n.startswith(".") and DIR_HINT.search(n)] + deep.append((cve, syn, key, sha, dirs[:args.dirs])) + rows.extend(resolved_rows) + + # Second pass: the write-up is sometimes filed under docs/ or poc/ + # rather than at the root. + listing = subdir_paths([(key, d) for _, _, key, _, ds in deep for d in ds]) + deep_want = [] + for cve, syn, key, sha, dirs in deep: + paths = [] + for d in dirs: + for name in listing.get((key, d), ())[:args.docs]: + if eligible(name) and not name.startswith("."): + paths.append(f"{d}/{name}") + deep_want.append((cve, syn, key, sha, paths[:args.docs])) + blobs2 = fetch_blobs([(key, p) for _, _, key, _, ps in deep_want for p in ps]) + for cve, syn, key, sha, paths in deep_want: + hit = hitfile = None + for p in paths: + text = blobs2.get((key, p)) + hit = extract_payload(text, syn) if text else None + if hit: + hitfile = p + break + rows.append({"cve_id": cve, "repo": "/".join(key), "sha": sha, + "file": hitfile, "payload": hit, + "status": "payload" if hit else "no_payload"}) + return rows + + # Whole-archive downloads were bandwidth-bound; reading only the listed + # documents removes the transfer from the critical path, so chunks can just + # run concurrently with no producer/consumer machinery. + chunks = [todo[i:i + args.gql_batch] for i in range(0, len(todo), args.gql_batch)] + seen = 0 + with ThreadPoolExecutor(max_workers=args.workers) as ex: + for rows in ex.map(do_chunk, chunks): + for r in rows: + batch.append(r) + if r["sha"]: + pins[r["repo"]] = r["sha"] + seen += len(rows) + flush() + got = con.execute("SELECT COUNT(*) FROM remote_payload " + "WHERE payload IS NOT NULL").fetchone()[0] + print(f" {seen}/{len(todo)} payloads={got} " + f"{seen / max(time.time() - t0, 1):.1f}/s", file=sys.stderr, flush=True) + if batch: + flush() + + total = con.execute("SELECT COUNT(*) FROM remote_payload").fetchone()[0] + print(f"\nfetched {total} repos; pins in {PINS.relative_to(ROOT)}") + for st, n in con.execute("""SELECT status, COUNT(*) FROM remote_payload + GROUP BY 1 ORDER BY 2 DESC"""): + print(f" {st:12} {n}") + con.close() + + +if __name__ == "__main__": + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("-n", type=int, help="sample this many instead of the full set") + ap.add_argument("--seed", type=int, default=17) + ap.add_argument("--retry", action="store_true", + help="re-process repos previously found to have no payload") + ap.add_argument("--workers", type=int, default=8, + help="concurrent archive downloads; the work is I/O bound,\nso this is the lever, not core count") + ap.add_argument("--deep", action="store_true", + help="descend one level into doc/poc directories") + ap.add_argument("--dirs", type=int, default=3, + help="subdirectories to descend into per repo") + ap.add_argument("--docs", type=int, default=4, + help="root-level documents to read per repo") + ap.add_argument("--gql-batch", type=int, default=25, + help="repos per batched GraphQL request") + ap.add_argument("--no-gql", dest="gql", action="store_false", + help="skip GraphQL batching, resolve each SHA with git ls-remote") + ap.add_argument("--max-fanout", type=int, default=20, + help="drop repos linked from more CVEs than this (aggregators)") + run(ap.parse_args()) diff --git a/injection-research/pipeline/fetch_web.py b/injection-research/pipeline/fetch_web.py new file mode 100644 index 0000000..df5ab65 --- /dev/null +++ b/injection-research/pipeline/fetch_web.py @@ -0,0 +1,242 @@ +"""Stage 1c: recover payloads from Packet Storm and seclists advisory pages. + +These are the last sizeable PoC sources that host the advisory *text* rather +than another link to it, and unlike the commercial vulnerability databases they +need no API key. Together they cover roughly 2,200 injection CVEs that have no +local exploit file and no usable GitHub repo. + +Both allow this in robots.txt -- Packet Storm disallows only /tos/, seclists only +its search pages -- but seclists states plainly that "abusive IPs which make +hundreds of requests in a short period of time will be banned". The rate limit +below is therefore a condition of access, not politeness: one request per second +per *site*, with different sites running concurrently so the throttle costs +nothing in wall clock. + +Per site, not per hostname. An earlier version keyed the throttle on the +hostname, which gave packetstormsecurity.com and packetstormsecurity.org their +own budgets although they are one server; the resulting 2/s got us blocked. +Packet Storm serves that block as HTTP 200 with a refusal page, so it was +recorded as "no payload here" for a thousand advisories -- wrong data wearing +the shape of a result. Hence _BLOCKED, and a circuit breaker that abandons a +site after BLOCK_LIMIT consecutive refusals rather than continuing to hammer it. + +Reproducibility follows the same principle as the GitHub pins, adapted to pages +that carry no commit id: the sha256 of each fetched page is stored, so a later +run can tell a changed advisory from an unchanged one. + +Only the extracted payload is kept, never the page. + +Usage: + python3 pipeline/fetch_web.py # full run, resumable + python3 pipeline/fetch_web.py -n 50 # sample, for measurement +""" +import argparse +import hashlib +import html +import queue +import re +import sqlite3 +import sys +import threading +import time +import urllib.error +import urllib.request +from pathlib import Path + +from report import extract_payload + +ROOT = Path(__file__).resolve().parents[1] +DB = ROOT / "data" / "cve.db" + +HOSTS = { + "packetstormsecurity.com": "packetstorm", + "packetstormsecurity.org": "packetstorm", + "seclists.org": "seclists", +} +UA = ("Mozilla/5.0 (compatible; matchertext-research/1.0; " + "academic study of injection payload structure)") +TIMEOUT = 25 + +DDL = """ +CREATE TABLE IF NOT EXISTS web_payload( + cve_id TEXT PRIMARY KEY, source TEXT, url TEXT, sha256 TEXT, + payload TEXT, status TEXT); +""" + +_TAG = re.compile(r"<(script|style)\b[^>]*>.*?", re.I | re.S) +_ANY_TAG = re.compile(r"<[^>]+>") +_HOST = re.compile(r"https?://(?:www\.)?([^/]+)", re.I) +# A block is served as HTTP 200 with a refusal page, so status codes alone do +# not reveal it. Without this check a ban is silently recorded as "this advisory +# contains no payload", which is worse than an error: it is wrong data that looks +# like a finding. +_BLOCKED = re.compile( + r"velocity rate limiting|detected misuse|\bbanned\b|access denied" + r"|rate limit exceeded|too many requests|temporarily blocked", re.I) +# Consecutive blocks after which a site is abandoned for the rest of the run. +BLOCK_LIMIT = 3 + + +class Throttle: + """One request per interval per host, so concurrency across hosts is free.""" + + def __init__(self, interval): + self.interval = interval + self._locks = {} + self._next = {} + self._guard = threading.Lock() + + def wait(self, host): + with self._guard: + lock = self._locks.setdefault(host, threading.Lock()) + with lock: + now = time.monotonic() + due = self._next.get(host, 0.0) + if now < due: + time.sleep(due - now) + self._next[host] = max(now, due) + self.interval + + +def host_of(url): + m = _HOST.match(url.strip()) + return m.group(1).lower() if m else None + + +def candidates(con, done): + """One page per CVE: the first advisory URL on a host we can read.""" + rows = con.execute(""" + SELECT cl.cve_id, cl.syntax_type, p.ref + FROM classification cl JOIN poc p USING(cve_id) + WHERE cl.cve_id NOT IN (SELECT cve_id FROM syntactic_group) + ORDER BY cl.cve_id, p.ref""").fetchall() + out = {} + for cve, syn, ref in rows: + if cve in done or cve in out: + continue + h = host_of(ref) + if h in HOSTS: + # Keyed on the site, not the hostname: packetstormsecurity.com and + # .org are one server, and keying on the hostname handed it two + # independent rate budgets, doubling the request rate and getting + # us blocked. + out[cve] = (syn, ref, HOSTS[h], HOSTS[h]) + return [(k, *out[k]) for k in sorted(out)] + + +def to_text(raw): + """Advisory pages wrap the exploit in markup; recover the plain text. + + html.unescape rather than a hand-rolled entity table: an earlier ad-hoc + version missed ', which silently truncated every payload containing a + single quote -- the majority of SQL injections. + """ + body = _TAG.sub(" ", raw) + return html.unescape(_ANY_TAG.sub(" ", body)) + + +def fetch_one(item, throttle, retries=2): + cve, syn, url, source, host = item + for attempt in range(retries + 1): + throttle.wait(host) + try: + req = urllib.request.Request(url, headers={"User-Agent": UA}) + with urllib.request.urlopen(req, timeout=TIMEOUT) as r: + raw = r.read(1 << 20).decode("utf-8", "replace") + break + except urllib.error.HTTPError as e: + if e.code in (429, 503) and attempt < retries: + time.sleep(30) + continue + return {"cve_id": cve, "source": source, "url": url, "sha256": None, + "payload": None, "status": f"http_{e.code}"} + except Exception as e: # noqa: BLE001 + if attempt < retries: + time.sleep(5) + continue + return {"cve_id": cve, "source": source, "url": url, "sha256": None, + "payload": None, "status": type(e).__name__} + else: + return {"cve_id": cve, "source": source, "url": url, "sha256": None, + "payload": None, "status": "retries"} + text = to_text(raw) + if _BLOCKED.search(text[:2000]): + return {"cve_id": cve, "source": source, "url": url, "sha256": None, + "payload": None, "status": "blocked"} + digest = hashlib.sha256(raw.encode("utf-8", "replace")).hexdigest() + payload = extract_payload(text, syn) + return {"cve_id": cve, "source": source, "url": url, "sha256": digest, + "payload": payload, "status": "payload" if payload else "no_payload"} + + +def run(args): + con = sqlite3.connect(DB) + con.executescript(DDL) + done = {c for (c,) in con.execute("SELECT cve_id FROM web_payload")} + todo = candidates(con, done) + if args.n: + todo = todo[:args.n] + by_host = {} + for t in todo: + by_host[t[4]] = by_host.get(t[4], 0) + 1 + print(f"{len(done)} already fetched; {len(todo)} to go {by_host}", + file=sys.stderr, flush=True) + if not todo: + return + + throttle = Throttle(args.delay) + batch, t0 = [], time.monotonic() + # Partitioned by host, one thread per partition, results streamed back as + # they finish. Mapping over the combined list instead would let both threads + # draw consecutive same-host items and queue behind the same lock, wasting + # the other host's idle capacity; collecting per-lane lists instead would + # write nothing until the slowest host finished, losing every checkpoint. + lanes = {} + for t in todo: + lanes.setdefault(t[4], []).append(t) + out_q = queue.Queue() + + def drain(items): + strikes = 0 + for it in items: + if strikes >= BLOCK_LIMIT: + out_q.put({"cve_id": it[0], "source": it[3], "url": it[2], + "sha256": None, "payload": None, "status": "skipped_blocked"}) + continue + r = fetch_one(it, throttle) + strikes = strikes + 1 if r["status"] == "blocked" else 0 + if strikes == BLOCK_LIMIT: + print(f" {it[3]}: blocked {BLOCK_LIMIT} times, abandoning this site", + file=sys.stderr, flush=True) + out_q.put(r) + + threads = [threading.Thread(target=drain, args=(items,), daemon=True) + for items in lanes.values()] + for t in threads: + t.start() + + for i in range(1, len(todo) + 1): + batch.append(out_q.get()) + if i % 50 == 0 or i == len(todo): + con.executemany("""INSERT OR REPLACE INTO web_payload + VALUES(:cve_id, :source, :url, :sha256, :payload, :status)""", batch) + con.commit() + batch.clear() + got = con.execute("SELECT COUNT(*) FROM web_payload " + "WHERE payload IS NOT NULL").fetchone()[0] + print(f" {i}/{len(todo)} payloads={got} " + f"{i / max(time.monotonic() - t0, 1):.1f}/s", + file=sys.stderr, flush=True) + for t in threads: + t.join(timeout=5) + + for s, n in con.execute("SELECT status, COUNT(*) FROM web_payload GROUP BY 1 ORDER BY 2 DESC"): + print(f" {s:12} {n}") + con.close() + + +if __name__ == "__main__": + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("-n", type=int, help="fetch only this many, for measurement") + ap.add_argument("--delay", type=float, default=1.0, + help="minimum seconds between requests to the same host") + run(ap.parse_args()) diff --git a/injection-research/pipeline/latex.py b/injection-research/pipeline/latex.py new file mode 100644 index 0000000..bdd18e9 --- /dev/null +++ b/injection-research/pipeline/latex.py @@ -0,0 +1,422 @@ +"""Stage 5: emit every figure the paper quotes as LaTeX the document can \\input. + +The paper must never carry a hand-copied number. This stage writes +doc/generated/, which main.tex pulls in: + + numbers.tex scalar macros, e.g. \\dataInjectionCVEs + tbl-mech.tex containment outcome by syntax (tab:mech) + tbl-payload-corpus.tex VERIFY over the fuzzdb/PaTT/SecLists payloads + tbl-poc-sources.tex PoC linkage per source + tbl-anchors.tex ground-truth CWEs that resolve to an injection label + +Macros end in \\xspace so they can be written inline without a trailing {}. +Counts are formatted 13{,}691 and percentages 82\\%, matching the prose style. +""" +import argparse +import csv +import sqlite3 +from collections import defaultdict +from pathlib import Path + +import export +import matchertext + +ROOT = Path(__file__).resolve().parents[1] +DB = ROOT / "data" / "cve.db" +OUT = ROOT / "doc" / "generated" + +HEADER = ("%% GENERATED by pipeline/latex.py -- do not edit.\n" + "%% Regenerate with: python3 pipeline/latex.py\n") + +# syntax_type -> the label used in the paper's tables +DISPLAY = { + "html_dom": "HTML / DOM (XSS)", "sql": "SQL", "ldap": "LDAP", "nosql": "NoSQL", + "xpath_xquery": "XPath / XQuery", "shell_command": "Shell command", + "code_eval": "Code / eval", "crlf_header": "CRLF / header", + "formula_csv": "Formula (CSV)", "template": "Template", "xml": "XML", + "argument": "Argument", "expression_language": "Expression language", + "unknown": "Unknown", +} + + +def num(n): + return f"{n:,}".replace(",", "{,}") + + +def pct(x, digits=0): + return f"{x * 100:.{digits}f}\\%" + + +def macro(name, value): + return f"\\newcommand{{\\data{name}}}{{{value}\\xspace}}\n" + + +def containment(con): + """Per-syntax inert / rejected / outside over payload-backed CVEs.""" + inert, reject, outside = defaultdict(int), defaultdict(int), defaultdict(int) + semantic = nonmatcher = 0 + for syn, sk, n in con.execute("""SELECT syntax_type, skeleton, COUNT(*) + FROM syntactic_group GROUP BY group_id"""): + ok, mech, _ = matchertext.assess(syn, sk) + if ok: + (inert if mech == "inert" else reject)[syn] += n + else: + outside[syn] += n + # An outside case fails one of the two threat-model conditions: the + # sink executes the value, or the context has no matcher delimiters. + if syn in matchertext.SEMANTIC or syn == "html_dom": + semantic += n + else: + nonmatcher += n + return inert, reject, outside, semantic, nonmatcher + + +def post_stratify(con, inert, reject, outside): + """Reweight the measured containment rate by the corpus syntax mix. + + Payload-backed CVEs are not a random sample of the corpus. SQL is 1.7x + over-represented, because a SQL injection payload is a literal string a + write-up can quote, whereas code-eval and argument payloads are usually + built at run time and never appear verbatim. Payload availability therefore + correlates with syntax, and specifically with matcher-hostable syntax: 85% + of the payload-backed subset is hostable against 80% of the corpus. + + Multiplying the pooled containment rate by the corpus inherits that skew and + overstates the result by roughly five thousand CVEs. Estimating a rate per + syntax and weighting by the corpus counts removes it, which is the standard + post-stratification correction. + + A syntax with no payload-backed CVE has no measured rate and falls back to + the structural rule the model asserts: contained inside HOST, not outside. + + Returns (estimate, [(syntax, corpus_n, backed_n, rate, basis)]). + """ + corpus = dict(con.execute( + "SELECT syntax_type, COUNT(*) FROM classification GROUP BY 1")) + est, rows = 0.0, [] + for syn, n in sorted(corpus.items(), key=lambda kv: -kv[1]): + backed = inert[syn] + reject[syn] + outside[syn] + if backed: + rate, basis = (inert[syn] + reject[syn]) / backed, "measured" + else: + rate, basis = (1.0 if syn in matchertext.HOST else 0.0), "structural" + est += n * rate + rows.append((syn, n, backed, rate, basis)) + return est, rows + + +def tbl_strata(rows, top=8): + lines = ["\\begin{tabular}{lrrr}", "\\toprule", + "Syntax & CVEs & Payload-backed & Contained \\\\", "\\midrule"] + for syn, n, backed, rate, basis in rows[:top]: + mark = "" if basis == "measured" else "$^{\\dagger}$" + lines.append(f"{DISPLAY.get(syn, syn):<19} & {num(n):>9} & {num(backed):>7}{mark} " + f"& {rate * 100:.1f}\\% \\\\") + lines += ["\\bottomrule", "\\end{tabular}"] + return "\n".join(lines) + "\n" + + +def tbl_mech(inert, reject, outside): + hosted = [s for s in DISPLAY if s in matchertext.HOST + and (inert[s] or reject[s] or outside[s])] + other = [s for s in DISPLAY if s not in matchertext.HOST and outside[s]] + lines = ["\\begin{tabular}{lrrr}", "\\toprule", + "Syntax & Inert embed & Rejected & Outside \\\\", "\\midrule"] + for s in sorted(hosted, key=lambda s: -(inert[s] + reject[s] + outside[s])): + lines.append(f"{DISPLAY[s]:<19} & {num(inert[s]):>7} & {num(reject[s]):>3} " + f"& {num(outside[s]):>3} \\\\") + lines.append("\\midrule") + for s in sorted(other, key=lambda s: -outside[s]): + lines.append(f"{DISPLAY[s]:<19} & --- & --- & {num(outside[s]):>3} \\\\") + lines += ["\\midrule", + f"Total & {num(sum(inert.values()))} & {num(sum(reject.values()))} " + f"& {num(sum(outside.values()))} \\\\", + "\\bottomrule", "\\end{tabular}"] + return "\n".join(lines) + "\n" + + +def place(*pairs): + """Lay out (center_column, text) pairs on one line.""" + line = "" + for col, text in pairs: + start = col - len(text) // 2 + line += " " * max(0, start - len(line)) + text + return line + + +def fig_tree(grouped, contained, inert, reject, outside, semantic, nonmatcher): + """The two-decision containment tree. + + Emitted as a complete verbatim block rather than macros, because verbatim + does not expand them; the paper \\input{}s this file inside its figure. + """ + p = lambda a, b: f"({round(100 * a / b) if b else 0}%)" + return "\n".join([ + r"\begin{verbatim}", + place((35, f"{grouped:,} payload-backed CVEs")), + " ┌──────────" + "────┴─────────" + "─────┐", + " yes no", + " matcher-delimitable context? OUTSIDE", + place((20, f"{contained:,} {p(contained, grouped)}"), + (52, f"{outside:,} {p(outside, grouped)}")), + " ┌───────────┴" + "───────────┐ ┌" + "──────────┴───" + "───────┐", + place((8, "pass"), (32, "fail"), (42, str(semantic)), (64, str(nonmatcher))), + " VERIFY(v) VERIFY(v) execution sinks non-matcher delimiters", + " ▼ ▼ templates, eval, shell ; | &", + " INERT EMBED REJECTED javascript: CR/LF, XML <>", + # (A4) tags the execution-sink branch with the threat-model assumption + # it violates (threat.tex). + place((8, f"{inert:,} {p(inert, contained)}"), + (32, f"{reject:,} {p(reject, contained)}"), (44, "(A4)")), + r"\end{verbatim}", + ]) + "\n" + + +def tbl_payload_corpus(con): + lines = ["\\begin{tabular}{lrrrr}", "\\toprule", + "Syntax & Payloads & Inert & Rejected & Outside \\\\", "\\midrule"] + # mechanism is NULL for non-hostable syntaxes, and SUM over all-NULL + # comparisons is NULL rather than 0, so count with an explicit CASE. + for syn, n, i, r, o in con.execute(""" + SELECT syntax_type, COUNT(*), + SUM(CASE WHEN mechanism='inert' THEN 1 ELSE 0 END), + SUM(CASE WHEN mechanism='reject' THEN 1 ELSE 0 END), + SUM(CASE WHEN preventable=0 THEN 1 ELSE 0 END) + FROM payload_assessment GROUP BY 1 ORDER BY 2 DESC"""): + lines.append(f"{DISPLAY.get(syn, syn)} & {num(n)} & {num(i)} & {num(r)} " + f"& {num(o)} \\\\") + lines += ["\\bottomrule", "\\end{tabular}"] + return "\n".join(lines) + "\n" + + +def skeleton_count(con, skeleton): + return con.execute("SELECT COUNT(*) FROM syntactic_group WHERE skeleton=?", + (skeleton,)).fetchone()[0] + + +def tbl_syntax(con, top=6): + lines = ["\\begin{tabular}{lrr}", "\\toprule", + "Injection syntax & CVEs & with PoC \\\\", "\\midrule"] + for syn, n, withpoc in con.execute(""" + SELECT c.syntax_type, COUNT(*), + COUNT(DISTINCT CASE WHEN p.cve_id IS NOT NULL THEN c.cve_id END) + FROM classification c + LEFT JOIN (SELECT DISTINCT cve_id FROM poc) p USING(cve_id) + WHERE c.syntax_type <> 'unknown' + GROUP BY 1 ORDER BY 2 DESC LIMIT ?""", (top,)): + lines.append(f"{DISPLAY.get(syn, syn):<19} & {num(n):>9} & {num(withpoc):>7} \\\\") + lines += ["\\bottomrule", "\\end{tabular}"] + return "\n".join(lines) + "\n" + + +def tbl_poc_sources(con): + lines = ["\\begin{tabular}{lrrr}", "\\toprule", + "Source & PoC rows & CVEs & Injection CVEs \\\\", "\\midrule"] + for src, rows, cves, inj in con.execute(""" + SELECT p.source, COUNT(*), COUNT(DISTINCT p.cve_id), + COUNT(DISTINCT CASE WHEN c.cve_id IS NOT NULL THEN p.cve_id END) + FROM poc p LEFT JOIN classification c USING(cve_id) + GROUP BY 1 ORDER BY 2 DESC"""): + lines.append(f"\\texttt{{{src}}} & {num(rows)} & {num(cves)} & {num(inj)} \\\\") + lines += ["\\bottomrule", "\\end{tabular}"] + return "\n".join(lines) + "\n" + + +def tbl_anchors(rows): + lines = ["\\begin{tabular}{llrll}", "\\toprule", + "Suite & CWE & Cases & Family & Syntax \\\\", "\\midrule"] + for suite, cwe, n, fam, syn in rows: + lines.append(f"\\texttt{{{suite}}} & {cwe} & {num(n)} & " + f"{fam.replace('_', ' ')} & {DISPLAY.get(syn, syn)} \\\\") + lines += ["\\bottomrule", "\\end{tabular}"] + return "\n".join(lines) + "\n" + + +def run(args): + con = sqlite3.connect(DB) + q = lambda sql: con.execute(sql).fetchone()[0] + OUT.mkdir(parents=True, exist_ok=True) + + inert, reject, outside, semantic, nonmatcher = containment(con) + grouped = sum(inert.values()) + sum(reject.values()) + sum(outside.values()) + contained = sum(inert.values()) + sum(reject.values()) + + published = q("SELECT COUNT(*) FROM cve WHERE state='PUBLISHED'") + injection = q("SELECT COUNT(*) FROM classification") + with_poc = q("""SELECT COUNT(DISTINCT cve_id) FROM poc + WHERE cve_id IN (SELECT cve_id FROM classification)""") + + # Projection: the context condition is readable from the syntax label alone, + # so it extends to injection CVEs with no payload. The javascript: rate + # measured on the payload-backed HTML/DOM subset discounts the ceiling. + hosts = "','".join(sorted(matchertext.HOST)) + hostable = q(f"SELECT COUNT(*) FROM classification WHERE syntax_type IN ('{hosts}')") + htmldom = q("SELECT COUNT(*) FROM classification WHERE syntax_type='html_dom'") + hd_backed = inert["html_dom"] + reject["html_dom"] + outside["html_dom"] + js_rate = outside["html_dom"] / hd_backed if hd_backed else 0 + removed = round(htmldom * js_rate) + # Post-stratified rather than the pooled rate applied to the whole corpus. + # The naive form is kept only so the paper can show what the skew costs. + strat, strata = post_stratify(con, inert, reject, outside) + central = round(strat) + naive = contained / grouped * injection + + corpus_n = q("SELECT COUNT(*) FROM payload_assessment") + corpus_inert = q("SELECT COUNT(*) FROM payload_assessment WHERE mechanism='inert'") + corpus_reject = q("SELECT COUNT(*) FROM payload_assessment WHERE mechanism='reject'") + corpus_hostable = corpus_inert + corpus_reject + q( + f"""SELECT COUNT(*) FROM payload_assessment + WHERE preventable=0 AND syntax_type IN ('{hosts}')""") + + anchors = [r for r in con.execute("""SELECT suite, cwe_id, COUNT(*) FROM ground_truth + WHERE cwe_id IS NOT NULL GROUP BY 1,2""")] + from classify import load_hierarchy + from taxonomy import labels_from_cwes + parents, _ = load_hierarchy(con) + resolved = [] + for suite, cwe, n in anchors: + fam, generic, syn = labels_from_cwes([cwe], parents) + if fam and not generic: + resolved.append((suite, cwe, n, fam, syn or "")) + resolved.sort(key=lambda r: (r[0], -r[2])) + + # Naive-Bayes holdout scores, weighted by class support, from the CSV + # classify.py writes. Blank precision/recall mean the class never scored. + nb = list(csv.DictReader(open(ROOT / "data" / "exports" / "nb_holdout.csv"))) + nb_n = sum(int(r["test_n"]) for r in nb) or 1 + wmean = lambda k: sum(float(r[k] or 0) * int(r["test_n"]) for r in nb) / nb_n + per = {r["class"]: r for r in nb} + methods = dict(con.execute("SELECT method, COUNT(*) FROM classification GROUP BY 1")) + n_groups = q("SELECT COUNT(DISTINCT group_id) FROM syntactic_group") + singletons = q("""SELECT COUNT(*) FROM + (SELECT group_id FROM syntactic_group GROUP BY 1 HAVING COUNT(*)=1)""") + # How few containment outcomes the long tail of one-off skeletons reduces to. + singleton_verdicts = len({ + (s, matchertext.assess(s, sk)[1] or "outside") + for s, sk in con.execute("""SELECT syntax_type, skeleton FROM syntactic_group + WHERE group_id IN (SELECT group_id FROM syntactic_group + GROUP BY 1 HAVING COUNT(*)=1)""")}) + + vals = [ + ("PublishedCVEs", num(published)), + ("CVERecords", num(q("SELECT COUNT(*) FROM cve"))), + ("InjectionCVEs", num(injection)), + ("InjectionShare", pct(injection / published)), + ("InjectionSharePrecise", pct(injection / published, 1)), + ("InjectionCWEs", num(q("""SELECT COUNT(DISTINCT cwe_id) FROM cwe_assignment + WHERE cve_id IN (SELECT cve_id FROM classification)"""))), + ("InjectionKev", num(q("SELECT COUNT(*) FROM classification JOIN kev USING(cve_id)"))), + # labeling layers + ("MethodCwe", num(methods.get("cwe", 0))), + ("MethodCweShare", pct(methods.get("cwe", 0) / injection)), + ("MethodRule", num(methods.get("rule", 0))), + ("MethodNb", num(methods.get("nb", 0))), + ("MethodNbShare", pct(methods.get("nb", 0) / injection, 1)), + ("MethodUnknown", num(methods.get("unknown", 0))), + ("NbTestDocs", num(nb_n)), + ("NbPrecision", f"{wmean('precision'):.3f}"), + ("NbRecall", f"{wmean('recall'):.3f}"), + ("NbCoverage", pct(float(nb[0]["coverage"]) if nb else 0)), + ("NbPrecisionHtmlDom", f"{float(per['html_dom']['precision']):.2f}"), + ("NbRecallHtmlDom", f"{float(per['html_dom']['recall']):.2f}"), + ("NbPrecisionSql", f"{float(per['sql']['precision']):.2f}"), + ("NbRecallSql", f"{float(per['sql']['recall']):.2f}"), + ("NbPrecisionCodeEval", f"{float(per['code_eval']['precision']):.2f}"), + ("NbRecallCodeEval", f"{float(per['code_eval']['recall']):.2f}"), + ("MethodDeterministicShare", + pct((methods.get("cwe", 0) + methods.get("rule", 0)) / injection, 1)), + ("AuditPerMethod", num(export.AUDIT_PER_METHOD)), + ("InjectionWithPoc", num(with_poc)), + ("InjectionWithPocShare", pct(with_poc / injection)), + ("PocRows", num(q("SELECT COUNT(*) FROM poc"))), + # per-source PoC reach over the whole corpus, for \cref{sec:data} + *[(f"Poc{s.title().replace('-', '')}CVEs", num(n)) for s, n in con.execute( + "SELECT source, COUNT(DISTINCT cve_id) FROM poc GROUP BY 1 ORDER BY 2 DESC")], + ("KevRows", num(q("SELECT COUNT(*) FROM kev"))), + ("VedasScored", num(q("""SELECT COUNT(*) FROM cve v JOIN exploit_score USING(cve_id) + WHERE v.state='PUBLISHED'"""))), + # payload-backed containment + ("PayloadBackedCVEs", num(grouped)), + ("DistinctSkeletons", num(q("SELECT COUNT(DISTINCT group_id) FROM syntactic_group"))), + ("SingletonGroups", num(singletons)), + ("SingletonGroupShare", pct(singletons / n_groups)), + ("SingletonCVEShare", pct(singletons / grouped)), + ("SingletonVerdicts", num(singleton_verdicts)), + # The two dominant syntaxes, quoted in results.tex as a share. + ("TopTwoShare", pct(q("""SELECT COUNT(*) FROM classification + WHERE syntax_type IN ('html_dom','sql')""") / injection)), + # Counts for the three largest groups the text names, looked up by their + # exact skeleton so a changed skeleton shows up as 0 rather than silently + # keeping a stale number. + *[(f"Group{k}", num(skeleton_count(con, sk))) for k, sk in ( + ("AlertDocId", "< TAG > ALERT ( DOCUMENT . ) "), + ("AlertCookie", "< TAG > ALERT ( DOCUMENT . COOKIE ) "), + ("PhpOpen", "< ? "))], + # orthogonal subclass facets, keyed by (dimension, label) + *[(f"Sub{d.title().replace('_', '')}{l.title().replace('_', '')}", num(n)) + for d, l, n in con.execute("""SELECT dimension, label, COUNT(*) FROM subclass + WHERE dimension IN ('privilege','technique') + GROUP BY 1,2""")], + ("Contained", num(contained)), + ("ContainedShare", pct(contained / grouped)), + # The floor on the same denominator as the ceiling. ContainedShare is a + # share of the payload-backed subset, so quoting it beside HostableShare + # compares two different populations and makes the floor look larger than + # the ceiling. This counts every CVE without a recoverable payload as + # uncontained, which makes it a hard lower bound rather than an estimate. + ("FloorShare", pct(contained / injection, 1)), + ("InertCVEs", num(sum(inert.values()))), + ("RejectedCVEs", num(sum(reject.values()))), + ("OutsideCVEs", num(sum(outside.values()))), + ("OutsideSemantic", num(semantic)), + ("OutsideNonmatcher", num(nonmatcher)), + ("SqlRejected", num(reject["sql"])), + ("LdapInert", num(inert["ldap"])), + ("LdapRejected", num(reject["ldap"])), + # projection onto the full corpus + ("HostableCVEs", num(hostable)), + ("HostableShare", pct(hostable / injection)), + ("HtmlDomCVEs", num(htmldom)), + ("HtmlDomBacked", num(hd_backed)), + ("HtmlDomJsSinks", num(outside["html_dom"])), + ("JsSinkRate", pct(js_rate, 1)), + ("JsSinkRemoved", num(removed)), + ("CentralEstimate", num(central)), + ("NaiveEstimate", num(round(naive))), + ("NaiveShare", pct(naive / injection)), + ("SkewCost", num(round(naive) - central)), + ("CentralShare", pct(central / injection)), + # payload corpora (fuzzdb / PayloadsAllTheThings / SecLists) + ("CorpusPayloads", num(corpus_n)), + ("CorpusHostable", num(corpus_hostable)), + ("CorpusInert", num(corpus_inert)), + ("CorpusRejected", num(corpus_reject)), + ("CorpusInertShare", pct(corpus_inert / (corpus_inert + corpus_reject), 1)), + ("CorpusRejectedShare", pct(corpus_reject / (corpus_inert + corpus_reject), 1)), + # labeled ground truth + ("GroundTruthCases", num(q("SELECT COUNT(*) FROM ground_truth"))), + ("GroundTruthPairs", num(len(anchors))), + ("GroundTruthResolved", num(len(resolved))), + ] + (OUT / "numbers.tex").write_text( + HEADER + "".join(macro(k, v) for k, v in vals)) + (OUT / "tbl-mech.tex").write_text(HEADER + tbl_mech(inert, reject, outside)) + (OUT / "fig-tree.tex").write_text(HEADER + fig_tree( + grouped, contained, sum(inert.values()), sum(reject.values()), + sum(outside.values()), semantic, nonmatcher)) + (OUT / "tbl-syntax.tex").write_text(HEADER + tbl_syntax(con)) + (OUT / "tbl-strata.tex").write_text(HEADER + tbl_strata(strata)) + (OUT / "tbl-payload-corpus.tex").write_text(HEADER + tbl_payload_corpus(con)) + (OUT / "tbl-poc-sources.tex").write_text(HEADER + tbl_poc_sources(con)) + (OUT / "tbl-anchors.tex").write_text(HEADER + tbl_anchors(resolved)) + print(f"wrote {len(vals)} macros and 6 tables to {OUT.relative_to(ROOT)}") + con.close() + + +if __name__ == "__main__": + run(argparse.ArgumentParser(description=__doc__).parse_args()) diff --git a/injection-research/pipeline/report.py b/injection-research/pipeline/report.py index e795765..eb57c33 100644 --- a/injection-research/pipeline/report.py +++ b/injection-research/pipeline/report.py @@ -24,16 +24,38 @@ # Per-syntax payload signatures, ordered most-specific first. Applied to the # text of a linked exploit file to pull out the actual injection string. _SIGNS = { - "sql": [r"UNION(?:\s+ALL)?\s+SELECT\b[^\n]*", r"'\s*(?:OR|AND)\s*'?\d+'?\s*=\s*'?\d+[^\n]*", - r"'\s*(?:OR|AND)\b[^\n]*--", r"\bAND\s+\d+=\d+[^\n]*", r"';?\s*WAITFOR\s+DELAY[^\n]*", - r"\bextractvalue\s*\([^\n]*", r"\bSLEEP\s*\(\d+\)[^\n]*", r"\[sql\]"], - "html_dom": [r"]*>.*?", r"]*onerror\s*=[^\n]*?>", - r"]*on\w+\s*=[^\n]*?>", r'"> tag is not a payload. In curated exploit files that was + # harmless, but a linked repo is often the vulnerable application itself, + # whose own source is full of benign script tags and jQuery includes. Require + # the body to actually do something an attack does. + "html_dom": [r"]*>[^<]{0,150}?(?:alert|prompt|confirm|eval" + r"|document\s*\.\s*(?:cookie|domain|location|write))\s*[({][^<]{0,120}?", + r"]*onerror\s*=[^\n]*?>", + r"]*on\w+\s*=[^\n]*?>", + # Both of these fired on ordinary page source: `">\n]*" +# \b is wrong here: after a percent-escape the preceding character is a digit +# (the `0` of %20), so \bunion never fires on %20UNION. Guard on letters only. +_W = r"(? %27 -> ') is common in the + corpus; `+` is a query-string space, and an emptied SQL comment (/**/) is a + whitespace substitute used to evade naive filters. + """ + for _ in range(rounds): + decoded = _PCT.sub(lambda m: chr(int(m.group(1), 16)), frag) + if decoded == frag: + break + frag = decoded + return re.sub(r"/\*\*?/", " ", frag).replace("+", " ") + + +_PAIR = {")": "(", "]": "[", "}": "{"} + + +def is_truncated(frag): + """Did the signature cut the payload mid-expression? + + A breakout emits an unmatched *closer*: closing the slot early is the whole + manoeuvre, so `'r0t')` is a real payload. An unmatched *opener* left + at the tail is the regex stopping inside a function call instead, as in + `ASCII(SUBSTRING(passwd,`. Keeping those would count a regex artifact as a + VERIFY rejection -- they accounted for 37% of all rejections before this + check -- so treat them as failed extractions rather than payloads. + """ + stack = [] + for ch in frag: + if ch in "([{": + stack.append(ch) + elif ch in _PAIR and stack and stack[-1] == _PAIR[ch]: + stack.pop() + return bool(stack) + + +# Markdown prose yields false positives that exploit files did not: a README +# writes `deviceList` as an inline code span, which the shell backtick signature +# reads as a command substitution. Require something command-like inside. +_MD_SPAN = re.compile(r"^`[\w.@/ ()\[\]-]*`$") +_JS_STUB = re.compile(r"^javascript:.{0,4}$", re.I) +# `&id=62` is a URL parameter named id, not the id command. +_URL_PARAM = re.compile(r"^[&;|]\w+=") + + +def _accept(frag, truncation_check=True): + return (3 <= len(frag) <= 200 + and not is_placeholder(frag) + and not (truncation_check and is_truncated(frag)) + and not _MD_SPAN.match(frag) + and not _JS_STUB.match(frag) + and not _URL_PARAM.match(frag)) + + +def extend_balance(text, end, frag, limit=8): + """Reclaim closers a regex could not count. + + A pattern cannot match nested parentheses, so `eval(base64_decode($x))` is + captured one `)` short and the truncation guard would throw it away. If the + characters immediately following the match are closing matchers, they belong + to the payload: append them until it balances. + """ + while is_truncated(frag) and limit and end < len(text) and text[end] in ")]}": + frag += text[end] + end += 1 + limit -= 1 + return frag + + +# Exploit-DB write-ups and sqlmap transcripts often label the payload outright. +# The label is a locator the per-syntax signatures cannot supply: it marks a +# string as the attack even when that string uses a command or sink the +# signatures do not enumerate, as in `...¤tTSREmailTo=|date>/tmp/x`. +_LABELLED = [ + re.compile(r"^[ \t]*#?[ \t]*Payload[ \t]*:[ \t]*(\S.{4,180})$", re.I | re.M), + re.compile(r"^[ \t]*#?[ \t]*(?:PoC|Proof of Concept)[ \t]*:[ \t]*(\S.{4,180})$", re.I | re.M), + re.compile(r"^[ \t]*(?:GET|POST)[ \t]+(\S{8,180})[ \t]+HTTP", re.M), +] +# Trusting a label still needs the value to look like an attack rather than a +# bare path or a separator line: it must carry a delimiter, metacharacter or +# escape, and it must not be only structure. +_ATTACKISH = re.compile(r"""['"<>;|`]|\$\(|%[0-9A-Fa-f]{2}|&&|\|\||[(){}\[\]]""") +_ONLY_PUNCT = re.compile(r"^[\W_]+$") + + +def extract_labelled(text, syn): + for rx in _LABELLED: + for m in rx.finditer(text): + raw = " ".join(m.group(1).split()) + # The whole labelled value is preferred over a signature match inside + # it: a signature would capture some suffix such as `SLEEP(5)))vltp)`, + # whose stray closers make a balanced payload look like a rejection. + # is_truncated is skipped here for the same reason it exists -- it + # detects a regex stopping mid-expression, and a labelled line is a + # delimited whole, so a trailing `{` in `'};alert(1);{'` is the real + # payload rather than a cut. + if (_accept(raw, truncation_check=False) and _ATTACKISH.search(raw) + and not _ONLY_PUNCT.match(raw) and "=" in raw): + return raw + inner = extract_payload(raw, syn, labelled=False) + if inner: + return inner + return None + + +def extract_payload(text, syn, labelled=True): for rx in SIGNS.get(syn, ()): m = rx.search(text) if m: - frag = " ".join(m.group(0).split()) - if 3 <= len(frag) <= 200 and not is_placeholder(frag): + frag = " ".join(extend_balance(text, m.end(), m.group(0)).split()) + if _accept(frag): return frag - return None + # Literal forms first, so an unencoded payload is never routed through the + # decoder; only fall back to the URL forms when nothing else matched. + for rx in URL_SIGNS.get(syn, ()): + m = rx.search(text) + if m: + frag = " ".join(urlform_decode(m.group(0)).split()) + if _accept(frag): + return frag + return extract_labelled(text, syn) if labelled else None def sample_payloads(con, syn, n, rng): + # Seeding rng only makes the sample reproducible if the list it shuffles has + # a fixed order to begin with, hence the ORDER BY. links = con.execute( """SELECT DISTINCT c.cve_id, p.source, p.local_path FROM poc p JOIN classification c USING(cve_id) - WHERE c.syntax_type=? AND p.local_path IS NOT NULL""", (syn,)).fetchall() + WHERE c.syntax_type=? AND p.local_path IS NOT NULL + ORDER BY c.cve_id, p.source, p.local_path""", (syn,)).fetchall() rng.shuffle(links) out, seen = [], set() for cve_id, source, rel in links: diff --git a/injection-research/pipeline/run_all.py b/injection-research/pipeline/run_all.py index aeb4b73..b20dbb2 100644 --- a/injection-research/pipeline/run_all.py +++ b/injection-research/pipeline/run_all.py @@ -11,8 +11,10 @@ import classify import export import fetch +import latex import subclass import syntactic_group +import validate def main(): @@ -29,7 +31,9 @@ def main(): classify.run(args) subclass.run(args) syntactic_group.run(args) + validate.run(args) export.run(args) + latex.run(args) if __name__ == "__main__": diff --git a/injection-research/pipeline/subclass.py b/injection-research/pipeline/subclass.py index 2e00837..48d4457 100644 --- a/injection-research/pipeline/subclass.py +++ b/injection-research/pipeline/subclass.py @@ -160,10 +160,26 @@ def run(args): desc_of = dict(con.execute("""SELECT cve_id, COALESCE(description, '') FROM cve WHERE cve_id IN (SELECT cve_id FROM classification)""")) poc_paths = defaultdict(list) - for cid, lp in con.execute("SELECT cve_id, local_path FROM poc WHERE local_path IS NOT NULL"): + # Ordered so the representative payload per CVE is a property of the data, + # not of physical row order: without it, ingesting a new PoC source silently + # reshuffles which file each CVE's payload is extracted from. + for cid, lp in con.execute("""SELECT cve_id, local_path FROM poc + WHERE local_path IS NOT NULL + ORDER BY cve_id, source, ref"""): if cid in syn_of: poc_paths[cid].append(lp) vectors = best_vectors(con) + # Same fallback as syntactic_group: local file first, then a payload + # recovered from a linked GitHub repo. + def _table(name): + return con.execute("""SELECT COUNT(*) FROM sqlite_master + WHERE type='table' AND name=?""", (name,)).fetchone()[0] + remote = dict(con.execute( + "SELECT cve_id, payload FROM remote_payload WHERE payload IS NOT NULL") + if _table("remote_payload") else ()) + web = dict(con.execute( + "SELECT cve_id, payload FROM web_payload WHERE payload IS NOT NULL") + if _table("web_payload") else ()) rows = [] for cid, syn in syn_of.items(): @@ -176,6 +192,7 @@ def run(args): payload = None if payload: break + payload = payload or remote.get(cid) or web.get(cid) blob = f"{payload or ''} {desc}" for dim, label in cvss_facets(vectors.get(cid, "")).items(): diff --git a/injection-research/pipeline/syntactic_group.py b/injection-research/pipeline/syntactic_group.py index bf1fa59..f27cbfc 100644 --- a/injection-research/pipeline/syntactic_group.py +++ b/injection-research/pipeline/syntactic_group.py @@ -86,18 +86,37 @@ def skeleton(payload): def representative_payload(con): syn_of = dict(con.execute("SELECT cve_id, syntax_type FROM classification")) paths = defaultdict(list) - for cid, lp in con.execute("SELECT cve_id, local_path FROM poc WHERE local_path IS NOT NULL"): + # See subclass.py: ordered so payload selection is stable across ingestions. + for cid, lp in con.execute("""SELECT cve_id, local_path FROM poc + WHERE local_path IS NOT NULL + ORDER BY cve_id, source, ref"""): if cid in syn_of: paths[cid].append(lp) + # Payloads recovered from linked GitHub repos, which have no local file. + # Local files win: they are pinned in the corpus snapshot, whereas a remote + # payload depends on a repo that may since have vanished. + def _table(name): + return con.execute("""SELECT COUNT(*) FROM sqlite_master + WHERE type='table' AND name=?""", (name,)).fetchone()[0] + remote = dict(con.execute( + "SELECT cve_id, payload FROM remote_payload WHERE payload IS NOT NULL") + if _table("remote_payload") else ()) + # Advisory pages are the last resort: unlike a pinned commit they can be + # edited in place, so they are only consulted when nothing else has one. + web = dict(con.execute( + "SELECT cve_id, payload FROM web_payload WHERE payload IS NOT NULL") + if _table("web_payload") else ()) for cid, syn in syn_of.items(): + found = None for lp in paths.get(cid, ()): try: - p = extract_payload((RAW / lp).read_text(encoding="utf-8", errors="replace"), syn) + found = extract_payload((RAW / lp).read_text(encoding="utf-8", errors="replace"), syn) except OSError: - p = None - if p: - yield cid, syn, p + found = None + if found: break + if found or (found := remote.get(cid)) or (found := web.get(cid)): + yield cid, syn, found def run(args): diff --git a/injection-research/pipeline/validate.py b/injection-research/pipeline/validate.py new file mode 100644 index 0000000..50fb59d --- /dev/null +++ b/injection-research/pipeline/validate.py @@ -0,0 +1,103 @@ +"""Stage 3d: measure matchertext prevention on the payload corpora and check the +CWE taxonomy against labeled ground truth. + +Two things the CVE record alone cannot supply: + + 1. Prevention rate. The CVE-derived measurement covers only the CVEs with an + extractable PoC payload, a few thousand records. fuzzdb, PayloadsAllTheThings + and SecLists supply attack strings directly, per sink type, so every payload + in a matcher-hostable syntax can be run through VERIFY (matchertext.assess) + instead of only those a PoC file happened to expose. + + 2. Anchor coverage. OWASP Benchmark and the SARD Juliet suites label cases with + a CWE and, for Benchmark, a verdict. Resolving those CWEs through the same + FAMILY_ANCHORS/SYNTAX_ANCHORS walk used on real CVEs shows whether the + taxonomy resolves the weakness classes that a purpose-built injection suite + considers in scope, independently of how CNAs happen to assign CWEs. + +Both are corpus-level measurements; neither modifies the CVE classification. +""" +import argparse +import csv +import sqlite3 +from collections import Counter, defaultdict +from pathlib import Path + +import matchertext +from classify import load_hierarchy +from syntactic_group import skeleton +from taxonomy import labels_from_cwes + +ROOT = Path(__file__).resolve().parents[1] +DB = ROOT / "data" / "cve.db" +EXPORTS = ROOT / "data" / "exports" + + +def assess_payloads(con): + """Run VERIFY over every corpus payload; store one verdict per payload.""" + rows, tally = [], defaultdict(Counter) + for corpus, syn, payload in con.execute( + "SELECT corpus, syntax_type, payload FROM payload"): + sk = skeleton(payload) + preventable, mech, _ = matchertext.assess(syn, sk) + rows.append((corpus, syn, payload, sk, int(preventable), mech or None)) + tally[syn][mech if preventable else "not_applicable"] += 1 + con.executescript(""" + DROP TABLE IF EXISTS payload_assessment; + CREATE TABLE payload_assessment(corpus TEXT, syntax_type TEXT, payload TEXT, + skeleton TEXT, preventable INTEGER, mechanism TEXT); + """) + con.executemany("INSERT INTO payload_assessment VALUES(?,?,?,?,?,?)", rows) + con.execute("CREATE INDEX idx_pa_syn ON payload_assessment(syntax_type)") + con.commit() + return len(rows), tally + + +def check_ground_truth(con): + """Resolve each labeled suite CWE through the taxonomy anchors.""" + parents, _ = load_hierarchy(con) + rows = [] + for suite, cwe, n in con.execute( + """SELECT suite, cwe_id, COUNT(*) FROM ground_truth + WHERE cwe_id IS NOT NULL GROUP BY suite, cwe_id"""): + fam, generic, syn = labels_from_cwes([cwe], parents) + rows.append((suite, cwe, n, fam or "", int(bool(generic)), syn or "")) + return rows + + +def run(args): + con = sqlite3.connect(DB) + EXPORTS.mkdir(parents=True, exist_ok=True) + + total, tally = assess_payloads(con) + with open(EXPORTS / "payload_prevention.csv", "w", newline="") as f: + w = csv.writer(f) + w.writerow(["syntax_type", "payloads", "inert", "reject", + "not_applicable", "prevention_rate"]) + for syn in sorted(tally): + c = tally[syn] + n = sum(c.values()) + prevented = c["inert"] + c["reject"] + w.writerow([syn, n, c["inert"], c["reject"], c["not_applicable"], + round(prevented / n, 4) if n else ""]) + + gt = check_ground_truth(con) + with open(EXPORTS / "ground_truth_anchors.csv", "w", newline="") as f: + w = csv.writer(f) + w.writerow(["suite", "cwe_id", "cases", "family", "family_generic", "syntax"]) + w.writerows(sorted(gt, key=lambda r: (r[0], -r[2]))) + + hosted = {s: sum(c.values()) for s, c in tally.items() if s in matchertext.HOST} + prevented = sum(tally[s]["inert"] + tally[s]["reject"] for s in hosted) + n_hosted = sum(hosted.values()) + print(f"payloads assessed: {total}; matcher-hostable syntaxes: {n_hosted}; " + f"prevented: {prevented}" + + (f" ({prevented / n_hosted:.1%})" if n_hosted else "")) + resolved = sum(1 for r in gt if r[3] and not r[4]) + print(f"ground truth: {len(gt)} (suite, cwe) pairs, " + f"{resolved} resolve to a specific family") + con.close() + + +if __name__ == "__main__": + run(argparse.ArgumentParser(description=__doc__).parse_args()) diff --git a/doc/proof.lean b/lean/always_embeddable.lean similarity index 81% rename from doc/proof.lean rename to lean/always_embeddable.lean index c882670..0f65e01 100644 --- a/doc/proof.lean +++ b/lean/always_embeddable.lean @@ -1,31 +1,7 @@ -import Mathlib +import core -/- Premises given in the paper -/ - -variable {α : Type*} -- the alphabet Σ, kept abstract on purpose -variable (Pi : Set (α × α)) -- the set of pairs Π - --- -def Opener (x : α) : Prop := ∃ y, (x, y) ∈ Pi -def Closer (x : α) : Prop := ∃ y, (y, x) ∈ Pi -def Matcher (x : α) : Prop := Opener Pi x ∨ Closer Pi x -def Nonmatcher (x : α) : Prop := ¬ Matcher Pi x - --- Prove: no opener can be a closer, and vice versa -theorem disjoint - (h : ∀ x y z, (x, y) ∈ Pi → (z, x) ∈ Pi → False) - (x : α) : ¬ (Opener Pi x ∧ Closer Pi x) := by - intro hx - rcases hx with ⟨ho, hc⟩ - rcases ho with ⟨y, hy⟩ - rcases hc with ⟨z, hz⟩ - exact h x y z hy hz - --- The inductive definition of Matchertext -inductive MT (Pi : Set (α × α)) : List α → Prop where - | flat (n : List α) (h : ∀ x ∈ n, Nonmatcher Pi x) : MT Pi n - | nest (m₁ m₂ m₃ : List α) (o c : α) (hp : (o, c) ∈ Pi) (h₁ : MT Pi m₁) (h₂ : MT Pi m₂) (h₃ : MT Pi m₃) : - MT Pi (m₁ ++ [o] ++ m₂ ++ [c] ++ m₃) +variable {α : Type*} +variable (Pi : Set (α × α)) /- Main Proof -/ diff --git a/lean/core.lean b/lean/core.lean new file mode 100644 index 0000000..6648023 --- /dev/null +++ b/lean/core.lean @@ -0,0 +1,25 @@ +import Mathlib + +variable {α : Type*} -- the alphabet Σ, kept abstract +variable (Pi : Set (α × α)) -- the set of pairs Π + +def Opener (x : α) : Prop := ∃ y, (x, y) ∈ Pi +def Closer (x : α) : Prop := ∃ y, (y, x) ∈ Pi +def Matcher (x : α) : Prop := Opener Pi x ∨ Closer Pi x +def Nonmatcher (x : α) : Prop := ¬ Matcher Pi x + +-- Lemma: no opener can be a closer, and vice versa. +theorem disjoint + (h : ∀ x y z, (x, y) ∈ Pi → (z, x) ∈ Pi → False) + (x : α) : ¬ (Opener Pi x ∧ Closer Pi x) := by + intro hx + rcases hx with ⟨ho, hc⟩ + rcases ho with ⟨y, hy⟩ + rcases hc with ⟨z, hz⟩ + exact h x y z hy hz + +-- The inductive definition of matchertext. +inductive MT (Pi : Set (α × α)) : List α → Prop where + | flat (n : List α) (h : ∀ x ∈ n, Nonmatcher Pi x) : MT Pi n + | nest (m₁ m₂ m₃ : List α) (o c : α) (hp : (o, c) ∈ Pi) (h₁ : MT Pi m₁) (h₂ : MT Pi m₂) (h₃ : MT Pi m₃) : + MT Pi (m₁ ++ [o] ++ m₂ ++ [c] ++ m₃) diff --git a/injection-research/doc/proof.lean b/lean/embed_boundary.lean similarity index 69% rename from injection-research/doc/proof.lean rename to lean/embed_boundary.lean index 09fd22e..3094f36 100644 --- a/injection-research/doc/proof.lean +++ b/lean/embed_boundary.lean @@ -1,52 +1,22 @@ -import Mathlib - -/- Premises given in the paper -/ - -variable {α : Type*} -- the alphabet Σ, kept abstract on purpose -variable (Pi : Set (α × α)) -- the set of pairs Π - --- -def Opener (x : α) : Prop := ∃ y, (x, y) ∈ Pi -def Closer (x : α) : Prop := ∃ y, (y, x) ∈ Pi -def Matcher (x : α) : Prop := Opener Pi x ∨ Closer Pi x -def Nonmatcher (x : α) : Prop := ¬ Matcher Pi x - --- Prove: no opener can be a closer, and vice versa -theorem disjoint - (h : ∀ x y z, (x, y) ∈ Pi → (z, x) ∈ Pi → False) - (x : α) : ¬ (Opener Pi x ∧ Closer Pi x) := by - intro hx - rcases hx with ⟨ho, hc⟩ - rcases ho with ⟨y, hy⟩ - rcases hc with ⟨z, hz⟩ - exact h x y z hy hz - --- The inductive definition of Matchertext -inductive MT (Pi : Set (α × α)) : List α → Prop where - | flat (n : List α) (h : ∀ x ∈ n, Nonmatcher Pi x) : MT Pi n - | nest (m₁ m₂ m₃ : List α) (o c : α) (hp : (o, c) ∈ Pi) (h₁ : MT Pi m₁) (h₂ : MT Pi m₂) (h₃ : MT Pi m₃) : - MT Pi (m₁ ++ [o] ++ m₂ ++ [c] ++ m₃) - --- ============================================================================ --- L1: reading a matched-delimited region "to matcher balance" recovers a --- well-defined region that is itself matchertext. Stated declaratively over the --- language `MT`. --- ============================================================================ +import core + +variable {α : Type*} +variable (Pi : Set (α × α)) open Classical -/-- Net matcher depth: +1 per opener, -1 per closer, 0 per nonmatcher. - `noncomputable` since only a host implementation would need a computable version. -/ +-- Net matcher depth: +1 per opener, -1 per closer, 0 per nonmatcher. Noncomputable since only +-- a host implementation would need a computable version. noncomputable def delta (x : α) : Int := if Opener Pi x then 1 else if Closer Pi x then -1 else 0 noncomputable def depth (l : List α) : Int := (l.map (delta Pi)).sum -- Lemma: depth is additive over concatenation. theorem depth_append (a b : List α) : depth Pi (a ++ b) = depth Pi a + depth Pi b := by simp [depth] --- Lemma: a single character's contribution to the depth. +-- Lemma: one character's contribution. theorem depth_singleton (x : α) : depth Pi [x] = (if Opener Pi x then 1 else if Closer Pi x then -1 else 0) := by simp [depth, delta] --- Lemma: a matchertext string has net depth zero. +-- Lemma (balanced): a matchertext string has net depth 0, since it is well balanced. theorem depth_zero (hdisj : ∀ x y z, (x, y) ∈ Pi → (z, x) ∈ Pi → False) {m : List α} (hm : MT Pi m) : depth Pi m = 0 := by @@ -79,8 +49,8 @@ theorem depth_zero simp only [depth_append, ih₁, ih₂, ih₃, hdo, hdc] omega --- Lemma (floor): no prefix of a matchertext string dips below depth zero, so a reader tracking matcher balance --- never underflows inside the embedded value. +-- Lemma (floor, the crux): no prefix of a matchertext string dips below depth 0, so +-- a reader tracking matcher balance never underflows inside the embedding. theorem depth_prefix_nonneg (hdisj : ∀ x y z, (x, y) ∈ Pi → (z, x) ∈ Pi → False) {m : List α} (hm : MT Pi m) : ∀ p, p <+: m → 0 ≤ depth Pi p := by @@ -149,12 +119,11 @@ theorem depth_prefix_nonneg have := ih₃ p₄ hpre linarith -/-- **L1** Placing a matchertext value `m` in a - matched pair `(o, c)` and reading to balance recovers exactly `m`: every prefix - of `m` stays at depth ≥ 0, `m` returns to 0, and the context-closer `c` is the - first character to drive the depth negative — so the balance boundary is - precisely `|m|`. It follows from the three lemmas above, showing the boundary - result is a corollary, not new machinery. -/ +-- Theorem (L1): placing a matchertext value m in a hole closed by c and reading to +-- balance recovers exactly m: every prefix of m stays at depth ≥ 0, m itself returns +-- to 0, and c is the first character to drive the depth negative, so the balance +-- boundary is precisely |m|. It follows from the three lemmas above: the boundary +-- result is a corollary, not new machinery. theorem embed_boundary (hdisj : ∀ x y z, (x, y) ∈ Pi → (z, x) ∈ Pi → False) {m : List α} (hm : MT Pi m) {c : α} (hc : Closer Pi c) : diff --git a/lean/lake-manifest.json b/lean/lake-manifest.json new file mode 100644 index 0000000..8bfe5e1 --- /dev/null +++ b/lean/lake-manifest.json @@ -0,0 +1,96 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f424bc890c23f9fbe219c109f7f7304721f21e6f", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "57d3325be72a842920813bcb40f96a6f7393c185", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "d60e6444e6fd881dfa077ff36e96de75753afa28", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0-rc1", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "matchertext", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean/lakefile.toml b/lean/lakefile.toml new file mode 100644 index 0000000..52ab0d8 --- /dev/null +++ b/lean/lakefile.toml @@ -0,0 +1,14 @@ +name = "matchertext" +defaultTargets = ["Matchertext"] + +# Mathlib is pinned in lake-manifest.json; `lean-toolchain` must match the Lean +# version that revision uses. To build from a fresh clone (needs elan and network): +# lake exe cache get && lake build +[[require]] +name = "mathlib" +scope = "leanprover-community" +version = "git#master" + +[[lean_lib]] +name = "Matchertext" +globs = ["Core", "always_embeddable", "embed_boundary", "to_matchertext"] diff --git a/lean/lean-toolchain b/lean/lean-toolchain new file mode 100644 index 0000000..fd85b26 --- /dev/null +++ b/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.0-rc1 diff --git a/lean/to_matchertext.lean b/lean/to_matchertext.lean new file mode 100644 index 0000000..085614d --- /dev/null +++ b/lean/to_matchertext.lean @@ -0,0 +1,130 @@ +import core +import embed_boundary +import always_embeddable + +variable {α : Type*} +variable (Pi : Set (α × α)) + +open Classical + +-- A pending scan context: an opener awaiting its closer, with the output at its level. +abbrev Ctx (α : Type*) := α × List α + +-- End of input: every opener still pending is unmatched, so it is escaped. +noncomputable def unwind (esc : α → List α) : List (Ctx α) → List α → List α + | [], out => out + | (o, b) :: st, out => unwind esc st (b ++ esc o ++ out) + +-- One left-to-right pass. `st` holds the pending openers, `out` the output at the current +-- level. A closer is matched only if it pairs with the top; else it is unmatched and escaped. +noncomputable def encAux (esc : α → List α) : + List (Ctx α) → List α → List α → List α + | st, out, [] => unwind esc st out + | st, out, x :: xs => + if Opener Pi x then encAux esc ((x, out) :: st) [] xs + else if Closer Pi x then + match st with + | (o, b) :: st' => + if (o, x) ∈ Pi then encAux esc st' (b ++ [o] ++ out ++ [x]) xs + else encAux esc st (out ++ esc x) xs + | [] => encAux esc st (out ++ esc x) xs + else encAux esc st (out ++ [x]) xs + +noncomputable def toMatchertext (esc : α → List α) (v : List α) : List α := + encAux Pi esc [] [] v + +-- Lemma: an escape contains no matchers, hence is matchertext. +theorem esc_mt (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) (c : α) : + MT Pi (esc c) := + MT.flat _ (fun x hx => hesc c x hx) + +-- Lemma: unwinding the pending stack preserves matchertext. +theorem unwind_mt (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) + (st : List (Ctx α)) (hst : ∀ p ∈ st, MT Pi p.2) + (out : List α) (hout : MT Pi out) : + MT Pi (unwind esc st out) := by + induction st generalizing out with + | nil => simpa [unwind] using hout + | cons hd st' ih => + obtain ⟨o, b⟩ := hd + have hb : MT Pi b := hst (o, b) (by simp) + have htail : ∀ p ∈ st', MT Pi p.2 := fun p hp => hst p (List.mem_cons_of_mem _ hp) + simp only [unwind] + apply ih + · exact htail + · exact mt_append Pi (mt_append Pi hb (esc_mt Pi esc hesc o)) hout + +-- Invariant (the crux): every accumulated segment stays matchertext. +theorem encAux_mt (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) + (st : List (Ctx α)) (hst : ∀ p ∈ st, MT Pi p.2) + (out : List α) (hout : MT Pi out) + (v : List α) : + MT Pi (encAux Pi esc st out v) := by + induction v generalizing st out with + | nil => + rw [encAux] + exact unwind_mt Pi esc hesc st hst out hout + | cons x xs ih => + simp only [encAux] + by_cases hox : Opener Pi x + · -- opener: push `(x, out)`, start a fresh accumulator + rw [if_pos hox] + apply ih + · intro p hp + rcases List.mem_cons.mp hp with rfl | hmem + · exact hout + · exact hst p hmem + · exact mt_nil Pi + · rw [if_neg hox] + by_cases hcx : Closer Pi x + · rw [if_pos hcx] + rcases st with _ | ⟨⟨o, b⟩, st'⟩ + · -- empty stack: the closer is unmatched, escape it + show MT Pi (encAux Pi esc [] (out ++ esc x) xs) + apply ih + · simp + · exact mt_append Pi hout (esc_mt Pi esc hesc x) + · show MT Pi (if (o, x) ∈ Pi then encAux Pi esc st' (b ++ [o] ++ out ++ [x]) xs + else encAux Pi esc ((o, b) :: st') (out ++ esc x) xs) + by_cases hp' : (o, x) ∈ Pi + · -- matched: commit `[o] ++ body ++ [x]` into the parent level + rw [if_pos hp'] + have hb : MT Pi b := hst (o, b) (by simp) + apply ih + · intro p hp + exact hst p (List.mem_cons_of_mem _ hp) + · simpa using mt_append Pi hb (mt_wrap Pi hout hp') + · -- kind mismatch: unmatched closer, escape it, stack untouched + rw [if_neg hp'] + apply ih + · exact hst + · exact mt_append Pi hout (esc_mt Pi esc hesc x) + · -- nonmatcher: passes through verbatim + rw [if_neg hcx] + have hnx : Nonmatcher Pi x := by + simp only [Nonmatcher, Matcher, not_or] + exact ⟨hox, hcx⟩ + apply ih + · exact hst + · exact mt_append Pi hout (MT.flat [x] (by simpa using hnx)) + +-- Theorem (output ∈ L): any string at all, once encoded, is matchertext. +theorem toMatchertext_mt (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) (v : List α) : + MT Pi (toMatchertext Pi esc v) := + encAux_mt Pi esc hesc [] (by simp) [] (mt_nil Pi) v + +-- Corollary (write-path payoff): reading to matcher balance recovers exactly the encoded +-- value, for a freely chosen v. embed_boundary assumes MT Pi m, which toMatchertext_mt supplies. +theorem embed_boundary_encoded + (hdisj : ∀ x y z, (x, y) ∈ Pi → (z, x) ∈ Pi → False) + (esc : α → List α) + (hesc : ∀ c x, x ∈ esc c → Nonmatcher Pi x) + (v : List α) {c : α} (hc : Closer Pi c) : + (∀ p, p <+: toMatchertext Pi esc v → 0 ≤ depth Pi p) + ∧ depth Pi (toMatchertext Pi esc v) = 0 + ∧ depth Pi (toMatchertext Pi esc v ++ [c]) = -1 := + embed_boundary Pi hdisj (toMatchertext_mt Pi esc hesc v) hc