% Chapter 1

\chapter{Introduction} % Main chapter title

\label{Introduction} % 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}}

%boxes

\newcommand*{\mybox}[1]{\framebox{\strut #1}}

%\newcommand{\sflataux}[1]{\textit{sflat}\_\textit{aux} \, #1}

\newcommand\sflat[1]{\llparenthesis #1 \rrparenthesis }

\newcommand{\ASEQ}[3]{\textit{ASEQ}_{#1} \, #2 \, #3}

\newcommand{\bderssimp}[2]{#1 \backslash_{bsimps} #2}

\newcommand{\rderssimp}[2]{#1 \backslash_{rsimps} #2}

\def\derssimp{\textit{ders}\_\textit{simp}}

\def\rders{\textit{rders}}

\newcommand{\bders}[2]{#1 \backslash #2}

\newcommand{\bsimp}[1]{\textit{bsimp}(#1)}

\def\bsimps{\textit{bsimp}}

\newcommand{\rsimp}[1]{\textit{rsimp}\; #1}

\newcommand{\sflataux}[1]{\llparenthesis #1 \rrparenthesis'}

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

\newcommand{\denote}{\stackrel{\mbox{\scriptsize denote}}{=}}%

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

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

\newcommand{\AALTS}[2]{\oplus {\scriptstyle #1}\, #2}

\newcommand{\rdistinct}[2]{\textit{rdistinct} \;\; #1 \;\; #2}

\def\rdistincts{\textit{rdistinct}}

\def\rDistinct{\textit{rdistinct}}

\newcommand\hflat[1]{\llparenthesis  #1 \rrparenthesis_*}

\newcommand\hflataux[1]{\llparenthesis #1 \rrparenthesis_*'}

\newcommand\createdByStar[1]{\textit{createdByStar}(#1)}

\def\cbn{\textit{createdByNtimes}}

\def\hpa{\textit{highestPowerAux}}

\def\hpower{\textit{highestPower}}

\def\ntset{\textit{ntset}}

\def\optermsimp{\textit{optermsimp}}

\def\optermOsimp{\textit{optermOsimp}}

\def\optermosimp{\textit{optermosimp}}

\def\opterm{\textit{opterm}}

\def\nString{\textit{nonemptyString}}

\newcommand\myequiv{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny equiv}}}{=}}}

\def\SEQ{\textit{SEQ}}

\def\SEQs{\textit{SEQs}}

\def\case{\textit{case}}

\def\sequal{\stackrel{\mbox{\scriptsize rsimp}}{=}}

\def\rsimpalts{\textit{rsimp}_{ALTS}}

\def\good{\textit{good}}

\def\btrue{\textit{true}}

\def\bfalse{\textit{false}}

\def\bnullable{\textit{bnullable}}

\def\bnullables{\textit{bnullables}}

\def\Some{\textit{Some}}

\def\None{\textit{None}}

\def\code{\textit{code}}

\def\decode{\textit{decode}}

\def\internalise{\textit{internalise}}

\def\lexer{\mathit{lexer}}

\def\mkeps{\textit{mkeps}}

\newcommand{\rder}[2]{#2 \backslash_r #1}

\def\rerases{\textit{rerase}}

\def\nonnested{\textit{nonnested}}

\def\AZERO{\textit{AZERO}}

\def\sizeNregex{\textit{sizeNregex}}

\def\AONE{\textit{AONE}}

\def\ACHAR{\textit{ACHAR}}

\def\simpsulz{\textit{simp}_{Sulz}}

\def\scfrewrites{\stackrel{*}{\rightsquigarrow_{scf}}}

\def\frewrite{\rightsquigarrow_f}

\def\hrewrite{\rightsquigarrow_h}

\def\grewrite{\rightsquigarrow_g}

\def\frewrites{\stackrel{*}{\rightsquigarrow_f}}

\def\hrewrites{\stackrel{*}{\rightsquigarrow_h}}

\def\grewrites{\stackrel{*}{\rightsquigarrow_g}}

\def\fuse{\textit{fuse}}

\def\bder{\textit{bder}}

\def\der{\textit{der}}

\def\POSIX{\textit{POSIX}}

\def\ALTS{\textit{ALTS}}

\def\ASTAR{\textit{ASTAR}}

\def\DFA{\textit{DFA}}

\def\NFA{\textit{NFA}}

\def\bmkeps{\textit{bmkeps}}

\def\bmkepss{\textit{bmkepss}}

\def\retrieve{\textit{retrieve}}

\def\blexer{\textit{blexer}}

\def\flex{\textit{flex}}

\def\inj{\textit{inj}}

\def\Empty{\textit{Empty}}

\def\Left{\textit{Left}}

\def\Right{\textit{Right}}

\def\Stars{\textit{Stars}}

\def\Char{\textit{Char}}

\def\Seq{\textit{Seq}}

\def\Der{\textit{Der}}

\def\Ders{\textit{Ders}}

\def\nullable{\mathit{nullable}}

\def\Z{\mathit{Z}}

\def\S{\mathit{S}}

\def\rup{r^\uparrow}

%\def\bderssimp{\mathit{bders}\_\mathit{simp}}

\def\distinctWith{\textit{distinctWith}}

\def\lf{\textit{lf}}

\def\PD{\textit{PD}}

\def\suffix{\textit{Suffix}}

\def\distinctBy{\textit{distinctBy}}

\def\starupdate{\textit{starUpdate}}

\def\starupdates{\textit{starUpdates}}

\def\nupdate{\textit{nupdate}}

\def\nupdates{\textit{nupdates}}

\def\size{\mathit{size}}

\def\rexp{\mathbf{rexp}}

\def\simp{\mathit{simp}}

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

\def\map{\mathit{map}}

\def\distinct{\mathit{distinct}}

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

\def\blexerStrong{\textit{blexerStrong}}

\def\bsimpStrong{\textit{bsimpStrong}}

\def\bdersStrongs{\textit{bdersStrong}}

\newcommand{\bdersStrong}[2]{#1 \backslash_{bsimpStrongs} #2}

\def\map{\textit{map}}

\def\rrexp{\textit{rrexp}}

\newcommand\rnullable[1]{\textit{rnullable} \; #1 }

\newcommand\rsize[1]{\llbracket #1 \rrbracket_r}

\newcommand\asize[1]{\llbracket #1 \rrbracket}

\newcommand\rerase[1]{ (#1)_{\downarrow_r}}

\newcommand\ChristianComment[1]{\textcolor{blue}{#1}\\}

\def\rflts{\textit{rflts}}

\def\rrewrite{\textit{rrewrite}}

\def\bsimpalts{\textit{bsimp}_{ALTS}}

\def\bsimpaseq{\textit{bsimp}_{ASEQ}}

\def\rsimlalts{\textit{rsimp}_{ALTs}}

\def\rsimpseq{\textit{rsimp}_{SEQ}}

\def\erase{\textit{erase}}

\def\STAR{\textit{STAR}}

\def\flts{\textit{flts}}

\def\zeroable{\textit{zeroable}}

\def\nub{\textit{nub}}

\def\filter{\textit{filter}}

%\def\not{\textit{not}}

\def\RZERO{\mathbf{0}_r }

\def\RONE{\mathbf{1}_r}

\newcommand\RCHAR[1]{\mathbf{#1}_r}

\newcommand\RSEQ[2]{#1 \cdot #2}

\newcommand\RALTS[1]{\sum #1}

\newcommand\RSTAR[1]{#1^*}

\newcommand\vsuf[2]{\textit{Suffix} \;#1\;#2}

\lstdefinestyle{myScalastyle}{

  frame=tb,

  language=scala,

  aboveskip=3mm,

  belowskip=3mm,

  showstringspaces=false,

  columns=flexible,

  basicstyle={\small\ttfamily},

  numbers=none,

  numberstyle=\tiny\color{gray},

  keywordstyle=\color{blue},

  commentstyle=\color{dkgreen},

  stringstyle=\color{mauve},

  frame=single,

  breaklines=true,

  breakatwhitespace=true,

  tabsize=3,

}

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

%This part is about regular expressions, Brzozowski derivatives,

%and a bit-coded lexing algorithm with proven correctness and time bounds.

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

Regular expressions are widely used in computer science: 

be it in text-editors \parencite{atomEditor} with syntax highlighting and auto-completion;

command-line tools like $\mathit{grep}$ that facilitate easy 

text-processing; network intrusion

detection systems that inspect suspicious traffic; or compiler

front ends.

Given their usefulness and ubiquity, one would assume that

modern regular expression matching implementations

are mature and fully studied.

Indeed, in a popular programming language's regex engine, 

supplying it with regular expressions and strings,

in most cases one can

get the matching information in a very short time.

Those matchers can be blindingly fast--some 

network intrusion detection systems

use regex engines that are able to process 

megabytes or even gigabytes of data per second \parencite{Turo_ov__2020}.

However, those matchers can exhibit a surprising security vulnerability

under a certain class of inputs.

%However, , this is not the case for $\mathbf{all}$ inputs.

%TODO: get source for SNORT/BRO's regex matching engine/speed

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

strings of the form $aa..a$ can be matched by 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. 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 an absurd time to finish (see graphs in figure \ref{fig:aStarStarb}).

This is clearly exponential behaviour, and 

is triggered by some relatively simple regular expressions.

Java 9 and newer

versions improve this behaviour somewhat, but is still slow compared 

with the approach we are going to use in this thesis.

This superlinear blowup in regular expression engines

had repeatedly 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 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. 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{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}\\ 

\multicolumn{2}{c}{Graphs}

\end{tabular}    

\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 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. 

}\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 occasionally, but actually widespread.

They occur so often that they have a 

name: Regular-Expression-Denial-Of-Service (ReDoS)

attack.

\citeauthor{Davis18} detected more

than 1000 evil regular expressions

in Node.js, Python core libraries, npm and in pypi. 

They therefore concluded that evil regular expressions

are real problems rather than "a parlour trick".

This work aims to address this issue

with the help of formal proofs.

We describe a lexing algorithm based

on Brzozowski derivatives with verified correctness (in 

Isabelle/HOL)

and a finiteness property.

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 of course 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

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

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 just 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:

\[

	[0~-9]\stackrel{means}{=} (0 | 1 | \ldots | 9 ) \; \text{(all number digits)}

\]