Module ReDoSUtil

Provides classes for working with regular expressions that can perform backtracking in superlinear/exponential time.

This module contains a number of utility predicates for compiling a regular expression into a NFA and reasoning about this NFA.

The ReDoSConfiguration contains a isReDoSCandidate predicate that is used to to determine which states the prefix/suffix search should happen on. There is only meant to exist one ReDoSConfiguration at a time.

The predicate hasReDoSResult outputs a de-duplicated set of states that will cause backtracking (a rejecting suffix exists).

Import path

import semmle.code.java.security.performance.ReDoSUtil

Imports

ReDoSUtilSpecific

This module should provide a class hierarchy corresponding to a parse tree of regular expressions. This is the interface to the shared ReDoS library.

Predicates

after	Gets a state the NFA may be in after matching `t`.
delta	Holds if the NFA has a transition from `q1` to `q2` labelled with `lbl`.
deltaClosed	Holds if there is a state `q` that can be reached from `q1` along epsilon edges, such that there is a transition from `q` to `q2` that consumes symbol `s`.
epsilonPred	Gets a state that has an epsilon transition to `q`.
epsilonSucc	Gets a state that `q` has an epsilon transition to.
getAnInputSymbolMatching	Gets a symbol that matches `char`.
getCanonicalCharClass	Gets the canonical CharClass for `term`.
getCanonicalizationFlags	Gets a string reperesentation of the flags used with the regular expression. Only the flags that are relevant for the canonicalization are included.
getRoot	Gets the root containing the given term, that is, the root of the literal, or a branch of the root disjunction.
hasReDoSResult	Holds if the state `s` (represented by the term `t`) can have backtracking with repetitions of `pump`.
intersect	Gets a character that is represented by both `c` and `d`.
isStartState	Holds if `state` is a start state.
matchesEpsilon	Holds if `t` matches at least an epsilon symbol.
mkMatch	Gets a state that is about to match the regular expression `t`.

Classes

CharacterClass	An abstract input symbol that represents a character class.
EmptyPositiveSubPatttern	A lookahead/lookbehind that matches the empty string.
InputSymbol	An abstract input symbol, representing a set of concrete characters.
ReDoSConfiguration	A configuration for which parts of a regular expression should be considered relevant for the different predicates in `ReDoS.qll`. Used to adjust the computations for either superlinear or exponential backtracking.
RegExpRoot	A branch in a disjunction that is the root node in a literal, or a literal whose root node is not a disjunction.
RelevantRegExpTerm	A regexp term that is relevant for this ReDoS analysis.
State	A state in the NFA corresponding to a regular expression.

Datatypes

TState

A state in the NFA.