diff -r 599239394c51 -r a0f27e21b42c ChengsongTanPhdThesis/main.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ChengsongTanPhdThesis/main.tex Fri Mar 25 21:49:53 2022 +0000 @@ -0,0 +1,359 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Masters/Doctoral Thesis +% LaTeX Template +% Version 2.5 (27/8/17) +% +% This template was downloaded from: +% http://www.LaTeXTemplates.com +% +% Version 2.x major modifications by: +% Vel (vel@latextemplates.com) +% +% This template is based on a template by: +% Steve Gunn (http://users.ecs.soton.ac.uk/srg/softwaretools/document/templates/) +% Sunil Patel (http://www.sunilpatel.co.uk/thesis-template/) +% +% Template license: +% CC BY-NC-SA 3.0 (http://creativecommons.org/licenses/by-nc-sa/3.0/) +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%---------------------------------------------------------------------------------------- +% PACKAGES AND OTHER DOCUMENT CONFIGURATIONS +%---------------------------------------------------------------------------------------- + +\documentclass[ +11pt, % The default document font size, options: 10pt, 11pt, 12pt +%oneside, % Two side (alternating margins) for binding by default, uncomment to switch to one side +english, % ngerman for German +singlespacing, % Single line spacing, alternatives: onehalfspacing or doublespacing +%draft, % Uncomment to enable draft mode (no pictures, no links, overfull hboxes indicated) +%nolistspacing, % If the document is onehalfspacing or doublespacing, uncomment this to set spacing in lists to single +%liststotoc, % Uncomment to add the list of figures/tables/etc to the table of contents +%toctotoc, % Uncomment to add the main table of contents to the table of contents +%parskip, % Uncomment to add space between paragraphs +%nohyperref, % Uncomment to not load the hyperref package +headsepline, % Uncomment to get a line under the header +%chapterinoneline, % Uncomment to place the chapter title next to the number on one line +%consistentlayout, % Uncomment to change the layout of the declaration, abstract and acknowledgements pages to match the default layout +]{MastersDoctoralThesis} % The class file specifying the document structure + +\usepackage[utf8]{inputenc} % Required for inputting international characters +\usepackage[T1]{fontenc} % Output font encoding for international characters + +\usepackage{mathpazo} % Use the Palatino font by default +\usepackage{hyperref} +\usepackage[backend=bibtex,style=authoryear,natbib=true]{biblatex} % Use the bibtex backend with the authoryear citation style (which resembles APA) + +\addbibresource{example.bib} % The filename of the bibliography + +\usepackage[autostyle=true]{csquotes} % Required to generate language-dependent quotes in the bibliography + +%My Newly added Libraries in addition to template +\usepackage{graphic} +\usepackage{data} + +%\usepackage{algorithm} +\usepackage{amsmath} +\usepackage[noend]{algpseudocode} +\usepackage{enumitem} +\usepackage{nccmath} +\usepackage{tikz-cd} +\usepackage{tikz} +\usetikzlibrary{automata, positioning} + +%---------------------------------------------------------------------------------------- +% MARGIN SETTINGS +%---------------------------------------------------------------------------------------- + +\geometry{ + paper=a4paper, % Change to letterpaper for US letter + inner=2.5cm, % Inner margin + outer=3.8cm, % Outer margin + bindingoffset=.5cm, % Binding offset + top=1.5cm, % Top margin + bottom=1.5cm, % Bottom margin + %showframe, % Uncomment to show how the type block is set on the page +} + +%---------------------------------------------------------------------------------------- +% THESIS INFORMATION +%---------------------------------------------------------------------------------------- + +\thesistitle{POSIX Regular Expression Matching and Lexing} % Your thesis title, this is used in the title and abstract, print it elsewhere with \ttitle +\supervisor{Dr. Christian \textsc{Urban}} % Your supervisor's name, this is used in the title page, print it elsewhere with \supname +\examiner{} % Your examiner's name, this is not currently used anywhere in the template, print it elsewhere with \examname +\degree{Doctor of Philosophy} % Your degree name, this is used in the title page and abstract, print it elsewhere with \degreename +\author{Chengsong \textsc{Tan}} % Your name, this is used in the title page and abstract, print it elsewhere with \authorname +\addresses{} % Your address, this is not currently used anywhere in the template, print it elsewhere with \addressname + +\subject{Computer Science} % Your subject area, this is not currently used anywhere in the template, print it elsewhere with \subjectname +\keywords{} % Keywords for your thesis, this is not currently used anywhere in the template, print it elsewhere with \keywordnames +\university{\href{https://www.kcl.ac.uk}{King's College London}} % Your university's name and URL, this is used in the title page and abstract, print it elsewhere with \univname +\department{\href{https://www.kcl.ac.uk/informatics}{Department or Informatics}} % Your department's name and URL, this is used in the title page and abstract, print it elsewhere with \deptname +\group{\href{https://www.kcl.ac.uk/research/ssy}{Software Systems}} % Your research group's name and URL, this is used in the title page, print it elsewhere with \groupname +\faculty{\href{http://faculty.university.com}{Chengsong Tan}} % Your faculty's name and URL, this is used in the title page and abstract, print it elsewhere with \facname + +\AtBeginDocument{ +\hypersetup{pdftitle=\ttitle} % Set the PDF's title to your title +\hypersetup{pdfauthor=\authorname} % Set the PDF's author to your name +\hypersetup{pdfkeywords=\keywordnames} % Set the PDF's keywords to your keywords +} + +\begin{document} + +\frontmatter % Use roman page numbering style (i, ii, iii, iv...) for the pre-content pages + +\pagestyle{plain} % Default to the plain heading style until the thesis style is called for the body content + +%---------------------------------------------------------------------------------------- +% TITLE PAGE +%---------------------------------------------------------------------------------------- + +\begin{titlepage} +\begin{center} + +\vspace*{.06\textheight} +{\scshape\LARGE \univname\par}\vspace{1.5cm} % University name +\textsc{\Large Doctoral Thesis}\\[0.5cm] % Thesis type + +\HRule \\[0.4cm] % Horizontal line +{\huge \bfseries \ttitle\par}\vspace{0.4cm} % Thesis title +\HRule \\[1.5cm] % Horizontal line + +\begin{minipage}[t]{0.4\textwidth} +\begin{flushleft} \large +\emph{Author:}\\ +\href{https://kclpure.kcl.ac.uk/portal/en/persons/chengsong-tan(a63b381b-04bc-4cd7-beea-beb3e96cb153).html}{\authorname} % Author name - remove the \href bracket to remove the link +\end{flushleft} +\end{minipage} + + +\begin{minipage}[t]{0.4\textwidth} +\begin{flushright} \large +\emph{Supervisor:} \\ +\href{https://www.kcl.ac.uk/people/christian-urban}{\supname} % Supervisor name - remove the \href bracket to remove the link +\end{flushright} +\end{minipage}\\[3cm] + +\vfill + +\large \textit{A thesis submitted in fulfillment of the requirements\\ for the degree of \degreename}\\[0.3cm] % University requirement text +\textit{in the}\\[0.4cm] +\groupname\\\deptname\\[2cm] % Research group name and department name + +\vfill + +{\large \today}\\[4cm] % Date +%\includegraphics{Logo} % University/department logo - uncomment to place it + +\vfill +\end{center} +\end{titlepage} + +%---------------------------------------------------------------------------------------- +% DECLARATION PAGE +%---------------------------------------------------------------------------------------- + +\begin{declaration} +\addchaptertocentry{\authorshipname} % Add the declaration to the table of contents +\noindent I, \authorname, declare that this thesis titled, \enquote{\ttitle} and the work presented in it are my own. I confirm that: + +\begin{itemize} +\item This work was done wholly or mainly while in candidature for a research degree at this University. +\item Where any part of this thesis has previously been submitted for a degree or any other qualification at this University or any other institution, this has been clearly stated. +\item Where I have consulted the published work of others, this is always clearly attributed. +\item Where I have quoted from the work of others, the source is always given. With the exception of such quotations, this thesis is entirely my own work. +\item I have acknowledged all main sources of help. +\item Where the thesis is based on work done by myself jointly with others, I have made clear exactly what was done by others and what I have contributed myself.\\ +\end{itemize} + +\noindent Signed:\\ +\rule[0.5em]{25em}{0.5pt} % This prints a line for the signature + +\noindent Date:\\ +\rule[0.5em]{25em}{0.5pt} % This prints a line to write the date +\end{declaration} + +\cleardoublepage + +%---------------------------------------------------------------------------------------- +% QUOTATION PAGE +%---------------------------------------------------------------------------------------- + +\vspace*{0.2\textheight} + +\noindent\enquote{\itshape Thanks to my solid academic training, today I can write hundreds of words on virtually any topic without possessing a shred of information, which is how I got a good job in journalism.}\bigbreak + +\hfill Dave Barry + +%---------------------------------------------------------------------------------------- +% ABSTRACT PAGE +%---------------------------------------------------------------------------------------- + +\begin{abstract} +\addchaptertocentry{\abstractname} % Add the abstract to the table of contents +This work is a combination of functional algorithms +and formal methods. +Regular expression matching and lexing has been + widely-used and well-implemented +in software industry. + +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. + + +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. + +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. +The result is an algorithm with provable guarantees on +correctness and running time. We believe this is the first +work with these two guarantees together. + + + +\end{abstract} + +%---------------------------------------------------------------------------------------- +% ACKNOWLEDGEMENTS +%---------------------------------------------------------------------------------------- + +\begin{acknowledgements} +\addchaptertocentry{\acknowledgementname} % Add the acknowledgements to the table of contents +The acknowledgments and the people to thank go here, don't forget to include your project advisor\ldots +\end{acknowledgements} + +%---------------------------------------------------------------------------------------- +% LIST OF CONTENTS/FIGURES/TABLES PAGES +%---------------------------------------------------------------------------------------- + +\tableofcontents % Prints the main table of contents + +\listoffigures % Prints the list of figures + +\listoftables % Prints the list of tables + +%---------------------------------------------------------------------------------------- +% ABBREVIATIONS +%---------------------------------------------------------------------------------------- + +\begin{abbreviations}{ll} % Include a list of abbreviations (a table of two columns) + +\textbf{LAH} & \textbf{L}ist \textbf{A}bbreviations \textbf{H}ere\\ +\textbf{WSF} & \textbf{W}hat (it) \textbf{S}tands \textbf{F}or\\ + +\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} + +\end{abbreviations} + +%---------------------------------------------------------------------------------------- +% PHYSICAL CONSTANTS/OTHER DEFINITIONS +%---------------------------------------------------------------------------------------- + +\begin{constants}{lr@{${}={}$}l} % The list of physical constants is a three column table + +% The \SI{}{} command is provided by the siunitx package, see its documentation for instructions on how to use it + +Speed of Light & $c_{0}$ & \SI{2.99792458e8}{\meter\per\second} (exact)\\ +%Constant Name & $Symbol$ & $Constant Value$ with units\\ + +\end{constants} + +%---------------------------------------------------------------------------------------- +% SYMBOLS +%---------------------------------------------------------------------------------------- + +\begin{symbols}{lll} % Include a list of Symbols (a three column table) + +$a$ & distance & \si{\meter} \\ +$P$ & power & \si{\watt} (\si{\joule\per\second}) \\ +%Symbol & Name & Unit \\ + +\addlinespace % Gap to separate the Roman symbols from the Greek + +$\omega$ & angular frequency & \si{\radian} \\ + +\end{symbols} + +%---------------------------------------------------------------------------------------- +% DEDICATION +%---------------------------------------------------------------------------------------- + +\dedicatory{For/Dedicated to/To my\ldots} + +%---------------------------------------------------------------------------------------- +% THESIS CONTENT - CHAPTERS +%---------------------------------------------------------------------------------------- + +\mainmatter % Begin numeric (1,2,3...) page numbering + +\pagestyle{thesis} % Return the page headers back to the "thesis" style + +% Include the chapters of the thesis as separate files from the Chapters folder +% Uncomment the lines as you write the chapters + +\include{Chapters/Chapter1} +\include{Chapters/Chapter2} +\include{Chapters/Chapter3} +%\include{Chapters/Chapter4} +%\include{Chapters/Chapter5} + +%---------------------------------------------------------------------------------------- +% THESIS CONTENT - APPENDICES +%---------------------------------------------------------------------------------------- + +\appendix % Cue to tell LaTeX that the following "chapters" are Appendices + +% Include the appendices of the thesis as separate files from the Appendices folder +% Uncomment the lines as you write the Appendices + +\include{Appendices/AppendixA} +%\include{Appendices/AppendixB} +%\include{Appendices/AppendixC} + +%---------------------------------------------------------------------------------------- +% BIBLIOGRAPHY +%---------------------------------------------------------------------------------------- + +\printbibliography[heading=bibintoc] + +%---------------------------------------------------------------------------------------- + +\end{document}