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

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

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

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

text processing , network intrusion

detection systems that rejects suspicious traffic, or compiler

Given its usefulness and ubiquity, one would imagine that

modern regular expression matching implementations

are mature and fully-studied.

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.

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

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 are

blindingly fast already? Well it turns out it is not always the case.

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.

This superlinear blowup in matching algorithms sometimes cause

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 a $\mathit{DoS}$ 

attack and therefore stopped the servers from responding to any

requests. This made the whole site become unavailable. 

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

%TODO: data points for some new versions of languages

These problems with regular expressions 

are not isolated events that happen

very occasionally, but actually quite widespread.

They occur so often that they get a 

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

attack.

Davis et al. \parencite{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.

 \section{Why are current algorithm for regexes slow?}

%find literature/find out for yourself that REGEX->DFA on basic regexes

%does not blow up the size

Shouldn't regular expression matching be linear?

How can one explain the super-linear behaviour of the 

regex matching engines we have?

The time cost of regex matching algorithms in general

involve two phases: 

the construction phase, in which the algorithm builds some  

suitable data structure from the input regex $r$, we denote

the time cost by $P_1(r)$.

The lexing

phase, when the input string $s$ is read and the data structure

representing that regex $r$ is being operated on. We represent the time

it takes by $P_2(r, s)$.\\

In the case of a $\mathit{DFA}$,

we have $P_2(r, s) = O( |s| )$,

because we take at most $|s|$ steps, 

and each step takes

at most one transition--

a deterministic-finite-automata

by definition has at most one state active and at most one

transition upon receiving an input symbol.

But unfortunately in the  worst case

$P_1(r) = O(exp^{|r|})$. An example will be given later. \\

For $\mathit{NFA}$s, we have $P_1(r) = O(|r|)$ if we do not unfold 

expressions like $r^n$ into $\underbrace{r \cdots r}_{\text{n copies of r}}$.

The $P_2(r, s)$ is bounded by $|r|\cdot|s|$, if we do not backtrack.

On the other hand, if backtracking is used, the worst-case time bound bloats

to $|r| * 2^|s|$ .

%on the input

%And when calculating the time complexity of the matching algorithm,

%we are assuming that each input reading step requires constant time.

%which translates to that the number of 

%states active and transitions taken each time is bounded by a

%constant $C$.

%But modern  regex libraries in popular language engines

% often want to support much richer constructs than just

% sequences and Kleene stars,

%such as negation, intersection, 

%bounded repetitions and back-references.

%And de-sugaring these "extended" regular expressions 

%into basic ones might bloat the size exponentially.

%TODO: more reference for exponential size blowup on desugaring. 

\subsection{Tools that uses $\mathit{DFA}$s}

%TODO:more tools that use DFAs?

$\mathit{LEX}$ and $\mathit{JFLEX}$ are tools

in $C$ and $\mathit{JAVA}$ that generates $\mathit{DFA}$-based

lexers. The user provides a set of regular expressions

and configurations to such lexer generators, and then 

gets an output program encoding a minimized $\mathit{DFA}$

that can be compiled and run. 

The good things about $\mathit{DFA}$s is that once

generated, they are fast and stable, unlike

backtracking algorithms. 

However, they do not scale well with bounded repetitions.\\

Bounded repetitions, usually written in the form

$r^{\{c\}}$ (where $c$ is a constant natural number),

denotes a regular expression accepting strings

that can be divided into $c$ substrings, where each 

substring is in $r$. 

For the regular expression $(a|b)^*a(a|b)^{\{2\}}$,

an $\mathit{NFA}$ describing it would look like:

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

The red states are "countdown states" which counts 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 

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

$q_3$ is the last state, requiring 0 more character and is accepting.

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, independent from each other.

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$ contains

more than 1 string.

This is to represent all different 

scenarios which "countdown" states are active.

For those regexes, tools such as $\mathit{JFLEX}$ 

would generate gigantic $\mathit{DFA}$'s or

out of memory errors.

For this reason, regex libraries that support 

bounded repetitions often choose to use the $\mathit{NFA}$ 

approach.

\subsection{The $\mathit{NFA}$ approach to regex matching}

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.

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

The other way to use $\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 a lot of cases, but could end up

with exponential run time.\\

%TODO:COMPARE java python lexer speed with Rust and Go

The reason behind backtracking algorithms in languages like

Java and Python is that they support back-references.

\subsection{Back References in Regex--Non-Regular part}

If we have a regular expression like this (the sequence

operator is omitted for brevity):

\begin{center}

	$r_1(r_2(r_3r_4))$

\end{center}

We could label sub-expressions of interest 

by parenthesizing them and giving 

them a number by the order in which their opening parentheses appear.

One possible way of parenthesizing and labelling is given below:

\begin{center}

	$\underset{1}{(}r_1\underset{2}{(}r_2\underset{3}{(}r_3)\underset{4}{(}r_4)))$

\end{center}

$r_1r_2r_3r_4$, $r_1r_2r_3$, $r_3$, $r_4$ are labelled

by 1 to 4. $1$ would refer to the entire expression 

$(r_1(r_2(r_3)(r_4)))$, $2$ referring to $r_2(r_3)(r_4)$, etc.

These sub-expressions are called "capturing groups".

We can use the following syntax to denote that we want a string just matched by a 

sub-expression (capturing group) to appear at a certain location again, 

exactly as it was:

\begin{center}

$\ldots\underset{\text{i-th lparen}}{(}{r_i})\ldots 

\underset{s_i \text{ which just matched} \;r_i}{\backslash i}$

\end{center}

The backslash and number $i$ are used to denote such 

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}

