Static Analysis for Regular Expression Exponential
Runtime via Substructural Logics

arXiv:1405.7058v2 [] 13 Aug 2017

Asiri Rathnayakea, Hayo Thieleckea
a University

of Birmingham, Birmingham B15 2TT, United Kingdom

Abstract
Regular expression matching using backtracking can have exponential runtime,
leading to an algorithmic complexity attack known as REDoS in the systems
security literature. In this paper, we present a static analysis that detects
whether a given regular expression can have exponential runtime for some inputs. The analysis works by forming powers and products of transition relations
and thereby reducing the REDoS problem to reachability. The correctness of
the analysis is proved using a substructural calculus of search trees, where the
branching of the tree causing exponential blowup is characterized as a form of
non-linearity.

1. Introduction
Regular expressions are everywhere. Yet the backtracking virtual machines
that are used to match them (in Java, .NET and other frameworks) are very
different from the DFA (deterministic finite automata) construction used in
compiling. Whereas DFAs run in linear time but may be expensive to construct,
backtracking matchers have low initial cost, but may have exponential runtime
for some inputs [1]. This is a problem when such matchers may be exposed to
malicious input, say over a network, as an attacker could craft an input in order
for the matcher to take exponential time. This problem is known as REDoS,
short for Regular Expression Denial-of-Service.
For a straightforward example of an exponential blowup, consider the following regular expression:
∗
(a | b | ab) c
Matching this expression against input strings of the form (ab)n leads the Java
virtual machine to a halt for very moderate values of n (∼ 50) on a contemporary
computer. Certain other backtracking matchers like the PCRE library and the
matcher available in the .NET platform seem to handle this particular example
well. However, the ad-hoc nature of the workarounds implemented in these
Email addresses: apr015@cs.bham.ac.uk (Asiri Rathnayake),
h.thielecke@cs.bham.ac.uk (Hayo Thielecke)

Preprint submitted to Elsevier

March 21, 2018

frameworks are easily exposed with a slightly complicated expression / input
combination:
(a | b | ab)∗ bc
This expression, when matched against input strings of the form (ab)n ac, leads
to exponential blowups on all the three matchers mentioned.
The REDoS analysis builds on the idea of nondeterministic Kleene expressions. When matching the input string ab against the Kleene expression
∗
(a | b | ab) , a match could be found by taking either of the two different paths
through the corresponding NFA (nondeterminstic finite automata). If we repeat
this string to form abab, now there are four different paths through the NFA;
this process quickly builds up to an exponential amount of paths through the
NFA as the pumpable string ab is repeated.
Definition 1.1 For a given regular expression, a pumpable string is a substring
y of an input string of the form xy n z. The pumpable part y may be repeated
as many times as needed (n) to form larger input strings while maintaining an
exponential growth of search space in a backtracking matcher.
A matcher based on DFAs would not face a difficulty in dealing with such
expressions since the DFA construction eliminates such redundant paths. However, these expressions can be fatal for backtracking matchers based on NFAs,
as their operation depends on performing a depth-first traversal of the entire
search space.
We think of the various phases of the analysis as very simple and nonstandard logics for judgements for different implications of the form:
w : p1 → p2
Here p1 → p2 is a proposition and w is a proof of it, which we will call its
realizer. In this way, we can focus on what the analysis tries to construct,
not how. Hence the analysis can be seen as a form of proof search, and it is
implemented via straightforward closure algorithms.
A second use of logic or type theory in this paper comes in when proving
the soundness of the analysis, when we need to show that the constructed string
really leads to exponential runtime. While the backtracking machine that we
use as an idealization of backtracking matchers (like those in the Java platform) is not very complicated, it is not straightforward to reason about how
it behaves on some constructed malicious input. This is because the machine
traverses the search tree in a depth-first strategy, whereas the attack string is
best understood in terms of a composition of horizontal slices of the search tree.
To reason compositionally, we first introduce a calculus of search trees, inspired
by substructural logics. In a nutshell, the existence of a pumpable string as part
of a REDoS vulnerability amounts to the existence of a non-linear derivation in
the search tree logic, essentially as in a derivation of this form:
p
p, p
2

a, b, c
w, x, y, z
p, q
β, θ
Φ
σ
ε
։
7→

⇛

input symbols
strings of input symbols
NFA nodes or states
ordered sequences p1 . . . pn of NFA states
sets {p1 , . . . , pn } of NFA states
sequences of state/index pairs (p, j)
empty word or sequence
NFA transition relation (Definition 2.2)
ordered NFA transition function (Definition 2.1)
ordered multistate transition function (Definition 2.4)
multistate transition function (Definition 2.5)
transitions of backtracking machine (Definition 2.6)
Figure 1: Notational conventions

Thus we can reason about the exponential growth of the search tree in a compositional, logical style, separate of the search strategy of the backtracking matcher.
The exponential runtime of the machine then follows due to the fact that the
runtime is at least the width of the search tree if the matcher is forced to explore
the whole tree.
Outline of the paper
Section 2 presents some required background on regular expression matching
in a form that will be convenient for our purpose. We then define the three
phases (prefix, pumping, and suffix construction) of our REDoS analysis in
Section 3 and validate it on some examples in Section 4. Section 5 and Section 6
prove the soundness and the completeness of the analysis using a substructural
calculus of search trees. Section 7 presents a brief overview of the OCaml
implementation of the analysis and the practical performance of our tool. We
conclude with a discussion of related work in Section 8 and directions for further
work in Section 9.
2. Basic constructs
This section presents some background material that will be needed for the
analysis, such as nondeterministic automata. Figure 1 gives an overview of
notation. We assume that the regular expression has been converted into an
automaton following one of the standard constructions.
2.1. The ordered NFA
The usual text-book definitions of NFAs do not impose any ordering on
the transition function. For an example, a traditional NFA for the regular
expression a(bc | bd) would not prioritize any of the two transitions available

3

for character b over the other. Since backtracking matchers follow a greedy leftto-right evaluation of alternations, the alternation operator effectively becomes
non-commutative in their semantics for regular expressions. Capturing this
aspect in the analysis requires a specialized definition of NFAs.
If we are only concerned about acceptance, Kleene star is idempotent and
alternation is commutative. If we are interested in exponential runtime, they
are not. The non-commutativity of alternation is not that surprising in terms of
programming language semantics, as Boolean operators like && in C or andalso
in ML have a similar semantics: first the left alternative is evaluated, and if that
does not evaluate to true, the right alternative is evaluated. Since in our tool
the NFA is constructed from the syntax tree, the order is already available in
the data structures. The children of a NFA node have a left-to-right ordering.
Definition 2.1 (Ordered NFA) An ordered NFA N consists of a set of states,
an initial state p0 , a set of accepting states Acc and for each input symbol a a
transition function from states to sequences of states. We write this function as
a : p 7→ q1 . . . qn
For each input symbol a and current NFA state p, we have a sequence of successor states qi . The order is significant, as it determines the order of backtracking.
In the textbook definition of an ε-free NFA, the NFA has a transition function
δ of type
δ : (Q × Σ) → 2Q
where Q is the set of states and Σ the set of input symbols. Here we have
imposed an order on the sets in the image of the function, replacing 2Q by Q∗ ,
curried the function, and swapped the order of Q and Σ.
Σ
a

→ (Q
7
→
p

→
Q∗ )
7→ q1 . . . qn

Definition 2.2 The nondeterministic transition relation of the NFA is given
by the following inference:
a : p 7→ q1 . . . qn
a : p ։ qi
Note however, that we cannot recover the ordering of the successor states qi from
the nondeterministic transition relation. In this regard, the NFA on which the
matcher is based has a little extra structure compared to the standard definition
of NFA in automata theory. If we know that
a : p ։ q1 and a : p ։ q2
we cannot decide whether the ordered transition is
a : p 7→ q1 q2 or a : p 7→ q2 q1
4

Definition 2.3 The transition relation ։ is extended to strings with the following inference rules:
w :p։q
ε:p։p

a : q ։ q′

wa : p ։ q ′

We define ordered multistates β as finite sequences of NFA states p, where
the order is significant. In constrast, multistates Φ represent sets of NFA states,
so they can be represented as lists, but are identified up to reordering. Each
ordered multistate β can be turned into a multistate given by the set of its
elements. We write this set as Set(β). If
β = p1 . . . pn
then
Set(β) = {p1 , . . . , pn }
The difference between β and Set(β) may appear small, but the notion of equality for sets is less fine-grained than for sequences, which has an impact on the
search space that the analysis has to explore.
The transition relation  on ordered multistates is defined in the following
manner. Let ≫ be an operator on ordered multistates:
[] ≫ []
p β ≫ p β′
pβ

≫ β′

if (6 ∃β1 , β2 . β = β1 p β2 ) ∧ β ≫ β ′
if (∃β1 , β2 . β = β1 p β2 ) ∧ p β1 β2 ≫ β ′

The operator ≫ removes all but the leftmost occurrences in sequences. Note
that termination is guaranteed since ≫ is applied on shorter sequences on the
R.H.S. Moreover, in each reduced sequence each p can appear at most once, so
there are only finitely many sequences that can be reached for any NFA.
Definition 2.4 The transition relation  for ordered multistates is defined as:
β1 = (p1 . . . pn )

a : pi 7→ θi

(θ1 . . . θn ) ≫ β2

a : β1  β2
The  transition is extended to strings with the rules:
w : β1  β2
ε:ββ

a : β2  β3

(w a) : β1  β3

The transition relation  can be thought of as an ordered variant of the traditional DFA transition relation encountered in powerset construction:
Definition 2.5 (DFA Transition ⇛) The transition relation ⇛ is defined as
w : Φ1 ⇛ Φ2
if and only if
Φ2 = {p2 | ∃p1 ∈ Φ1 .w : p1 ։ p2 }
5

