lexing: comparison ChengsongTanPhdThesis/Chapters/Introduction.tex

equal deleted inserted replaced

-:99eceee5c4ac
+:f1edd5ee1a12
 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
+Those engines 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
+However, those engines 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
+Consider for example $(a^*)^*\,b$ and
-strings of the form $aa..a$ can be matched by this regular
+strings of the form $aa..a$, these strings cannot be matched by this regular
-expression. Obviously this is not the case---the expected $b$ in the last
+expression: Obviously the expected $b$ in the last
-position is missing. One would expect that modern regular expression
+position is missing. One would assume 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
 The merit of Brzozowski derivatives (more on this later)
 on this problem is that
 it can be naturally extended to support bounded repetitions.
 Moreover these extensions are still made up of only
 inductive datatypes and recursive functions,
-making it handy to deal with using theorem provers.
+making it handy to deal with them in theorem provers.
 %The point here is that Brzozowski derivatives and the algorithms by Sulzmann and Lu can be
 %straightforwardly extended to deal with bounded regular expressions
 %and moreover the resulting code still consists of only simple
 %recursive functions and inductive datatypes.
 Finally, bounded regular expressions do not destroy our finite
 is
 \begin{center}
 	$\langle (.^+) \rangle \ldots \langle / \backslash 1 \rangle$
 \end{center}
 Despite being useful, the expressive power of regexes
-go beyond the regular language hierarchy
+go beyond regular languages
 once back-references are included.
 In fact, they allow 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}.
+which cannot be expressed by context-free grammars \parencite{campeanu2003formal}.
 Such a language is contained in the context-sensitive hierarchy
 of formal languages.
 Also solving the matching problem involving back-references
 is known to be NP-complete \parencite{alfred2014algorithms}.
 Regex libraries supporting back-references such as
 (i) The ones  with  linear
 time guarantees like Go and Rust. The downside with them is that
 they impose restrictions
 on the regular expressions (not allowing back-references,
 bounded repetitions cannot exceed an ad hoc limit etc.).
-(ii) Those
+And (ii) those
 that allow large bounded regular expressions and back-references
 at the expense of using backtracking algorithms.
 They can potentially ``grind to a halt''
 on some very simple cases, resulting
-ReDoS attacks.
+ReDoS attacks if exposed to the internet.
-The proble with both approaches is the motivation for us
+The problems with both approaches are the motivation for us
 to look again at the regular expression matching problem.
 Another motivation is that regular expression matching algorithms
 that follow the POSIX standard often contain errors and bugs
 as we shall explain next.

changeset 633	f1edd5ee1a12
parent 631	bdb3ffdd39f8
child 634	b079aaee5e10