Query module ReDoS

name
Inefficient regular expression
description
A regular expression that requires exponential time to match certain inputs can be a performance bottleneck, and may be vulnerable to denial-of-service attacks.
kind
problem
problem.severity
error
precision
high
id
js/redos
tags
security external/cwe/cwe-730 external/cwe/cwe-400

Imports

javascript

Provides classes for working with JavaScript programs, as well as JSON, YAML and HTML.

Predicates

after

Gets a state the NFA may be in after matching t.

choose

Gets a character matched by character class cc.

compatible

Holds if s1 and s2 possibly have a non-empty intersection.

concretise

Gets a string corresponding to the trace t.

delta

Holds if the NFA has a transition from q1 to q2 labelled with lbl.

delta2
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.

escape

Gets the result of backslash-escaping newlines, carriage-returns and backslashes in s.

getAForkPair

Gets a state in the product automaton from which (fork, fork) is reachable in zero or more epsilon transitions.

getCCLowerBound

Gets a lower bound on the characters matched by the given character class term.

getCCUpperBound

Gets an upper bound on the characters matched by the given character class term.

getRoot

Gets the root containing the given term, that is, the root of the literal, or a branch of the root disjunction.

hasBounds

Holds if s belongs to l and is a character class whose set of matched characters is contained in the interval lo-hi.

highestCharacter

The highest character used in a regular expression. Used to represent intervals without an upper bound.

intersect

Gets a character that is represented by both c and d.

isFork

Holds if there are transitions from q to r1 and from q to r2 labelled with s1 and s2, respectively, where s1 and s2 do not trivially have an empty intersection.

isPumpable

Holds if fork is a pumpable fork with word w.

isReachableFromFork

Holds if r is reachable from (fork, fork) under input w, and there is a path from r back to (fork, fork) with rem steps.

isStatePair
isUniversalClass

Holds if character class cc matches all characters.

mkStatePair

Gets the state pair (q1, q2) or (q2, q1); note that only one or the other is defined.

process

Gets a state that can be reached from pumpable fork consuming the first i+1 characters of w.

statePairDist

Gets the minimum length of a path from q to r in the product automaton.

step

Holds if there are transitions from the components of q to the corresponding components of r labelled with s1 and s2, respectively.

step

Holds if there are transitions from the components of q to r1 and r2 labelled with s1 and s2, respectively.

Classes

EdgeLabel
InputSymbol

An abstract input symbol, representing a set of concrete characters.

RegExpRepetition

A term that matches repetitions of a given pattern, that is, E*, E+, or E{n,m}.

RegExpRoot

A branch in a disjunction that is the root node in a literal, or a literal whose root node is not a disjunction.

State

A state in the NFA corresponding to a regular expression.

StatePair

Datatypes

TInputSymbol

An abstract input symbol, representing a set of concrete characters.

TState
TStatePair

A state in the product automaton.

Trace

A list of pairs of input symbols that describe a path in the product automaton starting from some fork state.