2.2. The backtracking abstract machine
The analysis assumes exact matching semantics of regular expressions. Given
regular expression e and the input string w, the matcher is required to find a
match of the entire string, as opposed to a sub-string. Most practical matchers
search for a sub-match by default. However, such behavior can be modeled in
exact matching semantics by augmenting the regular expression with match-all
constructs at either end of the expression, as in (.∗ e.∗ ). Practical implementations offer special “anchoring” constructs that allow regular expression authors
to enforce exact matching semantics. For an example, expressions of the form
(ˆe$) require them to be matched against the entire input string.
While the theoretical formulation of our analysis assumes exact matching
semantics (thus avoiding unnecessary clutter), our implementation assumes submatch semantics, since it is more useful in practice. The translation between
the two semantics is quite straightforward.
Definition 2.6 (Backtracking abstract machine) Given an ordered NFA,
the backtracking machine is defined as follows. We assume an input string w
as given. Machine transitions may depend on w, but it does not change during
transitions, so that we do not explicitly list it as part of the machine state. The
input symbol at position j in w is written as w[j] (j is 0-based).
• States of the backtracking machine are finite sequences of the form
σ = (p0 , j0 ) . . . (pn , jn )
where each of the pi is an NFA state and each of the ji is an index into
the current input string. We refer to individual (p, i) pairs as frames (as
in stack frames).
• The initial state of the machine is the sequence of length 1 containing the
frame:
(p0 , 0)
• The machine has matching transitions, which are inferred from the transition function of the ordered NFA as follows:
a : p 7→ q1 . . . qn

w[j] = a
w

(p, j) σ

(q1 , j + 1) . . . (qn , j + 1) σ

• The machine has failing transitions, of the form:
(p, j) σ

σ

where there is no transition of the form w[j] : p 7→ q1 . . . qn OR j is the
length of w and p ∈
/ Acc.

6

• Accepting states are of the form:
w

(p, j) σ

where p ∈ Acc and j is the length of w.
• Transition sequences in n(n > 0) steps are written as
the following rules:
w
w
We write w

σ1

σ′

σ
σ
∗

1

σ

w

σ1

′

n

σ2

w

σ2 for ∃n.w

(σ1

σ1
n

w
n+m

n

σ2

and inferred using
m

σ3

σ3

σ2 ).

• Final states are either accepting or the empty sequence.
The state of the backtracking machine is a stack that implements failure
continuations. When the state is of the form (p, j)σ, the machine is currently
trying to match the symbol at position j in state p. Should this match fail, it
will pop the stack and proceed with the failure continuation σ.
Lemma 2.7 For any backtracking machine run (i.e. a transition sequence):
w

σ

n

σ′

And for any σ̄, the following run also exists:
w

σ σ̄

n

σ ′ σ̄

Proof Observe that each transition taken by the the first machine can be simulated on the extended machine. Moreover, each transition of the extended
machine leaves the additional σ̄ untouched.

The backtracking machine definition leaves a lot of leeway to the implementation. Implementation details are abstracted in the ordered transition relation. The most important choice in the definition is that the machine performs
a depth-first traversal of the search tree. In principle, a backtracking matcher
could also use breadth-first search. In that case, our REDoS analysis would not
be applicable, and such matchers may avoid exponential run-time. However,
the space requirements of breadth-first search are arguably prohibitive. A more
credible alternative to backtracking matchers is Thompson’s matcher [2, 1, 3],
which is immune to REDoS. However the relative inflexibility of the lockstep algorithm (when supporting extended, non-regular pattern matching constructs)
has made it less popular among practical regular expression libraries. The REDoS problem in the backtracking paradigm therefore remains quite significant.

7

3. The REDoS analysis
At a high-level, the analysis can be thought to work by exploring all the
Kleene sub-expressions within an input expression and then analysing each of
those sub-expressions for an exponential vulnerability. Given a regular expression input, for each Kleene sub-expression e2 ∗ , there exists a prefix expression e1
and a suffix expression e3 ; the prefix expression is what a backtracking matcher
has to match in order to reach the Kleene expression, the suffix expression
is what a backtracking matcher has to match in order to complete an overall
match. For each such decomposition of the form e1 e2 ∗ e3 , the analysis attempts
to derive an attack string of the form:
xy n z
The presence of a pumpable string y signals the analyser that a corresponding
prefix x and a suffix z need to be derived in order to form the final attack string
configuration. The requirements on the different segments of the attack string
are as follows:
x : x ∈ L(e1 )
y
z

: y ∈ L(e2 ∗ ) (with b > 1 paths)
: xy n z 6∈ L(e1 e2 ∗ e3 )

Intuitively, the prefix x leads a backtracking matcher to a point where it has
to match the (vulnerable) Kleene expression e2 ∗ . At this point the matcher is
presented with n (n > 0) copies of the pumpable string y, increasing the search
space of the matcher to the order of bn . At the end of each of the search attempts
(paths through the NFA), the suffix z causes the matcher to backtrack, forcing
an exploration of the entire search space.
3.1. The phases of the REDoS analysis
Overall, the REDoS analysis of a node pℓ (loop node) consists of three phases.
The phases all work by incrementally exploring a transition relation. These
relations are the DFA transition relation ⇛ (Definition 2.5) and its ordered
variant  (Definition 2.4). The three analysis phases construct a REDoS prefix
x, a pumpable string y and a REDoS suffix z:

x : p0  (β pℓ β ′ )
Prefix analysis

where Φx = Set(β pℓ )

 y1 : Φx ⇛ Φy1
a : Φy1 ⇛ Φy1a
Pumpable analysis


 y2 : Φy1a ⇛ Φy2 where Φy2 ⊆ Φx
Suffix analysis
z : Φy2 ⇛ Φfail where Φfail ∩ Acc = ∅

8

p0

x
p1

pRight

pℓ

y

y

p2

y
pℓ

pℓ

y

y

p3

x

x

pℓ

y

y
pℓ

pℓ

y
pℓ

z

z

z

z

z

fail

fail

fail

fail

fail

Figure 2: Branching search tree with left context for x y y z

3.2. Prefix analysis
The analysis needs to find a string that causes the matcher to reach pℓ .
However, due to the nondeterminism of the underlying NFA, it is not enough to
check reachability. The same string x could also lead to some other states before
pℓ is reached by the matcher. If one of these states could lead to acceptance, the
matcher will terminate successfully, and pℓ will never be reached. In this case,
there is no vulnerability, regardless of any exponential blowup in the subtree
under pℓ . See Figure 2.
The REDoS prefix analysis computes all ordered multistates β reachable
from p0 , together with a realizer w, using the following rules:
(w, β1 ) ∈ R
(ε, p0 ) ∈ R

a : β1  β2

6 ∃w′ .(w′ , β2 ) ∈ R

R := R ∪ {(wa, β2 )}

In the implementation, we keep a set R. It is initialized to (ε, p0 ). We then
repeatedly check if there is a (w, β1 ) in the set such that for some a there is a
transition a : β1  β2 . If there is, we add (w a, β2 ) to R and repeat the process.
We terminate when no new β2 has been found in the last iteration. Finally, the
analysis isolates (w, β) pairs of the form (x, β pℓ β ′ ) and takes Φx as Set(β pℓ )
for each such pair.
3.3. Pumping analysis
Definition 3.1 A branch point is a tuple:
(pN , a, {pN 1 , pN 2 })
Where ∃β, β ′ , β ′′ . a : pN 7→ βpN 1 β ′ pN 2 β ′′ . We call pN a nondeterministic node,
in that, there are multiple successor nodes for pN on the same input symbol a.

9

For example, if pN has three successor nodes p1 , p2 and p3 for the same input
symbol a, there are three different branch points:
(pN , a, {p1 , p2 })
(pN , a, {p1 , p3 })
(pN , a, {p2 , p3 })
There can be only finitely many nondeterministic nodes in the given NFA. For
each of them, we need to solve a reachability problem.
The pumping analysis can be visualized with the diagram in Figure 3. The
analysis aims to find two different paths leading from pℓ to itself. Such paths
must at some point include a nondeterministic node pN that has at least two
transitions to different nodes pN 1 and pN 2 for the same symbol a. For such
a node to lie on a path from pℓ to itself, there must be some path labeled y1
leading from pℓ to pN , and moreover there must be paths from the two child
nodes pN 1 and pN 2 leading back to pℓ , such that both these paths have the label
y2 . The left side of Figure 3 depicts this situation.
So far we have only considered what states may be reached. Due to the
nondeterminism of the transition relation a : p ։ q, there may be other states
that can be reached for the same strings y1 and y2 . Therefore, we also need to
perform a must analysis that keeps track of all states reachable via the strings
we construct. This analysis uses the transition relation ⇛ of the power DFA
between sets of NFA states. In Figure 3, it is shown on the right-hand side.
Intuitively, we run the two transition relations in parallel on the same input
string. More formally, this involves constructing a product of two relations.
Before we reach the branching point, we run the relations ։ and ⇛ in parallel.
After the nondeterministic node pN has produced two different successors, we
need to run two copies of ։ in parallel with ⇛. One may visualize this situation
by reading the diagram in Figure 3 horizontally: above the splitting at pN , there
are two arrows in parallel for y1 , whereas below that node, there are three arrows
in parallel for a and y2 .
The twofold transition relation ։2 for running ։ in parallel with ⇛ is given
by the rules in Figure 4. Analogously, the threefold product transition relation
։3 for running two copies of ։ in parallel with ⇛ is given by the rules in
Figure 5.
In summary, the pumping analysis consists of two phases:
1. Given pℓ and Φx , the analysis searches for a realizer y1 for reaching some
nondeterministic node pN :
y1 : (pℓ , Φx ) ։2 (pN , Φy1 )
2. Given the successor nodes pN 1 and pN 2 of some pN node, the analysis
searches for a realizer y2 for reaching pℓ :
y2 : (pN 1 , pN 2 , Φy1a ) ։3 (pℓ , pℓ , Φy2 )

10

pℓ

Φx
y1

y1
pN
a

Φy1
a

a

pN 1

pN 2
y2

Φy1a
y2

y2
pℓ

Φy2

Figure 3: Pumping analysis construction of y1 a y2 : “may” on the left using ։, and “must”
on the right using ⇛

w : (p1 , Φ1 ) ։2 (p2 , Φ2 )

b:

p2 ։ p3

b:

Φ2 ⇛ Φ3

(w b) : (p1 , Φ1 ) ։2 (p3 , Φ3 )

ε : (p, Φ) ։2 (p, Φ)
Figure 4: The twofold product transition relation ։2

Moreover, the analysis checks that the constructed state Φy2 satisfies the
inclusion:
Φy2 ⊆ Φx
If both phases of the analysis succeed, the string y1 a y2 is returned as the
pumpable string, together with the state Φy2 . Moreover, we call the string
y1 a y2 to be a pumpable string for the node pℓ , an NFA containing such a node
is then called a pumpable NFA.
Example 3.2 The following diagram shows an NFA corresponding to the regular expression (a|b|ab)∗ :
a

