% Chapter Template

\chapter{Regular Expressions and POSIX Lexing-Preliminaries} % Main chapter title

\label{Inj} % In chapter 2 \ref{Chapter2} we will introduce the concepts

%and notations we 

% used for describing the lexing algorithm by Sulzmann and Lu,

%and then give the algorithm and its variant and discuss

%why more aggressive simplifications are needed. 

We start with a technical overview of the catastrophic backtracking problem,

motivating rigorous approaches to regular expression matching and lexing.

Then we introduce basic notations and definitions of our problem.

\section{Technical Overview}

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.

For example, 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. A poorly written regular expression exhibited catastrophic backtracking

and exhausted CPUs 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.

In this chapter, we define the basic notions 

for regular languages and regular expressions.

This is essentially a description in ``English''

the functions and datatypes of our formalisation in Isabelle/HOL.

We also define what $\POSIX$ lexing means, 

followed by the first lexing algorithm by Sulzmanna and Lu \parencite{Sulzmann2014} 

that produces the output conforming

to the $\POSIX$ standard. 

This is a preliminary chapter which describes the results of

Sulzmann and Lu and Ausaf et al \ref{AusafDyckhoffUrban2016},

but the proof details and function definitions are needed to motivate our work

as we show in chapter \ref{Bitcoded2} how the proofs break down when

simplifications are applied.

%TODO: Actually show this in chapter 4.

In what follows 

we choose to use the Isabelle-style notation

for function and datatype constructor applications, where

the parameters of a function are not enclosed

inside a pair of parentheses (e.g. $f \;x \;y$

instead of $f(x,\;y)$). This is mainly

to make the text visually more concise.

\section{Preliminaries}%Regex, and the Problems with Regex Matchers}

Regular expressions and regular expression matchers 

have clearly been studied for many, 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