% Chapter 1

\chapter{Introduction} % Main chapter title

\label{Chapter1} % For referencing the chapter elsewhere, use \ref{Chapter1} 

%----------------------------------------------------------------------------------------

% Define some commands to keep the formatting separated from the content 

\newcommand{\keyword}[1]{\textbf{#1}}

\newcommand{\tabhead}[1]{\textbf{#1}}

\newcommand{\code}[1]{\texttt{#1}}

\newcommand{\file}[1]{\texttt{\bfseries#1}}

\newcommand{\option}[1]{\texttt{\itshape#1}}

\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%

\newcommand{\ZERO}{\mbox{\bf 0}}

\newcommand{\ONE}{\mbox{\bf 1}}

\def\lexer{\mathit{lexer}}

\def\mkeps{\mathit{mkeps}}

\def\DFA{\textit{DFA}}

\def\bmkeps{\textit{bmkeps}}

\def\retrieve{\textit{retrieve}}

\def\blexer{\textit{blexer}}

\def\flex{\textit{flex}}

\def\inj{\mathit{inj}}

\def\Empty{\mathit{Empty}}

\def\Left{\mathit{Left}}

\def\Right{\mathit{Right}}

\def\Stars{\mathit{Stars}}

\def\Char{\mathit{Char}}

\def\Seq{\mathit{Seq}}

\def\Der{\mathit{Der}}

\def\nullable{\mathit{nullable}}

\def\Z{\mathit{Z}}

\def\S{\mathit{S}}

\def\rup{r^\uparrow}

\def\simp{\mathit{simp}}

\def\simpALTs{\mathit{simp}\_\mathit{ALTs}}

\def\map{\mathit{map}}

\def\distinct{\mathit{distinct}}

\def\blexersimp{\mathit{blexer}\_\mathit{simp}}

%----------------------------------------------------------------------------------------

Regular expression matching and lexing has been 

 widely-used and well-implemented

in software industry. 

If you go to a popular programming language's

regex engine,

you can supply it with regex and strings of your own,

and get matching/lexing  information such as how a 

sub-part of the regex matches a sub-part of the string.

These lexing libraries are on average quite fast.

For example, the regex engines some network intrusion detection

systems use are able to process

 megabytes or even gigabytes of network traffic per second.

Why do we need to have our version, if the algorithms work well on 

average?

Take $(a^*)^*\,b$ and ask whether

strings of the form $aa..a$ match this regular

expression. Obviously this is not the case---the expected $b$ in the last

position is missing. One would expect that modern regular expression

matching engines can find this out very quickly. Alas, if one tries

this example in JavaScript, Python or Java 8 with strings like 28

$a$'s, one discovers that this decision takes around 30 seconds and

takes considerably longer when adding a few more $a$'s, as the graphs

below show:

\begin{center}

\begin{tabular}{@{}c@{\hspace{0mm}}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}\\

\multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings 

           of the form $\underbrace{aa..a}_{n}$.}

\end{tabular}    

\end{center}  

This is clearly exponential behaviour, and 

is triggered by some relatively simple regex patterns.

The opens up the possibility of

 a ReDoS (regular expression denial-of-service ) attack.

Theoretical results say that regular expression matching

should be linear with respect to the input. You could construct

an NFA via Thompson construction, and simulate  running it.

This would be linear.

Or you could determinize the NFA into a DFA, and minimize that

DFA. Once you have the DFA, the running time is also linear, requiring just 

one scanning pass of the input.

But modern  regex libraries in popular language engines

 often want to support richer constructs

than  the most basic regular expressions such as bounded repetitions

and back references. 

%put in illustrations

%a{1}{3}

These make a DFA construction impossible because

of an exponential states explosion.

 They also want to support lexing rather than just matching

 for tasks that involves text processing.

 Existing regex libraries either pose restrictions on the user input, or does 

 not give linear running time guarantee.

 %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

 %TODO: Java 17 updated graphs? Is it ok to still use Java 8 graphs?

 Another thing about the these libraries is that there

 is no correctness guarantee.

 In some cases they either fails to generate a lexing result when there is a match,

 or gives the wrong way of matching.

This superlinear blowup in matching algorithms sometimes causes

considerable grief in real life: 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}}

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 web servers to grind to a

halt. This happened when a post with 20,000 white spaces was submitted,

but importantly the white spaces were neither at the beginning nor at

the end. As a result, the regular expression matching engine needed to

backtrack over many choices. In this example, the time needed to process

the string was $O(n^2)$ with respect to the string length. This

quadratic overhead was enough for the homepage of Stack Exchange to

respond so slowly that the load balancer assumed there must be some

attack and therefore stopped the servers from responding to any

requests. This made the whole site become unavailable. Another very

recent example is a global outage of all Cloudflare servers on 2 July

2019. A poorly written regular expression exhibited exponential

behaviour 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/}}

 Is it possible to have a regex lexing algorithm with proven correctness and 

 time complexity, which allows easy extensions to

  constructs like 

 bounded repetitions, negation,  lookarounds, and even back-references? 

 We propose Brzozowski's derivatives as a solution to this problem.

 \section{Why Brzozowski}

 In the last fifteen or so years, Brzozowski's derivatives of regular

expressions have sparked quite a bit of interest in the functional

programming and theorem prover communities.  

The beauty of

Brzozowski's derivatives \parencite{Brzozowski1964} is that they are neatly

expressible in any functional language, and easily definable and

reasoned about in theorem provers---the definitions just consist of

inductive datatypes and simple recursive functions. 

Suppose we have an alphabet $\Sigma$, the strings  whose characters

are from $\Sigma$

can be expressed as $\Sigma^*$.

We use patterns to define a set of strings concisely. Regular expressions

are one of such patterns systems:

The basic regular expressions  are defined inductively

 by the following grammar:

\[			r ::=   \ZERO \mid  \ONE

			 \mid  c  

			 \mid  r_1 \cdot r_2

			 \mid  r_1 + r_2   

			 \mid r^*         

\]

The language or set of strings defined by regular expressions are defined as

%TODO: FILL in the other defs

\begin{center}

\begin{tabular}{lcl}

$L \; r_1 + r_2$ & $\dn$ & $ L \; r_1 \cup L \; r_2$\\

$L \; r_1 \cdot r_2$ & $\dn$ & $ L \; r_1 \cap L \; r_2$\\

\end{tabular}

\end{center}

Which are also called the "language interpretation".

The Brzozowski derivative w.r.t character $c$ is an operation on the regex,

where the operation transforms the regex to a new one containing

strings without the head character $c$.

Formally, we define first such a transformation on any string set, which

we call semantic derivative:

\begin{center}

$\Der \; c\; \textit{StringSet} = \{s \mid c :: s \in StringSet\}$

\end{center}

Mathematically, it can be expressed as the 

If the $\textit{StringSet}$ happen to have some structure, for example,

if it is regular, then we have that it

The the derivative of regular expression, denoted as

$r \backslash c$, is a function that takes parameters

$r$ and $c$, and returns another regular expression $r'$,

which is computed by the following recursive function:

\begin{center}

\begin{tabular}{lcl}

		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  

		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\

		$d \backslash c$     & $\dn$ & 

		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\

$(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\

$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\

	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\

	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\

	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\

\end{tabular}

\end{center}

\noindent

\noindent

The $\nullable$ function tests whether the empty string $""$ 

is in the language of $r$:

\begin{center}

		\begin{tabular}{lcl}

			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\  

			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\

			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\

			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\

			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\

			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\

		\end{tabular}

\end{center}

\noindent

The empty set does not contain any string and

therefore not the empty string, the empty string 

regular expression contains the empty string

by definition, the character regular expression

is the singleton that contains character only,

and therefore does not contain the empty string,

the alternative regular expression(or "or" expression)

might have one of its children regular expressions

being nullable and any one of its children being nullable

would suffice. The sequence regular expression

would require both children to have the empty string

to compose an empty string and the Kleene star

operation naturally introduced the empty string.

We can give the meaning of regular expressions derivatives

by language interpretation:

Derivatives give a simple solution

to the problem of matching a string $s$ with a regular

expression $r$: if the derivative of $r$ w.r.t.\ (in

succession) all the characters of the string matches the empty string,

then $r$ matches $s$ (and {\em vice versa}).  

However, there are two difficulties with derivative-based matchers:

First, Brzozowski's original matcher only generates a yes/no answer

for whether a regular expression matches a string or not.  This is too

little information in the context of lexing where separate tokens must

be identified and also classified (for example as keywords

or identifiers).  Sulzmann and Lu~\cite{Sulzmann2014} overcome this

difficulty by cleverly extending Brzozowski's matching

algorithm. Their extended version generates additional information on

\emph{how} a regular expression matches a string following the POSIX

rules for regular expression matching. They achieve this by adding a

second ``phase'' to Brzozowski's algorithm involving an injection

function.  In our own earlier work we provided the formal

specification of what POSIX matching means and proved in Isabelle/HOL

the correctness

of Sulzmann and Lu's extended algorithm accordingly

\cite{AusafDyckhoffUrban2016}.

The second difficulty is that Brzozowski's derivatives can 

grow to arbitrarily big sizes. For example if we start with the

regular expression $(a+aa)^*$ and take

successive derivatives according to the character $a$, we end up with

a sequence of ever-growing derivatives like 

\def\ll{\stackrel{\_\backslash{} a}{\longrightarrow}}

\begin{center}

\begin{tabular}{rll}

$(a + aa)^*$ & $\ll$ & $(\ONE + \ONE{}a) \cdot (a + aa)^*$\\

& $\ll$ & $(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* \;+\; (\ONE + \ONE{}a) \cdot (a + aa)^*$\\

& $\ll$ & $(\ZERO + \ZERO{}a + \ZERO) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^* \;+\; $\\

& & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\

& $\ll$ & \ldots \hspace{15mm}(regular expressions of sizes 98, 169, 283, 468, 767, \ldots)

\end{tabular}

\end{center}

\noindent where after around 35 steps we run out of memory on a

typical computer (we shall define shortly the precise details of our

regular expressions and the derivative operation).  Clearly, the

notation involving $\ZERO$s and $\ONE$s already suggests

simplification rules that can be applied to regular regular

expressions, for example $\ZERO{}\,r \Rightarrow \ZERO$, $\ONE{}\,r

\Rightarrow r$, $\ZERO{} + r \Rightarrow r$ and $r + r \Rightarrow

r$. While such simple-minded simplifications have been proved in our

earlier work to preserve the correctness of Sulzmann and Lu's

algorithm \cite{AusafDyckhoffUrban2016}, they unfortunately do

\emph{not} help with limiting the growth of the derivatives shown

above: the growth is slowed, but the derivatives can still grow rather

quickly beyond any finite bound.

Sulzmann and Lu overcome this ``growth problem'' in a second algorithm

\cite{Sulzmann2014} where they introduce bitcoded

regular expressions. In this version, POSIX values are

represented as bitsequences and such sequences are incrementally generated

when derivatives are calculated. The compact representation

of bitsequences and regular expressions allows them to define a more

``aggressive'' simplification method that keeps the size of the

derivatives finite no matter what the length of the string is.

They make some informal claims about the correctness and linear behaviour

of this version, but do not provide any supporting proof arguments, not

even ``pencil-and-paper'' arguments. They write about their bitcoded

\emph{incremental parsing method} (that is the algorithm to be formalised

in this paper):

\begin{quote}\it

  ``Correctness Claim: We further claim that the incremental parsing

  method [..] in combination with the simplification steps [..]

  yields POSIX parse trees. We have tested this claim

  extensively [..] but yet

  have to work out all proof details.'' \cite[Page 14]{Sulzmann2014}

\end{quote}  

\section{Backgound}

%Regular expression matching and lexing has been 

% widely-used and well-implemented

%in software industry. 

%TODO: expand the above into a full paragraph

%TODO: look up snort rules to use here--give readers idea of what regexes look like

Theoretical results say that regular expression matching

should be linear with respect to the input.

Under a certain class of regular expressions and inputs though,

practical implementations  suffer from non-linear or even 

exponential running time,

allowing a ReDoS (regular expression denial-of-service ) attack.

%----------------------------------------------------------------------------------------

\section{Existing Practical Approaches}

The reason behind is that regex libraries in popular language engines

 often want to support richer constructs

than  the most basic regular expressions, and lexing rather than matching

is needed for sub-match extraction.

\subsection{DFA Approach}

Exponential states.

\subsection{NFA Approach}

Backtracking.

%----------------------------------------------------------------------------------------

\section{Our Approach}

In the last fifteen or so years, Brzozowski's derivatives of regular

expressions have sparked quite a bit of interest in the functional

programming and theorem prover communities.  The beauty of

Brzozowski's derivatives \parencite{Brzozowski1964} is that they are neatly

expressible in any functional language, and easily definable and

reasoned about in theorem provers---the definitions just consist of

inductive datatypes and simple recursive functions.  Derivatives of a

regular expression, written $r \backslash c$, give a simple solution

to the problem of matching a string $s$ with a regular

expression $r$: if the derivative of $r$ w.r.t.\ (in

succession) all the characters of the string matches the empty string,

then $r$ matches $s$ (and {\em vice versa}).  

This work aims to address the above vulnerability by the combination

of Brzozowski's derivatives and interactive theorem proving. We give an 

improved version of  Sulzmann and Lu's bit-coded algorithm using 

derivatives, which come with a formal guarantee in terms of correctness and 

running time as an Isabelle/HOL proof.

Then we improve the algorithm with an even stronger version of 

simplification, and prove a time bound linear to input and

cubic to regular expression size using a technique by

Antimirov.

\subsection{Existing Work}

We are aware

of a mechanised correctness proof of Brzozowski's derivative-based matcher in HOL4 by

Owens and Slind~\parencite{Owens2008}. Another one in Isabelle/HOL is part

of the work by Krauss and Nipkow \parencite{Krauss2011}.  And another one

in Coq is given by Coquand and Siles \parencite{Coquand2012}.

Also Ribeiro and Du Bois give one in Agda \parencite{RibeiroAgda2017}.

%----------------------------------------------------------------------------------------

\section{What this Template Includes}

\subsection{Folders}

This template comes as a single zip file that expands out to several files and folders. The folder names are mostly self-explanatory:

\keyword{Appendices} -- this is the folder where you put the appendices. Each appendix should go into its own separate \file{.tex} file. An example and template are included in the directory.

\keyword{Chapters} -- this is the folder where you put the thesis chapters. A thesis usually has about six chapters, though there is no hard rule on this. Each chapter should go in its own separate \file{.tex} file and they can be split as:

\begin{itemize}

\item Chapter 1: Introduction to the thesis topic

\item Chapter 2: Background information and theory

\item Chapter 3: (Laboratory) experimental setup

\item Chapter 4: Details of experiment 1

\item Chapter 5: Details of experiment 2

\item Chapter 6: Discussion of the experimental results

\item Chapter 7: Conclusion and future directions

\end{itemize}

This chapter layout is specialised for the experimental sciences, your discipline may be different.

\keyword{Figures} -- this folder contains all figures for the thesis. These are the final images that will go into the thesis document.

\subsection{Files}

Included are also several files, most of them are plain text and you can see their contents in a text editor. After initial compilation, you will see that more auxiliary files are created by \LaTeX{} or BibTeX and which you don't need to delete or worry about:

\keyword{example.bib} -- this is an important file that contains all the bibliographic information and references that you will be citing in the thesis for use with BibTeX. You can write it manually, but there are reference manager programs available that will create and manage it for you. Bibliographies in \LaTeX{} are a large subject and you may need to read about BibTeX before starting with this. Many modern reference managers will allow you to export your references in BibTeX format which greatly eases the amount of work you have to do.

\keyword{MastersDoctoralThesis.cls} -- this is an important file. It is the class file that tells \LaTeX{} how to format the thesis. 

\keyword{main.pdf} -- this is your beautifully typeset thesis (in the PDF file format) created by \LaTeX{}. It is supplied in the PDF with the template and after you compile the template you should get an identical version.

\keyword{main.tex} -- this is an important file. This is the file that you tell \LaTeX{} to compile to produce your thesis as a PDF file. It contains the framework and constructs that tell \LaTeX{} how to layout the thesis. It is heavily commented so you can read exactly what each line of code does and why it is there. After you put your own information into the \emph{THESIS INFORMATION} block -- you have now started your thesis!

Files that are \emph{not} included, but are created by \LaTeX{} as auxiliary files include:

\keyword{main.aux} -- this is an auxiliary file generated by \LaTeX{}, if it is deleted \LaTeX{} simply regenerates it when you run the main \file{.tex} file.

\keyword{main.bbl} -- this is an auxiliary file generated by BibTeX, if it is deleted, BibTeX simply regenerates it when you run the \file{main.aux} file. Whereas the \file{.bib} file contains all the references you have, this \file{.bbl} file contains the references you have actually cited in the thesis and is used to build the bibliography section of the thesis.

\keyword{main.blg} -- this is an auxiliary file generated by BibTeX, if it is deleted BibTeX simply regenerates it when you run the main \file{.aux} file.