b

p1
b
a
p2

11

w:

(p1 , p′1 , Φ1 )

։3 (p2 , p′2 , Φ2 )

(w b) :

(p1 , p′1 , Φ1 )

b:

p2 ։ p3

b:

p′2 ։ p′3

b:

Φ2 ⇛ Φ3

։3 (p3 , p′3 , Φ3 )

ε : (p, p′ , Φ) ։3 (p, p′ , Φ)
Figure 5: The threefold product transition relation ։3

Taking pℓ = p1 and Φx = {p1 }, the pumping analysis leads to the following
derivation:
y1 = ε
(p1 , a, {p1 , p2 })
y2 = b

ε : (p1 , {p1 }) ։2 (p1 , {p1 })
a : {p1 } ⇛ {p1 , p2 }
b : (p1 , p2 , {p1 , p2 }) ։3 (p1 , p1 , {p1 , p2 })

Here we have an unstable derivation since {p1 , p2 } 6⊆ {p1 } (i.e. Φy2 6⊆ Φx ).
If we were to take Φx = {p1 , p2 } (i.e. x = a), the resulting derivation would
be stable (for the same pumpable string ab). Stable derivations ensure that
multiple pumpings of a pumpable string do not diverge Φy2 , which in turn
ensures the correctness of the failure suffix. We treat this inclusion more formally
in Lemma 5.7.
3.4. Suffix analysis
For each Φy2 constructed by the pumping analysis, the REDoS failure analysis computes all multistates Φfail such that there is a z with:
z : Φy2 ⇛ Φfail

∧

Φfail ∩ Acc = ∅

Intuitively, z fails all the states in Φy2 by taking them to Φfail , which does
not contain any accepting states.
4. Test cases for the REDoS analysis
In order to demonstrate the behavior of the analyser, here we present examples that exercise the most important aspects of its operation.
4.1. Non commutativity of alternation
This aspect of the analysis can be illustrated with the following two example
expressions:
∗
.∗ | (a | b | ab) c
∗

(a | b | ab) c | .∗
12

Even though the two expressions correspond to the same language, only the
second expression yields a successful attack. In the first expression, all the
multi-states starting from Φx (Set(βpℓ )) consist of a state corresponding to the
expression (.∗ ), which implies that this expression is capable of consuming any
input string thrown at it without invoking the vulnerable Kleene expression.
On the other hand, Φx calculated for the second expression lacks a state corresponding to (.∗ ), leading to the following attack string configuration:
x=ε

y = ab z = ε

4.2. Prefix construction
Prefix construction plays one of the most crucial roles in finding an attack
string. In the following example, only a certain prefix leads to a successful
attack string derivation:
c.∗ |(c | d)(a | b | ab)∗ e
Notice that a prefix c would trigger the (.∗ ) on the left due to the left-biased
treatment of alternation in backtracking matchers. The prefix d on the other
hand forces the matcher out of this possibility. The difference between these
two prefixes is captured in two different values of (x, Φx ):
(c, {p1 , p2 }) (d, {p2 })
Where p1 corresponds to the sub-expression (.∗ ) and p2 corresponds to (a | b | ab)∗ e.
Only the latter of these two leads to a successful attack string:
x = d y = ab

z=ε

Prefix construction may also lead to loop unrolling when necessary. For an
example, consider the following regex:
∗

(a | b).∗ |c∗ (a | ab | b) d
Without the unrolling of the Kleene expression c∗ , any pumpable string intended
for the vulnerable Kleene expression will be consumed by the alternation on the
left. The analyser captures this situation again as two different values of (x, Φx ),
one for x = c and the other for either x = a or x = b. Only the former value
leads to a successful attack string:
x=c

y = ab

z=ε

The amount of loop unrolling is limited by the finiteness of the Φx values. In
the following example, the loop c∗ needs to be unrolled twice:
(c | a | b)(a | b).∗ |c∗ (a | b | ab)∗ d
Here, unrolling c∗ 0 - 2 times leads to three distinct values of Φx due to the
different matching states on the left alternation. Only one of those unrollings
leads to a successful attack string:
x = cc

y = ab
13

z=ε

4.3. Pumpable construction
As is the case with prefixes, the existence of an attack string may depend on
the construction of an appropriate pumpable string. For an example, consider
the following regex:
∗
(a | a | b | b) (a.∗ | c)
Here the pumpable string a does not yield an attack string since it also triggers
the (.∗ ) continuation. On the other hand, the pumpable string b avoids this
situation and leads to the following attack string configuration:
x=ε y=b z=ε
Similar to the prefix analysis, pumpable analysis utilises (y, Φy ) values to select
between pumpable strings.
In some cases, the pumpable construction overlaps with prefix construction.
In the example below, an attack string may be composed in two different ways:
∗

d.∗ |((c | d)(a | a)) b
Here, choosing ca as the pumpable string leads to a successful attack string
derivation:
x = ε y = ca z = ε
However, it is also possible to form an attack string with the following configuration:
x = ca y = da z = ε
The important point here is that the attack string must begin with a c instead
of a d in order to avoid the obvious match on the left. The analyser is capable
of finding both the configurations that meet this requirement.
Pumpable construction may also lead to loop unrolling when necessary, as
demonstrated by the following example:
∗

a.∗ |(c∗ a(b | b)) d
Without unrolling the inner loop c∗ , the pumpable string ab would trigger the
alternation on the left. A successful attack string requires the unrolling of this
inner loop, as in the following configuration:
x=ε

y = cab z = ε

As with the previous example, the unrolling of the inner loop c∗ may be performed as part of the prefix construction, leading to the following alternate
attack string configuration:
x = cab

y = ab

z=ε

The latter configuration may be considered more desirable in that it makes the
the pumpable string shorter, leading to much smaller attack strings.
14

5. Soundness of the analysis
The backtracking machine performs a depth-first search of a search tree.
Proofs about runs of the machine are thus complicated by the fact that the
construction of the tree and its traversal are conflated. To make reasoning more
compositional, we define a substructural calculus for constructing search trees.
Machine runs correspond to paths from roots to leaves in these trees.
5.1. Search tree logic
Definition 5.1 (Search tree logic) The search tree logic has judgements of
the form
w : β1 △ β2
where w is an input string, and both β1 and β2 are sequences of NFA states.
The inference rules are given in Figure 6.
Intuitively, the judgement
w : β1 △ β2
means that there is a horizontal slice of the search tree, such that the nodes at
the top form the sequence β1 , the nodes at the bottom form the sequence β2 ,
and all paths have the same sequence of labels, forming w:
β1
w

w
β2

Each w represents an NFA run w : p1 ։ p2 for some p1 that occurs in β1 and
some p2 that occurs in β2 . The string w labels the sides of the trapezoid, since
that determines the compatible boundary for parallel composition. Again we
may like to think of w as a proof of reachability. Here the reachability is not in
the NFA, but in the matcher based on it.
The trapezoid can be stacked on top of each other if they share a common
β at the boundary. They can be placed side-by-side if they have the same w on
the inside:

15

a : p 7→ β
a:p△β
w1 : β1 △ β2

(Trans)

w2 : β2 △ β3

(w1 w2 ) : β1 △ β3
(εSeq)

ε:β△β

w : β1′ △ β2′

w : β1 △ β2

(SeqComp)

w : (β1 β1′ ) △ (β2 β2′ )

(ParComp)

(εPar)

w:ε△ε

Figure 6: Search tree logic

p

β1′

β1
w1

w1

w2

w2

β3

β3′

Note that the search tree logic in Figure 6 is substructural, in that, common
structural rules such as weakening and contraction do not hold in general:
w : β1 △ β1′
w : β1 β2 △ β1′

(NotWeaken)

w : ββ △ β ′
w : β △ β′

(NotContract)

5.2. Pumpable implies exponential tree growth
We use the search tree logic to construct a tree by closely following the phases
of our REDoS analysis. The exponential growth of the search tree in response to
pumping is easiest to see when thinking of horizontal slices across the search tree
for each pumping of y. The machine computes a diagonal cut across the search
tree as it moves towards the left corner. The analysis constructs horizontal cuts
with all states at the same depth. It is sufficient to show that the width of the
search tree grows exponentially. The width is easier to formalize than the size.
We need a series of technical lemmas connecting different transition relations.

16

Lemma 5.2 The following rule is admissible:
w : Φ′1 ⇛ Φ′2

w : Φ1 ⇛ Φ2

w : (Φ1 ∪ Φ′1 ) ⇛ (Φ2 ∪ Φ′2 )
Lemma 5.3 (⇛ △ simulation) If w : Φ1 ⇛ Φ2 , w : β1 △ β2 and Φ1 =
Set(β1 ), then Φ2 = Set(β2 ).
Proof Suppose:
β1 = (p1 . . . pn )

a : pi 7→ θi

Then from the search tree logic we get a : β1 △ (θ1 . . . θn ). Moreover, the
definition of ⇛ implies a : {pi } ⇛ Set(θi ). Now, applying Lemma 5.2 gives:
a : Set(β1 ) ⇛ Set(θ1 ) ∪ . . . ∪ Set(θn ) = Set(θ1 . . . θn )
Therefore, the result holds for strings of unit length. An induction on the length
of w completes the proof.

Lemma 5.4 ( △ simulation) If w : β1  β2 , w : β1′ △ β2′ and β1′ ≫ β1 , then
β2′ ≫ β2 .
Proof Suppose:
β1′ = (p11 . . . pmk )

a : pij 7→ θij

Where pij corresponds to the jth occurrence of the state pi . Equivalently:
pij = pi′ j ′ ⇐⇒ i = i′
Given β1′ ≫ β1 , we deduce:
(p11 . . . pmk ) ≫ (p11 . . . pm1 ) = β1
Now, given a : β1  β2 , the definition of  gives:
(θ11 . . . θm1 ) ≫ β2
On the other hand, a : β1′ △ β2′ gives:
β2′ = (θ11 . . . θmk )
The definition of ≫ can be generalized for multi-states, which leaves us with:
(θ11 . . . θmk ) ≫ (θ11 . . . θm1 )
That is, we have shown:
β2′ = (θ11 . . . θmk ) ≫ (θ11 . . . θm1 ) ≫ β2
An induction on the length of w completes the proof.
17



