% 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)}

\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\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 reject suspicious traffic; or compiler

front ends--the majority of the solutions to these tasks 

involve lexing with regular 

expressions.

Given its usefulness and ubiquity, one would imagine 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

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, even with strings of a small

length, say around 30 $a$'s,

the decision takes crazy time to finish (graph \ref{fig:aStarStarb}).

This is clearly exponential behaviour, and 

is triggered by some relatively simple regex patterns.

Java 9 and newer

versions improves this behaviour, but is still slow compared 

with the approach we are going to use.

This superlinear blowup in regular expression engines

had repeatedly caused grief in real life that they

get a name for them--``catastrophic backtracking''.

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@{\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}

  & \\

\multicolumn{3}{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.

   If the string does not match, the 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 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/}(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 get a 

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

attack.

\citeauthor{Davis18} detected more

than 1000 super-linear (SL) regular expressions

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

They therefore concluded that evil regular expressions

are problems "more than a parlour trick", but one that

requires

more research attention.

This work aims to address this issue

with the help of formal proofs.

We offer a lexing algorithm based

on Brzozowski derivatives with certified correctness (in 

Isabelle/HOL)

and finiteness property.

Such properties guarantee the absence of