The concrete example

$((a|b|c|\ldots|z)^*)\backslash 1$

would match the string like $\mathit{bobo}$, $\mathit{weewee}$ and etc.\\

Back-reference is a construct in the "regex" standard

that programmers found quite useful, but not exactly 

regular any more.

In fact, that allows 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\parencite{campeanu2003formal}.

Such a language is contained in the context-sensitive hierarchy

of formal languages. 

Solving the back-reference expressions matching problem

is NP-complete\parencite{alfred2014algorithms} and a non-bactracking,

efficient solution is not known to exist.

%TODO:read a bit more about back reference algorithms

It seems that languages like Java and Python made the trade-off

to support back-references at the expense of having to backtrack,

even in the case of regexes not involving back-references.\\

Summing these up, we can categorise existing 

practical regex libraries into the ones  with  linear

time guarantees like Go and Rust, which impose restrictions

on the user input (not allowing back-references, 

bounded repetitions canno exceed 1000 etc.), and ones  

 that allows the programmer much freedom, but grinds to a halt

 in some non-negligible portion of cases.

 %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?

\section{Buggy Regex Engines} 

 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.

It turns out that regex libraries not only suffer from 

exponential backtracking problems, 

but also undesired (or even buggy) outputs.

%TODO: comment from who

Kuklewicz\parencite{KuklewiczHaskell} commented that most regex libraries are not

correctly implementing the POSIX (maximum-munch)

rule of regular expression matching.

This experience is echoed by the writer's

tryout of a few online regex testers:

A concrete example would be 

the regex

\begin{verbatim}

(((((a*a*)b*)b){20})*)c

\end{verbatim}

and the string

\begin{verbatim}

baabaabababaabaaaaaaaaababaa

aababababaaaabaaabaaaaaabaab

aabababaababaaaaaaaaababaaaa

babababaaaaaaaaaaaaac

\end{verbatim}

This seemingly complex regex simply says "some $a$'s

followed by some $b$'s then followed by 1 single $b$,

and this iterates 20 times, finally followed by a $c$.

And a POSIX match would involve the entire string,"eating up"

all the $b$'s in it.

%TODO: give a coloured example of how this matches POSIXly

This regex would trigger catastrophic backtracking in 

languages like Python and Java,

whereas it gives a non-POSIX  and uninformative 

match in languages like Go or .NET--The match with only 

character $c$.

As Grathwohl\parencite{grathwohl2014crash} commented,

\begin{center}

	``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{center}

%\section{How people solve problems with regexes}

When a regular expression does not behave as intended,

people usually try to rewrite the regex to some equivalent form

or they try to avoid the possibly problematic patterns completely\parencite{Davis18},

of which there are many false positives.

Animated tools to "debug" regular expressions

are also quite popular, regexploit\parencite{regexploit2021}, regex101\parencite{regex101} 

to name a few.

There is also static analysis work on regular expressions that

aims to detect potentially expoential regex patterns. Rathnayake and Thielecke 

\parencite{Rathnayake2014StaticAF} proposed an algorithm

that detects regular expressions triggering exponential

behavious on backtracking matchers.

Weideman \parencite{Weideman2017Static} came up with 

non-linear polynomial worst-time estimates

for regexes, attack string that exploit the worst-time 

scenario, and "attack automata" that generates

attack strings.

%Arguably these methods limits the programmers' freedom

%or productivity when all they want is to come up with a regex

%that solves the text processing problem.

%TODO:also the regex101 debugger

\section{Our Solution--Formal Specification of POSIX and Brzozowski Derivatives}

 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?