Lemma 5.5 (։ △ simulation) Given w : p ։ q, there are sequences of
states β1 and β2 such that w : p △ β1 q β2 .
Proof The base case (w = a) holds from the definition of △. For the inductive
step, suppose w : p ։ q and a : q 7→ q ′ . Then from the induction hypothesis
we get w : p △ β1 q β2 for some β1 , β2 . Moreover, from the base case we have
a : q △ β3 q ′ β4 for some β3 , β4 . Assuming a : β1 △ β1′ and a : β2 △ β2′ for some

β1′ , β2′ , the definition of △ gives wa : p △ β1′ β3 q ′ β4 β2′ .
Lemma 5.6 (Pumpable realizes non-linearity) Let y be pumpable for some
node pℓ . Then there exist β1 , β2 , β3 such that:
y : p ℓ △ β1 p ℓ β2 p ℓ β3
Proof The pumpable analysis generates a string of the form:
y = y1 a y2
Where
y 1 : pℓ ։ pN
a : pN 7→ (β pN 1 β ′ pN 2 β ′′ )
y 2 : pN 1 ։ pℓ

y 2 : pN 2 ։ pℓ

Now, Lemma 5.5 leads to the desired result.



Lemma 5.7 Let x, y be constructed from the prefix analysis and the pumpable
analysis such that:
x
y

: p0  (β pℓ β ′ )
: Set(β pℓ ) ⇛ Φy

Φy ⊆ Set(β pℓ )

Then the following holds for any natural number n:
Φyn ⊆ Φyn−1
Where Φy0 = Set(β pℓ ) and y n : Φy0 ⇛ Φyn .
Proof By induction on n. Note that the base case (n = 1) holds by construction.
For the inductive step, suppose ∃ q ∈ Φyn , then from the definition of Φyn
we get ∃ p ∈ Φyn−1 . y : p ։ q. Moreover, the induction hypothesis gives
Φyn−1 ⊆ Φyn−2 . Therefore, we have p ∈ Φyn−2 , which in turn implies q ∈ Φyn−1 .

The importance of Lemma 5.7 is that it allows us to calculate a failure suffix
z independent of the number of pumping iterations; Φyn can only shrink as n
increases.

18

Lemma 5.8 (Exponential tree growth) Let x, y, z be constructed from the
analysis such that:
x :
y :
z :

p0  (β pℓ β ′ )
Set(β pℓ ) ⇛ Φy
Φy ⇛ Φfail

Φy ⊆ Set(β pℓ )
Φfail ∩ Acc = ∅

Then there exists βL , βR such that:
x : p0 △ βL pℓ βR ∧ Set(βL ) = Set(β)

(A)

y n : βL pℓ △ βn ⇒ |βn | ≥ 2n

(B)

′

′

z : Set(βn ) ⇛ Φ ⇒ Φ ∩ Acc = ∅

(C)

Proof
• Statement (A): Suppose x : p0 △ βx . Then from Lemma 5.4 it follows
that βx ≫ β pℓ β ′ . That is, pℓ must occur in βx . If we dissect βx into
βL pℓ βR such that pℓ 6∈ Set(βL ), then from the definition of ≫ it follows
that Set(βL ) = Set(β).
• Statement (B): Follows from Lemma 5.6. The number of copies of pℓ
doubles at each pumping iteration.
• Statement (C): Suppose y n : Set(βL pℓ ) ⇛ βn′ . Since Set(βL pℓ ) =
Set(β pℓ ) (statement A), Lemma 5.3 gives: Set(βn ) = Set(βn′ ). Now from
Lemma 5.7 it follows that Set(βn ) ⊆ Φy . Since z cannot lead to a successful
match from any state in Φy (by construction), the same should be true
for Set(βn ).

Lemma 5.8 may be visualized as in Figure 7. Note that the right hand
slice of the tree (emanating from β ′ ) is irrelevant, the depth-first strategy of a
backtracking matcher forces it to explore the left hand slice first. Since none of
the states at the bottom of the tree (βn′ ) are accepting, it is forced to explore the
(exponentially large, |βn | ≥ 2n ) entire slice (as proved in the following section).
5.3. From search tree to machine runs
Having proved that the attack strings lead to exponentially large search
trees, in this section we show how backtracking matchers are forced to traverse
all of it. We use the notation w[i : j] to represent the substring of w starting at
index i (inclusive) and ending at index j (exclusive). That is,
w[i : i] = ε
w[i : j] = w[i]...w[j − 1]

(i < j)

¯ β to identify an appearance of a state q within β:
We also use the notation q ∈
¯ β ⇔ ∃β ′ , β ′′ . β = β ′ qβ ′′
q∈
19

p0

pℓ

x
β

β′

yn

βn

z
βn′

Figure 7: Tree growth (Lemma 5.8)

Lemma 5.9 Let w be an input string of length n, s a (constant) offset into w
(0 ≤ s < n) and p a state such that:
w[s : i] : p △ βi

s≤i≤n

Set(βn ) ∩ Acc = ∅
¯ βi , and for any σ, the following run exists:
Then for any q ∈
w

(q, i)σ

∗

σ

Proof By induction on (n − i). For the base case (i = n), we have the machine
state:
(q, n) σ
¯ βn , this is not an accepting configuration. Therefore, we have:
Since q ∈
w

(q, n) σ

σ

For the inductive step, suppose i = k (s ≤ k < n), then we have the machine:
w

(q, k) σ

If q has no transitions on w[k], the proof is trivial. Let us assume:
′
w[k] : q 7→ q0′ . . . qm

Then we have the transition:
w

(q, k) σ

′
(q0′ , k + 1) . . . (qm
, k + 1) σ

′
are part of βk+1 . Therefore,
Now the definition of △ implies that q0′ , . . . , qm
we can apply the induction hypothesis to each of the newly spawned frames in
succession, which leads to the desired result.


20

Lemma 5.10 Let w be an input string of length n, s a (constant) offset into
w (0 ≤ s < n) and p a state such that:
w[s : i] : p △ βi

s≤i≤n

Set(βn ) ∩ Acc = ∅
¯ βi , the following run exists (for some σ):
Then for any q ∈
w

∗

(p, s)

(q, i)σ

Proof By induction on (i − s). The base case (i = s) holds trivially. For the
¯ βk . Then from the
inductive step, suppose i = k (s < k ≤ n) and that q̇ ∈
¯ βk−1 such that:
definition of △, there must be some q ′ ∈
βk−1 = β q ′ β ′

w[k − 1] : q ′ ։ q0 . . . q̇ . . . qm

Now from the induction hypothesis we get:
w

(p, s)

∗

(q ′ , k − 1) σ

Therefore, we deduce the run:
w

(p, s)

∗

(q ′ , k − 1)σ

(q0 , k) . . . (q̇, k) . . . (qm , k) σ

At this point, applying Lemma 5.9 to the newly spawned frames yields the
required result.

Given a search tree with all failure nodes at the bottom, Lemma 5.9 shows
that any intermediate frame reached during a simulation will eventually be
rejected. Moreover, Lemma 5.10 shows that a simulation corresponding to such
a search tree is forced to visit each and every node of the tree.
Lemma 5.11 (Tree traversal) Suppose w is an input string of length n such
that:
w[0 : s] : p0 △ β β
w[s : n] : β △ β ′
Set(β ′ ) ∩ Acc = ∅
¯ β, the following machine run exists (for some σ):
Then for any q ∈
w

(p0 , 0)

∗

(q, s) σ

Proof By induction on s. Note that the base case (s = 0) follows from
Lemma 5.10. For the inductive step, suppose s > 0. Here we focus on the
lowest common ancestor of all the states in β, this situation is illustrated in the
following figure:

21

p0

u
θ

θ

s
n

β

β

β′

β′

Let us assume that this state (lowest common ancestor of β) occurs at depth u
(u > 0, as otherwise we would have the base case again). Now from the diagram
we deduce:
w[0 : u] : p0 △ θ θ
w[u : n] : θ △ β ′
Set(β ′ ) ∩ Acc = ∅
Therefore, if q̇ is the lowest common ancestor of β, from the induction hypothesis
(since u < s) we get:
∗
w (p0 , 0)
(q̇, u) σ
For some σ. Moreover, from Lemma 5.10 we deduce:
w

(q̇, u)

∗

(q, s) σ ′

¯ β and a failure continuation σ ′ . Finally, we use Lemma 2.7 to
For some q ∈
compose these two runs into:
w

(p0 , 0)

∗

(q̇, u) σ

∗

(q, s) σ ′ σ


In sum, we have shown that the pumped part of the search tree grows exponentially in the size of the input, and that the backtracking machine is forced
to traverse all of it.
Theorem 5.12 (Redos analyis soundness) Let the strings x, y and z be
constructed by the REDoS analysis. Let k be an integer. Then the backtracking
machine takes at least 2k steps on the input string x y k z
Proof Follows from Lemma 5.8 and Lemma 5.11.
22



6. Completeness of the analysis
The analysis assumes that only a pumpable NFA can lead to an exponential
runtime vulnerability. For completeness, we need to ensure that there are no
other configurations that can cause such a vulnerability. Here we show that for
any non-pumpable NFA, the width of any search tree is bounded from above
by a polynomial. In places where an NFA is mentioned in a discussion below, a
non-pumpable NFA is to be assumed (unless otherwise mentioned).
Definition 6.1 For an ordered multi-state β and a state p, we define the funcp
tion [β]p as the number of ocurrences of p within β. Moreover, the relations ∼
(p-simulate) and ≃ (simulate) on ordered multi-states are incrementally defined
as follows:
p
β ∼ β ′ ⇔ [β]p = [β ′ ]p
p

β ≃ β′ ⇔ ∀ p ∈ Q . β ∼ β′
p

It can be shown that both ∼ and ≃ are reflexive, symmetric and transitive
relations.
Lemma 6.2 The relation ≃ can be shown to satisfy the following basic properties:
β ≃ β ′ ⇒ Set(β) = Set(β ′ ) ∧ |β| = |β ′ |
β1 β2 ≃ β3 β4 ⇔ ∀β . β1 ββ2 ≃ β3 ββ4
β ≃ β1 β ′ β2 ∧ β ′ ≃ β ′′ ⇒ β ≃ β1 β ′′ β2
β1 ≃ β1′ ∧ β2 ≃ β2′ ⇒ β1 β2 ≃ β1′ β2′
Lemma 6.3 Let w be an input string, β1 , β2 be ordered multi-states such that:
β1 ≃ β2

w : β1 △ β1′

w : β2 △ β2′

Then β1′ ≃ β2′ .
Proof Informally, β2 is merely a re-ordering of β1 (and vice versa). The trapezoid emanating from β1 will be composed of individual search trees rooted at
each constituent state of β1 . Therefore, the trapezoid emanating from β2 will
be a re-ordering of those search trees.
More formally, let n = |β1 | = |β2 | (the latter equality holds since β1 ≃ β2 ).
We perform an induction on n. The base case (n = 1) follows from the definition
of △ (β1 = β2 = p for some p ∈ Q). For the inductive step, note that any state
q introduced to both β1 and β2 (to make them n + 1 in size) must be the same
(in order to preserve β1 ≃ β2 ). Since the search tree rooted at q is same for
both β1 and β2 (regardless of where it appears within each of the multi-states),
its contribution to β1′ and β2′ is the same.


23

Definition 6.4 Given an NFA, a path γ is a sequence of triples:
(p0 , a0 , p1 )(p1 , a1 , p2 ) . . . (pn−1 , an−1 , pn )
where for 0 ≤ i < n, there is a transition ai : pi → pi+1 in the NFA. We write
dom(γ) for the first node p0 and cod(γ) for the last node pn in the path. The
sequence of input symbols a0 . . . an along the path is written as γ and called the
label of the path. Moreover, the set of nodes {p0 , . . . , pn } along the path γ is
written as nodes(γ).
Lemma 6.5 Given a tree judgement w : p △ β, for any state q appearing in β,
there exists a path γ with dom(γ) = p, cod(γ) = q and γ = w.
Proof By induction on the length of w.



Definition 6.6 We write w : p ⇒ q (p two-paths q) iff w = aw′ and:
∃β, β ′ , β ′′ . a : p 7→ βp1 β ′ p2 β ′′
(w′ = ε ∧ p1 = p2 = q) or (w′ : p1 ։ q ∧ w′ : p2 ։ q)
Definition 6.6 allows us to formulate pumpability in a different notation; if
we have w1 : p ⇒ q and w2 : q ։ p (loop), then the state p is pumpable on
the input string w1 w2 (see Figure 3).
Definition 6.7 Let γ be a path. We define the sets S(γ) and F (γ) as follows:
S(γ) = {p | ∃ γ1 , γ2 . γ = γ1 γ2
∧ γ 2 : dom(γ2 ) ⇒ cod(γ2 ) ∧ p = dom(γ2 )}
F (γ) = Q \ S(γ)
Essentially, S(γ) identifies the nondeterministic states along a path γ. There
are at least two paths from a given state in S(γ) to cod(γ) bearing the same
label (γ 2 above, a suffix of γ).
Lemma 6.8 Suppose γ is a path corresponding to a non-pumpable NFA such
that p = cod(γ). Then the following holds for any w:
w : p △ β ⇒ Set(β) ⊆ F (γ)
Proof From the definitions we have:
Set(β) ⊆ Q = S(γ) ∪ F (γ)
Suppose q ∈ Set(β) ∩ S(γ). Then q ∈ S(γ) gives:
∃ w′ . w′ : q ⇒ p

24

p0

q

w′
p

p
w

β

β
Figure 8: Sibling restriction on S(γ)

However, since q ∈ Set(β) we also have:
w:p։q
Leading to the contradiction:
w′ w : q ⇒ p ։ q
Therefore, it must be the case that Set(β) ∩ S(γ) = ∅. This leads to the
conclusion:
Set(β) ⊆ F (γ)

Lemma 6.8 is illustrated in Figure 8. Note that the fringes of the sibling trees
rooted at the two p’s are identical (△ logic is deterministic), making it impossible
for either of them to contain a q (q would be pumpable otherwise). In other
words, q ∈ S(γ) cannot appear again within search trees rooted at cod(γ).
It is this restriction on nondeterminism that leads us to the polynomial bound.
However, flushing out this polynomial bound requires quite an elaborate analysis
of the search tree structure, as we shall see next.
Definition 6.9 We define the reduction ⊲ on pairs of ordered multi-states according to the following rules:
(q1 . . . qn , β1 qβ2 ) ⊲ (q1 . . . qi q . . . qn , β1 β2 )

(∃ i . q = qi )

(q1 . . . qn , β1 qβ2 qβ3 ) ⊲ (q1 . . . qn qq, β1 β2 β3 ) (6 ∃ i . q = qi )
25

The reduction ⊲ groups repeated states together. Given that each transition
decreases the length of the second component, the reduction must terminate.
We use the notation ⊲⊲ to denote a maximal reduction:
(α1 , β1 ) ⊲ ⊲(α2 , β2 ) ⇒6 ∃(α3 , β3 ) . (α2 , β2 ) ⊲ (α3 , β3 )
Lemma 6.10 For a reduction (ε, β)⊲ ⊲(α, σ), the following basic properties can
be shown to hold:
β ≃ ασ
(a)
Set(α) ∪ Set(σ) = Set(β)

(b)

∀ p ∈ Set(α) . [α]p = [β]p > 1

(c)

|σ| = |Set(σ)|

(d)

