\chapter{Technical Overview}
\label{Overview}
We start with a technical overview of the
catastrophic backtracking problem,
motivating rigorous approaches to regular expression matching and lexing.
In doing so we also briefly
introduce common terminology such as
bounded repetitions and back-references.
\section{Motivating Examples}
Consider for example the regular expression $(a^*)^*\,b$ and
strings of the form $aa..a$. These strings cannot be matched by this regular
expression: obviously the expected $b$ in the last
position is missing. One would assume that modern regular expression
matching engines can find this out very quickly. Surprisingly, if one tries
this example in JavaScript, Python or Java 8, even with small strings,
say of lenght of around 30 $a$'s,
the decision takes large amounts of time to finish.
This is inproportional
to the simplicity of the input (see graphs in figure \ref{fig:aStarStarb}).
The algorithms clearly show exponential behaviour, and as can be seen
is triggered by some relatively simple regular expressions.
Java 9 and newer
versions mitigates this behaviour by several magnitudes,
but are still slow compared
with the approach we are going to use in this thesis.
This superlinear blowup in regular expression engines
has caused grief in ``real life'' where it is
given the name ``catastrophic backtracking'' or ``evil'' regular expressions.
A less serious example is a bug in the Atom editor:
a user found out when writing the following code
\begin{verbatim}
vVar.Type().Name() == "" && vVar.Kind() == reflect.Ptr
\end{verbatim}
\begin{verbatim}
&& vVar.Type().Elem().Name() == "" && vVar.Type().Elem().Kind() ==
\end{verbatim}
\begin{verbatim}
reflect.Slice
\end{verbatim}
it took the editor half a hour to finish computing.
This was subsequently fixed by Galbraith \cite{fixedAtom},
and the issue was due to the regex engine of Atom.
But evil regular expressions can be more than a nuisance in a text editor:
on 20 July 2016 one evil
regular expression brought the webpage
\href{http://stackexchange.com}{Stack Exchange} to its
knees.\footnote{\url{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}(Last accessed in 2019)}
In this instance, a regular expression intended to just trim white
spaces from the beginning and the end of a line actually consumed
massive amounts of CPU resources---causing the web servers to grind to a
halt. In this example, the time needed to process
the string was
$O(n^2)$ with respect to the string length $n$. This
quadratic overhead was enough for the homepage of Stack Exchange to
respond so slowly that the load balancer assumed a $\mathit{DoS}$
attack and therefore stopped the servers from responding to any
requests. This made the whole site become unavailable.
\begin{figure}[p]
\begin{center}
\begin{tabular}{@{}c@{\hspace{0mm}}c@{}}
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
ylabel={time in secs},
enlargelimits=false,
xtick={0,5,...,30},
xmax=33,
ymax=35,
ytick={0,5,...,30},
scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={JavaScript},
legend pos=north west,
legend cell align=left]
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
\end{axis}
\end{tikzpicture}
&
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
%ylabel={time in secs},
enlargelimits=false,
xtick={0,5,...,30},
xmax=33,
ymax=35,
ytick={0,5,...,30},
scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={Python},
legend pos=north west,
legend cell align=left]
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
\end{axis}
\end{tikzpicture}\\
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
ylabel={time in secs},
enlargelimits=false,
xtick={0,5,...,30},
xmax=33,
ymax=35,
ytick={0,5,...,30},
scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={Java 8},
legend pos=north west,
legend cell align=left]
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
\end{axis}
\end{tikzpicture}
&
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
%ylabel={time in secs},
enlargelimits=false,
xtick={0,5,...,30},
xmax=33,
ymax=35,
ytick={0,5,...,30},
scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={Dart},
legend pos=north west,
legend cell align=left]
\addplot[green,mark=*, mark options={fill=white}] table {re-dart.data};
\end{axis}
\end{tikzpicture}\\
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
ylabel={time in secs},
enlargelimits=false,
xtick={0,5,...,30},
xmax=33,
ymax=35,
ytick={0,5,...,30},
scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={Swift},
legend pos=north west,
legend cell align=left]
\addplot[purple,mark=*, mark options={fill=white}] table {re-swift.data};
\end{axis}
\end{tikzpicture}
&
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
%ylabel={time in secs},
enlargelimits=true,
%xtick={0,5000,...,40000},
%xmax=40000,
%ymax=35,
restrict x to domain*=0:40000,
restrict y to domain*=0:35,
%ytick={0,5,...,30},
%scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={Java9+},
legend pos=north west,
legend cell align=left]
\addplot[orange,mark=*, mark options={fill=white}] table {re-java9.data};
\end{axis}
\end{tikzpicture}\\
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
ylabel={time in secs},
enlargelimits=true,
%xtick={0,5,...,30},
%xmax=33,
%ymax=35,
restrict x to domain*=0:60000,
restrict y to domain*=0:35,
%ytick={0,5,...,30},
%scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={Scala},
legend pos=north west,
legend cell align=left]
\addplot[magenta,mark=*, mark options={fill=white}] table {re-blexersimp.data};
\end{axis}
\end{tikzpicture}
&
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
%ylabel={time in secs},
enlargelimits=true,
%xtick={0,5000,...,40000},
%xmax=40000,
%ymax=35,
restrict x to domain*=0:60000,
restrict y to domain*=0:45,
%ytick={0,5,...,30},
%scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend style={cells={align=left}},
legend entries={Isabelle \\ Extracted},
legend pos=north west,
legend cell align=left]
\addplot[magenta,mark=*, mark options={fill=white}] table {re-fromIsabelle.data};
\end{axis}
\end{tikzpicture}\\
\multicolumn{2}{c}{Graphs}
\end{tabular}
\end{center}
\caption{Graphs showing runtime for matching $(a^*)^*\,b$ with strings
of the form $\protect\underbrace{aa..a}_{n}$ in various existing regular expression libraries.
The reason for their fast growth %superlinear behaviour
is that they do a depth-first-search
using NFAs.
If the string does not match, the regular expression matching
engine starts to explore all possibilities.
The last two graphs are for our implementation in Scala, one manual
and one extracted from the verified lexer in Isabelle by $\textit{codegen}$.
Our lexer
performs better in this case, and
is formally verified.
Despite being almost identical, the codegen-generated lexer
% is generated directly from Isabelle using $\textit{codegen}$,
is slower than the manually written version since the code synthesised by
$\textit{codegen}$ does not use native integer or string
types of the target language.
%Note that we are comparing our \emph{lexer} against other languages' matchers.
}\label{fig:aStarStarb}
\end{figure}\afterpage{\clearpage}
A more recent example is a global outage of all Cloudflare servers on
2 July 2019.
The traffic Cloudflare services each day is more than
Twitter, Amazon, Instagram, Apple, Bing and Wikipedia combined, yet
it became completely unavailable for half an hour because of
a poorly-written regular expression roughly of the form $^*.^*=.^*$
exhausted CPU resources that serve HTTP traffic.
Although the outage
had several causes, at the heart was a regular expression that
was used to monitor network
traffic.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}(Last accessed in 2022)}
These problems with regular expressions
are not isolated events that happen
very rarely,
%but actually widespread.
%They occur so often that they have a
but they occur actually often enough that they have a
name: Regular-Expression-Denial-Of-Service (ReDoS)
attacks.
Davis et al. \cite{Davis18} detected more
than 1000 evil regular expressions
in Node.js, Python core libraries, npm and pypi.
They therefore concluded that evil regular expressions
are a real problem rather than just "a parlour trick".
The work in this thesis aims to address this issue
with the help of formal proofs.
We describe a lexing algorithm based
on Brzozowski derivatives with verified correctness
and a finiteness property for the size of derivatives
(which are all done in Isabelle/HOL).
Such properties %guarantee the absence of
are an important step in preventing
catastrophic backtracking once and for all.
We will give more details in the next sections
on (i) why the slow cases in graph \ref{fig:aStarStarb}
can occur in traditional regular expression engines
and (ii) why we choose our
approach based on Brzozowski derivatives and formal proofs.
\section{Preliminaries}%Regex, and the Problems with Regex Matchers}
Regular expressions and regular expression matchers
have been studied for many years.
Theoretical results in automata theory state
that basic regular expression matching should be linear
w.r.t the input.
This assumes that the regular expression
$r$ was pre-processed and turned into a
deterministic finite automaton (DFA) before matching \cite{Sakarovitch2009}.
By basic we mean textbook definitions such as the one
below, involving only regular expressions for characters, alternatives,
sequences, and Kleene stars:
\[
r ::= c | r_1 + r_2 | r_1 \cdot r_2 | r^*
\]
Modern regular expression matchers used by programmers,
however,
support much richer constructs, such as bounded repetitions,
negations,
and back-references.
To differentiate, we use the word \emph{regex} to refer
to those expressions with richer constructs while reserving the
term \emph{regular expression}
for the more traditional meaning in formal languages theory.
We follow this convention
in this thesis.
In the future, we aim to support all the popular features of regexes,
but for this work we mainly look at basic regular expressions
and bounded repetitions.
%Most modern regex libraries
%the so-called PCRE standard (Peral Compatible Regular Expressions)
%has the back-references
Regexes come with a number of constructs
that make it more convenient for
programmers to write regular expressions.
Depending on the types of constructs
the task of matching and lexing with them
will have different levels of complexity.
Some of those constructs are syntactic sugars that are
simply short hand notations
that save the programmers a few keystrokes.
These will not cause problems for regex libraries.
For example the
non-binary alternative involving three or more choices just means:
\[
(a | b | c) \stackrel{means}{=} ((a + b)+ c)
\]
Similarly, the range operator
%used to express the alternative
%of all characters between its operands,
is just a concise way
of expressing an alternative of consecutive characters:
\[
[0~-9]\stackrel{means}{=} (0 | 1 | \ldots | 9 )
\]
for an alternative. The
wildcard character '$.$' is used to refer to any single character,
\[
. \stackrel{means}{=} [0-9a-zA-Z+-()*\&\ldots]
\]
except the newline.
\subsection{Bounded Repetitions}
More interesting are bounded repetitions, which can
make the regular expressions much
more compact.
Normally there are four kinds of bounded repetitions:
$r^{\{n\}}$, $r^{\{\ldots m\}}$, $r^{\{n\ldots \}}$ and $r^{\{n\ldots m\}}$
(where $n$ and $m$ are constant natural numbers).
Like the star regular expressions, the set of strings or language
a bounded regular expression can match
is defined using the power operation on sets:
\begin{center}
\begin{tabular}{lcl}
$L \; r^{\{n\}}$ & $\dn$ & $(L \; r)^n$\\
$L \; r^{\{\ldots m\}}$ & $\dn$ & $\bigcup_{0 \leq i \leq m}. (L \; r)^i$\\
$L \; r^{\{n\ldots \}}$ & $\dn$ & $\bigcup_{n \leq i}. (L \; r)^i$\\
$L \; r^{\{n \ldots m\}}$ & $\dn$ & $\bigcup_{n \leq i \leq m}. (L \; r)^i$
\end{tabular}
\end{center}
The attraction of bounded repetitions is that they can be
used to avoid a size blow up: for example $r^{\{n\}}$
is a shorthand for
the much longer regular expression:
\[
\underbrace{r\ldots r}_\text{n copies of r}.
\]
%Therefore, a naive algorithm that simply unfolds
%them into their desugared forms
%will suffer from at least an exponential runtime increase.
The problem with matching
such bounded repetitions
is that tools based on the classic notion of
automata need to expand $r^{\{n\}}$ into $n$ connected
copies of the automaton for $r$. This leads to very inefficient matching
algorithms or algorithms that consume large amounts of memory.
Implementations using $\DFA$s will
in such situations
either become very slow
(for example Verbatim++ \cite{Verbatimpp}) or run
out of memory (for example $\mathit{LEX}$ and
$\mathit{JFLEX}$\footnote{LEX and JFLEX are lexer generators
in C and JAVA that generate $\mathit{DFA}$-based
lexers. The user provides a set of regular expressions
and configurations, and then
gets an output program encoding a minimized $\mathit{DFA}$
that can be compiled and run.
When given the above countdown regular expression,
a small $n$ (say 20) would result in a program representing a
DFA
with millions of states.}) for large counters.
A classic example for this phenomenon is the regular expression $(a+b)^* a (a+b)^{n}$
where the minimal DFA requires at least $2^{n+1}$ states.
For example, when $n$ is equal to 2,
the corresponding $\mathit{NFA}$ looks like:
\vspace{6mm}
\begin{center}
\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,auto]
\node[state,initial] (q_0) {$q_0$};
\node[state, red] (q_1) [right=of q_0] {$q_1$};
\node[state, red] (q_2) [right=of q_1] {$q_2$};
\node[state, accepting, red](q_3) [right=of q_2] {$q_3$};
\path[->]
(q_0) edge node {a} (q_1)
edge [loop below] node {a,b} ()
(q_1) edge node {a,b} (q_2)
(q_2) edge node {a,b} (q_3);
\end{tikzpicture}
\end{center}
and when turned into a DFA by the subset construction
requires at least $2^3$ states.\footnote{The
red states are "countdown states" which count down
the number of characters needed in addition to the current
string to make a successful match.
For example, state $q_1$ indicates a match that has
gone past the $(a|b)^*$ part of $(a|b)^*a(a|b)^{\{2\}}$,
and just consumed the "delimiter" $a$ in the middle, and
needs to match 2 more iterations of $(a|b)$ to complete.
State $q_2$ on the other hand, can be viewed as a state
after $q_1$ has consumed 1 character, and just waits
for 1 more character to complete.
The state $q_3$ is the last (accepting) state, requiring 0
more characters.
Depending on the suffix of the
input string up to the current read location,
the states $q_1$ and $q_2$, $q_3$
may or may
not be active.
A $\mathit{DFA}$ for such an $\mathit{NFA}$ would
contain at least $2^3$ non-equivalent states that cannot be merged,
because the subset construction during determinisation will generate
all the elements in the power set $\mathit{Pow}\{q_1, q_2, q_3\}$.
Generalizing this to regular expressions with larger
bounded repetitions number, we have that
regexes shaped like $r^*ar^{\{n\}}$ when converted to $\mathit{DFA}$s
would require at least $2^{n+1}$ states, if $r$ itself contains
more than 1 string.
This is to represent all different
scenarios in which "countdown" states are active.}
Bounded repetitions are important because they
tend to occur frequently in practical use,
for example in the regex library RegExLib, in
the rules library of Snort \cite{Snort1999}\footnote{
Snort is a network intrusion detection (NID) tool
for monitoring network traffic.
The network security community curates a list
of malicious patterns written as regexes,
which is used by Snort's detection engine
to match against network traffic for any hostile
activities such as buffer overflow attacks.},
as well as in XML Schema definitions (XSDs).
According to Bj\"{o}rklund et al \cite{xml2015},
more than half of the
XSDs they found on the Maven.org central repository
have bounded regular expressions in them.
Often the counters are quite large, with the largest being
close to ten million.
A smaller sample XSD they gave
is:
\lstset{
basicstyle=\fontsize{8.5}{9}\ttfamily,
language=XML,
morekeywords={encoding,
xs:schema,xs:element,xs:complexType,xs:sequence,xs:attribute}
}
\begin{lstlisting}
<sequence minOccurs="0" maxOccurs="65535">
<element name="TimeIncr" type="mpeg7:MediaIncrDurationType"/>
<element name="MotionParams" type="float" minOccurs="2" maxOccurs="12"/>
</sequence>
\end{lstlisting}
This can be seen as the regex
$(ab^{2\ldots 12})^{0 \ldots 65535}$, where $a$ and $b$ are themselves
regular expressions
satisfying certain constraints (such as
satisfying the floating point number format).
It is therefore quite unsatisfying that
some regular expressions matching libraries
impose adhoc limits
for bounded regular expressions:
For example, in the regular expression matching library in the Go
language the regular expression $a^{1001}$ is not permitted, because no counter
can be above 1000, and in the built-in Rust regular expression library
expressions such as $a^{\{1000\}\{100\}\{5\}}$ give an error message
for being too big~\footnote{Try it out here: https://rustexp.lpil.uk}.
As Becchi and Crawley \cite{Becchi08} have pointed out,
the reason for these restrictions
is that they simulate a non-deterministic finite
automata (NFA) with a breadth-first search.
This way the number of active states could
be equal to the counter number.
When the counters are large,
the memory requirement could become
infeasible, and a regex engine
like in Go will reject this pattern straight away.
\begin{figure}[H]
\begin{center}
\begin{tikzpicture} [node distance = 2cm, on grid, auto]
\node (q0) [state, initial] {$0$};
\node (q1) [state, right = of q0] {$1$};
%\node (q2) [state, right = of q1] {$2$};
\node (qdots) [right = of q1] {$\ldots$};
\node (qn) [state, right = of qdots] {$n$};
\node (qn1) [state, right = of qn] {$n+1$};
\node (qn2) [state, right = of qn1] {$n+2$};
\node (qn3) [state, accepting, right = of qn2] {$n+3$};
\path [-stealth, thick]
(q0) edge [loop above] node {a} ()
(q0) edge node {a} (q1)
%(q1) edge node {.} (q2)
(q1) edge node {.} (qdots)
(qdots) edge node {.} (qn)
(qn) edge node {.} (qn1)
(qn1) edge node {b} (qn2)
(qn2) edge node {$c$} (qn3);
\end{tikzpicture}
%\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,auto]
% \node[state,initial] (q_0) {$0$};
% \node[state, ] (q_1) [right=of q_0] {$1$};
% \node[state, ] (q_2) [right=of q_1] {$2$};
% \node[state,
% \node[state, accepting, ](q_3) [right=of q_2] {$3$};
% \path[->]
% (q_0) edge node {a} (q_1)
% edge [loop below] node {a,b} ()
% (q_1) edge node {a,b} (q_2)
% (q_2) edge node {a,b} (q_3);
%\end{tikzpicture}
\end{center}
\caption{The example given by Becchi and Crawley
that NFA simulation can consume large
amounts of memory: $.^*a.^{\{n\}}bc$ matching
strings of the form $aaa\ldots aaaabc$.
When traversing in a breadth-first manner,
all states from 0 till $n+1$ will become active.}\label{fig:inj}
\end{figure}
%Languages like $\mathit{Go}$ and $\mathit{Rust}$ use this
%type of $\mathit{NFA}$ simulation and guarantees a linear runtime
%in terms of input string length.
%TODO:try out these lexers
These problems can of course be solved in matching algorithms where
automata go beyond the classic notion and for instance include explicit
counters \cite{Turo_ov__2020}.
These solutions can be quite efficient,
with the ability to process
gigabits of strings input per second
even with large counters \cite{Becchi08}.
These practical solutions do not come with
formal guarantees, and as pointed out by
Kuklewicz \cite{KuklewiczHaskell}, can be error-prone.
%But formal reasoning about these automata especially in Isabelle
%can be challenging
%and un-intuitive.
%Therefore, we take correctness and runtime claims made about these solutions
%with a grain of salt.
In the work reported in \cite{ITP2023} and here,
we add better support using derivatives
for bounded regular expression $r^{\{n\}}$.
Our results
extend straightforwardly to
repetitions with intervals such as
$r^{\{n\ldots m\}}$.
The merit of Brzozowski derivatives (more on this later)
on this problem is that
it can be naturally extended to support bounded repetitions.
Moreover these extensions are still made up of only small
inductive datatypes and recursive functions,
making it handy to deal with them in theorem provers.
%The point here is that Brzozowski derivatives and the algorithms by Sulzmann and Lu can be
%straightforwardly extended to deal with bounded regular expressions
%and moreover the resulting code still consists of only simple
%recursive functions and inductive datatypes.
Finally, bounded regular expressions do not destroy our finite
boundedness property, which we shall prove later on.
\subsection{Back-References}
The other way to simulate an $\mathit{NFA}$ for matching is choosing
a single transition each time, keeping all the other options in
a queue or stack, and backtracking if that choice eventually
fails.
This method, often called a "depth-first-search",
is efficient in many cases, but could end up
with exponential run time.
The backtracking method is employed in regex libraries
that support \emph{back-references}, for example
in Java and Python.
%\section{Back-references and The Terminology Regex}
%When one constructs an $\NFA$ out of a regular expression
%there is often very little to be done in the first phase, one simply
%construct the $\NFA$ states based on the structure of the input regular expression.
%In the lexing phase, one can simulate the $\mathit{NFA}$ running in two ways:
%one by keeping track of all active states after consuming
%a character, and update that set of states iteratively.
%This can be viewed as a breadth-first-search of the $\mathit{NFA}$
%for a path terminating
%at an accepting state.
Consider the following regular expression where the sequence
operator is omitted for brevity:
\begin{center}
$r_1r_2r_3r_4$
\end{center}
In this example,
one could label sub-expressions of interest
by parenthesizing them and giving
them a number in the order in which their opening parentheses appear.
One possible way of parenthesizing and labelling is:
\begin{center}
$\underset{1}{(}r_1\underset{2}{(}r_2\underset{3}{(}r_3)\underset{4}{(}r_4)))$
\end{center}
The sub-expressions
$r_1r_2r_3r_4$, $r_1r_2r_3$, $r_3$ and $r_4$ are labelled
by 1 to 4, and can be ``referred back'' by their respective numbers.
%These sub-expressions are called "capturing groups".
To do so, one uses the syntax $\backslash i$
to denote that we want the sub-string
of the input matched by the i-th
sub-expression to appear again,
exactly the same as it first appeared:
\begin{center}
$\ldots\underset{\text{i-th lparen}}{(}{r_i})\ldots
\underset{s_i \text{ which just matched} \;r_i}{\backslash i} \ldots$
\end{center}
Once the sub-string $s_i$ for the sub-expression $r_i$
has been fixed, there is no variability on what the back-reference
label $\backslash i$ can be---it is tied to $s_i$.
The overall string will look like $\ldots s_i \ldots s_i \ldots $
%The backslash and number $i$ are the
%so-called "back-references".
%Let $e$ be an expression made of regular expressions
%and back-references. $e$ contains the expression $e_i$
%as its $i$-th capturing group.
%The semantics of back-reference can be recursively
%written as:
%\begin{center}
% \begin{tabular}{c}
% $L ( e \cdot \backslash i) = \{s @ s_i \mid s \in L (e)\quad s_i \in L(r_i)$\\
% $s_i\; \text{match of ($e$, $s$)'s $i$-th capturing group string}\}$
% \end{tabular}
%\end{center}
A concrete example
for back-references is
\begin{center}
$(.^*)\backslash 1$,
\end{center}
which matches
strings that can be split into two identical halves,
for example $\mathit{foofoo}$, $\mathit{ww}$ and so on.
Note that this is different from
repeating the sub-expression verbatim like
\begin{center}
$(.^*)(.^*)$,
\end{center}
which does not impose any restrictions on what strings the second
sub-expression $.^*$
might match.
Another example for back-references is
\begin{center}
$(.)(.)\backslash 2\backslash 1$
\end{center}
which matches four-character palindromes
like $abba$, $x??x$ and so on.
Back-references are a regex construct
that programmers find quite useful.
According to Becchi and Crawley \cite{Becchi08},
6\% of Snort rules (up until 2008) use them.
The most common use of back-references
is to express well-formed html files,
where back-references are convenient for matching
opening and closing tags like
\begin{center}
$\langle html \rangle \ldots \langle / html \rangle$
\end{center}
A regex describing such a format
is
\begin{center}
$\langle (.^+) \rangle \ldots \langle / \backslash 1 \rangle$
\end{center}
Despite being useful, the expressive power of regexes
go beyond regular languages
once back-references are included.
In fact, they allow the regex construct to express
languages that cannot be contained in context-free
languages either.
For example, the back-reference $(a^*)b\backslash1 b \backslash 1$
expresses the language $\{a^n b a^n b a^n\mid n \in \mathbb{N}\}$,
which cannot be expressed by
context-free grammars \cite{campeanu2003formal}.
Such a language is contained in the context-sensitive hierarchy
of formal languages.
Also solving the matching problem involving back-references
is known to be NP-complete \parencite{alfred2014algorithms}.
Regex libraries supporting back-references such as
PCRE \cite{pcre} therefore have to
revert to a depth-first search algorithm including backtracking.
What is unexpected is that even in the cases
not involving back-references, there is still
a (non-negligible) chance they might backtrack super-linearly,
as shown in the graphs in figure \ref{fig:aStarStarb}.
Summing up, we can categorise existing
practical regex libraries into two kinds:
(i) The ones with linear
time guarantees like Go and Rust. The downside with them is that
they impose restrictions
on the regular expressions (not allowing back-references,
bounded repetitions cannot exceed an ad hoc limit etc.).
And (ii) those
that allow large bounded regular expressions and back-references
at the expense of using backtracking algorithms.
They can potentially ``grind to a halt''
on some very simple cases, resulting
ReDoS attacks if exposed to the internet.
The problems with both approaches are the motivation for us
to look again at the regular expression matching problem.
Another motivation is that regular expression matching algorithms
that follow the POSIX standard often contain errors and bugs
as we shall explain next.
%We would like to have regex engines that can
%deal with the regular part (e.g.
%bounded repetitions) of regexes more
%efficiently.
%Also we want to make sure that they do it correctly.
%It turns out that such aim is not so easy to achieve.
%TODO: give examples such as RE2 GOLANG 1000 restriction, rust no repetitions
% For example, the Rust regex engine claims to be linear,
% but does not support lookarounds and back-references.
% The GoLang regex library does not support over 1000 repetitions.
% Java and Python both support back-references, but shows
%catastrophic backtracking behaviours on inputs without back-references(
%when the language is still regular).
%TODO: test performance of Rust on (((((a*a*)b*)b){20})*)c baabaabababaabaaaaaaaaababaaaababababaaaabaaabaaaaaabaabaabababaababaaaaaaaaababaaaababababaaaaaaaaaaaaac
%TODO: verify the fact Rust does not allow 1000+ reps
%The time cost of regex matching algorithms in general
%involve two different phases, and different things can go differently wrong on
%these phases.
%$\DFA$s usually have problems in the first (construction) phase
%, whereas $\NFA$s usually run into trouble
%on the second phase.
\section{Error-prone POSIX Implementations}
Very often there are multiple ways of matching a string
with a regular expression.
In such cases the regular expressions matcher needs to
disambiguate.
The more widely used strategy is called POSIX,
which roughly speaking always chooses the longest initial match.
The POSIX strategy is widely adopted in many regular expression matchers
because it is a natural strategy for lexers.
However, many implementations (including the C libraries
used by Linux and OS X distributions) contain bugs
or do not meet the specification they claim to adhere to.
Kuklewicz maintains a unit test repository which lists some
problems with existing regular expression engines \cite{KuklewiczHaskell}.
In some cases, they either fail to generate a
result when there exists a match,
or give results that are inconsistent with the POSIX standard.
A concrete example is the regex:
\begin{center}
$(aba + ab + a)^* \text{and the string} \; ababa$
\end{center}
The correct POSIX match for the above
involves the entire string $ababa$,
split into two Kleene star iterations, namely $[ab], [aba]$ at positions
$[0, 2), [2, 5)$
respectively.
But feeding this example to the different engines
listed at regex101 \footnote{
regex101 is an online regular expression matcher which
provides API for trying out regular expression
engines of multiple popular programming languages like
Java, Python, Go, etc.} \parencite{regex101}.
yields
only two incomplete matches: $[aba]$ at $[0, 3)$
and $a$ at $[4, 5)$.
Fowler \cite{fowler2003} and Kuklewicz \cite{KuklewiczHaskell}
commented that most regex libraries are not
correctly implementing the central POSIX
rule, called the maximum munch rule.
Grathwohl \parencite{grathwohl2014crash} wrote:
\begin{quote}\it
``The POSIX strategy is more complicated than the
greedy because of the dependence on information about
the length of matched strings in the various subexpressions.''
\end{quote}
%\noindent
People have recognised that the implementation complexity of POSIX rules also come from
the specification being not very precise.
The developers of the regexp package of Go
\footnote{\url{https://pkg.go.dev/regexp\#pkg-overview}}
commented that
\begin{quote}\it
``
The POSIX rule is computationally prohibitive
and not even well-defined.
``
\end{quote}
There are many informal summaries of this disambiguation
strategy, which are often quite long and delicate.
For example Kuklewicz \cite{KuklewiczHaskell}
described the POSIX rule as (section 1, last paragraph):
\begin{quote}
\begin{itemize}
\item
regular expressions (REs) take the leftmost starting match, and the longest match starting there
earlier subpatterns have leftmost-longest priority over later subpatterns\\
\item
higher-level subpatterns have leftmost-longest priority over their component subpatterns\\
\item
REs have right associative concatenation which can be changed with parenthesis\\
\item
parenthesized subexpressions return the match from their last usage\\
\item
text of component subexpressions must be contained in the text of the
higher-level subexpressions\\
\item
if "p" and "q" can never match the same text then "p|q" and "q|p" are equivalent, up to trivial renumbering of captured subexpressions\\
\item
if "p" in "p*" is used to capture non-empty text then additional repetitions of "p" will not capture an empty string\\
\end{itemize}
\end{quote}
%The text above
%is trying to capture something very precise,
%and is crying out for formalising.