mirror of
https://github.com/github/codeql.git
synced 2026-04-25 16:55:19 +02:00
Add query for polynomial ReDoS
This commit is contained in:
@@ -381,11 +381,25 @@ module ExprNodes {
|
||||
final override StringLiteral getExpr() { result = super.getExpr() }
|
||||
}
|
||||
|
||||
/** A control-flow node that wraps a `RegExpLiteral` AST expression. */
|
||||
class RegExpLiteralCfgNode extends ExprCfgNode {
|
||||
override RegExpLiteral e;
|
||||
|
||||
final override RegExpLiteral getExpr() { result = super.getExpr() }
|
||||
}
|
||||
|
||||
/** A control-flow node that wraps a `ComparisonOperation` AST expression. */
|
||||
class ComparisonOperationCfgNode extends BinaryOperationCfgNode {
|
||||
ComparisonOperationCfgNode() { e instanceof ComparisonOperation }
|
||||
|
||||
final override ComparisonOperation getExpr() { result = super.getExpr() }
|
||||
override ComparisonOperation getExpr() { result = super.getExpr() }
|
||||
}
|
||||
|
||||
/** A control-flow node that wraps a `RelationalOperation` AST expression. */
|
||||
class RelationalOperationCfgNode extends ComparisonOperationCfgNode {
|
||||
RelationalOperationCfgNode() { e instanceof RelationalOperation }
|
||||
|
||||
final override RelationalOperation getExpr() { result = super.getExpr() }
|
||||
}
|
||||
|
||||
/** A control-flow node that wraps an `ElementReference` AST expression. */
|
||||
|
||||
37
ql/lib/codeql/ruby/regexp/PolynomialReDoS.qll
Normal file
37
ql/lib/codeql/ruby/regexp/PolynomialReDoS.qll
Normal file
@@ -0,0 +1,37 @@
|
||||
/**
|
||||
* Provides a taint tracking configuration for reasoning about
|
||||
* polynomial regular expression denial-of-service attacks.
|
||||
*
|
||||
* Note, for performance reasons: only import this file if
|
||||
* `PolynomialReDoS::Configuration` is needed, otherwise
|
||||
* `PolynomialReDoSCustomizations` should be imported instead.
|
||||
*/
|
||||
|
||||
private import codeql.ruby.DataFlow
|
||||
private import codeql.ruby.TaintTracking
|
||||
|
||||
/**
|
||||
* Provides a taint-tracking configuration for detecting polynomial regular
|
||||
* expression denial of service vulnerabilities.
|
||||
*/
|
||||
module PolynomialReDoS {
|
||||
import PolynomialReDoSCustomizations::PolynomialReDoS
|
||||
|
||||
/**
|
||||
* A taint-tracking configuration for detecting polynomial regular expression
|
||||
* denial of service vulnerabilities.
|
||||
*/
|
||||
class Configuration extends TaintTracking::Configuration {
|
||||
Configuration() { this = "PolynomialReDoS" }
|
||||
|
||||
override predicate isSource(DataFlow::Node source) { source instanceof Source }
|
||||
|
||||
override predicate isSink(DataFlow::Node sink) { sink instanceof Sink }
|
||||
|
||||
override predicate isSanitizer(DataFlow::Node node) { node instanceof Sanitizer }
|
||||
|
||||
override predicate isSanitizerGuard(DataFlow::BarrierGuard node) {
|
||||
node instanceof SanitizerGuard
|
||||
}
|
||||
}
|
||||
}
|
||||
129
ql/lib/codeql/ruby/regexp/PolynomialReDoSCustomizations.qll
Normal file
129
ql/lib/codeql/ruby/regexp/PolynomialReDoSCustomizations.qll
Normal file
@@ -0,0 +1,129 @@
|
||||
/**
|
||||
* Provides default sources, sinks and sanitizers for reasoning about
|
||||
* polynomial regular expression denial-of-service attacks, as well
|
||||
* as extension points for adding your own.
|
||||
*/
|
||||
|
||||
private import codeql.ruby.AST as AST
|
||||
private import codeql.ruby.CFG
|
||||
private import codeql.ruby.DataFlow
|
||||
private import codeql.ruby.dataflow.RemoteFlowSources
|
||||
private import codeql.ruby.regexp.ParseRegExp as RegExp
|
||||
private import codeql.ruby.regexp.RegExpTreeView
|
||||
private import codeql.ruby.regexp.SuperlinearBackTracking
|
||||
|
||||
module PolynomialReDoS {
|
||||
/**
|
||||
* A data flow source node for polynomial regular expression denial-of-service vulnerabilities.
|
||||
*/
|
||||
abstract class Source extends DataFlow::Node { }
|
||||
|
||||
/**
|
||||
* A data flow sink node for polynomial regular expression denial-of-service vulnerabilities.
|
||||
*/
|
||||
abstract class Sink extends DataFlow::Node {
|
||||
/** Gets the regex that is being executed by this node. */
|
||||
abstract RegExpTerm getRegExp();
|
||||
|
||||
/** Gets the node to highlight in the alert message. */
|
||||
DataFlow::Node getHighlight() { result = this }
|
||||
}
|
||||
|
||||
/**
|
||||
* A sanitizer for polynomial regular expression denial-of-service vulnerabilities.
|
||||
*/
|
||||
abstract class Sanitizer extends DataFlow::Node { }
|
||||
|
||||
/**
|
||||
* A sanitizer guard for polynomial regular expression denial of service
|
||||
* vulnerabilities.
|
||||
*/
|
||||
abstract class SanitizerGuard extends DataFlow::BarrierGuard { }
|
||||
|
||||
/**
|
||||
* A source of remote user input, considered as a flow source.
|
||||
*/
|
||||
class RemoteFlowSourceAsSource extends Source, RemoteFlowSource { }
|
||||
|
||||
/**
|
||||
* Gets the AST of a regular expression object that can flow to `node`.
|
||||
*/
|
||||
RegExpTerm getRegExpObjectFromNode(DataFlow::Node node) {
|
||||
exists(DataFlow::LocalSourceNode regexp |
|
||||
regexp.flowsTo(node) and
|
||||
result = regexp.asExpr().(CfgNodes::ExprNodes::RegExpLiteralCfgNode).getExpr().getParsed()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* A regexp match against a superlinear backtracking term, seen as a sink for
|
||||
* polynomial regular expression denial-of-service vulnerabilities.
|
||||
*/
|
||||
class PolynomialBackTrackingTermMatch extends Sink {
|
||||
PolynomialBackTrackingTerm term;
|
||||
DataFlow::ExprNode matchNode;
|
||||
|
||||
PolynomialBackTrackingTermMatch() {
|
||||
exists(DataFlow::Node regexp |
|
||||
term.getRootTerm() = getRegExpObjectFromNode(regexp) and
|
||||
(
|
||||
// `=~` or `!~`
|
||||
exists(CfgNodes::ExprNodes::BinaryOperationCfgNode op |
|
||||
matchNode.asExpr() = op and
|
||||
(
|
||||
op.getExpr() instanceof AST::RegExpMatchExpr or
|
||||
op.getExpr() instanceof AST::NoRegExpMatchExpr
|
||||
) and
|
||||
(
|
||||
this.asExpr() = op.getLeftOperand() and regexp.asExpr() = op.getRightOperand()
|
||||
or
|
||||
this.asExpr() = op.getRightOperand() and regexp.asExpr() = op.getLeftOperand()
|
||||
)
|
||||
)
|
||||
or
|
||||
// Any of the methods on `String` that take a regexp.
|
||||
exists(CfgNodes::ExprNodes::MethodCallCfgNode call |
|
||||
matchNode.asExpr() = call and
|
||||
call.getExpr().getMethodName() =
|
||||
[
|
||||
"[]", "gsub", "gsub!", "index", "match", "match?", "partition", "rindex",
|
||||
"rpartition", "scan", "slice!", "split", "sub", "sub!"
|
||||
] and
|
||||
this.asExpr() = call.getReceiver() and
|
||||
regexp.asExpr() = call.getArgument(0)
|
||||
)
|
||||
or
|
||||
// A call to `match` or `match?` where the regexp is the receiver.
|
||||
exists(CfgNodes::ExprNodes::MethodCallCfgNode call |
|
||||
matchNode.asExpr() = call and
|
||||
call.getExpr().getMethodName() = ["match", "match?"] and
|
||||
regexp.asExpr() = call.getReceiver() and
|
||||
this.asExpr() = call.getArgument(0)
|
||||
)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
override RegExpTerm getRegExp() { result = term }
|
||||
|
||||
override DataFlow::Node getHighlight() { result = matchNode }
|
||||
}
|
||||
|
||||
/**
|
||||
* A check on the length of a string, seen as a sanitizer guard.
|
||||
*/
|
||||
class LengthGuard extends SanitizerGuard, CfgNodes::ExprNodes::RelationalOperationCfgNode {
|
||||
private DataFlow::Node input;
|
||||
|
||||
LengthGuard() {
|
||||
exists(DataFlow::CallNode length, DataFlow::ExprNode operand |
|
||||
length.asExpr().getExpr().(AST::MethodCall).getMethodName() = "length" and
|
||||
length.getReceiver() = input and
|
||||
length.flowsTo(operand) and
|
||||
operand.getExprNode() = this.getAnOperand()
|
||||
)
|
||||
}
|
||||
|
||||
override DataFlow::Node getAGuardedNode() { result = input }
|
||||
}
|
||||
}
|
||||
@@ -12,7 +12,7 @@
|
||||
* states that will cause backtracking (a rejecting suffix exists).
|
||||
*/
|
||||
|
||||
private import RegExpTreeView
|
||||
import RegExpTreeView
|
||||
private import codeql.Locations
|
||||
|
||||
/**
|
||||
|
||||
420
ql/lib/codeql/ruby/regexp/SuperlinearBackTracking.qll
Normal file
420
ql/lib/codeql/ruby/regexp/SuperlinearBackTracking.qll
Normal file
@@ -0,0 +1,420 @@
|
||||
/**
|
||||
* Provides classes for working with regular expressions that can
|
||||
* perform backtracking in superlinear time.
|
||||
*/
|
||||
|
||||
import ReDoSUtil
|
||||
|
||||
/*
|
||||
* This module implements the analysis described in the paper:
|
||||
* Valentin Wustholz, Oswaldo Olivo, Marijn J. H. Heule, and Isil Dillig:
|
||||
* Static Detection of DoS Vulnerabilities in
|
||||
* Programs that use Regular Expressions
|
||||
* (Extended Version).
|
||||
* (https://arxiv.org/pdf/1701.04045.pdf)
|
||||
*
|
||||
* Theorem 3 from the paper describes the basic idea.
|
||||
*
|
||||
* The following explains the idea using variables and predicate names that are used in the implementation:
|
||||
* We consider a pair of repetitions, which we will call `pivot` and `succ`.
|
||||
*
|
||||
* We create a product automaton of 3-tuples of states (see `StateTuple`).
|
||||
* There exists a transition `(a,b,c) -> (d,e,f)` in the product automaton
|
||||
* iff there exists three transitions in the NFA `a->d, b->e, c->f` where those three
|
||||
* transitions all match a shared character `char`. (see `getAThreewayIntersect`)
|
||||
*
|
||||
* We start a search in the product automaton at `(pivot, pivot, succ)`,
|
||||
* and search for a series of transitions (a `Trace`), such that we end
|
||||
* at `(pivot, succ, succ)` (see `isReachableFromStartTuple`).
|
||||
*
|
||||
* For example, consider the regular expression `/^\d*5\w*$/`.
|
||||
* The search will start at the tuple `(\d*, \d*, \w*)` and search
|
||||
* for a path to `(\d*, \w*, \w*)`.
|
||||
* This path exists, and consists of a single transition in the product automaton,
|
||||
* where the three corresponding NFA edges all match the character `"5"`.
|
||||
*
|
||||
* The start-state in the NFA has an any-transition to itself, this allows us to
|
||||
* flag regular expressions such as `/a*$/` - which does not have a start anchor -
|
||||
* and can thus start matching anywhere.
|
||||
*
|
||||
* The implementation is not perfect.
|
||||
* It has the same suffix detection issue as the `js/redos` query, which can cause false positives.
|
||||
* It also doesn't find all transitions in the product automaton, which can cause false negatives.
|
||||
*/
|
||||
|
||||
/**
|
||||
* An instantiaion of `ReDoSConfiguration` for superlinear ReDoS.
|
||||
*/
|
||||
class SuperLinearReDoSConfiguration extends ReDoSConfiguration {
|
||||
SuperLinearReDoSConfiguration() { this = "SuperLinearReDoSConfiguration" }
|
||||
|
||||
override predicate isReDoSCandidate(State state, string pump) { isPumpable(_, state, pump) }
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets any root (start) state of a regular expression.
|
||||
*/
|
||||
private State getRootState() { result = mkMatch(any(RegExpRoot r)) }
|
||||
|
||||
private newtype TStateTuple =
|
||||
MkStateTuple(State q1, State q2, State q3) {
|
||||
// starts at (pivot, pivot, succ)
|
||||
isStartLoops(q1, q3) and q1 = q2
|
||||
or
|
||||
step(_, _, _, _, q1, q2, q3) and FeasibleTuple::isFeasibleTuple(q1, q2, q3)
|
||||
}
|
||||
|
||||
/**
|
||||
* A state in the product automaton.
|
||||
* The product automaton contains 3-tuples of states.
|
||||
*
|
||||
* We lazily only construct those states that we are actually
|
||||
* going to need.
|
||||
* Either a start state `(pivot, pivot, succ)`, or a state
|
||||
* where there exists a transition from an already existing state.
|
||||
*
|
||||
* The exponential variant of this query (`js/redos`) uses an optimization
|
||||
* trick where `q1 <= q2`. This trick cannot be used here as the order
|
||||
* of the elements matter.
|
||||
*/
|
||||
class StateTuple extends TStateTuple {
|
||||
State q1;
|
||||
State q2;
|
||||
State q3;
|
||||
|
||||
StateTuple() { this = MkStateTuple(q1, q2, q3) }
|
||||
|
||||
/**
|
||||
* Gest a string repesentation of this tuple.
|
||||
*/
|
||||
string toString() { result = "(" + q1 + ", " + q2 + ", " + q3 + ")" }
|
||||
|
||||
/**
|
||||
* Holds if this tuple is `(r1, r2, r3)`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate isTuple(State r1, State r2, State r3) { r1 = q1 and r2 = q2 and r3 = q3 }
|
||||
}
|
||||
|
||||
/**
|
||||
* A module for determining feasible tuples for the product automaton.
|
||||
*
|
||||
* The implementation is split into many predicates for performance reasons.
|
||||
*/
|
||||
private module FeasibleTuple {
|
||||
/**
|
||||
* Holds if the tuple `(r1, r2, r3)` might be on path from a start-state to an end-state in the product automaton.
|
||||
*/
|
||||
pragma[inline]
|
||||
predicate isFeasibleTuple(State r1, State r2, State r3) {
|
||||
// The first element is either inside a repetition (or the start state itself)
|
||||
isRepetitionOrStart(r1) and
|
||||
// The last element is inside a repetition
|
||||
stateInsideRepetition(r3) and
|
||||
// The states are reachable in the NFA in the order r1 -> r2 -> r3
|
||||
delta+(r1) = r2 and
|
||||
delta+(r2) = r3 and
|
||||
// The first element can reach a beginning (the "pivot" state in a `(pivot, succ)` pair).
|
||||
canReachABeginning(r1) and
|
||||
// The last element can reach a target (the "succ" state in a `(pivot, succ)` pair).
|
||||
canReachATarget(r3)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `s` is either inside a repetition, or is the start state (which is a repetition).
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate isRepetitionOrStart(State s) { stateInsideRepetition(s) or s = getRootState() }
|
||||
|
||||
/**
|
||||
* Holds if state `s` might be inside a backtracking repetition.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate stateInsideRepetition(State s) {
|
||||
s.getRepr().getParent*() instanceof InfiniteRepetitionQuantifier
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there exists a path in the NFA from `s` to a "pivot" state
|
||||
* (from a `(pivot, succ)` pair that starts the search).
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate canReachABeginning(State s) {
|
||||
delta+(s) = any(State pivot | isStartLoops(pivot, _))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there exists a path in the NFA from `s` to a "succ" state
|
||||
* (from a `(pivot, succ)` pair that starts the search).
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate canReachATarget(State s) { delta+(s) = any(State succ | isStartLoops(_, succ)) }
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `pivot` and `succ` are a pair of loops that could be the beginning of a quadratic blowup.
|
||||
*
|
||||
* There is a slight implementation difference compared to the paper: this predicate requires that `pivot != succ`.
|
||||
* The case where `pivot = succ` causes exponential backtracking and is handled by the `js/redos` query.
|
||||
*/
|
||||
predicate isStartLoops(State pivot, State succ) {
|
||||
pivot != succ and
|
||||
succ.getRepr() instanceof InfiniteRepetitionQuantifier and
|
||||
delta+(pivot) = succ and
|
||||
(
|
||||
pivot.getRepr() instanceof InfiniteRepetitionQuantifier
|
||||
or
|
||||
pivot = mkMatch(any(RegExpRoot root))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a state for which there exists a transition in the NFA from `s'.
|
||||
*/
|
||||
State delta(State s) { delta(s, _, result) }
|
||||
|
||||
/**
|
||||
* Holds if there are transitions from the components of `q` to the corresponding
|
||||
* components of `r` labelled with `s1`, `s2`, and `s3`, respectively.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate step(StateTuple q, InputSymbol s1, InputSymbol s2, InputSymbol s3, StateTuple r) {
|
||||
exists(State r1, State r2, State r3 |
|
||||
step(q, s1, s2, s3, r1, r2, r3) and r = MkStateTuple(r1, r2, r3)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there are transitions from the components of `q` to `r1`, `r2`, and `r3
|
||||
* labelled with `s1`, `s2`, and `s3`, respectively.
|
||||
*/
|
||||
pragma[noopt]
|
||||
predicate step(
|
||||
StateTuple q, InputSymbol s1, InputSymbol s2, InputSymbol s3, State r1, State r2, State r3
|
||||
) {
|
||||
exists(State q1, State q2, State q3 | q.isTuple(q1, q2, q3) |
|
||||
deltaClosed(q1, s1, r1) and
|
||||
deltaClosed(q2, s2, r2) and
|
||||
deltaClosed(q3, s3, r3) and
|
||||
// use noopt to force the join on `getAThreewayIntersect` to happen last.
|
||||
exists(getAThreewayIntersect(s1, s2, s3))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a char that is matched by all the edges `s1`, `s2`, and `s3`.
|
||||
*
|
||||
* The result is not complete, and might miss some combination of edges that share some character.
|
||||
*/
|
||||
pragma[noinline]
|
||||
string getAThreewayIntersect(InputSymbol s1, InputSymbol s2, InputSymbol s3) {
|
||||
result = minAndMaxIntersect(s1, s2) and result = [intersect(s2, s3), intersect(s1, s3)]
|
||||
or
|
||||
result = minAndMaxIntersect(s1, s3) and result = [intersect(s2, s3), intersect(s1, s2)]
|
||||
or
|
||||
result = minAndMaxIntersect(s2, s3) and result = [intersect(s1, s2), intersect(s1, s3)]
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the minimum and maximum characters that intersect between `a` and `b`.
|
||||
* This predicate is used to limit the size of `getAThreewayIntersect`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
string minAndMaxIntersect(InputSymbol a, InputSymbol b) {
|
||||
result = [min(intersect(a, b)), max(intersect(a, b))]
|
||||
}
|
||||
|
||||
private newtype TTrace =
|
||||
Nil() or
|
||||
Step(InputSymbol s1, InputSymbol s2, InputSymbol s3, TTrace t) {
|
||||
exists(StateTuple p |
|
||||
isReachableFromStartTuple(_, _, p, t, _) and
|
||||
step(p, s1, s2, s3, _)
|
||||
)
|
||||
or
|
||||
exists(State pivot, State succ | isStartLoops(pivot, succ) |
|
||||
t = Nil() and step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, _)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* A list of tuples of input symbols that describe a path in the product automaton
|
||||
* starting from some start state.
|
||||
*/
|
||||
class Trace extends TTrace {
|
||||
/**
|
||||
* Gets a string representation of this Trace that can be used for debug purposes.
|
||||
*/
|
||||
string toString() {
|
||||
this = Nil() and result = "Nil()"
|
||||
or
|
||||
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace t | this = Step(s1, s2, s3, t) |
|
||||
result = "Step(" + s1 + ", " + s2 + ", " + s3 + ", " + t + ")"
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a string corresponding to the trace `t`.
|
||||
*/
|
||||
string concretise(Trace t) {
|
||||
t = Nil() and result = ""
|
||||
or
|
||||
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace rest | t = Step(s1, s2, s3, rest) |
|
||||
result = concretise(rest) + getAThreewayIntersect(s1, s2, s3)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there exists a transition from `r` to `q` in the product automaton.
|
||||
* Notice that the arguments are flipped, and thus the direction is backwards.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate tupleDeltaBackwards(StateTuple q, StateTuple r) { step(r, _, _, _, q) }
|
||||
|
||||
/**
|
||||
* Holds if `tuple` is an end state in our search.
|
||||
* That means there exists a pair of loops `(pivot, succ)` such that `tuple = (pivot, succ, succ)`.
|
||||
*/
|
||||
predicate isEndTuple(StateTuple tuple) { tuple = getAnEndTuple(_, _) }
|
||||
|
||||
/**
|
||||
* Gets the minimum length of a path from `r` to some an end state `end`.
|
||||
*
|
||||
* The implementation searches backwards from the end-tuple.
|
||||
* This approach was chosen because it is way more efficient if the first predicate given to `shortestDistances` is small.
|
||||
* The `end` argument must always be an end state.
|
||||
*/
|
||||
int distBackFromEnd(StateTuple r, StateTuple end) =
|
||||
shortestDistances(isEndTuple/1, tupleDeltaBackwards/2)(end, r, result)
|
||||
|
||||
/**
|
||||
* Holds if there exists a pair of repetitions `(pivot, succ)` in the regular expression such that:
|
||||
* `tuple` is reachable from `(pivot, pivot, succ)` in the product automaton,
|
||||
* and there is a distance of `dist` from `tuple` to the nearest end-tuple `(pivot, succ, succ)`,
|
||||
* and a path from a start-state to `tuple` follows the transitions in `trace`.
|
||||
*/
|
||||
predicate isReachableFromStartTuple(State pivot, State succ, StateTuple tuple, Trace trace, int dist) {
|
||||
// base case. The first step is inlined to start the search after all possible 1-steps, and not just the ones with the shortest path.
|
||||
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, State q1, State q2, State q3 |
|
||||
isStartLoops(pivot, succ) and
|
||||
step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, tuple) and
|
||||
tuple = MkStateTuple(q1, q2, q3) and
|
||||
trace = Step(s1, s2, s3, Nil()) and
|
||||
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ))
|
||||
)
|
||||
or
|
||||
// recursive case
|
||||
exists(StateTuple p, Trace v, InputSymbol s1, InputSymbol s2, InputSymbol s3 |
|
||||
isReachableFromStartTuple(pivot, succ, p, v, dist + 1) and
|
||||
dist = isReachableFromStartTupleHelper(pivot, succ, tuple, p, s1, s2, s3) and
|
||||
trace = Step(s1, s2, s3, v)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Helper predicate for the recursive case in `isReachableFromStartTuple`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private int isReachableFromStartTupleHelper(
|
||||
State pivot, State succ, StateTuple r, StateTuple p, InputSymbol s1, InputSymbol s2,
|
||||
InputSymbol s3
|
||||
) {
|
||||
result = distBackFromEnd(r, MkStateTuple(pivot, succ, succ)) and
|
||||
step(p, s1, s2, s3, r)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the tuple `(pivot, succ, succ)` from the product automaton.
|
||||
*/
|
||||
StateTuple getAnEndTuple(State pivot, State succ) {
|
||||
isStartLoops(pivot, succ) and
|
||||
result = MkStateTuple(pivot, succ, succ)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if matching repetitions of `pump` can:
|
||||
* 1) Transition from `pivot` back to `pivot`.
|
||||
* 2) Transition from `pivot` to `succ`.
|
||||
* 3) Transition from `succ` to `succ`.
|
||||
*
|
||||
* From theorem 3 in the paper linked in the top of this file we can therefore conclude that
|
||||
* the regular expression has polynomial backtracking - if a rejecting suffix exists.
|
||||
*
|
||||
* This predicate is used by `SuperLinearReDoSConfiguration`, and the final results are
|
||||
* available in the `hasReDoSResult` predicate.
|
||||
*/
|
||||
predicate isPumpable(State pivot, State succ, string pump) {
|
||||
exists(StateTuple q, Trace t |
|
||||
isReachableFromStartTuple(pivot, succ, q, t, _) and
|
||||
q = getAnEndTuple(pivot, succ) and
|
||||
pump = concretise(t)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if repetitions of `pump` at `t` will cause polynomial backtracking.
|
||||
*/
|
||||
predicate polynimalReDoS(RegExpTerm t, string pump, string prefixMsg, RegExpTerm prev) {
|
||||
exists(State s, State pivot |
|
||||
hasReDoSResult(t, pump, s, prefixMsg) and
|
||||
isPumpable(pivot, s, _) and
|
||||
prev = pivot.getRepr()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a message for why `term` can cause polynomial backtracking.
|
||||
*/
|
||||
string getReasonString(RegExpTerm term, string pump, string prefixMsg, RegExpTerm prev) {
|
||||
polynimalReDoS(term, pump, prefixMsg, prev) and
|
||||
result =
|
||||
"Strings " + prefixMsg + "with many repetitions of '" + pump +
|
||||
"' can start matching anywhere after the start of the preceeding " + prev
|
||||
}
|
||||
|
||||
/**
|
||||
* A term that may cause a regular expression engine to perform a
|
||||
* polynomial number of match attempts, relative to the input length.
|
||||
*/
|
||||
class PolynomialBackTrackingTerm extends InfiniteRepetitionQuantifier {
|
||||
string reason;
|
||||
string pump;
|
||||
string prefixMsg;
|
||||
RegExpTerm prev;
|
||||
|
||||
PolynomialBackTrackingTerm() {
|
||||
reason = getReasonString(this, pump, prefixMsg, prev) and
|
||||
// there might be many reasons for this term to have polynomial backtracking - we pick the shortest one.
|
||||
reason = min(string msg | msg = getReasonString(this, _, _, _) | msg order by msg.length(), msg)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if all non-empty successors to the polynomial backtracking term matches the end of the line.
|
||||
*/
|
||||
predicate isAtEndLine() {
|
||||
forall(RegExpTerm succ | this.getSuccessor+() = succ and not matchesEpsilon(succ) |
|
||||
succ instanceof RegExpDollar
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the string that should be repeated to cause this regular expression to perform polynomially.
|
||||
*/
|
||||
string getPumpString() { result = pump }
|
||||
|
||||
/**
|
||||
* Gets a message for which prefix a matching string must start with for this term to cause polynomial backtracking.
|
||||
*/
|
||||
string getPrefixMessage() { result = prefixMsg }
|
||||
|
||||
/**
|
||||
* Gets a predecessor to `this`, which also loops on the pump string, and thereby causes polynomial backtracking.
|
||||
*/
|
||||
RegExpTerm getPreviousLoop() { result = prev }
|
||||
|
||||
/**
|
||||
* Gets the reason for the number of match attempts.
|
||||
*/
|
||||
string getReason() { result = reason }
|
||||
}
|
||||
113
ql/src/queries/security/cwe-1333/PolynomialReDoS.qhelp
Normal file
113
ql/src/queries/security/cwe-1333/PolynomialReDoS.qhelp
Normal file
@@ -0,0 +1,113 @@
|
||||
<!DOCTYPE qhelp PUBLIC
|
||||
"-//Semmle//qhelp//EN"
|
||||
"qhelp.dtd">
|
||||
|
||||
<qhelp>
|
||||
|
||||
<include src="ReDoSIntroduction.inc.qhelp" />
|
||||
|
||||
<example>
|
||||
<p>
|
||||
|
||||
Consider this use of a regular expression, which removes
|
||||
all leading and trailing whitespace in a string:
|
||||
|
||||
</p>
|
||||
|
||||
<sample language="ruby">
|
||||
text.gsub!(/^\s+|\s+$/, '') # BAD
|
||||
</sample>
|
||||
|
||||
<p>
|
||||
|
||||
The sub-expression <code>"\s+$"</code> will match the
|
||||
whitespace characters in <code>text</code> from left to
|
||||
right, but it can start matching anywhere within a
|
||||
whitespace sequence. This is problematic for strings
|
||||
that do <strong>not</strong> end with a whitespace
|
||||
character. Such a string will force the regular
|
||||
expression engine to process each whitespace sequence
|
||||
once per whitespace character in the sequence.
|
||||
|
||||
</p>
|
||||
|
||||
<p>
|
||||
|
||||
This ultimately means that the time cost of trimming a
|
||||
string is quadratic in the length of the string. So a
|
||||
string like <code>"a b"</code> will take milliseconds to
|
||||
process, but a similar string with a million spaces
|
||||
instead of just one will take several minutes.
|
||||
|
||||
</p>
|
||||
|
||||
<p>
|
||||
|
||||
Avoid this problem by rewriting the regular expression
|
||||
to not contain the ambiguity about when to start
|
||||
matching whitespace sequences. For instance, by using a
|
||||
negative look-behind
|
||||
(<code>/^\s+|(?<!\s)\s+$/</code>), or just by using
|
||||
the built-in strip method (<code>text.strip!</code>).
|
||||
|
||||
</p>
|
||||
|
||||
<p>
|
||||
|
||||
Note that the sub-expression <code>"^\s+"</code> is
|
||||
<strong>not</strong> problematic as the <code>^</code>
|
||||
anchor restricts when that sub-expression can start
|
||||
matching, and as the regular expression engine matches
|
||||
from left to right.
|
||||
|
||||
</p>
|
||||
|
||||
</example>
|
||||
|
||||
<example>
|
||||
|
||||
<p>
|
||||
|
||||
As a similar, but slightly subtler problem, consider the
|
||||
regular expression that matches lines with numbers, possibly written
|
||||
using scientific notation:
|
||||
</p>
|
||||
|
||||
<sample language="ruby">
|
||||
/^0\.\d+E?\d+$/ # BAD
|
||||
</sample>
|
||||
|
||||
<p>
|
||||
|
||||
The problem with this regular expression is in the
|
||||
sub-expression <code>\d+E?\d+</code> because the second
|
||||
<code>\d+</code> can start matching digits anywhere
|
||||
after the first match of the first <code>\d+</code> if
|
||||
there is no <code>E</code> in the input string.
|
||||
|
||||
</p>
|
||||
|
||||
<p>
|
||||
|
||||
This is problematic for strings that do
|
||||
<strong>not</strong> end with a digit. Such a string
|
||||
will force the regular expression engine to process each
|
||||
digit sequence once per digit in the sequence, again
|
||||
leading to a quadratic time complexity.
|
||||
|
||||
</p>
|
||||
|
||||
<p>
|
||||
|
||||
To make the processing faster, the regular expression
|
||||
should be rewritten such that the two <code>\d+</code>
|
||||
sub-expressions do not have overlapping matches:
|
||||
<code>/^0\.\d+(E\d+)?$/</code>.
|
||||
|
||||
</p>
|
||||
|
||||
</example>
|
||||
|
||||
<include src="ReDoSReferences.inc.qhelp"/>
|
||||
|
||||
</qhelp>
|
||||
30
ql/src/queries/security/cwe-1333/PolynomialReDoS.ql
Normal file
30
ql/src/queries/security/cwe-1333/PolynomialReDoS.ql
Normal file
@@ -0,0 +1,30 @@
|
||||
/**
|
||||
* @name Polynomial regular expression used on uncontrolled data
|
||||
* @description A regular expression that can require polynomial time
|
||||
* to match may be vulnerable to denial-of-service attacks.
|
||||
* @kind path-problem
|
||||
* @problem.severity warning
|
||||
* @precision high
|
||||
* @id rb/polynomial-redos
|
||||
* @tags security
|
||||
* external/cwe/cwe-1333
|
||||
* external/cwe/cwe-730
|
||||
* external/cwe/cwe-400
|
||||
*/
|
||||
|
||||
import DataFlow::PathGraph
|
||||
import codeql.ruby.DataFlow
|
||||
import codeql.ruby.regexp.PolynomialReDoS
|
||||
import codeql.ruby.regexp.SuperlinearBackTracking
|
||||
|
||||
from
|
||||
PolynomialReDoS::Configuration config, DataFlow::PathNode source, DataFlow::PathNode sink,
|
||||
PolynomialReDoS::Sink sinkNode, PolynomialBackTrackingTerm regexp
|
||||
where
|
||||
config.hasFlowPath(source, sink) and
|
||||
sinkNode = sink.getNode() and
|
||||
regexp = sinkNode.getRegExp()
|
||||
select sinkNode.getHighlight(), source, sink,
|
||||
"This $@ that depends on $@ may run slow on strings " + regexp.getPrefixMessage() +
|
||||
"with many repetitions of '" + regexp.getPumpString() + "'.", regexp, "regular expression",
|
||||
source.getNode(), "a user-provided value"
|
||||
@@ -30,5 +30,10 @@
|
||||
"CFG": [
|
||||
"codeql/csharp/ql/lib/semmle/code/csharp/controlflow/internal/ControlFlowGraphImplShared.qll",
|
||||
"ql/lib/codeql/ruby/controlflow/internal/ControlFlowGraphImplShared.qll"
|
||||
],
|
||||
"ReDoS Polynomial Ruby/Python/JS": [
|
||||
"codeql/javascript/ql/lib/semmle/javascript/security/performance/SuperlinearBackTracking.qll",
|
||||
"codeql/python/ql/lib/semmle/python/security/performance/SuperlinearBackTracking.qll",
|
||||
"ql/lib/codeql/ruby/regexp/SuperlinearBackTracking.qll"
|
||||
]
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user