Definition 6.11 We introduce an ordering variant of the search tree logic:
¯ ′ , α′ , σ ′ )
w : (β, α, σ)△(β
with the following inference rules:
a : β1 α1 △ β2

a : σ1 △ β3 (ε, β3 ) ⊲ ⊲(α2 , σ2 )
¯ 2 , α2 , σ2 )
a : (β1 , α1 , σ1 )△(β

¯ 2 , α2 , σ2 )
w : (β1 , α1 , σ1 )△(β

¯ 3 , α3 , σ3 )
a : (β2 , α2 , σ2 )△(β
¯ 3 , α3 , σ3 )
wa : (β1 , α1 , σ1 )△(β

¯ semantics recursively re-arranges the search tree into β, α and σ comThe △
¯ semantics may be visualized
ponents at each depth. A derivation using the △
as in Figure 9. Note that in this hypothetical derivation, we encounter repeated
states at depth w1 , thus giving rise to the first non-empty α component (α1 ).
From w1 to w1 w2 , we have non-empty β and σ components. Again at depth
w1 w2 we can observe a non-empty α component, which is the result of the previous σ component generating duplicates at this depth. The β component can
be thought of as the shadow/projection of all the previous α components.
Lemma 6.12 Let p be a state and w an input string such that:
w:p△β

¯ ′ , α, σ)
w : (ε, ε, p)△(β

Then β ′ ασ ≃ β.
Proof By induction on the length of w. For the base case (w = a), suppose
¯ we get:
a : p △ β. Then from the definition of △
¯
a : (ε, ε, p)△(ε,
α, σ)

26

p
w1
α1

σ1

w2
β2

α2

σ2

w3
¯ derivation.
Figure 9: An example △

Where (ε, β) ⊲ ⊲(α, σ). Therefore, Lemma 6.10 (a) gives β ≃ ασ. For the
inductive step (w = w′ a), suppose:
w ′ : p △ β1
¯ ′ , α1 , σ1 )
w′ : (ε, ε, p)△(β
1

(A.1)
(A.2)

Then the induction hypothesis yields β1 ≃ β1′ α1 σ1 . Now let us assume:
a : β1 △ β2
β1′ α1

(B.1)
β2′

a:
△
a : σ1 △ β3′

(B.2)
(B.3)

(ε, β3′ ) ⊲ ⊲(α2 , σ2 )

(B.4)

¯ leads to:
Assumptions (A.1), (B.2) - (B.4) and the definition of △
¯ ′ , α2 , σ2 )
w′ : (ε, ε, p)△(β
2
Moreover, assumptions (B.2), (B.3) implies
a : β1′ α1 σ1 △ β2′ β3′
That is, we have:

a:

β1 ≃ β1′ α1 σ1

(I.H)

a : β1 △ β2

(B.1)

β1′ α1 σ1

△ β2′ β3′

Applying Lemma 6.3 to these three relations yield β2 ≃ β2′ β3′ . Furthermore,
Lemma 6.10 (a) implies (with B.4) β3′ ≃ α2 σ2 . Finally, Lemma 6.2 (c) gives

β2 ≃ β2′ α2 σ2 as required.
Lemma 6.13 Let γ be a path with p = cod(γ) and w an input string such
that:
¯
w : (ε, ε, p)△(β,
α, σ)
27

Then the following properties hold:
Set(βασ) ⊆ F (γ)

(a)

|σ| ≤ |F (γ)|

(b)

|ασ| ≤ |F (γ)| ∗ o

(c)

Where o is the fan-out of the NFA.
Proof For property (a), suppose w : p △ β ′ . From Lemma 6.8 we get Set(β ′ ) ⊆
F (γ). Moreover, Lemma 6.12 gives βασ ≃ β ′ . Now, Lemma 6.2 (a) gives
βασ ⊆ F (γ).
For property (b), note that it follows from property (a) that Set(σ) ⊆ F (γ).
¯ it follows that ∃ β ′ . (ε, β ′ ) ⊲ ⊲(α, σ). Therefore, from
From the definition of △
Lemma 6.10 (d) we get |σ| = |Set(σ)| ≤ |F (γ)|.
For property (c), suppose w = w′ a (the result holds trivially for w = ε).
¯ there exist σ ′ , β ′ such that:
Then from the definition of △
¯ , , σ′ )
w′ : (ε, ε, p)△(
′

′

a:σ △β
(ε, β ′ ) ⊲ ⊲(α, σ)

(A.1)
(A.2)
(A.3)

From (A.2) and the structure of the NFA, we derive |β ′ | ≤ |σ ′ | ∗ o. Furthermore,
(A.3) and Lemma 6.10 (a) implies ασ ≃ β ′ . Therefore, Lemma 6.2 (a) and
property (b) above leads to |ασ| = |β ′ | ≤ |σ ′ | ∗ o ≤ |F (γ)| ∗ o.

Lemma 6.14 Let w be an input string and p a state. Let k be a constant offset
into w and i an index such that:
0 < i ≤ k ≤ |w|
¯ i , αi , σi )
w[0 : i] : (ε, ε, p)△(β
w[i : k] : αi △ α(i,k)
Then βk = α(1,k) . . . α(k−1,k)
Proof By induction on k (omitted).

With reference to Figure 9, Lemma 6.14 establishes the connection between
the fringe of the overall triangle and those of individual trapezoidal slices (the
concatenation of the bases of the trapezoids make up the base of the overall
triangle).
Lemma 6.15 Let γ be a path with p = cod(γ) and w an input string such
that:
¯
w : (ε, ε, p)△(β,
α, σ)
¯ α, there exists a path γ ′ from p to q such that F (γγ ′ ) ( F (γ).
Then for any q ∈

28

Proof Follows from Lemma 6.8; q is repeated within α, making p ∈ S(γγ ′ ). 
Lemma 6.16 Suppose γ is a path with p = cod(γ) and w an input string of
length n such that:
w:p△β
Then the following holds:
|β| < k k ∗ ok ∗ nk
Where k = |F (γ)|.
Proof By induction on k.
Base case - 1: Suppose k = 0. Then it follows from Lemma 6.8 that |β| = 0,
which is within the bounds of our polynomial.
Base case - 2: Suppose k = c (for some constant c) and:
6 ∃γ ′ . γ ′ = γγ ′′ ∧ F (γ ′ ) < c
This means the search tree rooted at cod(γ) cannot contain duplicates at any
depth, for if it does, we can always find an extended path γ ′ for which F (γ ′ )
is less. This restriction immediately implies that the fringe of the search tree
cannot grow beyond c, which is well within the bounds of our (over-estimating)
polynomial (cc ∗ oc ∗ nc ).
Inductive step: Suppose:
¯ i , αi , σi )
w[0 : i] : (ε, ε, p)△(β
w[i : n] : αi △ α(i,n)
Where 0 < i ≤ n. From Lemma 6.14 we deduce:
βn αn σn = α(1,n) . . . α(n−1,n) αn σn

(A)

It follows from Lemma 6.15 that we can apply the induction hypothesis to each
path ending in some state within an αi . Therefore, we derive:
∀i ∃v < k . α(i,n) < |αi | ∗ v v ∗ ov ∗ |w[i : n]|

v

In terms of the illustration in Figure 9, this statement measures the bottom
edges of the trapezoids. Now, taking into account that v < k and |w[i : k]| < n,
we arrive at:
∀i . α(i,n) < |αi | ∗ k k ∗ ok ∗ nk
Moreover, it follows from Lemma 6.13 (c) that |αi | ≤ k ∗ o. Therefore, we get:
∀i . α(i,n) < k k+1 ∗ ok+1 ∗ nk

29

(B)

Now, we combine (A) and (B) to obtain:
|βn αn σn | < (n − 1) ∗ k k+1 ∗ ok+1 ∗ nk + |αn σn |
Furthermore, it follows from Lemma 6.13 (c) that:
|αn σn | ≤ k ∗ o < k k+1 ∗ ok+1 ∗ nk
Therefore, we get:
|βn αn σn | < k k+1 ∗ ok+1 ∗ nk+1
Since we know β ≃ βn αn σn from Lemma 6.12, the inductive step holds.



Theorem 6.17 (Redos analysis completeness) Given an NFA with an exponential runtime vulnerability, the REDoS analysis presented in Section 3 will
produce an attack string which triggers this behaviour on a backtracking regular
expression matcher.
Proof Lemma 6.16 implies that for a non-pumpable NFA, the search tree width
is polynomially bounded. Since w is finite, the entire search space in turn
becomes polynomially bounded. This suggests that only a pumpable NFA can
lead to an exponentially large search space.
The analysis presented in Section 3 derives an attack string of the form:
x :
y :
z :

p0  (β pℓ β ′ )
Set(β pℓ ) ⇛ Φy
Φy ⇛ Φfail

Φy ⊆ Set(β pℓ )
Φfail ∩ Acc = ∅

For completeness, we must show that all of these conditions (in addition to a
pumpable node pℓ ) are necessary for a backtracking matcher to have an exponential runtime.
Case - 1: Suppose the analysis cannot find a prefix x such that x : p0  β pℓ β ′ .
Given that the prefix analysis is exhaustive (in that, it iterates through all the
unique ordered multi-states corresponding to Q), it would only fail to find a
prefix for some pℓ only if that node is un-reachable in the NFA. This in turn
implies that a backtracking machine would not have to explore the exponentially
large search tree emanatig from pℓ .
Case - 2: Now suppose the analysis finds a prefix x of the form:
x : p0  (β pℓ β ′ )
The next step of the analysis is to find a pumpable string y of the form:
y : Set(β pℓ ) ⇛ Φy

Φy ⊆ Set(β pℓ )

Here we have to establish that a pumpable string of this form must be available
for any vulnerable NFA.
30

It follows from Lemma 6.16 that any successful attack string would have
to exploit a pumpable node in order to generate an exponentially large search
space. Suppose xρi is such an attack string, so that:
x :
ρi =
ρi :

p0  (β pℓ β ′ )
a0 a1 a2 . . . ai
ai ∈ Z
Set(β pℓ ) ⇛ Φρi

In other words, the attack string xρi must allow the ρi component to be extended
while maintaining the exponential search-space expansion. Given the finiteness
of Q, it immediately follows that:
∃j, k . (j < k) ∧ Φρk ⊆ Φρj
That is, as we keep extending ρi , there must come a point where Φρi shrinks.
We now have:
x : p0  (β pℓ β ′ )
ρj : Set(β pℓ ) ⇛ Φρj
Φρk ⊆ Φρj
aj+1 . . . ak : Φρj ⇛ Φρk
Now suppose xρj : p0  (β̄ pℓ β̄ ′ ). It follows from Lemma 5.3 and Lemma 5.4
that Set(β̄ pℓ ) = Φρj . Finally, allowing y = aj+1 . . . ak , we arrive at:
xρi
y

: p0  (β̄ pℓ β̄ ′ )
: Set(β̄ pℓ ) ⇛ Φρk

Φρk ⊆ Set(β̄ pℓ )

That is, for a valid attack string to exist, there must also exist a (prefix, pumpable
string) pair that meets the criteria of the analysis. The fact that the analysis
rejects some configurations not meeting the stability condition is largely irrelevant; the analyser is bound to find a suitable (prefix, pumpable string) pair
eventually (if a valid attack string configuration does indeed exist).
Case - 3: Let x, y be constructed from the analysis such that:
x
y

: p0  (β pℓ β ′ )
: Set(β pℓ ) ⇛ Φy

Φy ⊆ Set(β pℓ )

The final step of the analysis is to construct a failure suffix z such that:
Φfail ∩ Acc = ∅

z : Φy ⇛ Φfail

It is immediately clear that such a suffix must be available for a valid attack
string to exist, as otherwise a backtracking machine would lead to acceptance
and not have to explore the exponentially large search space constructed by the
(x, y) pair.


31

7. Implementation
We implemented the analysis presented above in OCaml [4] (code-named
RXXR). Apart from the code used for parsing regular expressions (and some
other boilerplate code), the main source modules have an almost one-to-one correspondence with the concepts discussed thus far. This relationship is illustrated
in Table 10.
Concept (Theory)
NFA
β
Φ
։2
։3
Prefix analysis
Pumpable analysis (y1 )
Pumpable analysis (ay2 )
Suffix analysis
Overall analysis

Implementation (OCaml Module)
Nfa.mli/ml
Beta.mli/ml
Phi.mli/ml
Product.mli/ml
Triple.mli/ml
XAnalyser.mli/ml
Y1Analyser.mli/ml
Y2Analyser.mli/ml
ZAnalyser.mli/ml
AnalyserMain.mli/ml

Figure 10: Theory to source-code correspondence

Each module interface (.mli file) contains function definitions which directly
correspond to various aspects of the analysis presented earlier. For an example,
the NFA module provides the following function for querying ordered transitions:
val g e t _ t r a n s i t i o n s : Nfa . t -> int ->
(( char * char ) * int ) list ;;

The NFA states are represented as integers. Each symbol of the input alphabet
is encoded as a pair of characters, allowing a uniform representation of character
classes ([a-z]) as well as individual characters.
The NFA used in the implementation (Nfa.mli/ml) contains ε transitions,
which were not part of the NFA formalization presented earlier. The reason
for this deviation is that having ε transitions allows us to preserve the structure of the regular expression within the NFA representation, which in turn
preserves the order of the transitions. The correctness of the implementation is
unaffected as the two forms of NFA representation are semantically equivalent
(i.e. represents the same language). Only a slight mental adjustment (from
ordered NFAs to ε-NFAs) is required to correlate the theoretical formalizations
to the OCaml code. For an example, Figure 11 presents the module interface
for β. The function advance() is utilized inside the XAnalyser.ml module to
perfom the closure computation (i.e. compute all βs reachable from the root
node), whereas evolve() is a utility function used to work around the ε transitions. The modules (Phi / Product / Triple).mli define similar interfaces
for Φ, ։2 and ։3 constructs introduced in the analysis.
32

(* internal r e p r e s e n t a t i o n of beta *)
type t ;;
module BetaSet : ( Set . S with type elt = t ) ;;
(* beta with just one state *)
val make : int -> t ;;
(* returns the set of states contained within this beta *)
val elems : t -> IntSet . t ;;
(* calculate all one - character reachable betas *)
val advance : ( Nfa . t * Word . t * t ) -> ( Word . t * t ) list ;;
(* consume all epsilon transitio n s while recording pumpable kleene
encounter s *)
val evolve : ( Nfa . t * Word . t * t ) -> IntSet . t ->
Flags . t * t * ( int * t ) list ;;

Figure 11: Beta.mli

The different phases of the analysis is implemented inside the corresponding analyser modules. As an example, Figure 12 presents the Y2Analyser.mli
module responsible for carrying out the analysis after the branch point (։3
simulation). The internal representation of the analyser (type t) holds the
state of the closure computation, which is initialized with an initial triple argument through the init() function. We defer the interested reader to module
definition (.ml) files for further details on the implementation.
7.1. Evaluation data
The analysis was tested on two corpora of regexes. The first of these was extracted from an online regex library called RegExLib [5], which is a communitymaintained regex archive; programmers from various disciplines submit their
solutions to various pattern matching tasks, so that other developers can reuse
these expressions for their own pattern matching needs. The second corpus was
extracted from the popular intrusion detection and prevention system Snort [6],
which contains regex-based pattern matching rules for inspecting IP packets
across network boundaries. The contrasting purposes of these two corpora (one
used for casual pattern matching tasks and the other used in a security critical application) allow us to get a better view of the seriousness of exponential
vulnerabilities in practical regular expressions.
The regex archive for RegExLib was only available through the corresponding website [5]. Therefore, as the first step the expressions had to be scraped
from their web source and adapted so that they can be fed into our tool. These
adaptations include removing unnecessary white-space, comments and spurious
line breaks. A detailed description of these adjustments as well as copies of

33

(* internal r e p r e s e n t a t i o n of the analyser *)
type t ;;
(* initialize analyser instance for the specified triple and the
kleene state *)
val init : ( Nfa . t * Word . t * Triple . t ) -> int -> t ;;
(* calculate the next ( y2 , phi ) *)
val next : t -> ( Word . t * Phi . t ) option ;;
(* read analyser flags *)
val flags : t -> Flags . t ;;

Figure 12: Y2Analyser.mli

both adjusted and un-adjusted data sets have been included with the resources
linked from the RXXR distribution [4] (also including the Python script used
for scraping). The regexes for Snort, on the other hand, are embedded within
plain text files that define the Snort rule set. A Python script (also linked from
the RXXR webpage) allowed the extraction of these regexes, and no further
processing was necessary.
7.2. Results
The results of running the analysis on these two corpora of regexes are
presented in Table 13. The figures show that we can process around 75% of
each of the corpora with the current level of syntax support. Out of these
analyzable amounts, it is notable that regular expressions from the RegExLib
archive use the Kleene operator more frequently (about 50% of the analyzable
expressions) than those from the Snort rule set (close to 30%). About 11.5% of
the Kleene-based RegExLib expressions were found to have a pumpable Kleene
expression as well as a suitable suffix, whereas for Snort this figure stands around
0.55%.

Total patterns
Parsable
Pumpable
Vulnerable
Interrupted
Pruned
Time

RegExLib
2992
2290
159
131
4
0
61.51 (s)

Snort
12499
9801
19
15
0
2
30.10 (s)

Figure 13: RXXR2 results - statistics

34

The tool makes every attempt to analyse a given pattern, even the ones
which contain non-regular constructs like backreferences. An expression (e1 |e2 )
may be vulnerable due to a pumpable Kleene that occurs within e1 , whereas
e2 might contain a backreference. In these situations, the analyser attempts
to derive an attack string which avoids the non-regular construct. If such a
non-regular construct cannot be avoided, the analysis is terminated with the
interrupted flag.
On certain rare occasions, search pruning is employed as an optimization.
It is activated when there have been a number of unstable derivations (failing
to meet Φy2 ⊆ Φx ) for a given prefix. For an example, consider the regular
expression:
∗ ∗
([ˆa] b) [ˆc]{1000}
∗

Here the Kleene expression ([ˆa]∗ b) is pumpable for any string which contains
two copies of b (e.g. bb, bab, abb, cbb . . .). However, if the analysis were to pick a
pumpable string that does not contain the symbol c, it will lead to an unstable
derivation. Intuitively, the followup expression [ˆc]{1000} (which has a large
state space) will also consume the pumpable string and introduce a new state in
Φy2 , breaking the inclusion Φy2 ⊆ Φx . Pruning allows the analysis to attempt
different variants of the pumpable string without getting stuck on a single search
path where all of the pumpable strings lead to unstable (but unique) derivations
(e.g. bb, bab, baab, baaab, . . . ). Needless to say, this is an ad-hoc optimization
that can be further improved with more sophisticated heuristics. Given that
pruning was only triggered in two instances for the entire data set above, we
believe the current heuristic (a static bound on the number of unstable derivations) is adequate. If a pruned search does not report a vulnerability, it should
be re-run with a higher (or infinite) prune limit in order to obtain a conclusive
result.
7.2.1. Validation
The task of validating vulnerabilities is complicated by the fact that different
regular expression implementations (Java, Python, .NET etc.) have different
syntax flavours. RXXR itself is written to accept PCRE like patterns of the
form /<REGEX>/<FLAGS> where REGEX contains the main expression and FLAGS
are used to control various aspects of the matching process (e.g. whether to
match multi-line input or not). Java, Python and .NET use separate library
calls to configure such behavior. Moreover, they can also differ from one another
in terms of the syntax allowed within the main expression. For an example, Java
requires tricky escape sequences when working with meta-characters (e.g a literal
backslash requires \\\\), whereas Python is more flexible with its support for
raw (un-interpreted) input strings.
For these reasons we chose Python as our main validation platform (Python’s
support for raw strings makes the porting relatively simple). A sample of vulnerabilities were then manually validated on other platforms (Java, .NET and
PCRE). Table 14 illustrates how Python responds to above vulnerabilities.

35

Total vulnerabilities
Successfully validated
Python parsing bug
Python not vulnerable

RegExLib
131
115
12
4

Snort
15
14
0
1

Figure 14: Validation of vulnerabilities - Python

The Python scripts developed for this validation are also included with the
RXXR distribution [4], along with instructions on how to reproduce the above
results. We discovered that Python was not able to compile regular expressions
∗ ∗
of the form ([a − z] ) , which is a known Python defect [7]. Variants of this
bug affected 12 of the RegExLib vulnerabilities which we could not validate
on Python. The remaining few cases were down to trivial vulnerabilities that
Python manages to work around. We observed that both Python and .NET are
∗
∗
capable of avoiding vulnerabilities in expressions like ([a − c]|b) d or (a|a) b,
where the redundancies are quite obvious. Interestingly however, Java does not
seem to implement any such workarounds; even when matching the expression
(a|a)∗ b against the input string an (n ∼ 50), the JVM (Java Virtual Machine)
becomes non-responsive.
7.2.2. Sample vulnerabilities
The vulnerabilities reported range from trivial programming errors to more
complicated cases. For an example, the following regular expression is meant to
validate time values in 24-hour format (from RegExLib):
^(([01][0-9]|[012][0-3]):([0-5][0-9]))*$
Here the author has mistakenly used the Kleene operator instead of the ? operator to suggest the presence or non-presence of the value. This pattern works
perfectly for all intended inputs. However, our analysis reports that this expression is vulnerable with the pumpable string “13:59” and the suffix “/”. This
result gives the programmer a warning that the regular expression presents a
DoS security risk if exposed to user-malleable input strings to match.
For a moderately complicated example, consider the following regular expression (again from RegExLib):
^([a-zA-z]:((\\([-*\.*\w+\s+\d+]+)|(\w+)\\)+)(\w+.zip)|(\w+.ZIP))$

This expression is meant to validate file paths to zip archives. Our tool identifies this expression as vulnerable and generates the prefix “z:\ ”, the pumpable
string “\zzz\” and the empty string as the suffix. This is probably an unexpected input in the author’s eye, and this is another way in which our tool can
be useful in that it can point out potential mis-interpretations which may have
materialized as vulnerabilities.
Out of the over 12,000 patterns examined, there were two cases that failed
to terminate within any reasonable amount of time. Closer inspection reveals
36

that a pumpable Kleene expression with a vast number of states is to blame.
Consider the following example (from RegExLib):
^(([a-zA-Z0-9_\-\.]+)@([a-zA-Z0-9_\-\.]+)\.
([a-zA-Z]{2,5}){1,25})+
([;.](([a-zA-Z0-9_\-\.]+)@([a-zA-Z0-9_\-\.]+)\.
([a-zA-Z]{2,5}){1,25})+)*$

If we change the counted expressions of the form e{1,25} into e{1,5}, the
analyser returns immediately. This shows that the analysis itself can take a
long time on certain inputs. However, such cases are extremely rare.
7.3. Comparison to fuzzers
REDoS analysers commonly used in practice are based on a brute-force
approach known as fuzzing, where the runtime of a pattern is tested against a
set of strings. A leading example of this approach is the Microsoft’s SDL Regex
Fuzzer [8].
As is common with most brute-force approaches, the main problem with
fuzzing is that it can take a considerable amount of time to detect a vulnerability. This is especially pronounced in the case of REDoS analysis as vulnerable
patterns tend to take increasing amounts of time with each iteration of testing.
This property alone disqualifies fuzzing based REDoS analysers from being integrated into code-analysis tools, as their operation would impose unacceptable
delays. For an example, consider the following simple pattern:
^(a|b|ab)*c$
Even with a lenient fuzzer configuration (ASCII only, 100 fuzzing iterations),
SDL fuzzer takes 5-10 minutes to report a vulnerability on this pattern. By
comparison, our analyser can process tens of thousands of patterns in less time.
Fuzzers can also miss out on vulnerabilities. For an example, consider the
following two patterns:
^.*|(a|b|ab)*c$
^(a|b|ab)*c|.*$
SDL Fuzzer reports both of these patterns as being safe. However, the noncommutative property of the alternation renders the second pattern vulnerable
(as explained in Section 4). Another such example is:
^(a|b|c|ab|bc)*a.*$
For this pattern, only one of the pumpable strings (bc) can lead to an attack
string, and it must not end in an a. Such relationships are difficult to be caught
in a heuristics-based fuzzer.
Yet another problem with fuzzers is caused by the element of randomness
present in their string generating algorithms. Since fuzzers are not based on
any sound theory, some form of randomness is necessary in order to increase
the chance of stumbling upon a valid attack string. However, this can make the
fuzzer yield inconsistent results for the same pattern. Consider the following
pattern for an example:
37

(a|b)*[^c].*|(c)*(a|b|ab)*d
The SDL fuzzer reports this pattern as being safe in most invocations, but in
few cases it finds an attack string.
Finally, the ultimate purpose of using a static analyser is to detect potential
vulnerabilities upfront and lead to the corresponding fixes. Our analyser pinpoints the exact pumpable Kleene expression and generates a string (pumpable
string) which witnesses vulnerability, making the fixing of the error a straightforward task. This is notably in contrast to the fuzzer, which outputs a random
string (mostly in hex format) that does not provide any insight into the source
of the problem.
8. Related work
The starting point for the present paper was the regular expression analysis
RXXR [9]. While that paper was aimed at a security audience, the present
paper complements it by using a programming language approach inspired by
type theory and logic.
Program analysis for security is by now a well established field [10]. REDoS is known in the literature as a special case of algorithmic complexity attacks [11, 12]. Sugiyama and Minamide [13] has recently explored a static
analysis for checking wheather a given regular expression matching operation
can be performed in linear time. Their analysis assumes that the input string is
available at analysis time, which could make it less efficient in that the analysis
must be run each time prior to the actual matching operation. Nevertheless, we
can imagine such an analysis acting as a white-list filter for input strings that
are accepted by a system. On the other hand, our analysis can be run off-line,
allowing system administrators to filter out vulnerable regular expressions much
earlier.
Parsing Expression Grammars (PEGs) have been proposed as an alternative
to regular expressions [14] that avoid their nondeterminism. In a series of tutorials [1, 3], Cox has argued for Thompson’s lockstep matcher [2] as a superior
alternative to backtracking. Cox’s implementation of the lockstep algorithm,
called RE2 [1], guarantees linear time matching of purely regular expressions.
While RE2 also supports few extensions to basic regular expressions (such as
submatch extraction), backtracking matchers still have an advantage when it
comes to complex irregular constructs, backreferences [15] being the case in
point. We believe that this is one of the reasons why the backtracking implementations are is still commonplace. In any case, as long as backtracking
matchers remain widely deployed, the REDoS problem will also remain with us
for the foreseeable future.
Backtracking is a classic application of continuations, and regular expression
matchers similar to the backtracking machine have been investigated in the
functional programming literature [16, 17, 18]. Other recent work on regular
expressions in the programming language community includes regular expression
inclusion [19] and submatching [20].
38

Apart from some basic constructions like the power DFA covered in standard
textbooks [21], we have not explicitly relied on automata theory. Instead, we
regarded the matcher as an abstract machine that can be analyzed with tools
from programming language research. Specifically, the techniques in this paper
are inspired by substructural logics, such as Linear Logic [22, 23] and Separation
Logic [24, 25]. Concerning the latter, it may be instructive to compare the
sharing of w or absence of sharing of β in Figure 6 to the connective of Separation
logic. In a conjunction, the heap h is shared:
h |= P1

h |= P2

h |= P1 ∧ P2
By contrast, in a separating conjunction, the heap is split into disjoint parts
that are not shared:
h1 |= P1

h2 |= P2

h1 ∩ h2 = ∅

h1 ∪ h2 |= P1 ∗ P2
Tree-shaped data structures have been one of the leading examples of separation logic and variations of it, such as Context Logic [26]. However, a difference
to the search trees we have used in this paper is that the whole search tree is not
actually constructed as a data structure in memory. Rather, only a diagonal
cut across it is maintained at any time in the backtracking machine. The whole
tree does not exist in memory, but only in space and time, so to speak. In that
regard the search trees are like parse trees, which the parser only needs to construct in principle by traversing them, and not necessarily as a data structure
in memory complete with details of all nodes [27, 28].
Even though the backtracking machine is sequential, parts of the analysis
are reminiscent of transition systems in process algebras, particularly running
two or more automata in parallel (Figures 4 and 5). Seen that way, the may
and must part of the analysis are analogous to the two modalities hai and [a] in
Henessy-Milner logic [29].
9. Directions for further research
At present, the analysis constructs attack strings when there is the possibility
of exponential runtime. It should be possible to extend the analysis to compute
a polynomial as an upper bound for the runtime when there is no REDoS
vulnerability causing exponential runtime.
The efficiency of the analyser compares favorably with that of the Microsoft
SDL Regex Fuzzer [8]. Given that we are computing sets of sets of states, the
analysis may explore a large search space. One may take some comfort from the
fact that type checking and inference for functional programming languages can
have high complexity in the worst case [30, 31] that may not manifest itself in
practice. Nonetheless, we aim to revisit the design of the analysis and optimize
it.
39

Pruning the search space may lead to improvements in efficiency. An intriguing possibility is to implement the analysis on many-core graphics hardware
(GPUs). Using the right data structure representation for transitions, GPUs
can efficiently explore nondeterministic transitions in parallel, as demonstrated
in the iNFAnt regular expression matcher [32].
The search tree logic (Figure 6) may have independent interest and possible
connections to other substructural logics such as Linear Logic [22, 23], Separation Logic [24, 25], Lambek’s syntactic calculus [33], or substructural calculi for
parse trees [34]. Search trees are dual to parse trees in the sense that the nodes
represent a disjunction rather than a conjunction.
References
[1] R. Cox, Regular Expression Matching Can Be Simple And Fast (but is
slow in Java, Perl, Php, Python, Ruby, ...), Available at http://swtch.
com/~rsc/regexp/regexp1.html (January 2007).
[2] K. Thompson, Programming Techniques: Regular Expression Search
Algorithm, Communications of the ACM 11 (6) (1968) 419–422.
doi:10.1145/363347.363387.
[3] R. Cox, Regular expression matching: the virtual machine approach,
Available at http://swtch.com/~rsc/regexp/regexp2.html (December
2009).
[4] H. Thielecke, A. Rathnayake, RXXR2: Regular expression denial of service
(REDoS) static analysis, Available at http://www.cs.bham.ac.uk/~hxt/
research/rxxr2/index.shtml (2014).
[5] RegExLib.com, Regular Expression Library, Available at http://
regexlib.com/ (2012).
[6] Sourcefire, Snort (IDS/IPS), Available at http://www.snort.org/ (2012).
[7] P. B. Tracker, Issue 2537: re.compile(...) should not fail, Available at
http://bugs.python.org/issue2537 (2008).
[8] Microsoft, SDL Regex Fuzzer, Available at http://www.microsoft.com/
en-gb/download/details.aspx?id=20095 (2011).
[9] J. Kirrage, A. Rathnayake, H. Thielecke, Static analysis for regular expression denial-of-service attacks, in: International Conference on Network and
System Security (NSS 2013), no. LNCS 7873 in LNCS, Springer, 2013, pp.
135–148. doi:10.1007/978-3-642-38631-2_11.
[10] B. Chess, G. McGraw, Static analysis for security, Security & Privacy,
IEEE 2 (6) (2004) 76–79.

40

[11] S. A. Crosby, D. S. Wallach, Denial of Service via Algorithmic Complexity Attacks, in: Proceedings of the 12th USENIX Security Symposium,
Washington, DC, 2003.
[12] R. Smith, C. Estan, S. Jha, Backtracking Algorithmic Complexity Attacks
Against a NIDS, in: Proceedings of the 22nd Annual Computer Security
Applications Conference, ACSAC ’06, IEEE Computer Society, Washington, DC, USA, 2006, pp. 89–98. doi:10.1109/ACSAC.2006.17.
[13] S. Sugiyama, Y. Minamide, Checking Time Linearity of Regular Expression
Matching Based on Backtracking, IPSJ Online Transactions 7 (2014) 82–
92. doi:10.2197/ipsjtrans.7.82.
[14] B. Ford, Parsing expression grammars: a recognition-based syntactic foundation, in: Principles of Programming Languages (POPL 2004), ACM,
2004, pp. 111–122.
[15] A. V. Aho, Algorithms for Finding Patterns in Strings, in: J. van Leeuwen
(Ed.), Handbook of theoretical computer science (vol. A), MIT Press, Cambridge, MA, USA, 1990, pp. 255–300.
URL http://dl.acm.org/citation.cfm?id=114872.114877
[16] O. Danvy, L. R. Nielsen, Defunctionalization at Work, in: Proceedings of
the 3rd ACM SIGPLAN international conference on Principles and practice
of declarative programming, PPDP ’01, ACM, New York, NY, USA, 2001,
pp. 162–174. doi:10.1145/773184.773202.
URL http://doi.acm.org/10.1145/773184.773202
[17] R. Harper, Proof-Directed Debugging, J. Funct. Program. 9 (4) (1999)
463–469. doi:10.1017/S0956796899003378.
[18] A. Frisch, L. Cardelli, Greedy regular expression matching, in: ICALP,
2004, pp. 618–629.
[19] F. Henglein, L. Nielsen, Regular expression containment: coinductive axiomatization and computational interpretation, in: Principles of Programming Languages (POPL 2011), 2011, pp. 385–398.
[20] M. Sulzmann, K. Z. M. Lu, Regular expression sub-matching using partial
derivatives, in: PPDP, 2012, pp. 79–90.
[21] J. E. Hopcroft, J. D. Ullman, Introduction to Automata Theory, Languages
and Computation, Addison-Wesley, 1979.
[22] J.-Y. Girard, Linear logic, Theoretical Computer Science 50 (1987) 1–102.
[23] J.-Y. Girard, Y. Lafont, P. Taylor, Proof and Types, Cambridge University
Press, 1989.

41

[24] S. S. Ishtiaq, P. O’Hearn, BI as an assertion language for mutable data
structures, in: Principles of Programming Languages (POPL), ACM, 2001,
pp. 14–26.
[25] J. C. Reynolds, Separation logic: A logic for shared mutable data structures, in: Logic in Computer Science (LICS), IEEE, 2002, pp. 55–74.
[26] C. Calcagno, P. Gardner, U. Zarfaty, Context logic and tree update., in:
POPL, 2005, pp. 271–282.
[27] A. W. Appel, J. Palsberg, Modern Compiler Implementation in Java, Cambridge University Press, 1997.
[28] A. V. Aho, M. Lam, R. Sethi, J. D. Ullman, Compilers - Principles, Techniques and Tools, 2nd Edition, Addison Wesley, 2007.
[29] M. Hennessy, R. Milner, On observing nondeterminism and concurrency,
in: ICALP, 1980, pp. 299–309.
[30] H. Mairson, Deciding ML typability is complete for deterministic exponential time, in: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium
on Principles of programming languages, ACM, 1989, pp. 382–401.
[31] H. Seidl, Haskell overloading is DEXPTIME-complete, Information Processing Letters 52 (2) (1994) 57–60.
[32] N. Cascarano, P. Rolando, F. Risso, R. Sisto, iNFAnt: NFA Pattern Matching on GPGPU Devices, SIGCOMM Comput. Commun. Rev. 40 (5) (2010)
20–26. doi:10.1145/1880153.1880157.
[33] J. Lambek, The mathematics of sentence structure, American Mathematical Monthly 65 (3) (1958) 154–170.
[34] H. Thielecke, On the semantics of parsing actions, Science of Computer
Programming 84 (2014) 52–76. doi:10.1016/j.scico.2013.04.010.

42

