% !TEX program = pfdlatex
\documentclass{article}
\usepackage{url}
\usepackage{color}\definecolor{darkblue}{rgb}{0,0,0.5}
\usepackage[a4paper,colorlinks=true,linkcolor=darkblue,citecolor=darkblue,filecolor=darkblue,pagecolor=darkblue,urlcolor=darkblue]{hyperref}
\usepackage{style}
%\usepackage{langs}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{pgfplots}
\usepackage{stackengine}
\addtolength{\oddsidemargin}{-6mm}
\addtolength{\evensidemargin}{-6mm}
\addtolength{\textwidth}{12mm}
%% \usepackage{accents}
\newcommand\barbelow[1]{\stackunbder[1.2pt]{#1}{\raisebox{-4mm}{\boldmath$\uparrow$}}}
\begin{filecontents}{re-python2.data}
1 0.033
5 0.036
10 0.034
15 0.036
18 0.059
19 0.084
20 0.141
21 0.248
22 0.485
23 0.878
24 1.71
25 3.40
26 7.08
27 14.12
28 26.69
\end{filecontents}
\begin{filecontents}{re-java.data}
5 0.00298
10 0.00418
15 0.00996
16 0.01710
17 0.03492
18 0.03303
19 0.05084
20 0.10177
21 0.19960
22 0.41159
23 0.82234
24 1.70251
25 3.36112
26 6.63998
27 13.35120
28 29.81185
\end{filecontents}
\begin{filecontents}{re-java9.data}
1000 0.01410
2000 0.04882
3000 0.10609
4000 0.17456
5000 0.27530
6000 0.41116
7000 0.53741
8000 0.70261
9000 0.93981
10000 0.97419
11000 1.28697
12000 1.51387
14000 2.07079
16000 2.69846
20000 4.41823
24000 6.46077
26000 7.64373
30000 9.99446
34000 12.966885
38000 16.281621
42000 19.180228
46000 21.984721
50000 26.950203
60000 43.0327746
\end{filecontents}
\begin{document}
\section*{PPProposal: \\
Fast Regular Expression Matching\\
with Brzozowski bderivatives}
\subsubsection*{Summary}
If you want to connect a computer directly to the Internet, it must be
immediately \mbox{hardened} against outside attacks. The current
technology for this is to use regular expressions in order to
automatically scan all incoming network traffic for signs when a
computer is under attack and if found, to take appropriate
counter-actions. One possible action could be to slow down the traffic
from sites where repeated password-guesses originate. Well-known
network intrusion prevention systems that use regular expressions for
traffic analysis are Snort and Bro.
Given the large volume of Internet traffic even the smallest servers
can handle nowadays, the regular expressions for traffic analysis have
become a real bottleneck. This is not just a nuisance, but actually a
security vulnerability in itself: it can lead to denial-of-service
attacks. The proposed project aims to remove this bottleneck by using
a little-known technique of building bderivatives of regular
expressions. These derivatives have not yet been used in the area of
network traffic analysis, but have the potential to solve some
tenacious problems with existing approaches. The project will require
theoretical work, but also a practical implementation (a
proof-of-concept at least). The work will build on earlier work by
Ausaf and Urban from King's College London
\cite{AusafDyckhoffUrban2016}.
\subsubsection*{Background}
If every 10 minutes a thief turned up at your car and rattled
violently at the doorhandles to see if he could get in, you would move
your car to a safer neighbourhood. Computers, however, need to stay
connected to the Internet all the time and there they have to withstand such
attacks. A rather typical instance of an attack can be seen in the
following log entries from a server at King's:
{\small
\begin{verbatim}
Jan 2 00:53:19 talisker sshd: Received disconnect from 110.53.183.227: [preauth]
Jan 2 00:58:31 talisker sshd: Received disconnect from 110.53.183.252: [preauth]
Jan 2 01:01:28 talisker sshd: Received disconnect from 221.194.47.236: [preauth]
Jan 2 01:03:59 talisker sshd: Received disconnect from 110.53.183.228: [preauth]
Jan 2 01:06:53 talisker sshd: Received disconnect from 221.194.47.245: [preauth]
...
\end{verbatim}}
\noindent
This is a record of the network activities from the server
\href{http://talisker.inf.kcl.ac.uk/cgi-bin/repos.cgi}{talisker.inf.kcl.ac.uk},
which hosts lecture material for students. The log indicates several
unsuccessful login attempts via the \texttt{ssh} program from
computers with the addresses \texttt{110.53.183.227} and so on. This
is a clear sign of a \emph{brute-force attack} where hackers
systematically try out password candidates. Such attacks are blunt,
but unfortunately very powerful. They can originate from anywhere in
the World; they are automated and often conducted from computers that
have been previously hijacked. Once the attacker ``hits'' on the
correct password, then he or she gets access to the server. The only
way to prevent this methodical password-guessing is to spot the
corresponding traces in the log and then slow down the traffic from
such sites in a way that perhaps only one password per hour can be
tried out. This does not affect ``normal'' operations of the server,
but drastically decreases the chances of hitting the correct password
by a brute-force attack.
Server administrators use \emph{regular expressions} for scanning log
files. The purpose of these expressions is to specify patterns of
interest (for example \texttt{Received disconnect from 110.53.183.227}
where the address needs to be variable). A program will
then continuously scan for such patterns and trigger an action if a
pattern is found. Popular examples of such programs are Snort and Bro
\cite{snort,bro}. Clearly, there are also other kinds of
vulnerabilities hackers try to take advantage of---mainly programming
mistakes that can be abused to gain access to a computer. This means
server administrators have a suite of sometimes thousands of regular
expressions, all prescribing some suspicious pattern for when a
computer is unbder attack.
The unbderlying algorithmic problem is to decide whether a string in
the logs matches the patterns determined by the regular
expressions. Such decisions need to be done as fast as possible,
otherwise the scanning programs would not be useful as a hardening
technique for servers. The quest for speed with these decisions is
presently a rather big challenge for the amount of traffic typical
servers have to cope with and the large number of patterns that might
be of interest. The problem is that when thousands of regular
expressions are involved, the process of detecting whether a string
matches a regular expression can be excruciating slow. This might not
happen in most instances, but in some small number of
instances. However in these small number of instances the algorithm
for regular expression matching can grind to a halt. This phenomenon
is called \emph{catastrophic backtracking} \cite{catast}.
Unfortunately, catastrophic backtracking is not just a nuisance, but a
security vulnerability in itself. The reason is that attackers look
for these instances where the scan is very slow and then trigger a
\emph{denial-of-service attack} against the server\ldots meaning the
server will not be reachable anymore to normal users.
Existing approaches try to mitigate the speed problem with regular
expressions by implementing the matching algorithms in hardware,
rather than in software \cite{hardware}. Although this solution offers
speed, it is often unappealing because attack patterns can change or
need to be augmented. A software solution is clearly more desirable in
these circumstances. Also given that regular expressions were
introduced in 1950 by Kleene, one might think regular expressions have
since been studied and implemented to death. But this would definitely
be a mistake: in fact they are still an active research area and
off-the-shelf implementations are still extremely prone to the
problem of catastrophic backtracking. This can be seen in the
following two graphs:
\begin{center}
\begin{tabular}{@{}cc@{}}
%\multicolumn{2}{c}{Graph: $(a^*)^*\cdot b$ and strings
% $\unbderbrace{a\ldots a}_{n}$}\smallskip\\
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,0.0)}},
ylabel={time in secs},
y label style={at={(0.06,0.5)}},
enlargelimits=false,
xtick={0,5,...,30},
xmax=33,
ymax=45,
ytick={0,10,...,40},
scaled ticks=false,
axis lines=left,
width=6cm,
height=4.5cm,
legend entries={Python, Java 8},
legend pos=north west]
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
\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.0)}},
ylabel={time in secs},
y label style={at={(0.06,0.5)}},
%enlargelimits=false,
%xtick={0,5000,...,30000},
xmax=65000,
ymax=45,
ytick={0,10,...,40},
scaled ticks=false,
axis lines=left,
width=6cm,
height=4.5cm,
legend entries={Java 9},
legend pos=north west]
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java9.data};
\end{axis}
\end{tikzpicture}
\end{tabular}
\end{center}
\noindent
These graphs show how long strings can be when using the rather simple
regular expression $(a^*)^* \,b$ and the built-in regular expression
matchers in the popular programming languages Python and Java (Version
8 and Version 9). There are many more regular expressions that show
the same behaviour. On the left-hand side the graphs show that for a
string consisting of just 28 $a\,$'s, Python and the olbder Java (which
was the latest version of Java until September 2017) already need 30
seconds to decide whether this string is matched or not. This is an
abysmal result given that Python and Java are very popular programming
languages. We already know that this problem can be decided much, much
faster. If these slow regular expression matchers would be employed
in network traffic analysis, then this example is already an
opportunity for mounting an easy denial-of-service attack: one just
has to send to the server a large enough string of a's. The newer
version of Java is better---it can match strings of around 50,000
$a\,$'s in 30 seconds---however this would still not be good enough
for being a useful tool for network traffic analysis. What is
interesting is that even a relatively simple-minded regular expression
matcher based on Brzozowski bderivatives can out-compete the regular
expressions matchers in Java and Python on such catastrophic
backtracking examples. This gain in speed is the motivation and
starting point for the proposed project. \smallskip
\subsection*{Research Plan}
Regular expressions are already an old and well-studied topic in
Computer Science. They were originally introduced by Kleene in 1951
and are utilised in text search algorithms for ``find'' or ``find and
replace'' operations \cite{Brian,Kleene51}. Because of their wide
range of applications, many programming languages provide capabilities
for regular expression matching via libraries. The classic theory
of regular expressions involves just 6 different kinds of regular
expressions, often defined in terms of the following grammar:
\begin{center}\small
\begin{tabular}{lcll}
$r$ & $::=$ & $\ZERO$ & cannot match anything\\
& $|$ & $\ONE$ & can only match the empty string\\
& $|$ & $c$ & can match a single character (in this case $c$)\\
& $|$ & $r_1 + r_2$ & can match a string either with $r_1$ or with $r_2$\\
& $|$ & $r_1\cdot r_2$ & can match the first part of a string with $r_1$ and\\
& & & then the second part with $r_2$\\
& $|$ & $r^*$ & can match zero or more times $r$\\
\end{tabular}
\end{center}
\noindent
For practical purposes, however, regular expressions have been
extended in various ways in orbder to make them even more powerful and
even more useful for applications. Some of the problems to do with
catastrophic backtracking stem, unfortunately, from these extensions.
The crux in this project is to not use automata for regular expression
matching (the traditional technique), but to use bderivatives of
regular expressions instead. These bderivatives were introduced by
Brzozowski in 1964 \cite{Brzozowski1964}, but somehow had been lost
``in the sands of time'' \cite{Owens2009}. However, they recently have
become again a ``hot'' research topic with numerous research papers
appearing in the last five years. One reason for this interest is that
Brzozowski bderivatives straightforwardly extend to more general
regular expression constructors, which cannot be easily treated with
standard techniques. They can also be implemented with ease in any
functional programming language: the definition for bderivatives
consists of just two simple recursive functions shown in
Figure~\ref{f}. Moreover, it can be easily shown (by a mathematical
proof) that the resulting regular matcher is in fact always producing
a correct answer. This is an area where Urban can provide a lot of
expertise for this project: he is one of the main developers of the
Isabelle theorem prover, which is a program designed for such proofs
\cite{Isabelle}.
\begin{figure}[t]
\begin{center}\small
\begin{tabular}{lcl}
$\textit{nullable}(\ZERO)$ & $\dn$ & $\textit{false}$\\
$\textit{nullable}(\ONE)$ & $\dn$ & $\textit{true}$\\
$\textit{nullable}(c)$ & $\dn$ & $\textit{false}$\\
$\textit{nullable}(r_1 + r_2)$ & $\dn$ & $\textit{nullable}(r_1) \vee \textit{nullable}(r_2)$\\
$\textit{nullable}(r_1 \cdot r_2)$ & $\dn$ & $\textit{nullable}(r_1) \wedge \textit{nullable}(r_2)$\\
$\textit{nullable}(r^*)$ & $\dn$ & $\textit{true}$\medskip\\
$\textit{bder}\;c\;(\ZERO)$ & $\dn$ & $\ZERO$\\
$\textit{bder}\;c\;(\ONE)$ & $\dn$ & $\ZERO$\\
$\textit{bder}\;c\;(d)$ & $\dn$ & $\textit{if}\; c = d\;\textit{then} \;\ONE \; \textit{else} \;\ZERO$\\
$\textit{bder}\;c\;(r_1 + r_2)$ & $\dn$ & $(\textit{bder}\;c\;r_1) + (\textit{bder}\;c\;r_2)$\\
$\textit{bder}\;c\;(r_1 \cdot r_2)$ & $\dn$ & $\textit{if}\;\textit{nullable}(r_1)$\\
& & $\textit{then}\;((\textit{bder}\;c\;r_1)\cdot r_2) + (\textit{bder}\;c\;r_2)$\\
& & $\textit{else}\;(\textit{bder}\;c\;r_1)\cdot r_2$\\
$\textit{bder}\;c\;(r^*)$ & $\dn$ & $(\textit{bder}\;c\;r)\cdot (r^*)$\\[-5mm]
\end{tabular}
\end{center}
\caption{The complete definition of bderivatives of regular expressions
\cite{Brzozowski1964}.
This definition can be implemented with ease in functional programming languages and can be easily extended to regular expressions used in practice.
The are more flexible for applications and easier to manipulate in
mathematical proofs, than traditional techniques for regular expression
matching.\medskip\label{f}}
\end{figure}
There are a number of avenues for research on Brzozowski bderivatives.
One problem I like to immediately tackle in this project is how to
handle \emph{back-references} in regular expressions. It is known that
the inclusion of back-references causes the unbderlying algorithmic
problem to become NP-hard \cite{Aho}, and is the main reason why
regular expression matchers suffer from the catastrophic backtracking
problem. However, the full generality of back-references are not
needed in practical applications. The goal therefore is to sufficiently
restrict the problem so that an efficient algorithm can be
designed. There seem to be good indications that Brzozowski
bderivatives are useful for that.
Another problem is \emph{how} regular expressions match a string
\cite{Sulzmann2014}. In this case the algorithm does not just give a
yes/no answer about whether the regular expression matches the string,
but also generates a value that encodes which part of the string is
matched by which part of the regular expression. This is important in
applications, like network analysis where from a matching log entry a
specific computer address needs to be extracted. Also compilers make
extensive use of such an extension when they lex their source
programs, i.e.~break up code into word-like components. Again Ausaf
and Urban from King's made some initial progress about proving the
correctness of such an extension, but their algorithm is not yet fast
enough for practical purposes \cite{AusafDyckhoffUrban2016}. It would
be desirable to study optimisations that make the algorithm faster,
but preserve the correctness guaranties obtained by Ausaf and Urban.
\mbox{}\\[-11mm]
\subsubsection*{Conclusion}
Much research has already gone into regular expressions, and one might
think they have been studied and implemented to death. But this is far
from the truth. In fact regular expressions have become a ``hot''
research topic in recent years because of problems with the
traditional methods (in applications such as network traffic
analysis), but also because the technique of bderivatives of regular
expression has been re-discovered. These bderivatives provide an
alternative approach to regular expression matching. Their potential
lies in the fact that they are more flexible in implementations and
much easier to manipulate in mathematical proofs. Therefore I like to
research them in this project.\medskip
\noindent {\bf Impact:} Regular expression matching is a core
technology in Computer Science with numerous applications. I will
focus on the area of network traffic analysis and also lexical
analysis. In these areas this project can have a quite large impact:
for example the program Bro has been downloaded at least 10,000 times and Snort
even has 5 million downloads and over 600,000 registered users
\cite{snort,bro}. Lexical analysis is a core component in every
compiler, which are the bedrock on which nearly all programming is
built on.
% {\small
% \begin{itemize}
% \item[$\bullet$] \url{http://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}
% \item[$\bullet$] \url{https://vimeo.com/112065252}
% \item[$\bullet$] \url{http://davidvgalbraith.com/how-i-fixed-atom/}
% \end{itemize}}
\mbox{}\\[-11mm]
\small
\bibliographystyle{plain}
\renewcommand{\refname}{References\\[-7mm]\mbox{}}
\bibliography{proposal}
\newpage
\begin{center}\small
\begin{tabular}{lcl}
$\textit{bder}\;c\;_{[]}(\ZERO)$ & $\dn$ & $_{[]}\ZERO$\\
$\textit{bder}\;c\;_{bs}(\ONE)$ & $\dn$ & $_{[]}\ZERO$\\
$\textit{bder}\;c\;_{bs}(d)$ & $\dn$ & $\textit{if}\; c = d\;\textit{then} \;_{bs}\ONE \; \textit{else} \;_{[]}\ZERO$\\
$\textit{bder}\;c\;_{bs}(r_1 + r_2)$ & $\dn$ & $_{bs}(\textit{bder}\;c\;r_1 + \textit{bder}\;c\;r_2)$\\
$\textit{bder}\;c\;_{bs}(r_1 \cdot r_2)$ & $\dn$ & $\textit{if}\;\textit{nullable}(r_1)$\\
& & $\textit{then}\;_{bs}(_{[]}(\textit{bder}\;c\;r_1)\cdot r_2) + (_{\textit{bmkeps}\,r_1\rightarrow}\textit{bder}\;c\;r_2)$\\
& & $\textit{else}\;_{bs}(\textit{bder}\;c\;r_1)\cdot r_2$\\
$\textit{bder}\;c\;_{bs}(r^*)$ & $\dn$ & $_{bs}(_{0\rightarrow}\textit{bder}\;c\;r)\cdot (r^*)$\\[-5mm]
\end{tabular}
\end{center}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: