hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-05-04 05:05:12 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #6175 from yoff/python-port-ReDoS

Browse Source 
Python: port ReDoS queries from Javascript
This commit is contained in:
Taus
2021-06-30 16:26:07 +02:00
committed by GitHub
parent 6a77b890af a176e6ac30
commit e4af14638b
35 changed files with 4530 additions and 408 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
python/ql/src/Security/CWE-730/PolynomialBackTracking.ql Normal file
View File

@@ -0,0 +1,6 @@
import python
import semmle.python.security.performance.SuperlinearBackTracking
from PolynomialBackTrackingTerm t
where t.getLocation().getFile().getBaseName() = "KnownCVEs.py"
select t.getRegex(), t, t.getReason()

33
python/ql/src/Security/CWE-730/PolynomialReDoS.ql Normal file
View File

@@ -0,0 +1,33 @@
/**
* @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 py/polynomial-redos
* @tags security
* external/cwe/cwe-730
* external/cwe/cwe-400
*/
import python
import semmle.python.security.performance.SuperlinearBackTracking
import semmle.python.security.dataflow.PolynomialReDoS
import DataFlow::PathGraph
from
PolynomialReDoSConfiguration config, DataFlow::PathNode source, DataFlow::PathNode sink,
PolynomialReDoSSink sinkNode, PolynomialBackTrackingTerm regexp
where
config.hasFlowPath(source, sink) and
sinkNode = sink.getNode() and
regexp.getRootTerm() = sinkNode.getRegExp()
// not (
// source.getNode().(Source).getKind() = "url" and
// regexp.isAtEndLine()
// )
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"

25
python/ql/src/Security/CWE-730/ReDoS.ql Normal file
View File

@@ -0,0 +1,25 @@
/**
* @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 py/redos
* @tags security
* external/cwe/cwe-730
* external/cwe/cwe-400
*/
import python
import semmle.python.security.performance.ExponentialBackTracking
from RegExpTerm t, string pump, State s, string prefixMsg
where
hasReDoSResult(t, pump, s, prefixMsg) and
// exclude verbose mode regexes for now
not t.getRegex().getAMode() = "VERBOSE"
select t,
"This part of the regular expression may cause exponential backtracking on strings " + prefixMsg +
"containing many repetitions of '" + pump + "'."

42
python/ql/src/semmle/python/PrintAst.qll
View File

@@ -7,6 +7,7 @@
*/
import python
import semmle.python.RegexTreeView
private newtype TPrintAstConfiguration = MkPrintAstConfiguration()
@@ -53,6 +54,9 @@ private newtype TPrintAstNode =
not list = any(Module mod).getBody() and
not forall(AstNode child | child = list.getAnItem() | isNotNeeded(child)) and
exists(list.getAnItem())
} or
TRegExpTermNode(RegExpTerm term) {
exists(StrConst str | term.getRootTerm() = getParsedRegExp(str) and shouldPrint(str, _))
}
/**
@@ -419,6 +423,42 @@ class ParameterNode extends AstElementNode {
}
}
/**
* A print node for a `StrConst`.
*
* The string has a child, if the child is used as a regular expression,
* which is the root of the regular expression.
*/
class StrConstNode extends AstElementNode {
override StrConst element;
override PrintAstNode getChild(int childIndex) {
childIndex = 0 and result.(RegExpTermNode).getTerm() = getParsedRegExp(element)
}
}
/**
* A print node for a regular expression term.
*/
class RegExpTermNode extends TRegExpTermNode, PrintAstNode {
RegExpTerm term;
RegExpTermNode() { this = TRegExpTermNode(term) }
/** Gets the `RegExpTerm` for this node. */
RegExpTerm getTerm() { result = term }
override PrintAstNode getChild(int childIndex) {
result.(RegExpTermNode).getTerm() = term.getChild(childIndex)
}
override string toString() {
result = "[" + strictconcat(term.getPrimaryQLClass(), " | ") + "] " + term.toString()
}
override Location getLocation() { result = term.getLocation() }
}
/**
* Gets the `i`th child from `node` ordered by location.
*/
@@ -447,7 +487,7 @@ private module PrettyPrinting {
string getQlClass(AstNode a) {
shouldPrint(a, _) and
(
not exists(getQlCustomClass(a)) and result = a.toString()
not exists(getQlCustomClass(a)) and result = strictconcat(a.toString(), " | ")
or
result = strictconcat(getQlCustomClass(a), " | ")
)

966
python/ql/src/semmle/python/RegexTreeView.qll Normal file
View File

@@ -0,0 +1,966 @@
/** Provides a class hierarchy corresponding to a parse tree of regular expressions. */
import python
private import semmle.python.regex
/**
* An element containing a regular expression term, that is, either
* a string literal (parsed as a regular expression)
* or another regular expression term.
*/
newtype TRegExpParent =
/** A string literal used as a regular expression */
TRegExpLiteral(Regex re) or
/** A quantified term */
TRegExpQuantifier(Regex re, int start, int end) { re.qualifiedItem(start, end, _, _) } or
/** A sequence term */
TRegExpSequence(Regex re, int start, int end) { re.sequence(start, end) } or
/** An alternatio term */
TRegExpAlt(Regex re, int start, int end) { re.alternation(start, end) } or
/** A character class term */
TRegExpCharacterClass(Regex re, int start, int end) { re.charSet(start, end) } or
/** A character range term */
TRegExpCharacterRange(Regex re, int start, int end) { re.charRange(_, start, _, _, end) } or
/** A group term */
TRegExpGroup(Regex re, int start, int end) { re.group(start, end) } or
/** A special character */
TRegExpSpecialChar(Regex re, int start, int end) { re.specialCharacter(start, end, _) } or
/** A normal character */
TRegExpNormalChar(Regex re, int start, int end) { re.normalCharacter(start, end) } or
/** A back reference */
TRegExpBackRef(Regex re, int start, int end) { re.backreference(start, end) }
/**
* An element containing a regular expression term, that is, either
* a string literal (parsed as a regular expression)
* or another regular expression term.
*/
class RegExpParent extends TRegExpParent {
string toString() { result = "RegExpParent" }
/** Gets the `i`th child term. */
abstract RegExpTerm getChild(int i);
/** Gets a child term . */
RegExpTerm getAChild() { result = getChild(_) }
/** Gets the number of child terms. */
int getNumChild() { result = count(getAChild()) }
/** Gets the associated regex. */
abstract Regex getRegex();
}
/** A string literal used as a regular expression */
class RegExpLiteral extends TRegExpLiteral, RegExpParent {
Regex re;
RegExpLiteral() { this = TRegExpLiteral(re) }
override RegExpTerm getChild(int i) { i = 0 and result.getRegex() = re and result.isRootTerm() }
predicate isDotAll() { re.getAMode() = "DOTALL" }
override Regex getRegex() { result = re }
string getPrimaryQLClass() { result = "RegExpLiteral" }
}
/**
* A regular expression term, that is, a syntactic part of a regular expression.
*/
class RegExpTerm extends RegExpParent {
Regex re;
int start;
int end;
RegExpTerm() {
this = TRegExpAlt(re, start, end)
or
this = TRegExpBackRef(re, start, end)
or
this = TRegExpCharacterClass(re, start, end)
or
this = TRegExpCharacterRange(re, start, end)
or
this = TRegExpNormalChar(re, start, end)
or
this = TRegExpGroup(re, start, end)
or
this = TRegExpQuantifier(re, start, end)
or
this = TRegExpSequence(re, start, end) and
exists(seqChild(re, start, end, 1)) // if a sequence does not have more than one element, it should be treated as that element instead.
or
this = TRegExpSpecialChar(re, start, end)
}
/**
* Gets the outermost term of this regular expression.
*/
RegExpTerm getRootTerm() {
this.isRootTerm() and result = this
or
result = getParent().(RegExpTerm).getRootTerm()
}
/**
* Holds if this term is part of a string literal
* that is interpreted as a regular expression.
*/
predicate isUsedAsRegExp() { any() }
/**
* Holds if this is the root term of a regular expression.
*/
predicate isRootTerm() { start = 0 and end = re.getText().length() }
override RegExpTerm getChild(int i) {
result = this.(RegExpAlt).getChild(i)
or
result = this.(RegExpBackRef).getChild(i)
or
result = this.(RegExpCharacterClass).getChild(i)
or
result = this.(RegExpCharacterRange).getChild(i)
or
result = this.(RegExpNormalChar).getChild(i)
or
result = this.(RegExpGroup).getChild(i)
or
result = this.(RegExpQuantifier).getChild(i)
or
result = this.(RegExpSequence).getChild(i)
or
result = this.(RegExpSpecialChar).getChild(i)
}
/**
* Gets the parent term of this regular expression term, or the
* regular expression literal if this is the root term.
*/
RegExpParent getParent() { result.getAChild() = this }
override Regex getRegex() { result = re }
/** Gets the offset at which this term starts. */
int getStart() { result = start }
/** Gets the offset at which this term ends. */
int getEnd() { result = end }
override string toString() { result = re.getText().substring(start, end) }
/**
* Gets the location of the surrounding regex, as locations inside the regex do not exist.
* To get location information corresponding to the term inside the regex,
* use `hasLocationInfo`.
*/
Location getLocation() { result = re.getLocation() }
/** Holds if this term is found at the specified location offsets. */
predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
exists(int re_start, int re_end |
re.getLocation().hasLocationInfo(filepath, startline, re_start, endline, re_end) and
startcolumn = re_start + start + 4 and
endcolumn = re_start + end + 3
)
}
/** Gets the file in which this term is found. */
File getFile() { result = this.getLocation().getFile() }
/** Gets the raw source text of this term. */
string getRawValue() { result = this.toString() }
/** Gets the string literal in which this term is found. */
RegExpLiteral getLiteral() { result = TRegExpLiteral(re) }
/** Gets the regular expression term that is matched (textually) before this one, if any. */
RegExpTerm getPredecessor() {
exists(RegExpTerm parent | parent = getParent() |
result = parent.(RegExpSequence).previousElement(this)
or
not exists(parent.(RegExpSequence).previousElement(this)) and
not parent instanceof RegExpSubPattern and
result = parent.getPredecessor()
)
}
/** Gets the regular expression term that is matched (textually) after this one, if any. */
RegExpTerm getSuccessor() {
exists(RegExpTerm parent | parent = getParent() |
result = parent.(RegExpSequence).nextElement(this)
or
not exists(parent.(RegExpSequence).nextElement(this)) and
not parent instanceof RegExpSubPattern and
result = parent.getSuccessor()
)
}
/** Gets the primary QL class for this term. */
string getPrimaryQLClass() { result = "RegExpTerm" }
}
/**
* A quantified regular expression term.
*
* Example:
*
* ```
* ((ECMA|Java)[sS]cript)*
* ```
*/
class RegExpQuantifier extends RegExpTerm, TRegExpQuantifier {
int part_end;
boolean maybe_empty;
boolean may_repeat_forever;
RegExpQuantifier() {
this = TRegExpQuantifier(re, start, end) and
re.qualifiedPart(start, part_end, end, maybe_empty, may_repeat_forever)
}
override RegExpTerm getChild(int i) {
i = 0 and
result.getRegex() = re and
result.getStart() = start and
result.getEnd() = part_end
}
predicate mayRepeatForever() { may_repeat_forever = true }
string getQualifier() { result = re.getText().substring(part_end, end) }
override string getPrimaryQLClass() { result = "RegExpQuantifier" }
}
/**
* A regular expression term that permits unlimited repetitions.
*/
class InfiniteRepetitionQuantifier extends RegExpQuantifier {
InfiniteRepetitionQuantifier() { this.mayRepeatForever() }
}
/**
* A star-quantified term.
*
* Example:
*
* ```
* \w*
* ```
*/
class RegExpStar extends InfiniteRepetitionQuantifier {
RegExpStar() { this.getQualifier().charAt(0) = "*" }
override string getPrimaryQLClass() { result = "RegExpStar" }
}
/**
* A plus-quantified term.
*
* Example:
*
* ```
* \w+
* ```
*/
class RegExpPlus extends InfiniteRepetitionQuantifier {
RegExpPlus() { this.getQualifier().charAt(0) = "+" }
override string getPrimaryQLClass() { result = "RegExpPlus" }
}
/**
* An optional term.
*
* Example:
*
* ```
* ;?
* ```
*/
class RegExpOpt extends RegExpQuantifier {
RegExpOpt() { this.getQualifier().charAt(0) = "?" }
override string getPrimaryQLClass() { result = "RegExpOpt" }
}
/**
* A range-quantified term
*
* Examples:
*
* ```
* \w{2,4}
* \w{2,}
* \w{2}
* ```
*/
class RegExpRange extends RegExpQuantifier {
string upper;
string lower;
RegExpRange() { re.multiples(part_end, end, lower, upper) }
string getUpper() { result = upper }
string getLower() { result = lower }
/**
* Gets the upper bound of the range, if any.
*
* If there is no upper bound, any number of repetitions is allowed.
* For a term of the form `r{lo}`, both the lower and the upper bound
* are `lo`.
*/
int getUpperBound() { result = this.getUpper().toInt() }
/** Gets the lower bound of the range. */
int getLowerBound() { result = this.getLower().toInt() }
override string getPrimaryQLClass() { result = "RegExpRange" }
}
/**
* A sequence term.
*
* Example:
*
* ```
* (ECMA|Java)Script
* ```
*
* This is a sequence with the elements `(ECMA|Java)` and `Script`.
*/
class RegExpSequence extends RegExpTerm, TRegExpSequence {
RegExpSequence() {
this = TRegExpSequence(re, start, end) and
exists(seqChild(re, start, end, 1)) // if a sequence does not have more than one element, it should be treated as that element instead.
}
override RegExpTerm getChild(int i) { result = seqChild(re, start, end, i) }
/** Gets the element preceding `element` in this sequence. */
RegExpTerm previousElement(RegExpTerm element) { element = nextElement(result) }
/** Gets the element following `element` in this sequence. */
RegExpTerm nextElement(RegExpTerm element) {
exists(int i |
element = this.getChild(i) and
result = this.getChild(i + 1)
)
}
override string getPrimaryQLClass() { result = "RegExpSequence" }
}
pragma[nomagic]
private int seqChildEnd(Regex re, int start, int end, int i) {
result = seqChild(re, start, end, i).getEnd()
}
// moved out so we can use it in the charpred
private RegExpTerm seqChild(Regex re, int start, int end, int i) {
re.sequence(start, end) and
(
i = 0 and
result.getRegex() = re and
result.getStart() = start and
exists(int itemEnd |
re.item(start, itemEnd) and
result.getEnd() = itemEnd
)
or
i > 0 and
result.getRegex() = re and
exists(int itemStart | itemStart = seqChildEnd(re, start, end, i - 1) |
result.getStart() = itemStart and
re.item(itemStart, result.getEnd())
)
)
}
/**
* An alternative term, that is, a term of the form `a|b`.
*
* Example:
*
* ```
* ECMA|Java
* ```
*/
class RegExpAlt extends RegExpTerm, TRegExpAlt {
RegExpAlt() { this = TRegExpAlt(re, start, end) }
override RegExpTerm getChild(int i) {
i = 0 and
result.getRegex() = re and
result.getStart() = start and
exists(int part_end |
re.alternationOption(start, end, start, part_end) and
result.getEnd() = part_end
)
or
i > 0 and
result.getRegex() = re and
exists(int part_start |
part_start = this.getChild(i - 1).getEnd() + 1 // allow for the |
|
result.getStart() = part_start and
re.alternationOption(start, end, part_start, result.getEnd())
)
}
override string getPrimaryQLClass() { result = "RegExpAlt" }
}
/**
* An escaped regular expression term, that is, a regular expression
* term starting with a backslash, which is not a backreference.
*
* Example:
*
* ```
* \.
* \w
* ```
*/
class RegExpEscape extends RegExpNormalChar {
RegExpEscape() { re.escapedCharacter(start, end) }
/**
* Gets the name of the escaped; for example, `w` for `\w`.
* TODO: Handle named escapes.
*/
override string getValue() {
this.isIdentityEscape() and result = this.getUnescaped()
or
this.getUnescaped() = "n" and result = "\n"
or
this.getUnescaped() = "r" and result = "\r"
or
this.getUnescaped() = "t" and result = "\t"
or
// TODO: Find a way to include a formfeed character
// this.getUnescaped() = "f" and result = " "
// or
isUnicode() and
result = getUnicode()
}
predicate isIdentityEscape() { not this.getUnescaped() in ["n", "r", "t", "f"] }
override string getPrimaryQLClass() { result = "RegExpEscape" }
string getUnescaped() { result = this.getText().suffix(1) }
/**
* Gets the text for this escape. That is e.g. "\w".
*/
private string getText() { result = re.getText().substring(start, end) }
/**
* Holds if this is a unicode escape.
*/
private predicate isUnicode() { getText().prefix(2) = ["\\u", "\\U"] }
/**
* Gets the unicode char for this escape.
* E.g. for `\u0061` this returns "a".
*/
private string getUnicode() {
// TODO: Enable this once a supporting CLI is released.
// exists(int codepoint | codepoint = sum(getHexValueFromUnicode(_)) |
// result = codepoint.toUnicode()
// )
none()
}
// TODO: Enable this once a supporting CLI is released.
// /**
// * Gets int value for the `index`th char in the hex number of the unicode escape.
// * E.g. for `\u0061` and `index = 2` this returns 96 (the number `6` interpreted as hex).
// */
// private int getHexValueFromUnicode(int index) {
// isUnicode() and
// exists(string hex, string char | hex = getText().suffix(2) |
// char = hex.charAt(index) and
// result = 16.pow(hex.length() - index - 1) * toHex(char)
// )
// }
}
// TODO: Enable this once a supporting CLI is released.
// /**
// * Gets the hex number for the `hex` char.
// */
// private int toHex(string hex) {
// hex = [0 .. 9].toString() and
// result = hex.toInt()
// or
// result = 10 and hex = ["a", "A"]
// or
// result = 11 and hex = ["b", "B"]
// or
// result = 12 and hex = ["c", "C"]
// or
// result = 13 and hex = ["d", "D"]
// or
// result = 14 and hex = ["e", "E"]
// or
// result = 15 and hex = ["f", "F"]
// }
/**
* A character class escape in a regular expression.
* That is, an escaped charachter that denotes multiple characters.
*
* Examples:
*
* ```
* \w
* \S
* ```
*/
class RegExpCharacterClassEscape extends RegExpEscape {
// string value;
RegExpCharacterClassEscape() {
// value = re.getText().substring(start + 1, end) and
// value in ["d", "D", "s", "S", "w", "W"]
this.getValue() in ["d", "D", "s", "S", "w", "W"]
}
/** Gets the name of the character class; for example, `w` for `\w`. */
// override string getValue() { result = value }
override RegExpTerm getChild(int i) { none() }
override string getPrimaryQLClass() { result = "RegExpCharacterClassEscape" }
}
/**
* A character class in a regular expression.
*
* Examples:
*
* ```
* [a-z_]
* [^<>&]
* ```
*/
class RegExpCharacterClass extends RegExpTerm, TRegExpCharacterClass {
RegExpCharacterClass() { this = TRegExpCharacterClass(re, start, end) }
predicate isInverted() { re.getChar(start + 1) = "^" }
string getCharThing(int i) { result = re.getChar(i + start) }
predicate isUniversalClass() {
// [^]
isInverted() and not exists(getAChild())
or
// [\w\W] and similar
not isInverted() and
exists(string cce1, string cce2 |
cce1 = getAChild().(RegExpCharacterClassEscape).getValue() and
cce2 = getAChild().(RegExpCharacterClassEscape).getValue()
|
cce1 != cce2 and cce1.toLowerCase() = cce2.toLowerCase()
)
}
override RegExpTerm getChild(int i) {
i = 0 and
result.getRegex() = re and
exists(int itemStart, int itemEnd |
result.getStart() = itemStart and
re.char_set_start(start, itemStart) and
re.char_set_child(start, itemStart, itemEnd) and
result.getEnd() = itemEnd
)
or
i > 0 and
result.getRegex() = re and
exists(int itemStart | itemStart = this.getChild(i - 1).getEnd() |
result.getStart() = itemStart and
re.char_set_child(start, itemStart, result.getEnd())
)
}
override string getPrimaryQLClass() { result = "RegExpCharacterClass" }
}
/**
* A character range in a character class in a regular expression.
*
* Example:
*
* ```
* a-z
* ```
*/
class RegExpCharacterRange extends RegExpTerm, TRegExpCharacterRange {
int lower_end;
int upper_start;
RegExpCharacterRange() {
this = TRegExpCharacterRange(re, start, end) and
re.charRange(_, start, lower_end, upper_start, end)
}
predicate isRange(string lo, string hi) {
lo = re.getText().substring(start, lower_end) and
hi = re.getText().substring(upper_start, end)
}
override RegExpTerm getChild(int i) {
i = 0 and
result.getRegex() = re and
result.getStart() = start and
result.getEnd() = lower_end
or
i = 1 and
result.getRegex() = re and
result.getStart() = upper_start and
result.getEnd() = end
}
override string getPrimaryQLClass() { result = "RegExpCharacterRange" }
}
/**
* A normal character in a regular expression, that is, a character
* without special meaning. This includes escaped characters.
*
* Examples:
* ```
* t
* \t
* ```
*/
class RegExpNormalChar extends RegExpTerm, TRegExpNormalChar {
RegExpNormalChar() { this = TRegExpNormalChar(re, start, end) }
predicate isCharacter() { any() }
string getValue() { result = re.getText().substring(start, end) }
override RegExpTerm getChild(int i) { none() }
override string getPrimaryQLClass() { result = "RegExpNormalChar" }
}
/**
* A constant regular expression term, that is, a regular expression
* term matching a single string. Currently, this will always be a single character.
*
* Example:
*
* ```
* a
* ```
*/
class RegExpConstant extends RegExpTerm {
string value;
RegExpConstant() {
this = TRegExpNormalChar(re, start, end) and
not this instanceof RegExpCharacterClassEscape and
// exclude chars in qualifiers
// TODO: push this into regex library
not exists(int qstart, int qend | re.qualifiedPart(_, qstart, qend, _, _) |
qstart <= start and end <= qend
) and
value = this.(RegExpNormalChar).getValue()
// This will never hold
// or
// this = TRegExpSpecialChar(re, start, end) and
// re.inCharSet(start) and
// value = this.(RegExpSpecialChar).getChar()
}
predicate isCharacter() { any() }
string getValue() { result = value }
override RegExpTerm getChild(int i) { none() }
override string getPrimaryQLClass() { result = "RegExpConstant" }
}
/**
* A grouped regular expression.
*
* Examples:
*
* ```
* (ECMA|Java)
* (?:ECMA|Java)
* (?<quote>['"])
* ```
*/
class RegExpGroup extends RegExpTerm, TRegExpGroup {
RegExpGroup() { this = TRegExpGroup(re, start, end) }
/**
* Gets the index of this capture group within the enclosing regular
* expression literal.
*
* For example, in the regular expression `/((a?).)(?:b)/`, the
* group `((a?).)` has index 1, the group `(a?)` nested inside it
* has index 2, and the group `(?:b)` has no index, since it is
* not a capture group.
*/
int getNumber() { result = re.getGroupNumber(start, end) }
/** Holds if this is a named capture group. */
predicate isNamed() { exists(this.getName()) }
/** Gets the name of this capture group, if any. */
string getName() { result = re.getGroupName(start, end) }
predicate isCharacter() { any() }
string getValue() { result = re.getText().substring(start, end) }
override RegExpTerm getChild(int i) {
result.getRegex() = re and
i = 0 and
re.groupContents(start, end, result.getStart(), result.getEnd())
}
override string getPrimaryQLClass() { result = "RegExpGroup" }
}
/**
* A special character in a regular expression.
*
* Examples:
* ```
* ^
* $
* .
* ```
*/
class RegExpSpecialChar extends RegExpTerm, TRegExpSpecialChar {
string char;
RegExpSpecialChar() {
this = TRegExpSpecialChar(re, start, end) and
re.specialCharacter(start, end, char)
}
predicate isCharacter() { any() }
string getChar() { result = char }
override RegExpTerm getChild(int i) { none() }
override string getPrimaryQLClass() { result = "RegExpSpecialChar" }
}
/**
* A dot regular expression.
*
* Example:
*
* ```
* .
* ```
*/
class RegExpDot extends RegExpSpecialChar {
RegExpDot() { this.getChar() = "." }
override string getPrimaryQLClass() { result = "RegExpDot" }
}
/**
* A dollar assertion `$` matching the end of a line.
*
* Example:
*
* ```
* $
* ```
*/
class RegExpDollar extends RegExpSpecialChar {
RegExpDollar() { this.getChar() = "$" }
override string getPrimaryQLClass() { result = "RegExpDollar" }
}
/**
* A caret assertion `^` matching the beginning of a line.
*
* Example:
*
* ```
* ^
* ```
*/
class RegExpCaret extends RegExpSpecialChar {
RegExpCaret() { this.getChar() = "^" }
override string getPrimaryQLClass() { result = "RegExpCaret" }
}
/**
* A zero-width match, that is, either an empty group or an assertion.
*
* Examples:
* ```
* ()
* (?=\w)
* ```
*/
class RegExpZeroWidthMatch extends RegExpGroup {
RegExpZeroWidthMatch() { re.zeroWidthMatch(start, end) }
override predicate isCharacter() { any() }
override RegExpTerm getChild(int i) { none() }
override string getPrimaryQLClass() { result = "RegExpZeroWidthMatch" }
}
/**
* A zero-width lookahead or lookbehind assertion.
*
* Examples:
*
* ```
* (?=\w)
* (?!\n)
* (?<=\.)
* (?<!\\)
* ```
*/
class RegExpSubPattern extends RegExpZeroWidthMatch {
RegExpSubPattern() { not re.emptyGroup(start, end) }
}
/**
* A zero-width lookahead assertion.
*
* Examples:
*
* ```
* (?=\w)
* (?!\n)
* ```
*/
abstract class RegExpLookahead extends RegExpSubPattern { }
/**
* A positive-lookahead assertion.
*
* Examples:
*
* ```
* (?=\w)
* ```
*/
class RegExpPositiveLookahead extends RegExpLookahead {
RegExpPositiveLookahead() { re.positiveLookaheadAssertionGroup(start, end) }
override string getPrimaryQLClass() { result = "RegExpPositiveLookahead" }
}
/**
* A negative-lookahead assertion.
*
* Examples:
*
* ```
* (?!\n)
* ```
*/
class RegExpNegativeLookahead extends RegExpLookahead {
RegExpNegativeLookahead() { re.negativeLookaheadAssertionGroup(start, end) }
override string getPrimaryQLClass() { result = "RegExpNegativeLookahead" }
}
/**
* A zero-width lookbehind assertion.
*
* Examples:
*
* ```
* (?<=\.)
* (?<!\\)
* ```
*/
abstract class RegExpLookbehind extends RegExpSubPattern { }
/**
* A positive-lookbehind assertion.
*
* Examples:
*
* ```
* (?<=\.)
* ```
*/
class RegExpPositiveLookbehind extends RegExpLookbehind {
RegExpPositiveLookbehind() { re.positiveLookbehindAssertionGroup(start, end) }
override string getPrimaryQLClass() { result = "RegExpPositiveLookbehind" }
}
/**
* A negative-lookbehind assertion.
*
* Examples:
*
* ```
* (?<!\\)
* ```
*/
class RegExpNegativeLookbehind extends RegExpLookbehind {
RegExpNegativeLookbehind() { re.negativeLookbehindAssertionGroup(start, end) }
override string getPrimaryQLClass() { result = "RegExpNegativeLookbehind" }
}
/**
* A back reference, that is, a term of the form `\i` or `\k<name>`
* in a regular expression.
*
* Examples:
*
* ```
* \1
* (?P=quote)
* ```
*/
class RegExpBackRef extends RegExpTerm, TRegExpBackRef {
RegExpBackRef() { this = TRegExpBackRef(re, start, end) }
/**
* Gets the number of the capture group this back reference refers to, if any.
*/
int getNumber() { result = re.getBackrefNumber(start, end) }
/**
* Gets the name of the capture group this back reference refers to, if any.
*/
string getName() { result = re.getBackrefName(start, end) }
/** Gets the capture group this back reference refers to. */
RegExpGroup getGroup() {
result.getLiteral() = this.getLiteral() and
(
result.getNumber() = this.getNumber() or
result.getName() = this.getName()
)
}
override RegExpTerm getChild(int i) { none() }
override string getPrimaryQLClass() { result = "RegExpBackRef" }
}
/** Gets the parse tree resulting from parsing `re`, if such has been constructed. */
RegExpTerm getParsedRegExp(StrConst re) { result.getRegex() = re and result.isRootTerm() }

335
python/ql/src/semmle/python/regex.qll
View File

@@ -121,8 +121,82 @@ deprecated string mode_from_mode_object(Value obj) {
abstract class RegexString extends Expr {
RegexString() { (this instanceof Bytes or this instanceof Unicode) }
/**
* Helper predicate for `char_set_start(int start, int end)`.
*
* In order to identify left brackets ('[') which actually start a character class,
* we perform a left to right scan of the string.
*
* To avoid negative recursion we return a boolean. See `escaping`,
* the helper for `escapingChar`, for a clean use of this pattern.
*
* result is true for those start chars that actually mark a start of a char set.
*/
boolean char_set_start(int pos) {
exists(int index |
// is opening bracket
this.char_set_delimiter(index, pos) = true and
(
// if this is the first bracket, `pos` starts a char set
index = 1 and result = true
or
// if the previous char set delimiter was not a closing bracket, `pos` does
// not start a char set. This is needed to handle cases such as `[[]` (a
// char set that matches the `[` char)
index > 1 and
not this.char_set_delimiter(index - 1, _) = false and
result = false
or
// special handling of cases such as `[][]` (the character-set of the characters `]` and `[`).
exists(int prev_closing_bracket_pos |
// previous bracket is a closing bracket
this.char_set_delimiter(index - 1, prev_closing_bracket_pos) = false and
if
// check if the character that comes before the previous closing bracket
// is an opening bracket (taking `^` into account)
exists(int pos_before_prev_closing_bracket |
if this.getChar(prev_closing_bracket_pos - 1) = "^"
then pos_before_prev_closing_bracket = prev_closing_bracket_pos - 2
else pos_before_prev_closing_bracket = prev_closing_bracket_pos - 1
|
this.char_set_delimiter(index - 2, pos_before_prev_closing_bracket) = true
)
then
// brackets without anything in between is not valid character ranges, so
// the first closing bracket in `[]]` and `[^]]` does not count,
//
// and we should _not_ mark the second opening bracket in `[][]` and `[^][]`
// as starting a new char set. ^ ^
exists(int pos_before_prev_closing_bracket |
this.char_set_delimiter(index - 2, pos_before_prev_closing_bracket) = true
|
result = this.char_set_start(pos_before_prev_closing_bracket).booleanNot()
)
else
// if not, `pos` does in fact mark a real start of a character range
result = true
)
)
)
}
/**
* Helper predicate for chars that could be character-set delimiters.
* Holds if the (non-escaped) char at `pos` in the string, is the (one-based) `index` occurrence of a bracket (`[` or `]`) in the string.
* Result if `true` is the char is `[`, and `false` if the char is `]`.
*/
boolean char_set_delimiter(int index, int pos) {
pos = rank[index](int p | this.nonEscapedCharAt(p) = "[" or this.nonEscapedCharAt(p) = "]") and
(
this.nonEscapedCharAt(pos) = "[" and result = true
or
this.nonEscapedCharAt(pos) = "]" and result = false
)
}
/** Hold is a character set starts between `start` and `end`. */
predicate char_set_start(int start, int end) {
this.nonEscapedCharAt(start) = "[" and
this.char_set_start(start) = true and
(
this.getChar(start + 1) = "^" and end = start + 2
or
@@ -143,8 +217,99 @@ abstract class RegexString extends Expr {
)
}
/** An indexed version of `char_set_token/3` */
private predicate char_set_token(int charset_start, int index, int token_start, int token_end) {
token_start =
rank[index](int start, int end | this.char_set_token(charset_start, start, end) | start) and
this.char_set_token(charset_start, token_start, token_end)
}
/** Either a char or a - */
private predicate char_set_token(int charset_start, int start, int end) {
this.char_set_start(charset_start, start) and
(
this.escapedCharacter(start, end)
or
exists(this.nonEscapedCharAt(start)) and end = start + 1
)
or
this.char_set_token(charset_start, _, start) and
(
this.escapedCharacter(start, end)
or
exists(this.nonEscapedCharAt(start)) and
end = start + 1 and
not this.getChar(start) = "]"
)
}
/**
* Holds if the character set starting at `charset_start` contains either
* a character or a range found between `start` and `end`.
*/
predicate char_set_child(int charset_start, int start, int end) {
this.char_set_token(charset_start, start, end) and
not exists(int range_start, int range_end |
this.charRange(charset_start, range_start, _, _, range_end) and
range_start <= start and
range_end >= end
)
or
this.charRange(charset_start, start, _, _, end)
}
/**
* Holds if the character set starting at `charset_start` contains a character range
* with lower bound found between `start` and `lower_end`
* and upper bound found between `upper_start` and `end`.
*/
predicate charRange(int charset_start, int start, int lower_end, int upper_start, int end) {
exists(int index |
this.charRangeEnd(charset_start, index) = true and
this.char_set_token(charset_start, index - 2, start, lower_end) and
this.char_set_token(charset_start, index, upper_start, end)
)
}
/**
* Helper predicate for `charRange`.
* We can determine where character ranges end by a left to right sweep.
*
* To avoid negative recursion we return a boolean. See `escaping`,
* the helper for `escapingChar`, for a clean use of this pattern.
*/
private boolean charRangeEnd(int charset_start, int index) {
this.char_set_token(charset_start, index, _, _) and
(
index in [1, 2] and result = false
or
index > 2 and
exists(int connector_start |
this.char_set_token(charset_start, index - 1, connector_start, _) and
this.nonEscapedCharAt(connector_start) = "-" and
result =
this.charRangeEnd(charset_start, index - 2)
.booleanNot()
.booleanAnd(this.charRangeEnd(charset_start, index - 1).booleanNot())
)
or
not exists(int connector_start |
this.char_set_token(charset_start, index - 1, connector_start, _) and
this.nonEscapedCharAt(connector_start) = "-"
) and
result = false
)
}
/** Holds if the character at `pos` is a "\" that is actually escaping what comes after. */
predicate escapingChar(int pos) { this.escaping(pos) = true }
/**
* Helper predicate for `escapingChar`.
* In order to avoid negative recusrion, we return a boolean.
* This way, we can refer to `escaping(pos - 1).booleanNot()`
* rather than to a negated version of `escaping(pos)`.
*/
private boolean escaping(int pos) {
pos = -1 and result = false
or
@@ -164,14 +329,14 @@ abstract class RegexString extends Expr {
string nonEscapedCharAt(int i) {
result = this.getText().charAt(i) and
not this.escapingChar(i - 1)
not exists(int x, int y | this.escapedCharacter(x, y) and i in [x .. y - 1])
}
private predicate isOptionDivider(int i) { this.nonEscapedCharAt(i) = "|" }
private predicate isGroupEnd(int i) { this.nonEscapedCharAt(i) = ")" }
private predicate isGroupEnd(int i) { this.nonEscapedCharAt(i) = ")" and not this.inCharSet(i) }
private predicate isGroupStart(int i) { this.nonEscapedCharAt(i) = "(" }
private predicate isGroupStart(int i) { this.nonEscapedCharAt(i) = "(" and not this.inCharSet(i) }
predicate failedToParse(int i) {
exists(this.getChar(i)) and
@@ -192,16 +357,25 @@ abstract class RegexString extends Expr {
not exists(int i | start + 2 < i and i < end - 1 | this.getChar(i) = "}")
}
private predicate escapedCharacter(int start, int end) {
/**
* Holds if an escaped character is found between `start` and `end`.
* Escaped characters include hex values, octal values and named escapes,
* but excludes backreferences.
*/
predicate escapedCharacter(int start, int end) {
this.escapingChar(start) and
not exists(this.getText().substring(start + 1, end + 1).toInt()) and
not this.numbered_backreference(start, _, _) and
(
// hex value \xhh
this.getChar(start + 1) = "x" and end = start + 4
or
// octal value \ooo
end in [start + 2 .. start + 4] and
exists(this.getText().substring(start + 1, end).toInt())
this.getText().substring(start + 1, end).toInt() >= 0 and
not (
end < start + 4 and
exists(this.getText().substring(start + 1, end + 1).toInt())
)
or
// 16-bit hex value \uhhhh
this.getChar(start + 1) = "u" and end = start + 6
@@ -213,18 +387,19 @@ abstract class RegexString extends Expr {
or
// escape not handled above, update when adding a new case
not this.getChar(start + 1) in ["x", "u", "U", "N"] and
not exists(this.getChar(start + 1).toInt()) and
end = start + 2
)
}
private predicate inCharSet(int index) {
/** Holds if `index` is inside a character set. */
predicate inCharSet(int index) {
exists(int x, int y | this.charSet(x, y) and index in [x + 1 .. y - 2])
}
/*
/**
* 'simple' characters are any that don't alter the parsing of the regex.
*/
private predicate simpleCharacter(int start, int end) {
end = start + 1 and
not this.charSet(start, _) and
@@ -238,7 +413,7 @@ abstract class RegexString extends Expr {
or
start = z - 2
or
start > y and start < z - 2 and not c = "-"
start > y and start < z - 2 and not this.charRange(_, _, start, end, _)
)
or
not this.inCharSet(start) and
@@ -246,7 +421,7 @@ abstract class RegexString extends Expr {
not c = "[" and
not c = ")" and
not c = "|" and
not this.qualifier(start, _, _)
not this.qualifier(start, _, _, _)
)
}
@@ -257,7 +432,8 @@ abstract class RegexString extends Expr {
or
this.escapedCharacter(start, end)
) and
not exists(int x, int y | this.group_start(x, y) and x <= start and y >= end)
not exists(int x, int y | this.group_start(x, y) and x <= start and y >= end) and
not exists(int x, int y | this.backreference(x, y) and x <= start and y >= end)
}
predicate normalCharacter(int start, int end) {
@@ -302,12 +478,13 @@ abstract class RegexString extends Expr {
or
this.negativeAssertionGroup(start, end)
or
positiveLookaheadAssertionGroup(start, end)
this.positiveLookaheadAssertionGroup(start, end)
or
this.positiveLookbehindAssertionGroup(start, end)
}
private predicate emptyGroup(int start, int end) {
/** Holds if an empty group is found between `start` and `end`. */
predicate emptyGroup(int start, int end) {
exists(int endm1 | end = endm1 + 1 |
this.group_start(start, endm1) and
this.isGroupEnd(endm1)
@@ -340,13 +517,29 @@ abstract class RegexString extends Expr {
)
}
private predicate positiveLookaheadAssertionGroup(int start, int end) {
/** Holds if a negative lookahead is found between `start` and `end` */
predicate negativeLookaheadAssertionGroup(int start, int end) {
exists(int in_start | this.negative_lookahead_assertion_start(start, in_start) |
this.groupContents(start, end, in_start, _)
)
}
/** Holds if a negative lookbehind is found between `start` and `end` */
predicate negativeLookbehindAssertionGroup(int start, int end) {
exists(int in_start | this.negative_lookbehind_assertion_start(start, in_start) |
this.groupContents(start, end, in_start, _)
)
}
/** Holds if a positive lookahead is found between `start` and `end` */
predicate positiveLookaheadAssertionGroup(int start, int end) {
exists(int in_start | this.lookahead_assertion_start(start, in_start) |
this.groupContents(start, end, in_start, _)
)
}
private predicate positiveLookbehindAssertionGroup(int start, int end) {
/** Holds if a positive lookbehind is found between `start` and `end` */
predicate positiveLookbehindAssertionGroup(int start, int end) {
exists(int in_start | this.lookbehind_assertion_start(start, in_start) |
this.groupContents(start, end, in_start, _)
)
@@ -405,6 +598,8 @@ abstract class RegexString extends Expr {
this.getChar(start + 1) = "?" and
this.getChar(start + 2) = "P" and
this.getChar(start + 3) = "=" and
// Should this be looking for unescaped ")"?
// TODO: test this
end = min(int i | i > start + 4 and this.getChar(i) = "?")
}
@@ -495,6 +690,7 @@ abstract class RegexString extends Expr {
private predicate numbered_backreference(int start, int end, int value) {
this.escapingChar(start) and
not this.getChar(start + 1) = "0" and
exists(string text, string svalue, int len |
end = start + len and
text = this.getText() and
@@ -503,7 +699,7 @@ abstract class RegexString extends Expr {
svalue = text.substring(start + 1, start + len) and
value = svalue.toInt() and
not exists(text.substring(start + 1, start + len + 1).toInt()) and
value != 0
value > 0
)
}
@@ -527,43 +723,55 @@ abstract class RegexString extends Expr {
this.group(start, end)
or
this.charSet(start, end)
or
this.backreference(start, end)
}
private predicate qualifier(int start, int end, boolean maybe_empty) {
this.short_qualifier(start, end, maybe_empty) and not this.getChar(end) = "?"
private predicate qualifier(int start, int end, boolean maybe_empty, boolean may_repeat_forever) {
this.short_qualifier(start, end, maybe_empty, may_repeat_forever) and
not this.getChar(end) = "?"
or
exists(int short_end | this.short_qualifier(start, short_end, maybe_empty) |
exists(int short_end | this.short_qualifier(start, short_end, maybe_empty, may_repeat_forever) |
if this.getChar(short_end) = "?" then end = short_end + 1 else end = short_end
)
}
private predicate short_qualifier(int start, int end, boolean maybe_empty) {
private predicate short_qualifier(
int start, int end, boolean maybe_empty, boolean may_repeat_forever
) {
(
this.getChar(start) = "+" and maybe_empty = false
this.getChar(start) = "+" and maybe_empty = false and may_repeat_forever = true
or
this.getChar(start) = "*" and maybe_empty = true
this.getChar(start) = "*" and maybe_empty = true and may_repeat_forever = true
or
this.getChar(start) = "?" and maybe_empty = true
this.getChar(start) = "?" and maybe_empty = true and may_repeat_forever = false
) and
end = start + 1
or
exists(int endin | end = endin + 1 |
this.getChar(start) = "{" and
this.getChar(endin) = "}" and
end > start and
exists(string multiples | multiples = this.getText().substring(start + 1, endin) |
multiples.regexpMatch("0+") and maybe_empty = true
or
multiples.regexpMatch("0*,[0-9]*") and maybe_empty = true
or
multiples.regexpMatch("0*[1-9][0-9]*") and maybe_empty = false
or
multiples.regexpMatch("0*[1-9][0-9]*,[0-9]*") and maybe_empty = false
) and
not exists(int mid |
this.getChar(mid) = "}" and
mid > start and
mid < endin
exists(string lower, string upper |
this.multiples(start, end, lower, upper) and
(if lower = "" or lower.toInt() = 0 then maybe_empty = true else maybe_empty = false) and
if upper = "" then may_repeat_forever = true else may_repeat_forever = false
)
}
/**
* Holds if a repetition quantifier is found between `start` and `end`,
* with the given lower and upper bounds. If a bound is omitted, the corresponding
* string is empty.
*/
predicate multiples(int start, int end, string lower, string upper) {
this.getChar(start) = "{" and
this.getChar(end - 1) = "}" and
exists(string inner | inner = this.getText().substring(start + 1, end - 1) |
inner.regexpMatch("[0-9]+") and
lower = inner and
upper = lower
or
inner.regexpMatch("[0-9]*,[0-9]*") and
exists(int commaIndex | commaIndex = inner.indexOf(",") |
lower = inner.prefix(commaIndex) and
upper = inner.suffix(commaIndex + 1)
)
)
}
@@ -572,19 +780,29 @@ abstract class RegexString extends Expr {
* Whether the text in the range start,end is a qualified item, where item is a character,
* a character set or a group.
*/
predicate qualifiedItem(int start, int end, boolean maybe_empty) {
this.qualifiedPart(start, _, end, maybe_empty)
predicate qualifiedItem(int start, int end, boolean maybe_empty, boolean may_repeat_forever) {
this.qualifiedPart(start, _, end, maybe_empty, may_repeat_forever)
}
private predicate qualifiedPart(int start, int part_end, int end, boolean maybe_empty) {
/**
* Holds if a qualified part is found between `start` and `part_end` and the qualifier is
* found between `part_end` and `end`.
*
* `maybe_empty` is true if the part is optional.
* `may_repeat_forever` is true if the part may be repeated unboundedly.
*/
predicate qualifiedPart(
int start, int part_end, int end, boolean maybe_empty, boolean may_repeat_forever
) {
this.baseItem(start, part_end) and
this.qualifier(part_end, end, maybe_empty)
this.qualifier(part_end, end, maybe_empty, may_repeat_forever)
}
private predicate item(int start, int end) {
this.qualifiedItem(start, end, _)
/** Holds if the range `start`, `end` contains a character, a quantifier, a character set or a group. */
predicate item(int start, int end) {
this.qualifiedItem(start, end, _, _)
or
this.baseItem(start, end) and not this.qualifier(end, _, _)
this.baseItem(start, end) and not this.qualifier(end, _, _, _)
}
private predicate subsequence(int start, int end) {
@@ -607,7 +825,7 @@ abstract class RegexString extends Expr {
*/
predicate sequence(int start, int end) {
this.sequenceOrQualified(start, end) and
not this.qualifiedItem(start, end, _)
not this.qualifiedItem(start, end, _, _)
}
private predicate sequenceOrQualified(int start, int end) {
@@ -618,7 +836,8 @@ abstract class RegexString extends Expr {
private predicate item_start(int start) {
this.character(start, _) or
this.isGroupStart(start) or
this.charSet(start, _)
this.charSet(start, _) or
this.backreference(start, _)
}
private predicate item_end(int end) {
@@ -628,7 +847,7 @@ abstract class RegexString extends Expr {
or
this.charSet(_, end)
or
this.qualifier(_, end, _)
this.qualifier(_, end, _, _)
}
private predicate top_level(int start, int end) {
@@ -680,14 +899,14 @@ abstract class RegexString extends Expr {
or
exists(int x | this.firstPart(x, end) |
this.emptyMatchAtStartGroup(x, start) or
this.qualifiedItem(x, start, true) or
this.qualifiedItem(x, start, true, _) or
this.specialCharacter(x, start, "^")
)
or
exists(int y | this.firstPart(start, y) |
this.item(start, end)
or
this.qualifiedPart(start, end, y, _)
this.qualifiedPart(start, end, y, _, _)
)
or
exists(int x, int y | this.firstPart(x, y) |
@@ -704,7 +923,7 @@ abstract class RegexString extends Expr {
exists(int y | this.lastPart(start, y) |
this.emptyMatchAtEndGroup(end, y)
or
this.qualifiedItem(end, y, true)
this.qualifiedItem(end, y, true, _)
or
this.specialCharacter(end, y, "$")
or
@@ -716,7 +935,7 @@ abstract class RegexString extends Expr {
this.item(start, end)
)
or
exists(int y | this.lastPart(start, y) | this.qualifiedPart(start, end, y, _))
exists(int y | this.lastPart(start, y) | this.qualifiedPart(start, end, y, _, _))
or
exists(int x, int y | this.lastPart(x, y) |
this.groupContents(x, y, start, end)
@@ -733,7 +952,7 @@ abstract class RegexString extends Expr {
(
this.character(start, end)
or
this.qualifiedItem(start, end, _)
this.qualifiedItem(start, end, _, _)
or
this.charSet(start, end)
) and
@@ -748,7 +967,7 @@ abstract class RegexString extends Expr {
(
this.character(start, end)
or
this.qualifiedItem(start, end, _)
this.qualifiedItem(start, end, _, _)
or
this.charSet(start, end)
) and

177
python/ql/src/semmle/python/security/dataflow/PolynomialReDoS.qll Normal file
View File

@@ -0,0 +1,177 @@
/**
* Provides a taint-tracking configuration for detecting polynomial regular expression denial of service (ReDoS)
* vulnerabilities.
*/
import python
import semmle.python.dataflow.new.DataFlow
import semmle.python.dataflow.new.DataFlow2
import semmle.python.dataflow.new.TaintTracking
import semmle.python.Concepts
import semmle.python.dataflow.new.RemoteFlowSources
import semmle.python.dataflow.new.BarrierGuards
import semmle.python.RegexTreeView
import semmle.python.ApiGraphs
/** A configuration for finding uses of compiled regexes. */
class RegexDefinitionConfiguration extends DataFlow2::Configuration {
RegexDefinitionConfiguration() { this = "RegexDefinitionConfiguration" }
override predicate isSource(DataFlow::Node source) { source instanceof RegexDefinitonSource }
override predicate isSink(DataFlow::Node sink) { sink instanceof RegexDefinitionSink }
}
/** A regex compilation. */
class RegexDefinitonSource extends DataFlow::CallCfgNode {
DataFlow::Node regexNode;
RegexDefinitonSource() {
this = API::moduleImport("re").getMember("compile").getACall() and
regexNode in [this.getArg(0), this.getArgByName("pattern")]
}
/** Gets the regex that is being compiled by this node. */
RegExpTerm getRegExp() { result.getRegex() = regexNode.asExpr() and result.isRootTerm() }
/** Gets the data flow node for the regex being compiled by this node. */
DataFlow::Node getRegexNode() { result = regexNode }
}
/** A use of a compiled regex. */
class RegexDefinitionSink extends DataFlow::Node {
RegexExecutionMethod method;
DataFlow::CallCfgNode executingCall;
RegexDefinitionSink() {
exists(DataFlow::AttrRead reMethod |
executingCall.getFunction() = reMethod and
reMethod.getAttributeName() = method and
this = reMethod.getObject()
)
}
/** Gets the method used to execute the regex. */
RegexExecutionMethod getMethod() { result = method }
/** Gets the data flow node for the executing call. */
DataFlow::CallCfgNode getExecutingCall() { result = executingCall }
}
/**
* A taint-tracking configuration for detecting regular expression denial-of-service vulnerabilities.
*/
class PolynomialReDoSConfiguration extends TaintTracking::Configuration {
PolynomialReDoSConfiguration() { this = "PolynomialReDoSConfiguration" }
override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
override predicate isSink(DataFlow::Node sink) { sink instanceof PolynomialReDoSSink }
}
/** A data flow node executing a regex. */
abstract class RegexExecution extends DataFlow::Node {
/** Gets the data flow node for the regex being compiled by this node. */
abstract DataFlow::Node getRegexNode();
/** Gets a dataflow node for the string to be searched or matched against. */
abstract DataFlow::Node getString();
}
private class RegexExecutionMethod extends string {
RegexExecutionMethod() {
this in ["match", "fullmatch", "search", "split", "findall", "finditer", "sub", "subn"]
}
}
/** Gets the index of the argument representing the string to be searched by a regex. */
int stringArg(RegexExecutionMethod method) {
method in ["match", "fullmatch", "search", "split", "findall", "finditer"] and
result = 1
or
method in ["sub", "subn"] and
result = 2
}
/**
* A class to find `re` methods immediately executing an expression.
*
* See `RegexExecutionMethods`
*/
class DirectRegex extends DataFlow::CallCfgNode, RegexExecution {
RegexExecutionMethod method;
DirectRegex() { this = API::moduleImport("re").getMember(method).getACall() }
override DataFlow::Node getRegexNode() {
result in [this.getArg(0), this.getArgByName("pattern")]
}
override DataFlow::Node getString() {
result in [this.getArg(stringArg(method)), this.getArgByName("string")]
}
}
/**
* A class to find `re` methods immediately executing a compiled expression by `re.compile`.
*
* Given the following example:
*
* ```py
* pattern = re.compile(input)
* pattern.match(s)
* ```
*
* This class will identify that `re.compile` compiles `input` and afterwards
* executes `re`'s `match`. As a result, `this` will refer to `pattern.match(s)`
* and `this.getRegexNode()` will return the node for `input` (`re.compile`'s first argument)
*
*
* See `RegexExecutionMethods`
*
* See https://docs.python.org/3/library/re.html#regular-expression-objects
*/
private class CompiledRegex extends DataFlow::CallCfgNode, RegexExecution {
DataFlow::Node regexNode;
RegexExecutionMethod method;
CompiledRegex() {
exists(
RegexDefinitionConfiguration conf, RegexDefinitonSource source, RegexDefinitionSink sink
|
conf.hasFlow(source, sink) and
regexNode = source.getRegexNode() and
method = sink.getMethod() and
this = sink.getExecutingCall()
)
}
override DataFlow::Node getRegexNode() { result = regexNode }
override DataFlow::Node getString() {
result in [this.getArg(stringArg(method) - 1), this.getArgByName("string")]
}
}
/**
* A data flow sink node for polynomial regular expression denial-of-service vulnerabilities.
*/
class PolynomialReDoSSink extends DataFlow::Node {
RegExpTerm t;
PolynomialReDoSSink() {
exists(RegexExecution re |
re.getRegexNode().asExpr() = t.getRegex() and
this = re.getString()
) and
t.isRootTerm()
}
/** Gets the regex that is being executed by this node. */
RegExpTerm getRegExp() { result = t }
/**
* Gets the node to highlight in the alert message.
*/
DataFlow::Node getHighlight() { result = this }
}

342
python/ql/src/semmle/python/security/performance/ExponentialBackTracking.qll Normal file
View File

@@ -0,0 +1,342 @@
/**
* This library implements the analysis described in the following two papers:
*
* James Kirrage, Asiri Rathnayake, Hayo Thielecke: Static Analysis for
* Regular Expression Denial-of-Service Attacks. NSS 2013.
* (http://www.cs.bham.ac.uk/~hxt/research/reg-exp-sec.pdf)
* Asiri Rathnayake, Hayo Thielecke: Static Analysis for Regular Expression
* Exponential Runtime via Substructural Logics. 2014.
* (https://www.cs.bham.ac.uk/~hxt/research/redos_full.pdf)
*
* The basic idea is to search for overlapping cycles in the NFA, that is,
* states `q` such that there are two distinct paths from `q` to itself
* that consume the same word `w`.
*
* For any such state `q`, an attack string can be constructed as follows:
* concatenate a prefix `v` that takes the NFA to `q` with `n` copies of
* the word `w` that leads back to `q` along two different paths, followed
* by a suffix `x` that is _not_ accepted in state `q`. A backtracking
* implementation will need to explore at least 2^n different ways of going
* from `q` back to itself while trying to match the `n` copies of `w`
* before finally giving up.
*
* Now in order to identify overlapping cycles, all we have to do is find
* pumpable forks, that is, states `q` that can transition to two different
* states `r1` and `r2` on the same input symbol `c`, such that there are
* paths from both `r1` and `r2` to `q` that consume the same word. The latter
* condition is equivalent to saying that `(q, q)` is reachable from `(r1, r2)`
* in the product NFA.
*
* This is what the library does. It makes a simple attempt to construct a
* prefix `v` leading into `q`, but only to improve the alert message.
* And the library tries to prove the existence of a suffix that ensures
* rejection. This check might fail, which can cause false positives.
*
* Finally, sometimes it depends on the translation whether the NFA generated
* for a regular expression has a pumpable fork or not. We implement one
* particular translation, which may result in false positives or negatives
* relative to some particular JavaScript engine.
*
* More precisely, the library constructs an NFA from a regular expression `r`
* as follows:
*
* * Every sub-term `t` gives rise to an NFA state `Match(t,i)`, representing
* the state of the automaton before attempting to match the `i`th character in `t`.
* * There is one accepting state `Accept(r)`.
* * There is a special `AcceptAnySuffix(r)` state, which accepts any suffix string
* by using an epsilon transition to `Accept(r)` and an any transition to itself.
* * Transitions between states may be labelled with epsilon, or an abstract
* input symbol.
* * Each abstract input symbol represents a set of concrete input characters:
* either a single character, a set of characters represented by a
* character class, or the set of all characters.
* * The product automaton is constructed lazily, starting with pair states
* `(q, q)` where `q` is a fork, and proceding along an over-approximate
* step relation.
* * The over-approximate step relation allows transitions along pairs of
* abstract input symbols where the symbols have overlap in the characters they accept.
* * Once a trace of pairs of abstract input symbols that leads from a fork
* back to itself has been identified, we attempt to construct a concrete
* string corresponding to it, which may fail.
* * Lastly we ensure that any state reached by repeating `n` copies of `w` has
* a suffix `x` (possible empty) that is most likely __not__ accepted.
*/
import ReDoSUtil
/**
* Holds if state `s` might be inside a backtracking repetition.
*/
pragma[noinline]
predicate stateInsideBacktracking(State s) {
s.getRepr().getParent*() instanceof MaybeBacktrackingRepetition
}
/**
* A infinitely repeating quantifier that might backtrack.
*/
class MaybeBacktrackingRepetition extends InfiniteRepetitionQuantifier {
MaybeBacktrackingRepetition() {
exists(RegExpTerm child |
child instanceof RegExpAlt or
child instanceof RegExpQuantifier
|
child.getParent+() = this
)
}
}
/**
* A state in the product automaton.
*/
newtype TStatePair =
/**
* We lazily only construct those states that we are actually
* going to need: `(q, q)` for every fork state `q`, and any
* pair of states that can be reached from a pair that we have
* already constructed. To cut down on the number of states,
* we only represent states `(q1, q2)` where `q1` is lexicographically
* no bigger than `q2`.
*
* States are only constructed if both states in the pair are
* inside a repetition that might backtrack.
*/
MkStatePair(State q1, State q2) {
isFork(q1, _, _, _, _) and q2 = q1
or
(step(_, _, _, q1, q2) or step(_, _, _, q2, q1)) and
rankState(q1) <= rankState(q2)
}
/**
* Gets a unique number for a `state`.
* Is used to create an ordering of states, where states with the same `toString()` will be ordered differently.
*/
int rankState(State state) {
state =
rank[result](State s, Location l |
l = s.getRepr().getLocation()
|
s order by l.getStartLine(), l.getStartColumn(), s.toString()
)
}
/**
* A state in the product automaton.
*/
class StatePair extends TStatePair {
State q1;
State q2;
StatePair() { this = MkStatePair(q1, q2) }
/** Gets a textual representation of this element. */
string toString() { result = "(" + q1 + ", " + q2 + ")" }
/** Gets the first component of the state pair. */
State getLeft() { result = q1 }
/** Gets the second component of the state pair. */
State getRight() { result = q2 }
}
/**
* Holds for all constructed state pairs.
*
* Used in `statePairDist`
*/
predicate isStatePair(StatePair p) { any() }
/**
* Holds if there are transitions from the components of `q` to the corresponding
* components of `r`.
*
* Used in `statePairDist`
*/
predicate delta2(StatePair q, StatePair r) { step(q, _, _, r) }
/**
* Gets the minimum length of a path from `q` to `r` in the
* product automaton.
*/
int statePairDist(StatePair q, StatePair r) =
shortestDistances(isStatePair/1, delta2/2)(q, r, result)
/**
* 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.
*
* This predicate only holds for states associated with regular expressions
* that have at least one repetition quantifier in them (otherwise the
* expression cannot be vulnerable to ReDoS attacks anyway).
*/
pragma[noopt]
predicate isFork(State q, InputSymbol s1, InputSymbol s2, State r1, State r2) {
stateInsideBacktracking(q) and
exists(State q1, State q2 |
q1 = epsilonSucc*(q) and
delta(q1, s1, r1) and
q2 = epsilonSucc*(q) and
delta(q2, s2, r2) and
// Use pragma[noopt] to prevent intersect(s1,s2) from being the starting point of the join.
// From (s1,s2) it would find a huge number of intermediate state pairs (q1,q2) originating from different literals,
// and discover at the end that no `q` can reach both `q1` and `q2` by epsilon transitions.
exists(intersect(s1, s2))
|
s1 != s2
or
r1 != r2
or
r1 = r2 and q1 != q2
or
// If q can reach itself by epsilon transitions, then there are two distinct paths to the q1/q2 state:
// one that uses the loop and one that doesn't. The engine will separately attempt to match with each path,
// despite ending in the same state. The "fork" thus arises from the choice of whether to use the loop or not.
// To avoid every state in the loop becoming a fork state,
// we arbitrarily pick the InfiniteRepetitionQuantifier state as the canonical fork state for the loop
// (every epsilon-loop must contain such a state).
//
// We additionally require that the there exists another InfiniteRepetitionQuantifier `mid` on the path from `q` to itself.
// This is done to avoid flagging regular expressions such as `/(a?)*b/` - that only has polynomial runtime, and is detected by `js/polynomial-redos`.
// The below code is therefore a heuritic, that only flags regular expressions such as `/(a*)*b/`,
// and does not flag regular expressions such as `/(a?b?)c/`, but the latter pattern is not used frequently.
r1 = r2 and
q1 = q2 and
epsilonSucc+(q) = q and
exists(RegExpTerm term | term = q.getRepr() | term instanceof InfiniteRepetitionQuantifier) and
// One of the mid states is an infinite quantifier itself
exists(State mid, RegExpTerm term |
mid = epsilonSucc+(q) and
term = mid.getRepr() and
term instanceof InfiniteRepetitionQuantifier and
q = epsilonSucc+(mid) and
not mid = q
)
) and
stateInsideBacktracking(r1) and
stateInsideBacktracking(r2)
}
/**
* Gets the state pair `(q1, q2)` or `(q2, q1)`; note that only
* one or the other is defined.
*/
StatePair mkStatePair(State q1, State q2) {
result = MkStatePair(q1, q2) or result = MkStatePair(q2, q1)
}
/**
* Holds if there are transitions from the components of `q` to the corresponding
* components of `r` labelled with `s1` and `s2`, respectively.
*/
predicate step(StatePair q, InputSymbol s1, InputSymbol s2, StatePair r) {
exists(State r1, State r2 | step(q, s1, s2, r1, r2) and r = mkStatePair(r1, r2))
}
/**
* Holds if there are transitions from the components of `q` to `r1` and `r2`
* labelled with `s1` and `s2`, respectively.
*
* We only consider transitions where the resulting states `(r1, r2)` are both
* inside a repetition that might backtrack.
*/
pragma[noopt]
predicate step(StatePair q, InputSymbol s1, InputSymbol s2, State r1, State r2) {
exists(State q1, State q2 | q.getLeft() = q1 and q.getRight() = q2 |
deltaClosed(q1, s1, r1) and
deltaClosed(q2, s2, r2) and
// use noopt to force the join on `intersect` to happen last.
exists(intersect(s1, s2))
) and
stateInsideBacktracking(r1) and
stateInsideBacktracking(r2)
}
private newtype TTrace =
Nil() or
Step(InputSymbol s1, InputSymbol s2, TTrace t) {
exists(StatePair p |
isReachableFromFork(_, p, t, _) and
step(p, s1, s2, _)
)
or
t = Nil() and isFork(_, s1, s2, _, _)
}
/**
* A list of pairs of input symbols that describe a path in the product automaton
* starting from some fork state.
*/
class Trace extends TTrace {
/** Gets a textual representation of this element. */
string toString() {
this = Nil() and result = "Nil()"
or
exists(InputSymbol s1, InputSymbol s2, Trace t | this = Step(s1, s2, t) |
result = "Step(" + s1 + ", " + s2 + ", " + t + ")"
)
}
}
/**
* Gets a string corresponding to the trace `t`.
*/
string concretise(Trace t) {
t = Nil() and result = ""
or
exists(InputSymbol s1, InputSymbol s2, Trace rest | t = Step(s1, s2, rest) |
result = concretise(rest) + intersect(s1, s2)
)
}
/**
* 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.
*/
predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) {
// base case
exists(InputSymbol s1, InputSymbol s2, State q1, State q2 |
isFork(fork, s1, s2, q1, q2) and
r = MkStatePair(q1, q2) and
w = Step(s1, s2, Nil()) and
rem = statePairDist(r, MkStatePair(fork, fork))
)
or
// recursive case
exists(StatePair p, Trace v, InputSymbol s1, InputSymbol s2 |
isReachableFromFork(fork, p, v, rem + 1) and
step(p, s1, s2, r) and
w = Step(s1, s2, v) and
rem >= statePairDist(r, MkStatePair(fork, fork))
)
}
/**
* Gets a state in the product automaton from which `(fork, fork)` is
* reachable in zero or more epsilon transitions.
*/
StatePair getAForkPair(State fork) {
isFork(fork, _, _, _, _) and
result = MkStatePair(epsilonPred*(fork), epsilonPred*(fork))
}
/**
* Holds if `fork` is a pumpable fork with word `w`.
*/
predicate isPumpable(State fork, string w) {
exists(StatePair q, Trace t |
isReachableFromFork(fork, q, t, _) and
q = getAForkPair(fork) and
w = concretise(t)
)
}
/**
* An instantiation of `ReDoSConfiguration` for exponential backtracking.
*/
class ExponentialReDoSConfiguration extends ReDoSConfiguration {
ExponentialReDoSConfiguration() { this = "ExponentialReDoSConfiguration" }
override predicate isReDoSCandidate(State state, string pump) { isPumpable(state, pump) }
}

1034
python/ql/src/semmle/python/security/performance/ReDoSUtil.qll Normal file
View File

File diff suppressed because it is too large Load Diff

15
python/ql/src/semmle/python/security/performance/RegExpTreeView.qll Normal file
View File

@@ -0,0 +1,15 @@
/**
* This module should provide a class hierarchy corresponding to a parse tree of regular expressions.
*/
import python
import semmle.python.RegexTreeView
/**
* Holds if the regular expression should not be considered.
*
* For javascript we make the pragmatic performance optimization to ignore files we did not extract.
*/
predicate isExcluded(RegExpParent parent) {
not exists(parent.getRegex().getLocation().getFile().getRelativePath())
}

449
python/ql/src/semmle/python/security/performance/SuperlinearBackTracking.qll Normal file
View File

@@ -0,0 +1,449 @@
/**
* 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()
)
}
/**
* Holds if `t` matches at least an epsilon symbol.
*
* That is, this term does not restrict the language of the enclosing regular expression.
*
* This is implemented as an under-approximation, and this predicate does not hold for sub-patterns in particular.
*/
private predicate matchesEpsilon(RegExpTerm t) {
t instanceof RegExpStar
or
t instanceof RegExpOpt
or
t.(RegExpRange).getLowerBound() = 0
or
exists(RegExpTerm child |
child = t.getAChild() and
matchesEpsilon(child)
|
t instanceof RegExpAlt or
t instanceof RegExpGroup or
t instanceof RegExpPlus or
t instanceof RegExpRange
)
or
matchesEpsilon(t.(RegExpBackRef).getGroup())
or
forex(RegExpTerm child | child = t.(RegExpSequence).getAChild() | matchesEpsilon(child))
}
/**
* 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 }
}