diff --git a/config/identical-files.json b/config/identical-files.json index 2ff65c453f0..841274f3a3a 100644 --- a/config/identical-files.json +++ b/config/identical-files.json @@ -475,20 +475,23 @@ "python/ql/lib/semmle/python/security/internal/SensitiveDataHeuristics.qll", "ruby/ql/lib/codeql/ruby/security/internal/SensitiveDataHeuristics.qll" ], - "ReDoS Util Python/JS/Ruby": [ + "ReDoS Util Python/JS/Ruby/Java": [ "javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtil.qll", "python/ql/lib/semmle/python/security/performance/ReDoSUtil.qll", - "ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtil.qll" + "ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtil.qll", + "java/ql/lib/semmle/code/java/security/performance/ReDoSUtil.qll" ], - "ReDoS Exponential Python/JS/Ruby": [ + "ReDoS Exponential Python/JS/Ruby/Java": [ "javascript/ql/lib/semmle/javascript/security/performance/ExponentialBackTracking.qll", "python/ql/lib/semmle/python/security/performance/ExponentialBackTracking.qll", - "ruby/ql/lib/codeql/ruby/security/performance/ExponentialBackTracking.qll" + "ruby/ql/lib/codeql/ruby/security/performance/ExponentialBackTracking.qll", + "java/ql/lib/semmle/code/java/security/performance/ExponentialBackTracking.qll" ], - "ReDoS Polynomial Python/JS/Ruby": [ + "ReDoS Polynomial Python/JS/Ruby/Java": [ "javascript/ql/lib/semmle/javascript/security/performance/SuperlinearBackTracking.qll", "python/ql/lib/semmle/python/security/performance/SuperlinearBackTracking.qll", - "ruby/ql/lib/codeql/ruby/security/performance/SuperlinearBackTracking.qll" + "ruby/ql/lib/codeql/ruby/security/performance/SuperlinearBackTracking.qll", + "java/ql/lib/semmle/code/java/security/performance/SuperlinearBackTracking.qll" ], "BadTagFilterQuery Python/JS/Ruby": [ "javascript/ql/lib/semmle/javascript/security/BadTagFilterQuery.qll", diff --git a/java/ql/lib/semmle/code/java/PrintAst.qll b/java/ql/lib/semmle/code/java/PrintAst.qll index 22ee6a30d00..05453baa045 100644 --- a/java/ql/lib/semmle/code/java/PrintAst.qll +++ b/java/ql/lib/semmle/code/java/PrintAst.qll @@ -7,6 +7,7 @@ */ import java +import semmle.code.java.regex.RegexTreeView private newtype TPrintAstConfiguration = MkPrintAstConfiguration() @@ -132,6 +133,9 @@ private newtype TPrintAstNode = } or TImportsNode(CompilationUnit cu) { shouldPrint(cu, _) and exists(Import i | i.getCompilationUnit() = cu) + } or + TRegExpTermNode(RegExpTerm term) { + exists(StringLiteral str | term.getRootTerm() = getParsedRegExp(str) and shouldPrint(str, _)) } /** @@ -164,6 +168,19 @@ class PrintAstNode extends TPrintAstNode { */ Location getLocation() { none() } + /** + * Holds if this node is at the specified location. + * The location spans column `startcolumn` of line `startline` to + * column `endcolumn` of line `endline` in file `filepath`. + * For more information, see + * [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/). + */ + predicate hasLocationInfo( + string filepath, int startline, int startcolumn, int endline, int endcolumn + ) { + this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) + } + /** * Gets the value of the property of this node, where the name of the property * is `key`. @@ -290,6 +307,47 @@ final class AnnotationPartNode extends ExprStmtNode { } } +/** + * A node representing a `StringLiteral`. + * If it is used as a regular expression, then it has a single child, the root of the parsed regular expression. + */ +final class StringLiteralNode extends ExprStmtNode { + StringLiteralNode() { element instanceof StringLiteral } + + override PrintAstNode getChild(int childIndex) { + childIndex = 0 and + result.(RegExpTermNode).getTerm() = getParsedRegExp(element) + } +} + +/** + * A node representing 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() } + + override predicate hasLocationInfo( + string filepath, int startline, int startcolumn, int endline, int endcolumn + ) { + term.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) + } +} + /** * A node representing a `LocalVariableDeclExpr`. */ diff --git a/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll b/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll index f186fd62bf5..7584acfab09 100644 --- a/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll +++ b/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll @@ -142,6 +142,7 @@ private module Frameworks { private import semmle.code.java.frameworks.jOOQ private import semmle.code.java.frameworks.JMS private import semmle.code.java.frameworks.RabbitMQ + private import semmle.code.java.regex.RegexFlowModels } private predicate sourceModelCsv(string row) { diff --git a/java/ql/lib/semmle/code/java/regex/RegexFlowConfigs.qll b/java/ql/lib/semmle/code/java/regex/RegexFlowConfigs.qll new file mode 100644 index 00000000000..8936de5a923 --- /dev/null +++ b/java/ql/lib/semmle/code/java/regex/RegexFlowConfigs.qll @@ -0,0 +1,193 @@ +/** + * Defines configurations and steps for handling regexes + */ + +import java +import semmle.code.java.dataflow.ExternalFlow +private import semmle.code.java.dataflow.DataFlow +private import semmle.code.java.dataflow.DataFlow2 +private import RegexFlowModels +private import semmle.code.java.security.SecurityTests + +private class ExploitableStringLiteral extends StringLiteral { + ExploitableStringLiteral() { this.getValue().matches(["%+%", "%*%", "%{%}%"]) } +} + +/** + * Holds if `kind` is an external sink kind that is relevant for regex flow. + * `full` is true if sinks with this kind match against the full string of its input. + * `strArg` is the index of the argument to methods with this sink kind that contan the string to be matched against, + * where -1 is the qualifier; or -2 if no such argument exists. + */ +private predicate regexSinkKindInfo(string kind, boolean full, int strArg) { + sinkModel(_, _, _, _, _, _, _, kind, _) and + exists(string fullStr, string strArgStr | + ( + full = true and fullStr = "f" + or + full = false and fullStr = "" + ) and + ( + strArgStr.toInt() = strArg + or + strArg = -2 and + strArgStr = "" + ) + | + kind = "regex-use[" + fullStr + strArgStr + "]" + ) +} + +/** A sink that is relevant for regex flow. */ +private class RegexFlowSink extends DataFlow::Node { + boolean full; + int strArg; + + RegexFlowSink() { + exists(string kind | + regexSinkKindInfo(kind, full, strArg) and + sinkNode(this, kind) + ) + } + + /** Holds if a regex that flows here is matched against a full string (rather than a substring). */ + predicate matchesFullString() { full = true } + + /** Gets the string expression that a regex that flows here is matched against, if any. */ + Expr getStringArgument() { + exists(MethodAccess ma | + this.asExpr() = argOf(ma, _) and + result = argOf(ma, strArg) + ) + } +} + +private Expr argOf(MethodAccess ma, int arg) { + arg = -1 and result = ma.getQualifier() + or + result = ma.getArgument(arg) +} + +/** + * A unit class for adding additional regex flow steps. + * + * Extend this class to add additional flow steps that should apply to regex flow configurations. + */ +class RegexAdditionalFlowStep extends Unit { + /** + * Holds if the step from `node1` to `node2` should be considered a flow + * step for regex flow configurations. + */ + abstract predicate step(DataFlow::Node node1, DataFlow::Node node2); +} + +// TODO: This may be able to be done with models-as-data if query-specific flow steps beome supported. +private class JdkRegexFlowStep extends RegexAdditionalFlowStep { + override predicate step(DataFlow::Node node1, DataFlow::Node node2) { + exists(MethodAccess ma, Method m, string package, string type, string name, int arg | + ma.getMethod().getSourceDeclaration().overrides*(m) and + m.hasQualifiedName(package, type, name) and + node1.asExpr() = argOf(ma, arg) and + node2.asExpr() = ma + | + package = "java.util.regex" and + type = "Pattern" and + ( + name = ["asMatchPredicate", "asPredicate", "matcher"] and + arg = -1 + or + name = "compile" and + arg = 0 + ) + or + package = "java.util.function" and + type = "Predicate" and + name = ["and", "or", "not", "negate"] and + arg = [-1, 0] + ) + } +} + +private class GuavaRegexFlowStep extends RegexAdditionalFlowStep { + override predicate step(DataFlow::Node node1, DataFlow::Node node2) { + exists(MethodAccess ma, Method m, string package, string type, string name, int arg | + ma.getMethod().getSourceDeclaration().overrides*(m) and + m.hasQualifiedName(package, type, name) and + node1.asExpr() = argOf(ma, arg) and + node2.asExpr() = ma + | + package = "com.google.common.base" and + type = "Splitter" and + ( + name = "on" and + m.getParameterType(0).(RefType).hasQualifiedName("java.util.regex", "Pattern") and + arg = 0 + or + name = "withKeyValueSeparator" and + m.getParameterType(0).(RefType).hasQualifiedName("com.google.common.base", "Splitter") and + arg = 0 + or + name = "onPattern" and + arg = 0 + or + name = ["limit", "omitEmptyStrings", "trimResults", "withKeyValueSeparator"] and + arg = -1 + ) + ) + } +} + +private class RegexFlowConf extends DataFlow2::Configuration { + RegexFlowConf() { this = "RegexFlowConfig" } + + override predicate isSource(DataFlow::Node node) { + node.asExpr() instanceof ExploitableStringLiteral + } + + override predicate isSink(DataFlow::Node node) { node instanceof RegexFlowSink } + + override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { + any(RegexAdditionalFlowStep s).step(node1, node2) + } + + override predicate isBarrier(DataFlow::Node node) { + node.getEnclosingCallable().getDeclaringType() instanceof NonSecurityTestClass + } +} + +/** + * Holds if `regex` is used as a regex, with the mode `mode` (if known). + * If regex mode is not known, `mode` will be `"None"`. + * + * As an optimisation, only regexes containing an infinite repitition quatifier (`+`, `*`, or `{x,}`) + * and therefore may be relevant for ReDoS queries are considered. + */ +predicate usedAsRegex(StringLiteral regex, string mode, boolean match_full_string) { + any(RegexFlowConf c).hasFlow(DataFlow2::exprNode(regex), _) and + mode = "None" and // TODO: proper mode detection + (if matchesFullString(regex) then match_full_string = true else match_full_string = false) +} + +/** + * Holds if `regex` is used as a regular expression that is matched against a full string, + * as though it was implicitly surrounded by ^ and $. + */ +private predicate matchesFullString(StringLiteral regex) { + exists(RegexFlowConf c, RegexFlowSink sink | + sink.matchesFullString() and + c.hasFlow(DataFlow2::exprNode(regex), sink) + ) +} + +/** + * Holds if the string literal `regex` is a regular expression that is matched against the expression `str`. + * + * As an optimisation, only regexes containing an infinite repitition quatifier (`+`, `*`, or `{x,}`) + * and therefore may be relevant for ReDoS queries are considered. + */ +predicate regexMatchedAgainst(StringLiteral regex, Expr str) { + exists(RegexFlowConf c, RegexFlowSink sink | + str = sink.getStringArgument() and + c.hasFlow(DataFlow2::exprNode(regex), sink) + ) +} diff --git a/java/ql/lib/semmle/code/java/regex/RegexFlowModels.qll b/java/ql/lib/semmle/code/java/regex/RegexFlowModels.qll new file mode 100644 index 00000000000..6934540116f --- /dev/null +++ b/java/ql/lib/semmle/code/java/regex/RegexFlowModels.qll @@ -0,0 +1,32 @@ +/** Definitions of data flow steps for determining flow of regular expressions. */ + +import java +import semmle.code.java.dataflow.ExternalFlow + +private class RegexSinkCsv extends SinkModelCsv { + override predicate row(string row) { + row = + [ + //"namespace;type;subtypes;name;signature;ext;input;kind" + "java.util.regex;Matcher;false;matches;();;Argument[-1];regex-use[f]", + "java.util.regex;Pattern;false;asMatchPredicate;();;Argument[-1];regex-use[f]", + "java.util.regex;Pattern;false;compile;(String);;Argument[0];regex-use[]", + "java.util.regex;Pattern;false;compile;(String,int);;Argument[0];regex-use[]", + "java.util.regex;Pattern;false;matcher;(CharSequence);;Argument[-1];regex-use[0]", + "java.util.regex;Pattern;false;matches;(String,CharSequence);;Argument[0];regex-use[f1]", + "java.util.regex;Pattern;false;split;(CharSequence);;Argument[-1];regex-use[0]", + "java.util.regex;Pattern;false;split;(CharSequence,int);;Argument[-1];regex-use[0]", + "java.util.regex;Pattern;false;splitAsStream;(CharSequence);;Argument[-1];regex-use[0]", + "java.util.function;Predicate;false;test;(Object);;Argument[-1];regex-use[0]", + "java.lang;String;false;matches;(String);;Argument[0];regex-use[f-1]", + "java.lang;String;false;split;(String);;Argument[0];regex-use[-1]", + "java.lang;String;false;split;(String,int);;Argument[0];regex-use[-1]", + "java.lang;String;false;replaceAll;(String,String);;Argument[0];regex-use[-1]", + "java.lang;String;false;replaceFirst;(String,String);;Argument[0];regex-use[-1]", + "com.google.common.base;Splitter;false;onPattern;(String);;Argument[0];regex-use[]", + "com.google.common.base;Splitter;false;split;(CharSequence);;Argument[-1];regex-use[0]", + "com.google.common.base;Splitter;false;splitToList;(CharSequence);;Argument[-1];regex-use[0]", + "com.google.common.base;Splitter$MapSplitter;false;split;(CharSequence);;Argument[-1];regex-use[0]", + ] + } +} diff --git a/java/ql/lib/semmle/code/java/regex/RegexTreeView.qll b/java/ql/lib/semmle/code/java/regex/RegexTreeView.qll new file mode 100644 index 00000000000..c3592634fa0 --- /dev/null +++ b/java/ql/lib/semmle/code/java/regex/RegexTreeView.qll @@ -0,0 +1,1084 @@ +/** Provides a class hierarchy corresponding to a parse tree of regular expressions. */ + +private import java +private import semmle.code.java.regex.regex + +/** + * An element containing a regular expression term, that is, either + * a string literal (parsed as a regular expression; the root of the parse tree) + * or another regular expression term (a decendent of the root). + * + * For sequences and alternations, we require at least two children. + * Otherwise, we wish to represent the term differently. + * This avoids multiple representations of the same term. + */ +private 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.quantifiedItem(start, end, _, _) } or + /** A sequence term */ + TRegExpSequence(Regex re, int start, int end) { + re.sequence(start, end) and + // Only create sequence nodes for sequences with two or more children. + exists(int mid | + re.item(start, mid) and + re.item(mid, _) + ) + } or + /** An alternation term */ + TRegExpAlt(Regex re, int start, int end) { + re.alternation(start, end) and + exists(int part_end | + re.alternationOption(start, end, start, part_end) and + part_end < end + ) // if an alternation does not have more than one element, it should be treated as that element instead. + } 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 quoted sequence */ + TRegExpQuote(Regex re, int start, int end) { re.quote(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; the root of the parse tree) + * or another regular expression term (a decendent of the root). + */ +class RegExpParent extends TRegExpParent { + /** Gets a textual representation of this element. */ + string toString() { result = "RegExpParent" } + + /** Gets the `i`th child term. */ + RegExpTerm getChild(int i) { none() } + + /** Gets a child term . */ + RegExpTerm getAChild() { result = this.getChild(_) } + + /** Gets the number of child terms. */ + int getNumChild() { result = count(this.getAChild()) } + + /** Gets the associated regex. */ + abstract Regex getRegex(); +} + +/** + * A string literal used as a regular expression. + * + * As an optimisation, only regexes containing an infinite repitition quatifier (`+`, `*`, or `{x,}`) + * and therefore may be relevant for ReDoS queries are considered. + */ +class RegExpLiteral extends TRegExpLiteral, RegExpParent { + Regex re; + + RegExpLiteral() { this = TRegExpLiteral(re) } + + override string toString() { result = re.toString() } + + override RegExpTerm getChild(int i) { i = 0 and result.getRegex() = re and result.isRootTerm() } + + /** Holds if dot, `.`, matches all characters, including newlines. */ + predicate isDotAll() { re.getAMode() = "DOTALL" } + + /** Holds if this regex matching is case-insensitive for this regex. */ + predicate isIgnoreCase() { re.getAMode() = "IGNORECASE" } + + /** Get a string representing all modes for this regex. */ + string getFlags() { result = concat(string mode | mode = re.getAMode() | mode, " | ") } + + override Regex getRegex() { result = re } + + /** Gets the primary QL class for this regex. */ + string getPrimaryQLClass() { result = "RegExpLiteral" } +} + +/** + * A regular expression term, that is, a syntactic part of a regular expression. + * These are the tree nodes that form the parse tree of a regular expression literal. + */ +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 = TRegExpQuote(re, start, end) + or + this = TRegExpGroup(re, start, end) + or + this = TRegExpQuantifier(re, start, end) + or + this = TRegExpSequence(re, start, end) + or + this = TRegExpSpecialChar(re, start, end) + } + + /** + * Gets the outermost term of this regular expression. + */ + RegExpTerm getRootTerm() { + this.isRootTerm() and result = this + or + result = this.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() } + + /** + * 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 } + + /** Holds if this term occurs in regex `inRe` offsets `startOffset` to `endOffset`. */ + predicate occursInRegex(Regex inRe, int startOffset, int endOffset) { + inRe = re and startOffset = start and endOffset = 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 + ) { + /* + * This is an approximation that handles the simple and common case of single, + * normal string literal written in the source, but does not give correct results in more complex cases + * such as compile-time concatenation, or multi-line string literals. + */ + + exists(int re_start, int re_end, int src_start, int src_end | + re.getLocation().hasLocationInfo(filepath, startline, re_start, endline, re_end) and + re.sourceCharacter(start, src_start, _) and + re.sourceCharacter(end - 1, _, src_end) and + startcolumn = re_start + src_start and + endcolumn = re_start + src_end - 1 + ) + } + + /** 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 = this.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 = this.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.quantifiedPart(start, part_end, end, maybe_empty, may_repeat_forever) + } + + override RegExpTerm getChild(int i) { + i = 0 and + result.occursInRegex(re, start, part_end) + } + + /** Holds if this term may match zero times. */ + predicate mayBeEmpty() { maybe_empty = true } + + /** Holds if this term may match an unlimited number of times. */ + predicate mayRepeatForever() { may_repeat_forever = true } + + /** Gets the quantifier for this term. That is e.g "?" for "a?". */ + string getQuantifier() { result = re.getText().substring(part_end, end) } + + /** Holds if this is a possessive quantifier, e.g. a*+. */ + predicate isPossessive() { + exists(string q | q = this.getQuantifier() | q.length() > 1 and q.charAt(q.length() - 1) = "+") + } + + 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.getQuantifier().charAt(0) = "*" } + + override string getPrimaryQLClass() { result = "RegExpStar" } +} + +/** + * A plus-quantified term. + * + * Example: + * + * ``` + * \w+ + * ``` + */ +class RegExpPlus extends InfiniteRepetitionQuantifier { + RegExpPlus() { this.getQuantifier().charAt(0) = "+" } + + override string getPrimaryQLClass() { result = "RegExpPlus" } +} + +/** + * An optional term. + * + * Example: + * + * ``` + * ;? + * ``` + */ +class RegExpOpt extends RegExpQuantifier { + RegExpOpt() { this.getQuantifier().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) } + + /** Gets the string defining the upper bound of this range, which is empty when no such bound exists. */ + string getUpper() { result = upper } + + /** Gets the string defining the lower bound of this range, which is empty when no such bound exists. */ + 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) } + + override RegExpTerm getChild(int i) { result = seqChild(re, start, end, i) } + + /** Gets the element preceding `element` in this sequence. */ + RegExpTerm previousElement(RegExpTerm element) { element = this.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 + exists(int itemEnd | + re.item(start, itemEnd) and + result.occursInRegex(re, start, itemEnd) + ) + or + i > 0 and + exists(int itemStart, int itemEnd | itemStart = seqChildEnd(re, start, end, i - 1) | + re.item(itemStart, itemEnd) and + result.occursInRegex(re, itemStart, itemEnd) + ) + ) +} + +/** + * 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 + exists(int part_end | + re.alternationOption(start, end, start, part_end) and + result.occursInRegex(re, start, part_end) + ) + or + i > 0 and + exists(int part_start, int part_end | + part_start = this.getChild(i - 1).getEnd() + 1 // allow for the | + | + re.alternationOption(start, end, part_start, part_end) and + result.occursInRegex(re, part_start, part_end) + ) + } + + 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 + this.getUnescaped() = "f" and result = 12.toUnicode() // form feed + or + this.getUnescaped() = "a" and result = 7.toUnicode() // alert/bell + or + this.getUnescaped() = "e" and result = 27.toUnicode() // escape (0x1B) + or + this.isUnicode() and + result = this.getUnicode() + } + + /** Holds if this terms name is given by the part following the escape character. */ + predicate isIdentityEscape() { not this.getUnescaped() in ["n", "r", "t", "f", "a", "e"] } + + override string getPrimaryQLClass() { result = "RegExpEscape" } + + /** Gets the part of the term following the escape character. That is e.g. "w" if the term is "\w". */ + private 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() { this.getText().matches(["\\u%", "\\x%"]) } + + /** + * Gets the unicode char for this escape. + * E.g. for `\u0061` this returns "a". + */ + private string getUnicode() { + exists(int codepoint | codepoint = sum(this.getHexValueFromUnicode(_)) | + result = codepoint.toUnicode() + ) + } + + /** Gets the part of this escape that is a hexidecimal string */ + private string getHexString() { + this.isUnicode() and + if this.getText().matches("\\u%") // \uhhhh + then result = this.getText().suffix(2) + else + if this.getText().matches("\\x{%") // \x{h..h} + then result = this.getText().substring(3, this.getText().length() - 1) + else result = this.getText().suffix(2) // \xhh + } + + /** + * 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) { + this.isUnicode() and + exists(string hex, string char | hex = this.getHexString() | + char = hex.charAt(index) and + result = 16.pow(hex.length() - index - 1) * toHex(char) + ) + } +} + +/** + * Gets the hex number for the `hex` char. + */ +private int toHex(string hex) { + result = [0 .. 9] and hex = result.toString() + 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 character that denotes multiple characters. + * + * Examples: + * + * ``` + * \w + * \S + * ``` + */ +class RegExpCharacterClassEscape extends RegExpEscape { + RegExpCharacterClassEscape() { + this.getValue() in ["d", "D", "s", "S", "w", "W", "h", "H", "v", "V"] or + this.getValue().charAt(0) in ["p", "P"] + } + + override RegExpTerm getChild(int i) { none() } + + override string getPrimaryQLClass() { result = "RegExpCharacterClassEscape" } +} + +/** + * A named character class in a regular expression. + * + * Examples: + * + * ``` + * \p{Digit} + * \p{IsLowerCase} + */ +class RegExpNamedProperty extends RegExpCharacterClassEscape { + boolean inverted; + string name; + + RegExpNamedProperty() { + name = this.getValue().substring(2, this.getValue().length() - 1) and + ( + inverted = false and + this.getValue().charAt(0) = "p" + or + inverted = true and + this.getValue().charAt(0) = "P" + ) + } + + /** Holds if this class is inverted. */ + predicate isInverted() { inverted = true } + + /** Gets the name of this class. */ + string getClassName() { result = name } + + /** + * Gets an equivalent single-chcracter escape sequence for this class (e.g. \d) if possible, excluding the escape character. + */ + string getBackslashEquivalent() { + exists(string eq | if inverted = true then result = eq.toUpperCase() else result = eq | + name = ["Digit", "IsDigit"] and + eq = "d" + or + name = ["Space", "IsWhite_Space"] and + eq = "s" + ) + } +} + +/** + * A character class in a regular expression. + * + * Examples: + * + * ``` + * [a-z_] + * [^<>&] + * ``` + */ +class RegExpCharacterClass extends RegExpTerm, TRegExpCharacterClass { + RegExpCharacterClass() { this = TRegExpCharacterClass(re, start, end) } + + /** Holds if this character class is inverted, matching the opposite of its content. */ + predicate isInverted() { re.getChar(start + 1) = "^" } + + /** Holds if this character class can match anything. */ + predicate isUniversalClass() { + // [^] + this.isInverted() and not exists(this.getAChild()) + or + // [\w\W] and similar + not this.isInverted() and + exists(string cce1, string cce2 | + cce1 = this.getAChild().(RegExpCharacterClassEscape).getValue() and + cce2 = this.getAChild().(RegExpCharacterClassEscape).getValue() + | + cce1 != cce2 and cce1.toLowerCase() = cce2.toLowerCase() + ) + } + + override RegExpTerm getChild(int i) { + i = 0 and + exists(int itemStart, int itemEnd | + re.charSetStart(start, itemStart) and + re.charSetChild(start, itemStart, itemEnd) and + result.occursInRegex(re, itemStart, itemEnd) + ) + or + i > 0 and + exists(int itemStart, int itemEnd | itemStart = this.getChild(i - 1).getEnd() | + result.occursInRegex(re, itemStart, itemEnd) and + re.charSetChild(start, itemStart, itemEnd) + ) + } + + 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) + } + + /** Holds if this range goes from `lo` to `hi`, in effect is `lo-hi`. */ + 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.occursInRegex(re, start, lower_end) + or + i = 1 and + result.occursInRegex(re, upper_start, end) + } + + override string getPrimaryQLClass() { result = "RegExpCharacterRange" } +} + +/** + * A normal character in a regular expression, that is, a character + * without special meaning. This includes escaped characters. + * It also includes escape sequences that represent character classes. + * + * Examples: + * ``` + * t + * \t + * ``` + */ +class RegExpNormalChar extends RegExpTerm, TRegExpNormalChar { + RegExpNormalChar() { this = TRegExpNormalChar(re, start, end) } + + /** + * Holds if this constant represents a valid Unicode character (as opposed + * to a surrogate code point that does not correspond to a character by itself.) + */ + predicate isCharacter() { any() } + + /** Gets the string representation of the char matched by this term. */ + string getValue() { result = re.getText().substring(start, end) } + + override RegExpTerm getChild(int i) { none() } + + override string getPrimaryQLClass() { result = "RegExpNormalChar" } +} + +/** + * A quoted sequence. + * + * Example: + * ``` + * \Qabc\E + * ``` + */ +class RegExpQuote extends RegExpTerm, TRegExpQuote { + string value; + + RegExpQuote() { + exists(int inner_start, int inner_end | + this = TRegExpQuote(re, start, end) and + re.quote(start, end, inner_start, inner_end) and + value = re.getText().substring(inner_start, inner_end) + ) + } + + /** Gets the string matched by this quote term. */ + string getValue() { result = value } + + override string getPrimaryQLClass() { result = "RegExpQuote" } +} + +/** + * A constant regular expression term, that is, a regular expression + * term matching a single string. This can be a single character or a quoted sequence. + * + * Example: + * + * ``` + * a + * ``` + */ +class RegExpConstant extends RegExpTerm { + string value; + + RegExpConstant() { + (value = this.(RegExpNormalChar).getValue() or value = this.(RegExpQuote).getValue()) and + not this instanceof RegExpCharacterClassEscape + } + + /** + * Holds if this constant represents a valid Unicode character (as opposed + * to a surrogate code point that does not correspond to a character by itself.) + */ + predicate isCharacter() { any() } + + /** Gets the string matched by this constant term. */ + string getValue() { result = value } + + override RegExpTerm getChild(int i) { none() } + + override string getPrimaryQLClass() { result = "RegExpConstant" } +} + +/** + * A grouped regular expression. + * + * Examples: + * + * ``` + * (ECMA|Java) + * (?:ECMA|Java) + * (?['"]) + * ``` + */ +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) } + + override RegExpTerm getChild(int i) { + i = 0 and + exists(int in_start, int in_end | re.groupContents(start, end, in_start, in_end) | + result.occursInRegex(re, in_start, in_end) + ) + } + + override string getPrimaryQLClass() { result = "RegExpGroup" } + + /** Holds if this is the `n`th numbered group of literal `lit`. */ + predicate isNumberedGroupOfLiteral(RegExpLiteral lit, int n) { + lit = this.getLiteral() and n = this.getNumber() + } + + /** Holds if this is a group with name `name` of literal `lit`. */ + predicate isNamedGroupOfLiteral(RegExpLiteral lit, string name) { + lit = this.getLiteral() and name = this.getName() + } +} + +/** + * 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) + } + + /** + * Holds if this constant represents a valid Unicode character (as opposed + * to a surrogate code point that does not correspond to a character by itself.) + */ + predicate isCharacter() { any() } + + /** Gets the char for this term. */ + 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 RegExpTerm getChild(int i) { none() } + + override string getPrimaryQLClass() { result = "RegExpZeroWidthMatch" } +} + +/** + * A zero-width lookahead or lookbehind assertion. + * + * Examples: + * + * ``` + * (?=\w) + * (?!\n) + * (?<=\.) + * (?` + * 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.isNumberedGroupOfLiteral(this.getLiteral(), this.getNumber()) + or + result.isNamedGroupOfLiteral(this.getLiteral(), 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(StringLiteral re) { result.getRegex() = re and result.isRootTerm() } diff --git a/java/ql/lib/semmle/code/java/regex/regex.qll b/java/ql/lib/semmle/code/java/regex/regex.qll new file mode 100644 index 00000000000..ff20b17b6fa --- /dev/null +++ b/java/ql/lib/semmle/code/java/regex/regex.qll @@ -0,0 +1,917 @@ +/** + * Definitions for parsing regular expressions. + */ + +import java +private import RegexFlowConfigs + +// In all ranges handled by this library, `start` is inclusive and `end` is exclusive. +/** + * A string literal that is used as a regular expression. + */ +abstract class RegexString extends StringLiteral { + /** Gets the text of this regex */ + string getText() { result = this.(StringLiteral).getValue() } + + /** Gets the `i`th character of this regex. */ + string getChar(int i) { result = this.getText().charAt(i) } + + /** Holds if the regex failed to parse. */ + predicate failedToParse(int i) { + exists(this.getChar(i)) and + not exists(int start, int end | + this.topLevel(start, end) and + start <= i and + end > i + ) + } + + /** + * Helper predicate for `escapingChar`. + * In order to avoid negative recursion, 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 + this.getChar(pos) = "\\" and + ( + if this.getChar(pos - 1) = "c" // in `\c\`, the latter `\` isn't escaping + then result = this.escaping(pos - 2).booleanNot() + else result = this.escaping(pos - 1).booleanNot() + ) + or + this.getChar(pos) != "\\" and result = false + } + + /** + * Helper predicate for `quote`. + * Holds if the char at `pos` could be the beginning of a quote delimiter, i.e. `\Q` (non-escaped) or `\E` (escaping not checked, as quote sequences turn off escapes). + * Result is `true` for `\Q` and `false` for `\E`. + */ + private boolean quoteDelimiter(int pos) { + result = true and + this.escaping(pos) = true and + this.getChar(pos + 1) = "Q" + or + result = false and + this.getChar(pos) = "\\" and + this.getChar(pos + 1) = "E" + } + + /** + * Helper predicate for `quote`. + * Holds if the char at `pos` is the one-based `index`th occurence of a quote delimiter (`\Q` or `\E`) + * Result is `true` for `\Q` and `false` for `\E`. + */ + private boolean quoteDelimiter(int index, int pos) { + result = this.quoteDelimiter(pos) and + pos = rank[index](int p | exists(this.quoteDelimiter(p))) + } + + /** Holds if a quoted sequence is found between `start` and `end` */ + predicate quote(int start, int end) { this.quote(start, end, _, _) } + + /** Holds if a quoted sequence is found between `start` and `end`, with content found between `inner_start` and `inner_end`. */ + predicate quote(int start, int end, int inner_start, int inner_end) { + exists(int index | + this.quoteDelimiter(index, start) = true and + ( + index = 1 + or + this.quoteDelimiter(index - 1, _) = false + ) and + inner_start = start + 2 and + inner_end = end - 2 and + inner_end = + min(int end_delimiter | + this.quoteDelimiter(end_delimiter) = false and end_delimiter > inner_start + ) + ) + } + + /** Holds if the character at `pos` is a "\" that is actually escaping what comes after. */ + predicate escapingChar(int pos) { + this.escaping(pos) = true and + not exists(int x, int y | this.quote(x, y) and pos in [x .. y - 1]) + } + + /** + * Holds if there is a control sequence, `\cx`, between `start` and `end`. + * `x` may be any ascii character including special characters. + */ + predicate controlEscape(int start, int end) { + this.escapingChar(start) and + this.getChar(start + 1) = "c" and + end = start + 3 + } + + private predicate namedBackreference(int start, int end, string name) { + this.escapingChar(start) and + this.getChar(start + 1) = "k" and + this.getChar(start + 2) = "<" and + end = min(int i | i > start + 2 and this.getChar(i) = ">") + 1 and + name = this.getText().substring(start + 3, end - 1) + } + + private predicate numberedBackreference(int start, int end, int value) { + this.escapingChar(start) and + // starting with 0 makes it an octal escape + not this.getChar(start + 1) = "0" and + exists(string text, string svalue, int len | + end = start + len and + text = this.getText() and + len in [2 .. 3] + | + svalue = text.substring(start + 1, start + len) and + value = svalue.toInt() and + // value is composed of digits + forall(int i | i in [start + 1 .. start + len - 1] | this.getChar(i) = [0 .. 9].toString()) and + // a longer reference is not possible + not ( + len = 2 and + exists(text.substring(start + 1, start + len + 1).toInt()) + ) and + // 3 octal digits makes it an octal escape + not forall(int i | i in [start + 1 .. start + 4] | this.isOctal(i)) + // TODO: Inside a character set, all numeric escapes are treated as characters. + ) + } + + /** Holds if the text in the range start,end is a back reference */ + predicate backreference(int start, int end) { + this.numberedBackreference(start, end, _) + or + this.namedBackreference(start, end, _) + } + + /** Gets the number of the back reference in start,end */ + int getBackrefNumber(int start, int end) { this.numberedBackreference(start, end, result) } + + /** Gets the name, if it has one, of the back reference in start,end */ + string getBackrefName(int start, int end) { this.namedBackreference(start, end, result) } + + pragma[inline] + private predicate isOctal(int index) { this.getChar(index) = [0 .. 7].toString() } + + /** An escape sequence that includes braces, such as named characters (\N{degree sign}), named classes (\p{Lower}), or hex values (\x{h..h}) */ + private predicate escapedBraces(int start, int end) { + this.escapingChar(start) and + this.getChar(start + 1) = ["N", "p", "P", "x"] and + this.getChar(start + 2) = "{" and + end = min(int i | start + 2 < i and this.getChar(i - 1) = "}") + } + + /** + * 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 this.backreference(start, _) and + ( + // hex value \xhh + this.getChar(start + 1) = "x" and + this.getChar(start + 2) != "{" and + end = start + 4 + or + // octal value \0o, \0oo, or \0ooo. Max of 0377. + this.getChar(start + 1) = "0" and + this.isOctal(start + 2) and + ( + if this.isOctal(start + 3) + then + if this.isOctal(start + 4) and this.getChar(start + 2) in ["0", "1", "2", "3"] + then end = start + 5 + else end = start + 4 + else end = start + 3 + ) + or + // 16-bit hex value \uhhhh + this.getChar(start + 1) = "u" and end = start + 6 + or + this.escapedBraces(start, end) + or + // Boundary matchers \b, \b{g} + this.getChar(start + 1) = "b" and + ( + if this.getText().substring(start + 2, start + 5) = "{g}" + then end = start + 5 + else end = start + 2 + ) + or + this.controlEscape(start, end) + or + // escape not handled above, update when adding a new case + not this.getChar(start + 1) in ["x", "0", "u", "p", "P", "N", "b", "c"] and + not exists(this.getChar(start + 1).toInt()) and + end = start + 2 + ) + } + + private string nonEscapedCharAt(int i) { + result = this.getChar(i) and + not exists(int x, int y | this.escapedCharacter(x, y) and i in [x .. y - 1]) and + not exists(int x, int y | this.quote(x, y) and i in [x .. y - 1]) + } + + /** Holds if a character set starts between `start` and `end`, including any negation character (`^`). */ + private predicate charSetStart0(int start, int end) { + this.nonEscapedCharAt(start) = "[" and + (if this.getChar(start + 1) = "^" then end = start + 2 else end = start + 1) + } + + /** Holds if the character at `pos` marks the end of a character class. */ + private predicate charSetEnd0(int pos) { + this.nonEscapedCharAt(pos) = "]" and + /* special case: `[]]` and `[^]]` are valid char classes. */ + not this.charSetStart0(_, pos) + } + + /** + * Holds if the character at `pos` starts a character set delimiter. + * Result is 1 for `[` and -1 for `]`. + */ + private int charSetDelimiter(int pos) { + result = 1 and this.charSetStart0(pos, _) + or + result = -1 and this.charSetEnd0(pos) + } + + /** + * Holds if the char at `pos` is the one-based `index`th occourence of a character set delimiter (`[` or `]`). + * Result is 1 for `[` and -1 for `]`. + */ + private int charSetDelimiter(int index, int pos) { + result = this.charSetDelimiter(pos) and + pos = rank[index](int p | exists(this.charSetDelimiter(p))) + } + + /** + * Gets the nesting depth of character classes after position `pos`, + * where `pos` is the position of a character set delimiter. + */ + private int charSetDepth(int index, int pos) { + index = 1 and result = 0.maximum(this.charSetDelimiter(index, pos)) + or + result = 0.maximum(this.charSetDelimiter(index, pos) + this.charSetDepth(index - 1, _)) + } + + /** Hold if a top-level character set starts between `start` and `end`. */ + predicate charSetStart(int start, int end) { + this.charSetStart0(start, end) and + this.charSetDepth(_, start) = 1 + } + + /** Holds if a top-level character set ends at `pos`. */ + predicate charSetEnd(int pos) { + this.charSetEnd0(pos) and + this.charSetDepth(_, pos) = 0 + } + + /** + * Holds if there is a top-level character class beginning at `start` (inclusive) and ending at `end` (exclusive) + * + * For now, nested character classes are approximated by only considering the top-level class for parsing. + * This leads to very similar results for ReDoS queries. + */ + predicate charSet(int start, int end) { + exists(int inner_start, int inner_end | this.charSetStart(start, inner_start) | + end = inner_end + 1 and + inner_end = + min(int end_delimiter | this.charSetEnd(end_delimiter) and end_delimiter > inner_start) + ) + } + + /** Either a char or a - */ + private predicate charSetToken(int charset_start, int start, int end) { + this.charSetStart(charset_start, start) and + ( + this.escapedCharacter(start, end) + or + exists(this.nonEscapedCharAt(start)) and end = start + 1 + or + this.quote(start, end) + ) + or + this.charSetToken(charset_start, _, start) and + ( + this.escapedCharacter(start, end) + or + exists(this.nonEscapedCharAt(start)) and + end = start + 1 and + not this.charSetEnd(start) + or + this.quote(start, end) + ) + } + + /** An indexed version of `charSetToken/3` */ + private predicate charSetToken(int charset_start, int index, int token_start, int token_end) { + token_start = rank[index](int start | this.charSetToken(charset_start, start, _) | start) and + this.charSetToken(charset_start, token_start, token_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.charSetToken(charset_start, index, _, _) and + ( + index in [1, 2] and result = false + or + index > 2 and + exists(int connector_start | + this.charSetToken(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.charSetToken(charset_start, index - 1, connector_start, _) and + this.nonEscapedCharAt(connector_start) = "-" + ) and + result = false + ) + } + + /** + * 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.charSetToken(charset_start, index - 2, start, lower_end) and + this.charSetToken(charset_start, index, upper_start, end) + ) + } + + /** + * Holds if the character set starting at `charset_start` contains either + * a character or a range found between `start` and `end`. + */ + predicate charSetChild(int charset_start, int start, int end) { + this.charSetToken(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 `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 + not this.charSet(_, start + 1) and + exists(string c | c = this.getChar(start) | + exists(int x, int y, int z | + this.charSet(x, z) and + this.charSetStart(x, y) + | + start = y + or + start = z - 2 + or + start > y and start < z - 2 and not this.charRange(_, _, start, end, _) + ) + or + not this.inCharSet(start) and + not c = "(" and + not c = "[" and + not c = ")" and + not c = "|" and + not c = "{" and + not exists(int qstart, int qend | this.quantifier(qstart, qend, _, _) | + qstart <= start and start < qend + ) + ) + } + + private predicate character(int start, int end) { + ( + this.simpleCharacter(start, end) and + not exists(int x, int y | this.escapedCharacter(x, y) and x <= start and y >= end) and + not exists(int x, int y | this.quote(x, y) and x <= start and y >= end) + or + this.escapedCharacter(start, end) + ) and + not exists(int x, int y | this.groupStart(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) + } + + /** Holds if a normal character or escape sequence is between `start` and `end`. */ + predicate normalCharacter(int start, int end) { + this.character(start, end) and + not this.specialCharacter(start, end, _) + } + + /** Holds if a special character `char` is between `start` and `end`. */ + predicate specialCharacter(int start, int end, string char) { + this.character(start, end) and + end = start + 1 and + char = this.getChar(start) and + (char = "$" or char = "^" or char = ".") and + not this.inCharSet(start) + } + + private predicate isGroupEnd(int i) { this.nonEscapedCharAt(i) = ")" and not this.inCharSet(i) } + + private predicate isGroupStart(int i) { this.nonEscapedCharAt(i) = "(" and not this.inCharSet(i) } + + /** Holds if an empty group is found between `start` and `end`. */ + predicate emptyGroup(int start, int end) { + exists(int endm1 | end = endm1 + 1 | + this.groupStart(start, endm1) and + this.isGroupEnd(endm1) + ) + } + + private predicate nonCapturingGroupStart(int start, int end) { + this.isGroupStart(start) and + this.getChar(start + 1) = "?" and + this.getChar(start + 2) = ":" and + end = start + 3 + } + + private predicate simpleGroupStart(int start, int end) { + this.isGroupStart(start) and + this.getChar(start + 1) != "?" and + end = start + 1 + } + + private predicate namedGroupStart(int start, int end) { + this.isGroupStart(start) and + this.getChar(start + 1) = "?" and + this.getChar(start + 2) = "<" and + not this.getChar(start + 3) = "=" and + not this.getChar(start + 3) = "!" and + exists(int name_end | + name_end = min(int i | i > start + 3 and this.getChar(i) = ">") and + end = name_end + 1 + ) + } + + private predicate flagGroupStart(int start, int end, string c) { + this.isGroupStart(start) and + this.getChar(start + 1) = "?" and + end = start + 3 and + c = this.getChar(start + 2) and + c in ["i", "m", "s", "u", "x", "U"] + } + + /** + * Gets the mode of this regular expression string if + * it is defined by a prefix. + */ + string getModeFromPrefix() { + exists(string c | this.flagGroupStart(_, _, c) | + c = "i" and result = "IGNORECASE" + or + c = "m" and result = "MULTILINE" + or + c = "s" and result = "DOTALL" + or + c = "u" and result = "UNICODE" + or + c = "x" and result = "VERBOSE" + or + c = "U" and result = "UNICODECLASS" + ) + } + + private predicate lookaheadAssertionStart(int start, int end) { + this.isGroupStart(start) and + this.getChar(start + 1) = "?" and + this.getChar(start + 2) = "=" and + end = start + 3 + } + + private predicate negativeLookaheadAssertionStart(int start, int end) { + this.isGroupStart(start) and + this.getChar(start + 1) = "?" and + this.getChar(start + 2) = "!" and + end = start + 3 + } + + private predicate lookbehindAssertionStart(int start, int end) { + this.isGroupStart(start) and + this.getChar(start + 1) = "?" and + this.getChar(start + 2) = "<" and + this.getChar(start + 3) = "=" and + end = start + 4 + } + + private predicate negativeLookbehindAssertionStart(int start, int end) { + this.isGroupStart(start) and + this.getChar(start + 1) = "?" and + this.getChar(start + 2) = "<" and + this.getChar(start + 3) = "!" and + end = start + 4 + } + + private predicate atomicGroupStart(int start, int end) { + this.isGroupStart(start) and + this.getChar(start + 1) = "?" and + this.getChar(start + 2) = ">" and + end = start + 3 + } + + private predicate groupStart(int start, int end) { + this.nonCapturingGroupStart(start, end) + or + this.flagGroupStart(start, end, _) + or + this.namedGroupStart(start, end) + or + this.lookaheadAssertionStart(start, end) + or + this.negativeLookaheadAssertionStart(start, end) + or + this.lookbehindAssertionStart(start, end) + or + this.negativeLookbehindAssertionStart(start, end) + or + this.atomicGroupStart(start, end) + or + this.simpleGroupStart(start, end) + } + + /** Holds if the text in the range start,end is a group with contents in the range in_start,in_end */ + predicate groupContents(int start, int end, int in_start, int in_end) { + this.groupStart(start, in_start) and + end = in_end + 1 and + this.topLevel(in_start, in_end) and + this.isGroupEnd(in_end) + } + + /** Holds if the text in the range start,end is a group */ + predicate group(int start, int end) { + this.groupContents(start, end, _, _) + or + this.emptyGroup(start, end) + } + + /** Gets the number of the group in start,end */ + int getGroupNumber(int start, int end) { + this.group(start, end) and + result = + count(int i | this.group(i, _) and i < start and not this.nonCapturingGroupStart(i, _)) + 1 + } + + /** Gets the name, if it has one, of the group in start,end */ + string getGroupName(int start, int end) { + this.group(start, end) and + exists(int name_end | + this.namedGroupStart(start, name_end) and + result = this.getText().substring(start + 3, name_end - 1) + ) + } + + /** Holds if a negative lookahead is found between `start` and `end` */ + predicate negativeLookaheadAssertionGroup(int start, int end) { + exists(int in_start | this.negativeLookaheadAssertionStart(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.negativeLookbehindAssertionStart(start, in_start) | + this.groupContents(start, end, in_start, _) + ) + } + + private predicate negativeAssertionGroup(int start, int end) { + exists(int in_start | + this.negativeLookaheadAssertionStart(start, in_start) + or + this.negativeLookbehindAssertionStart(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.lookaheadAssertionStart(start, in_start) | + this.groupContents(start, end, in_start, _) + ) + } + + /** Holds if a positive lookbehind is found between `start` and `end` */ + predicate positiveLookbehindAssertionGroup(int start, int end) { + exists(int in_start | this.lookbehindAssertionStart(start, in_start) | + this.groupContents(start, end, in_start, _) + ) + } + + /** Holds if the text in the range start, end is a group and can match the empty string. */ + predicate zeroWidthMatch(int start, int end) { + this.emptyGroup(start, end) + or + this.negativeAssertionGroup(start, end) + or + this.positiveLookaheadAssertionGroup(start, end) + or + this.positiveLookbehindAssertionGroup(start, end) + } + + private predicate baseItem(int start, int end) { + this.character(start, end) and + not exists(int x, int y | this.charSet(x, y) and x <= start and y >= end) + or + this.group(start, end) + or + this.charSet(start, end) + or + this.backreference(start, end) + or + this.quote(start, end) + } + + private predicate shortQuantifier( + int start, int end, boolean maybe_empty, boolean may_repeat_forever + ) { + ( + this.getChar(start) = "+" and maybe_empty = false and may_repeat_forever = true + or + this.getChar(start) = "*" and maybe_empty = true and may_repeat_forever = true + or + this.getChar(start) = "?" and maybe_empty = true and may_repeat_forever = false + ) and + end = start + 1 + or + 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) { + exists(string text, string match, string inner | + text = this.getText() and + end = start + match.length() and + inner = match.substring(1, match.length() - 1) + | + match = text.regexpFind("\\{[0-9]+\\}", _, start) and + lower = inner and + upper = lower + or + match = text.regexpFind("\\{[0-9]*,[0-9]*\\}", _, start) and + exists(int commaIndex | + commaIndex = inner.indexOf(",") and + lower = inner.prefix(commaIndex) and + upper = inner.suffix(commaIndex + 1) + ) + ) + } + + private predicate quantifier(int start, int end, boolean maybe_empty, boolean may_repeat_forever) { + this.shortQuantifier(start, end, maybe_empty, may_repeat_forever) and + not this.getChar(end) = ["?", "+"] + or + exists(int short_end | this.shortQuantifier(start, short_end, maybe_empty, may_repeat_forever) | + if this.getChar(short_end) = ["?", "+"] then end = short_end + 1 else end = short_end + ) + } + + /** + * Holds if a quantified part is found between `start` and `part_end` and the quantifier 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 quantifiedPart( + int start, int part_end, int end, boolean maybe_empty, boolean may_repeat_forever + ) { + this.baseItem(start, part_end) and + this.quantifier(part_end, end, maybe_empty, may_repeat_forever) + } + + /** + * Holds if the text in the range start,end is a quantified item, where item is a character, + * a character set or a group. + */ + predicate quantifiedItem(int start, int end, boolean maybe_empty, boolean may_repeat_forever) { + this.quantifiedPart(start, _, end, maybe_empty, may_repeat_forever) + } + + /** Holds if the range `start`, `end` contains a character, a quantifier, a character set or a group. */ + predicate item(int start, int end) { + this.quantifiedItem(start, end, _, _) + or + this.baseItem(start, end) and not this.quantifier(end, _, _, _) + } + + private predicate itemStart(int start) { + this.character(start, _) or + this.isGroupStart(start) or + this.charSet(start, _) or + this.backreference(start, _) or + this.quote(start, _) + } + + private predicate itemEnd(int end) { + this.character(_, end) + or + exists(int endm1 | this.isGroupEnd(endm1) and end = endm1 + 1) + or + this.charSet(_, end) + or + this.quantifier(_, end, _, _) + or + this.quote(_, end) + } + + private predicate isOptionDivider(int i) { this.nonEscapedCharAt(i) = "|" } + + private predicate subsequence(int start, int end) { + ( + start = 0 or + this.groupStart(_, start) or + this.isOptionDivider(start - 1) + ) and + this.item(start, end) + or + exists(int mid | + this.subsequence(start, mid) and + this.item(mid, end) + ) + } + + private predicate sequenceOrQuantified(int start, int end) { + this.subsequence(start, end) and + not this.itemStart(end) + } + + /** + * Holds if the text in the range start,end is a sequence of 1 or more items, where an item is a character, + * a character set or a group. + */ + predicate sequence(int start, int end) { + this.sequenceOrQuantified(start, end) and + not this.quantifiedItem(start, end, _, _) + } + + private predicate subalternation(int start, int end, int itemStart) { + this.sequenceOrQuantified(start, end) and + not this.isOptionDivider(start - 1) and + itemStart = start + or + start = end and + not this.itemEnd(start) and + this.isOptionDivider(end) and + itemStart = start + or + exists(int mid | + this.subalternation(start, mid, _) and + this.isOptionDivider(mid) and + itemStart = mid + 1 + | + this.sequenceOrQuantified(itemStart, end) + or + not this.itemStart(end) and end = itemStart + ) + } + + private predicate topLevel(int start, int end) { + not this.inCharSet(start) and + this.subalternation(start, end, _) and + not this.isOptionDivider(end) + } + + /** + * Holds if the text in the range start,end is an alternation + */ + predicate alternation(int start, int end) { + this.topLevel(start, end) and + exists(int less | this.subalternation(start, less, _) and less < end) + } + + /** + * Holds if the text in the range start,end is an alternation and the text in part_start, part_end is one of the + * options in that alternation. + */ + predicate alternationOption(int start, int end, int part_start, int part_end) { + this.alternation(start, end) and + this.subalternation(start, part_end, part_start) + } + + /** + * Gets the `i`th character of this literal as it was written in the source code. + */ + string getSourceChar(int i) { result = this.(StringLiteral).getLiteral().charAt(i) } + + /** + * Helper predicate for `sourceEscapingChar` that + * results in a boolean in order to avoid negative recursion. + */ + private boolean sourceEscaping(int pos) { + pos = -1 and result = false + or + this.getSourceChar(pos) = "\\" and + result = this.sourceEscaping(pos - 1).booleanNot() + or + this.getSourceChar(pos) != "\\" and result = false + } + + /** + * Equivalent of `escapingChar` for the literal source rather than the string value. + * Holds if the character at position `pos` in the source literal is a '\' that is + * actually escaping what comes after it. + */ + private predicate sourceEcapingChar(int pos) { this.sourceEscaping(pos) = true } + + /** + * Holds if an escaped character exists between `start` and `end` in the source iteral. + */ + private predicate sourceEscapedCharacter(int start, int end) { + this.sourceEcapingChar(start) and + (if this.getSourceChar(start + 1) = "u" then end = start + 6 else end = start + 2) + } + + private predicate sourceNonEscapedCharacter(int i) { + exists(this.getSourceChar(i)) and + not exists(int x, int y | this.sourceEscapedCharacter(x, y) and i in [x .. y - 1]) + } + + /** + * Holds if a character is represented between `start` and `end` in the source literal. + */ + private predicate sourceCharacter(int start, int end) { + this.sourceEscapedCharacter(start, end) + or + this.sourceNonEscapedCharacter(start) and + end = start + 1 + } + + /** + * Holds if the `i`th character of the string is represented between offsets + * `start` (inclusive) and `end` (exclusive) in the source code of this literal. + * This only gives correct results if the literal is written as a normal single-line string literal; + * without compile-time concatenation involved. + */ + predicate sourceCharacter(int pos, int start, int end) { + exists(this.getChar(pos)) and + this.sourceCharacter(start, end) and + start = rank[pos + 2](int s | this.sourceCharacter(s, _)) + } +} + +/** A string literal used as a regular expression */ +class Regex extends RegexString { + boolean matches_full_string; + + Regex() { usedAsRegex(this, _, matches_full_string) } + + /** + * Gets a mode (if any) of this regular expression. Can be any of: + * DEBUG + * IGNORECASE + * MULTILINE + * DOTALL + * UNICODE + * VERBOSE + * UNICODECLASS + */ + string getAMode() { + result != "None" and + usedAsRegex(this, result, _) + or + result = this.getModeFromPrefix() + } + + /** + * Holds if this regex is used to match against a full string, + * as though it was implicitly surrounded by ^ and $. + */ + predicate matchesFullString() { matches_full_string = true } +} diff --git a/java/ql/lib/semmle/code/java/security/performance/ExponentialBackTracking.qll b/java/ql/lib/semmle/code/java/security/performance/ExponentialBackTracking.qll new file mode 100644 index 00000000000..5e0fe18ea00 --- /dev/null +++ b/java/ql/lib/semmle/code/java/security/performance/ExponentialBackTracking.qll @@ -0,0 +1,371 @@ +/** + * 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] +private predicate stateInsideBacktracking(State s) { + s.getRepr().getParent*() instanceof MaybeBacktrackingRepetition +} + +/** + * A infinitely repeating quantifier that might backtrack. + */ +private class MaybeBacktrackingRepetition extends InfiniteRepetitionQuantifier { + MaybeBacktrackingRepetition() { + exists(RegExpTerm child | + child instanceof RegExpAlt or + child instanceof RegExpQuantifier + | + child.getParent+() = this + ) + } +} + +/** + * A state in the product automaton. + */ +private 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. + */ +private 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. + */ +private 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` + */ +private predicate isStatePair(StatePair p) { any() } + +/** + * Holds if there are transitions from the components of `q` to the corresponding + * components of `r`. + * + * Used in `statePairDist` + */ +private predicate delta2(StatePair q, StatePair r) { step(q, _, _, r) } + +/** + * Gets the minimum length of a path from `q` to `r` in the + * product automaton. + */ +private 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] +private 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. + */ +private 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. + */ +private 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] +private 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. + */ +private 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 + ")" + ) + } +} + +/** + * 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. + */ +private 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. + */ +private StatePair getAForkPair(State fork) { + isFork(fork, _, _, _, _) and + result = MkStatePair(epsilonPred*(fork), epsilonPred*(fork)) +} + +private predicate hasSuffix(Trace suffix, Trace t, int i) { + // Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the + // recursive case, so instead we check it explicitly here. + t instanceof RelevantTrace and + i = 0 and + suffix = t + or + hasSuffix(Step(_, _, suffix), t, i - 1) +} + +pragma[noinline] +private predicate hasTuple(InputSymbol s1, InputSymbol s2, Trace t, int i) { + hasSuffix(Step(s1, s2, _), t, i) +} + +private class RelevantTrace extends Trace, Step { + RelevantTrace() { + exists(State fork, StatePair q | + isReachableFromFork(fork, q, this, _) and + q = getAForkPair(fork) + ) + } + + pragma[noinline] + private string intersect(int i) { + exists(InputSymbol s1, InputSymbol s2 | + hasTuple(s1, s2, this, i) and + result = intersect(s1, s2) + ) + } + + /** Gets a string corresponding to this trace. */ + // the pragma is needed for the case where `intersect(s1, s2)` has multiple values, + // not for recursion + language[monotonicAggregates] + string concretise() { + result = strictconcat(int i | hasTuple(_, _, this, i) | this.intersect(i) order by i desc) + } +} + +/** + * Holds if `fork` is a pumpable fork with word `w`. + */ +private predicate isPumpable(State fork, string w) { + exists(StatePair q, RelevantTrace t | + isReachableFromFork(fork, q, t, _) and + q = getAForkPair(fork) and + w = t.concretise() + ) +} + +/** + * An instantiation of `ReDoSConfiguration` for exponential backtracking. + */ +class ExponentialReDoSConfiguration extends ReDoSConfiguration { + ExponentialReDoSConfiguration() { this = "ExponentialReDoSConfiguration" } + + override predicate isReDoSCandidate(State state, string pump) { isPumpable(state, pump) } +} diff --git a/java/ql/lib/semmle/code/java/security/performance/PolynomialReDoSQuery.qll b/java/ql/lib/semmle/code/java/security/performance/PolynomialReDoSQuery.qll new file mode 100644 index 00000000000..2a33e15c74a --- /dev/null +++ b/java/ql/lib/semmle/code/java/security/performance/PolynomialReDoSQuery.qll @@ -0,0 +1,56 @@ +/** Definitions and configurations for the Polynomial ReDoS query */ + +import semmle.code.java.security.performance.SuperlinearBackTracking +import semmle.code.java.dataflow.DataFlow +import semmle.code.java.regex.RegexTreeView +import semmle.code.java.regex.RegexFlowConfigs +import semmle.code.java.dataflow.FlowSources + +/** A sink for polynomial redos queries, where a regex is matched. */ +class PolynomialRedosSink extends DataFlow::Node { + RegExpLiteral reg; + + PolynomialRedosSink() { regexMatchedAgainst(reg.getRegex(), this.asExpr()) } + + /** Gets the regex that is matched against this node. */ + RegExpTerm getRegExp() { result.getParent() = reg } +} + +/** + * A method whose result typically has a limited length, + * such as HTTP headers, and values derrived from them. + */ +private class LengthRestrictedMethod extends Method { + LengthRestrictedMethod() { + this.getName().toLowerCase().matches(["%header%", "%requesturi%", "%requesturl%", "%cookie%"]) + or + this.getDeclaringType().getName().toLowerCase().matches("%cookie%") and + this.getName().matches("get%") + or + this.getDeclaringType().getName().toLowerCase().matches("%request%") and + this.getName().toLowerCase().matches(["%get%path%", "get%user%", "%querystring%"]) + } +} + +/** A configuration for Polynomial ReDoS queries. */ +class PolynomialRedosConfig extends TaintTracking::Configuration { + PolynomialRedosConfig() { this = "PolynomialRedosConfig" } + + override predicate isSource(DataFlow::Node src) { src instanceof RemoteFlowSource } + + override predicate isSink(DataFlow::Node sink) { sink instanceof PolynomialRedosSink } + + override predicate isSanitizer(DataFlow::Node node) { + node.getType() instanceof PrimitiveType or + node.getType() instanceof BoxedType or + node.asExpr().(MethodAccess).getMethod() instanceof LengthRestrictedMethod + } +} + +/** Holds if there is flow from `source` to `sink` that is matched against the regexp term `regexp` that is vulnerable to Polynomial ReDoS. */ +predicate hasPolynomialReDoSResult( + DataFlow::PathNode source, DataFlow::PathNode sink, PolynomialBackTrackingTerm regexp +) { + any(PolynomialRedosConfig config).hasFlowPath(source, sink) and + regexp.getRootTerm() = sink.getNode().(PolynomialRedosSink).getRegExp() +} diff --git a/java/ql/lib/semmle/code/java/security/performance/ReDoSUtil.qll b/java/ql/lib/semmle/code/java/security/performance/ReDoSUtil.qll new file mode 100644 index 00000000000..8aa348bf62f --- /dev/null +++ b/java/ql/lib/semmle/code/java/security/performance/ReDoSUtil.qll @@ -0,0 +1,1198 @@ +/** + * Provides classes for working with regular expressions that can + * perform backtracking in superlinear/exponential time. + * + * This module contains a number of utility predicates for compiling a regular expression into a NFA and reasoning about this NFA. + * + * The `ReDoSConfiguration` contains a `isReDoSCandidate` predicate that is used to + * to determine which states the prefix/suffix search should happen on. + * There is only meant to exist one `ReDoSConfiguration` at a time. + * + * The predicate `hasReDoSResult` outputs a de-duplicated set of + * states that will cause backtracking (a rejecting suffix exists). + */ + +import ReDoSUtilSpecific + +/** + * A configuration for which parts of a regular expression should be considered relevant for + * the different predicates in `ReDoS.qll`. + * Used to adjust the computations for either superlinear or exponential backtracking. + */ +abstract class ReDoSConfiguration extends string { + bindingset[this] + ReDoSConfiguration() { any() } + + /** + * Holds if `state` with the pump string `pump` is a candidate for a + * ReDoS vulnerable state. + * This is used to determine which states are considered for the prefix/suffix construction. + */ + abstract predicate isReDoSCandidate(State state, string pump); +} + +/** + * Holds if repeating `pump` starting at `state` is a candidate for causing backtracking. + * No check whether a rejected suffix exists has been made. + */ +private predicate isReDoSCandidate(State state, string pump) { + any(ReDoSConfiguration conf).isReDoSCandidate(state, pump) and + ( + not any(ReDoSConfiguration conf).isReDoSCandidate(epsilonSucc+(state), _) + or + epsilonSucc+(state) = state and + state = + max(State s, Location l | + s = epsilonSucc+(state) and + l = s.getRepr().getLocation() and + any(ReDoSConfiguration conf).isReDoSCandidate(s, _) and + s.getRepr() instanceof InfiniteRepetitionQuantifier + | + s order by l.getStartLine(), l.getStartColumn(), l.getEndColumn(), l.getEndLine() + ) + ) +} + +/** + * Gets the char after `c` (from a simplified ASCII table). + */ +private string nextChar(string c) { exists(int code | code = ascii(c) | code + 1 = ascii(result)) } + +/** + * Gets an approximation for the ASCII code for `char`. + * Only the easily printable chars are included (so no newline, tab, null, etc). + */ +private int ascii(string char) { + char = + rank[result](string c | + c = + "! \"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\\]^_`abcdefghijklmnopqrstuvwxyz{|}~" + .charAt(_) + ) +} + +/** + * 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. + */ +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)) +} + +/** + * A lookahead/lookbehind that matches the empty string. + */ +class EmptyPositiveSubPatttern extends RegExpSubPattern { + EmptyPositiveSubPatttern() { + ( + this instanceof RegExpPositiveLookahead + or + this instanceof RegExpPositiveLookbehind + ) and + matchesEpsilon(this.getOperand()) + } +} + +/** + * A branch in a disjunction that is the root node in a literal, or a literal + * whose root node is not a disjunction. + */ +class RegExpRoot extends RegExpTerm { + RegExpRoot() { + exists(RegExpParent parent | + exists(RegExpAlt alt | + alt.isRootTerm() and + this = alt.getAChild() and + parent = alt.getParent() + ) + or + this.isRootTerm() and + not this instanceof RegExpAlt and + parent = this.getParent() + ) + } + + /** + * Holds if this root term is relevant to the ReDoS analysis. + */ + predicate isRelevant() { + // there is at least one repetition + getRoot(any(InfiniteRepetitionQuantifier q)) = this and + // is actually used as a RegExp + this.isUsedAsRegExp() and + // not excluded for library specific reasons + not isExcluded(this.getRootTerm().getParent()) + } +} + +/** + * A constant in a regular expression that represents valid Unicode character(s). + */ +private class RegexpCharacterConstant extends RegExpConstant { + RegexpCharacterConstant() { this.isCharacter() } +} + +/** + * A regexp term that is relevant for this ReDoS analysis. + */ +class RelevantRegExpTerm extends RegExpTerm { + RelevantRegExpTerm() { getRoot(this).isRelevant() } +} + +/** + * Holds if `term` is the chosen canonical representative for all terms with string representation `str`. + * The string representation includes which flags are used with the regular expression. + * + * Using canonical representatives gives a huge performance boost when working with tuples containing multiple `InputSymbol`s. + * The number of `InputSymbol`s is decreased by 3 orders of magnitude or more in some larger benchmarks. + */ +private predicate isCanonicalTerm(RelevantRegExpTerm term, string str) { + term = + min(RelevantRegExpTerm t, Location loc, File file | + loc = t.getLocation() and + file = t.getFile() and + str = t.getRawValue() + "|" + getCanonicalizationFlags(t.getRootTerm()) + | + t order by t.getFile().getRelativePath(), loc.getStartLine(), loc.getStartColumn() + ) +} + +/** + * Gets a string reperesentation of the flags used with the regular expression. + * Only the flags that are relevant for the canonicalization are included. + */ +string getCanonicalizationFlags(RegExpTerm root) { + root.isRootTerm() and + (if RegExpFlags::isIgnoreCase(root) then result = "i" else result = "") +} + +/** + * An abstract input symbol, representing a set of concrete characters. + */ +private newtype TInputSymbol = + /** An input symbol corresponding to character `c`. */ + Char(string c) { + c = + any(RegexpCharacterConstant cc | + cc instanceof RelevantRegExpTerm and + not RegExpFlags::isIgnoreCase(cc.getRootTerm()) + ).getValue().charAt(_) + or + // normalize everything to lower case if the regexp is case insensitive + c = + any(RegexpCharacterConstant cc, string char | + cc instanceof RelevantRegExpTerm and + RegExpFlags::isIgnoreCase(cc.getRootTerm()) and + char = cc.getValue().charAt(_) + | + char.toLowerCase() + ) + } or + /** + * An input symbol representing all characters matched by + * a (non-universal) character class that has string representation `charClassString`. + */ + CharClass(string charClassString) { + exists(RelevantRegExpTerm recc | isCanonicalTerm(recc, charClassString) | + recc instanceof RegExpCharacterClass and + not recc.(RegExpCharacterClass).isUniversalClass() + or + isEscapeClass(recc, _) + ) + } or + /** An input symbol representing all characters matched by `.`. */ + Dot() or + /** An input symbol representing all characters. */ + Any() or + /** An epsilon transition in the automaton. */ + Epsilon() + +/** + * Gets the canonical CharClass for `term`. + */ +CharClass getCanonicalCharClass(RegExpTerm term) { + exists(string str | isCanonicalTerm(term, str) | result = CharClass(str)) +} + +/** + * Holds if `a` and `b` are input symbols from the same regexp. + */ +private predicate sharesRoot(TInputSymbol a, TInputSymbol b) { + exists(RegExpRoot root | + belongsTo(a, root) and + belongsTo(b, root) + ) +} + +/** + * Holds if the `a` is an input symbol from a regexp that has root `root`. + */ +private predicate belongsTo(TInputSymbol a, RegExpRoot root) { + exists(State s | getRoot(s.getRepr()) = root | + delta(s, a, _) + or + delta(_, a, s) + ) +} + +/** + * An abstract input symbol, representing a set of concrete characters. + */ +class InputSymbol extends TInputSymbol { + InputSymbol() { not this instanceof Epsilon } + + /** + * Gets a string representation of this input symbol. + */ + string toString() { + this = Char(result) + or + this = CharClass(result) + or + this = Dot() and result = "." + or + this = Any() and result = "[^]" + } +} + +/** + * An abstract input symbol that represents a character class. + */ +abstract class CharacterClass extends InputSymbol { + /** + * Gets a character that is relevant for intersection-tests involving this + * character class. + * + * Specifically, this is any of the characters mentioned explicitly in the + * character class, offset by one if it is inverted. For character class escapes, + * the result is as if the class had been written out as a series of intervals. + * + * This set is large enough to ensure that for any two intersecting character + * classes, one contains a relevant character from the other. + */ + abstract string getARelevantChar(); + + /** + * Holds if this character class matches `char`. + */ + bindingset[char] + abstract predicate matches(string char); + + /** + * Gets a character matched by this character class. + */ + string choose() { result = this.getARelevantChar() and this.matches(result) } +} + +/** + * Provides implementations for `CharacterClass`. + */ +private module CharacterClasses { + /** + * Holds if the character class `cc` has a child (constant or range) that matches `char`. + */ + pragma[noinline] + predicate hasChildThatMatches(RegExpCharacterClass cc, string char) { + if RegExpFlags::isIgnoreCase(cc.getRootTerm()) + then + // normalize everything to lower case if the regexp is case insensitive + exists(string c | hasChildThatMatchesIgnoringCasingFlags(cc, c) | char = c.toLowerCase()) + else hasChildThatMatchesIgnoringCasingFlags(cc, char) + } + + /** + * Holds if the character class `cc` has a child (constant or range) that matches `char`. + * Ignores whether the character class is inside a regular expression that has the ignore case flag. + */ + pragma[noinline] + predicate hasChildThatMatchesIgnoringCasingFlags(RegExpCharacterClass cc, string char) { + exists(getCanonicalCharClass(cc)) and + exists(RegExpTerm child | child = cc.getAChild() | + char = child.(RegexpCharacterConstant).getValue() + or + rangeMatchesOnLetterOrDigits(child, char) + or + not rangeMatchesOnLetterOrDigits(child, _) and + char = getARelevantChar() and + exists(string lo, string hi | child.(RegExpCharacterRange).isRange(lo, hi) | + lo <= char and + char <= hi + ) + or + exists(string charClass | isEscapeClass(child, charClass) | + charClass.toLowerCase() = charClass and + classEscapeMatches(charClass, char) + or + char = getARelevantChar() and + charClass.toUpperCase() = charClass and + not classEscapeMatches(charClass, char) + ) + ) + } + + /** + * Holds if `range` is a range on lower-case, upper-case, or digits, and matches `char`. + * This predicate is used to restrict the searchspace for ranges by only joining `getAnyPossiblyMatchedChar` + * on a few ranges. + */ + private predicate rangeMatchesOnLetterOrDigits(RegExpCharacterRange range, string char) { + exists(string lo, string hi | + range.isRange(lo, hi) and lo = lowercaseLetter() and hi = lowercaseLetter() + | + lo <= char and + char <= hi and + char = lowercaseLetter() + ) + or + exists(string lo, string hi | + range.isRange(lo, hi) and lo = upperCaseLetter() and hi = upperCaseLetter() + | + lo <= char and + char <= hi and + char = upperCaseLetter() + ) + or + exists(string lo, string hi | range.isRange(lo, hi) and lo = digit() and hi = digit() | + lo <= char and + char <= hi and + char = digit() + ) + } + + private string lowercaseLetter() { result = "abdcefghijklmnopqrstuvwxyz".charAt(_) } + + private string upperCaseLetter() { result = "ABCDEFGHIJKLMNOPQRSTUVWXYZ".charAt(_) } + + private string digit() { result = [0 .. 9].toString() } + + /** + * Gets a char that could be matched by a regular expression. + * Includes all printable ascii chars, all constants mentioned in a regexp, and all chars matches by the regexp `/\s|\d|\w/`. + */ + string getARelevantChar() { + exists(ascii(result)) + or + exists(RegexpCharacterConstant c | result = c.getValue().charAt(_)) + or + classEscapeMatches(_, result) + } + + /** + * Gets a char that is mentioned in the character class `c`. + */ + private string getAMentionedChar(RegExpCharacterClass c) { + exists(RegExpTerm child | child = c.getAChild() | + result = child.(RegexpCharacterConstant).getValue() + or + child.(RegExpCharacterRange).isRange(result, _) + or + child.(RegExpCharacterRange).isRange(_, result) + or + exists(string charClass | isEscapeClass(child, charClass) | + result = min(string s | classEscapeMatches(charClass.toLowerCase(), s)) + or + result = max(string s | classEscapeMatches(charClass.toLowerCase(), s)) + ) + ) + } + + /** + * An implementation of `CharacterClass` for positive (non inverted) character classes. + */ + private class PositiveCharacterClass extends CharacterClass { + RegExpCharacterClass cc; + + PositiveCharacterClass() { this = getCanonicalCharClass(cc) and not cc.isInverted() } + + override string getARelevantChar() { result = getAMentionedChar(cc) } + + override predicate matches(string char) { hasChildThatMatches(cc, char) } + } + + /** + * An implementation of `CharacterClass` for inverted character classes. + */ + private class InvertedCharacterClass extends CharacterClass { + RegExpCharacterClass cc; + + InvertedCharacterClass() { this = getCanonicalCharClass(cc) and cc.isInverted() } + + override string getARelevantChar() { + result = nextChar(getAMentionedChar(cc)) or + nextChar(result) = getAMentionedChar(cc) + } + + bindingset[char] + override predicate matches(string char) { not hasChildThatMatches(cc, char) } + } + + /** + * Holds if the character class escape `clazz` (\d, \s, or \w) matches `char`. + */ + pragma[noinline] + private predicate classEscapeMatches(string clazz, string char) { + clazz = "d" and + char = "0123456789".charAt(_) + or + clazz = "s" and + char = [" ", "\t", "\r", "\n", 11.toUnicode(), 12.toUnicode()] // 11.toUnicode() = \v, 12.toUnicode() = \f + or + clazz = "w" and + char = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789_".charAt(_) + } + + /** + * An implementation of `CharacterClass` for \d, \s, and \w. + */ + private class PositiveCharacterClassEscape extends CharacterClass { + string charClass; + + PositiveCharacterClassEscape() { + exists(RegExpTerm cc | + isEscapeClass(cc, charClass) and + this = getCanonicalCharClass(cc) and + charClass = ["d", "s", "w"] + ) + } + + override string getARelevantChar() { + charClass = "d" and + result = ["0", "9"] + or + charClass = "s" and + result = " " + or + charClass = "w" and + result = ["a", "Z", "_", "0", "9"] + } + + override predicate matches(string char) { classEscapeMatches(charClass, char) } + + override string choose() { + charClass = "d" and + result = "9" + or + charClass = "s" and + result = " " + or + charClass = "w" and + result = "a" + } + } + + /** + * An implementation of `CharacterClass` for \D, \S, and \W. + */ + private class NegativeCharacterClassEscape extends CharacterClass { + string charClass; + + NegativeCharacterClassEscape() { + exists(RegExpTerm cc | + isEscapeClass(cc, charClass) and + this = getCanonicalCharClass(cc) and + charClass = ["D", "S", "W"] + ) + } + + override string getARelevantChar() { + charClass = "D" and + result = ["a", "Z", "!"] + or + charClass = "S" and + result = ["a", "9", "!"] + or + charClass = "W" and + result = [" ", "!"] + } + + bindingset[char] + override predicate matches(string char) { + not classEscapeMatches(charClass.toLowerCase(), char) + } + } +} + +private class EdgeLabel extends TInputSymbol { + string toString() { + this = Epsilon() and result = "" + or + exists(InputSymbol s | this = s and result = s.toString()) + } +} + +/** + * A RegExp term that acts like a plus. + * Either it's a RegExpPlus, or it is a range {1,X} where X is >= 30. + * 30 has been chosen as a threshold because for exponential blowup 2^30 is enough to get a decent DOS attack. + */ +private class EffectivelyPlus extends RegExpTerm { + EffectivelyPlus() { + this instanceof RegExpPlus + or + exists(RegExpRange range | + range.getLowerBound() = 1 and + (range.getUpperBound() >= 30 or not exists(range.getUpperBound())) + | + this = range + ) + } +} + +/** + * A RegExp term that acts like a star. + * Either it's a RegExpStar, or it is a range {0,X} where X is >= 30. + */ +private class EffectivelyStar extends RegExpTerm { + EffectivelyStar() { + this instanceof RegExpStar + or + exists(RegExpRange range | + range.getLowerBound() = 0 and + (range.getUpperBound() >= 30 or not exists(range.getUpperBound())) + | + this = range + ) + } +} + +/** + * A RegExp term that acts like a question mark. + * Either it's a RegExpQuestion, or it is a range {0,1}. + */ +private class EffectivelyQuestion extends RegExpTerm { + EffectivelyQuestion() { + this instanceof RegExpOpt + or + exists(RegExpRange range | range.getLowerBound() = 0 and range.getUpperBound() = 1 | + this = range + ) + } +} + +/** + * Gets the state before matching `t`. + */ +pragma[inline] +private State before(RegExpTerm t) { result = Match(t, 0) } + +/** + * Gets a state the NFA may be in after matching `t`. + */ +State after(RegExpTerm t) { + exists(RegExpAlt alt | t = alt.getAChild() | result = after(alt)) + or + exists(RegExpSequence seq, int i | t = seq.getChild(i) | + result = before(seq.getChild(i + 1)) + or + i + 1 = seq.getNumChild() and result = after(seq) + ) + or + exists(RegExpGroup grp | t = grp.getAChild() | result = after(grp)) + or + exists(EffectivelyStar star | t = star.getAChild() | + not isPossessive(star) and + result = before(star) + ) + or + exists(EffectivelyPlus plus | t = plus.getAChild() | + not isPossessive(plus) and + result = before(plus) + or + result = after(plus) + ) + or + exists(EffectivelyQuestion opt | t = opt.getAChild() | result = after(opt)) + or + exists(RegExpRoot root | t = root | + if matchesAnySuffix(root) then result = AcceptAnySuffix(root) else result = Accept(root) + ) +} + +/** + * Holds if the NFA has a transition from `q1` to `q2` labelled with `lbl`. + */ +predicate delta(State q1, EdgeLabel lbl, State q2) { + exists(RegexpCharacterConstant s, int i | + q1 = Match(s, i) and + ( + not RegExpFlags::isIgnoreCase(s.getRootTerm()) and + lbl = Char(s.getValue().charAt(i)) + or + // normalize everything to lower case if the regexp is case insensitive + RegExpFlags::isIgnoreCase(s.getRootTerm()) and + exists(string c | c = s.getValue().charAt(i) | lbl = Char(c.toLowerCase())) + ) and + ( + q2 = Match(s, i + 1) + or + s.getValue().length() = i + 1 and + q2 = after(s) + ) + ) + or + exists(RegExpDot dot | q1 = before(dot) and q2 = after(dot) | + if RegExpFlags::isDotAll(dot.getRootTerm()) then lbl = Any() else lbl = Dot() + ) + or + exists(RegExpCharacterClass cc | + cc.isUniversalClass() and q1 = before(cc) and lbl = Any() and q2 = after(cc) + or + q1 = before(cc) and + lbl = CharClass(cc.getRawValue() + "|" + getCanonicalizationFlags(cc.getRootTerm())) and + q2 = after(cc) + ) + or + exists(RegExpTerm cc | isEscapeClass(cc, _) | + q1 = before(cc) and + lbl = CharClass(cc.getRawValue() + "|" + getCanonicalizationFlags(cc.getRootTerm())) and + q2 = after(cc) + ) + or + exists(RegExpAlt alt | lbl = Epsilon() | q1 = before(alt) and q2 = before(alt.getAChild())) + or + exists(RegExpSequence seq | lbl = Epsilon() | q1 = before(seq) and q2 = before(seq.getChild(0))) + or + exists(RegExpGroup grp | lbl = Epsilon() | q1 = before(grp) and q2 = before(grp.getChild(0))) + or + exists(EffectivelyStar star | lbl = Epsilon() | + q1 = before(star) and q2 = before(star.getChild(0)) + or + q1 = before(star) and q2 = after(star) + ) + or + exists(EffectivelyPlus plus | lbl = Epsilon() | + q1 = before(plus) and q2 = before(plus.getChild(0)) + ) + or + exists(EffectivelyQuestion opt | lbl = Epsilon() | + q1 = before(opt) and q2 = before(opt.getChild(0)) + or + q1 = before(opt) and q2 = after(opt) + ) + or + exists(RegExpRoot root | q1 = AcceptAnySuffix(root) | + lbl = Any() and q2 = q1 + or + lbl = Epsilon() and q2 = Accept(root) + ) + or + exists(RegExpRoot root | q1 = Match(root, 0) | matchesAnyPrefix(root) and lbl = Any() and q2 = q1) + or + exists(RegExpDollar dollar | q1 = before(dollar) | + lbl = Epsilon() and q2 = Accept(getRoot(dollar)) + ) + or + exists(EmptyPositiveSubPatttern empty | q1 = before(empty) | + lbl = Epsilon() and q2 = after(empty) + ) +} + +/** + * Gets a state that `q` has an epsilon transition to. + */ +State epsilonSucc(State q) { delta(q, Epsilon(), result) } + +/** + * Gets a state that has an epsilon transition to `q`. + */ +State epsilonPred(State q) { q = epsilonSucc(result) } + +/** + * Holds if there is a state `q` that can be reached from `q1` + * along epsilon edges, such that there is a transition from + * `q` to `q2` that consumes symbol `s`. + */ +predicate deltaClosed(State q1, InputSymbol s, State q2) { delta(epsilonSucc*(q1), s, q2) } + +/** + * Gets the root containing the given term, that is, the root of the literal, + * or a branch of the root disjunction. + */ +RegExpRoot getRoot(RegExpTerm term) { + result = term or + result = getRoot(term.getParent()) +} + +/** + * A state in the NFA. + */ +newtype TState = + /** + * A state representing that the NFA is about to match a term. + * `i` is used to index into multi-char literals. + */ + Match(RelevantRegExpTerm t, int i) { + i = 0 + or + exists(t.(RegexpCharacterConstant).getValue().charAt(i)) + } or + /** + * An accept state, where exactly the given input string is accepted. + */ + Accept(RegExpRoot l) { l.isRelevant() } or + /** + * An accept state, where the given input string, or any string that has this + * string as a prefix, is accepted. + */ + AcceptAnySuffix(RegExpRoot l) { l.isRelevant() } + +/** + * Gets a state that is about to match the regular expression `t`. + */ +State mkMatch(RegExpTerm t) { result = Match(t, 0) } + +/** + * A state in the NFA corresponding to a regular expression. + * + * Each regular expression literal `l` has one accepting state + * `Accept(l)`, one state that accepts all suffixes `AcceptAnySuffix(l)`, + * and a state `Match(t, i)` for every subterm `t`, + * which represents the state of the NFA before starting to + * match `t`, or the `i`th character in `t` if `t` is a constant. + */ +class State extends TState { + RegExpTerm repr; + + State() { + this = Match(repr, _) or + this = Accept(repr) or + this = AcceptAnySuffix(repr) + } + + /** + * Gets a string representation for this state in a regular expression. + */ + string toString() { + exists(int i | this = Match(repr, i) | result = "Match(" + repr + "," + i + ")") + or + this instanceof Accept and + result = "Accept(" + repr + ")" + or + this instanceof AcceptAnySuffix and + result = "AcceptAny(" + repr + ")" + } + + /** + * Gets the location for this state. + */ + Location getLocation() { result = repr.getLocation() } + + /** + * Gets the term represented by this state. + */ + RegExpTerm getRepr() { result = repr } +} + +/** + * Gets the minimum char that is matched by both the character classes `c` and `d`. + */ +private string getMinOverlapBetweenCharacterClasses(CharacterClass c, CharacterClass d) { + result = min(getAOverlapBetweenCharacterClasses(c, d)) +} + +/** + * Gets a char that is matched by both the character classes `c` and `d`. + * And `c` and `d` is not the same character class. + */ +private string getAOverlapBetweenCharacterClasses(CharacterClass c, CharacterClass d) { + sharesRoot(c, d) and + result = [c.getARelevantChar(), d.getARelevantChar()] and + c.matches(result) and + d.matches(result) and + not c = d +} + +/** + * Gets a character that is represented by both `c` and `d`. + */ +string intersect(InputSymbol c, InputSymbol d) { + (sharesRoot(c, d) or [c, d] = Any()) and + ( + c = Char(result) and + d = getAnInputSymbolMatching(result) + or + result = getMinOverlapBetweenCharacterClasses(c, d) + or + result = c.(CharacterClass).choose() and + ( + d = c + or + d = Dot() and + not (result = "\n" or result = "\r") + or + d = Any() + ) + or + (c = Dot() or c = Any()) and + (d = Dot() or d = Any()) and + result = "a" + ) + or + result = intersect(d, c) +} + +/** + * Gets a symbol that matches `char`. + */ +bindingset[char] +InputSymbol getAnInputSymbolMatching(string char) { + result = Char(char) + or + result.(CharacterClass).matches(char) + or + result = Dot() and + not (char = "\n" or char = "\r") + or + result = Any() +} + +/** + * Holds if `state` is a start state. + */ +predicate isStartState(State state) { + state = mkMatch(any(RegExpRoot r)) + or + exists(RegExpCaret car | state = after(car)) +} + +/** + * Predicates for constructing a prefix string that leads to a given state. + */ +private module PrefixConstruction { + /** + * Holds if `state` is the textually last start state for the regular expression. + */ + private predicate lastStartState(State state) { + exists(RegExpRoot root | + state = + max(StateInPumpableRegexp s, Location l | + isStartState(s) and getRoot(s.getRepr()) = root and l = s.getRepr().getLocation() + | + s + order by + l.getStartLine(), l.getStartColumn(), s.getRepr().toString(), l.getEndColumn(), + l.getEndLine() + ) + ) + } + + /** + * Holds if there exists any transition (Epsilon() or other) from `a` to `b`. + */ + private predicate existsTransition(State a, State b) { delta(a, _, b) } + + /** + * Gets the minimum number of transitions it takes to reach `state` from the `start` state. + */ + int prefixLength(State start, State state) = + shortestDistances(lastStartState/1, existsTransition/2)(start, state, result) + + /** + * Gets the minimum number of transitions it takes to reach `state` from the start state. + */ + private int lengthFromStart(State state) { result = prefixLength(_, state) } + + /** + * Gets a string for which the regular expression will reach `state`. + * + * Has at most one result for any given `state`. + * This predicate will not always have a result even if there is a ReDoS issue in + * the regular expression. + */ + string prefix(State state) { + lastStartState(state) and + result = "" + or + // the search stops past the last redos candidate state. + lengthFromStart(state) <= max(lengthFromStart(any(State s | isReDoSCandidate(s, _)))) and + exists(State prev | + // select a unique predecessor (by an arbitrary measure) + prev = + min(State s, Location loc | + lengthFromStart(s) = lengthFromStart(state) - 1 and + loc = s.getRepr().getLocation() and + delta(s, _, state) + | + s + order by + loc.getStartLine(), loc.getStartColumn(), loc.getEndLine(), loc.getEndColumn(), + s.getRepr().toString() + ) + | + // greedy search for the shortest prefix + result = prefix(prev) and delta(prev, Epsilon(), state) + or + not delta(prev, Epsilon(), state) and + result = prefix(prev) + getCanonicalEdgeChar(prev, state) + ) + } + + /** + * Gets a canonical char for which there exists a transition from `prev` to `next` in the NFA. + */ + private string getCanonicalEdgeChar(State prev, State next) { + result = + min(string c | delta(prev, any(InputSymbol symbol | c = intersect(Any(), symbol)), next)) + } + + /** + * A state within a regular expression that has a pumpable state. + */ + class StateInPumpableRegexp extends State { + pragma[noinline] + StateInPumpableRegexp() { + exists(State s | isReDoSCandidate(s, _) | getRoot(s.getRepr()) = getRoot(this.getRepr())) + } + } +} + +/** + * Predicates for testing the presence of a rejecting suffix. + * + * These predicates are used to ensure that the all states reached from the fork + * by repeating `w` have a rejecting suffix. + * + * For example, a regexp like `/^(a+)+/` will accept any string as long the prefix is + * some number of `"a"`s, and it is therefore not possible to construct a rejecting suffix. + * + * A regexp like `/(a+)+$/` or `/(a+)+b/` trivially has a rejecting suffix, + * as the suffix "X" will cause both the regular expressions to be rejected. + * + * The string `w` is repeated any number of times because it needs to be + * infinitely repeatedable for the attack to work. + * For the regular expression `/((ab)+)*abab/` the accepting state is not reachable from the fork + * using epsilon transitions. But any attempt at repeating `w` will end in a state that accepts all suffixes. + */ +private module SuffixConstruction { + import PrefixConstruction + + /** + * Holds if all states reachable from `fork` by repeating `w` + * are likely rejectable by appending some suffix. + */ + predicate reachesOnlyRejectableSuffixes(State fork, string w) { + isReDoSCandidate(fork, w) and + forex(State next | next = process(fork, w, w.length() - 1) | isLikelyRejectable(next)) + } + + /** + * Holds if there likely exists a suffix starting from `s` that leads to the regular expression being rejected. + * This predicate might find impossible suffixes when searching for suffixes of length > 1, which can cause FPs. + */ + pragma[noinline] + private predicate isLikelyRejectable(StateInPumpableRegexp s) { + // exists a reject edge with some char. + hasRejectEdge(s) + or + hasEdgeToLikelyRejectable(s) + or + // stopping here is rejection + isRejectState(s) + } + + /** + * Holds if `s` is not an accept state, and there is no epsilon transition to an accept state. + */ + predicate isRejectState(StateInPumpableRegexp s) { not epsilonSucc*(s) = Accept(_) } + + /** + * Holds if there is likely a non-empty suffix leading to rejection starting in `s`. + */ + pragma[noopt] + predicate hasEdgeToLikelyRejectable(StateInPumpableRegexp s) { + // all edges (at least one) with some char leads to another state that is rejectable. + // the `next` states might not share a common suffix, which can cause FPs. + exists(string char | char = hasEdgeToLikelyRejectableHelper(s) | + // noopt to force `hasEdgeToLikelyRejectableHelper` to be first in the join-order. + exists(State next | deltaClosedChar(s, char, next) | isLikelyRejectable(next)) and + forall(State next | deltaClosedChar(s, char, next) | isLikelyRejectable(next)) + ) + } + + /** + * Gets a char for there exists a transition away from `s`, + * and `s` has not been found to be rejectable by `hasRejectEdge` or `isRejectState`. + */ + pragma[noinline] + private string hasEdgeToLikelyRejectableHelper(StateInPumpableRegexp s) { + not hasRejectEdge(s) and + not isRejectState(s) and + deltaClosedChar(s, result, _) + } + + /** + * Holds if there is a state `next` that can be reached from `prev` + * along epsilon edges, such that there is a transition from + * `prev` to `next` that the character symbol `char`. + */ + predicate deltaClosedChar(StateInPumpableRegexp prev, string char, StateInPumpableRegexp next) { + deltaClosed(prev, getAnInputSymbolMatchingRelevant(char), next) + } + + pragma[noinline] + InputSymbol getAnInputSymbolMatchingRelevant(string char) { + char = relevant(_) and + result = getAnInputSymbolMatching(char) + } + + /** + * Gets a char used for finding possible suffixes inside `root`. + */ + pragma[noinline] + private string relevant(RegExpRoot root) { + exists(ascii(result)) and exists(root) + or + exists(InputSymbol s | belongsTo(s, root) | result = intersect(s, _)) + or + // The characters from `hasSimpleRejectEdge`. Only `\n` is really needed (as `\n` is not in the `ascii` relation). + // The three chars must be kept in sync with `hasSimpleRejectEdge`. + result = ["|", "\n", "Z"] and exists(root) + } + + /** + * Holds if there exists a `char` such that there is no edge from `s` labeled `char` in our NFA. + * The NFA does not model reject states, so the above is the same as saying there is a reject edge. + */ + private predicate hasRejectEdge(State s) { + hasSimpleRejectEdge(s) + or + not hasSimpleRejectEdge(s) and + exists(string char | char = relevant(getRoot(s.getRepr())) | not deltaClosedChar(s, char, _)) + } + + /** + * Holds if there is no edge from `s` labeled with "|", "\n", or "Z" in our NFA. + * This predicate is used as a cheap pre-processing to speed up `hasRejectEdge`. + */ + private predicate hasSimpleRejectEdge(State s) { + // The three chars were chosen arbitrarily. The three chars must be kept in sync with `relevant`. + exists(string char | char = ["|", "\n", "Z"] | not deltaClosedChar(s, char, _)) + } + + /** + * Gets a state that can be reached from pumpable `fork` consuming all + * chars in `w` any number of times followed by the first `i+1` characters of `w`. + */ + pragma[noopt] + private State process(State fork, string w, int i) { + exists(State prev | prev = getProcessPrevious(fork, i, w) | + exists(string char, InputSymbol sym | + char = w.charAt(i) and + deltaClosed(prev, sym, result) and + // noopt to prevent joining `prev` with all possible `chars` that could transition away from `prev`. + // Instead only join with the set of `chars` where a relevant `InputSymbol` has already been found. + sym = getAProcessInputSymbol(char) + ) + ) + } + + /** + * Gets a state that can be reached from pumpable `fork` consuming all + * chars in `w` any number of times followed by the first `i` characters of `w`. + */ + private State getProcessPrevious(State fork, int i, string w) { + isReDoSCandidate(fork, w) and + ( + i = 0 and result = fork + or + result = process(fork, w, i - 1) + or + // repeat until fixpoint + i = 0 and + result = process(fork, w, w.length() - 1) + ) + } + + /** + * Gets an InputSymbol that matches `char`. + * The predicate is specialized to only have a result for the `char`s that are relevant for the `process` predicate. + */ + private InputSymbol getAProcessInputSymbol(string char) { + char = getAProcessChar() and + result = getAnInputSymbolMatching(char) + } + + /** + * Gets a `char` that occurs in a `pump` string. + */ + private string getAProcessChar() { result = any(string s | isReDoSCandidate(_, s)).charAt(_) } +} + +/** + * Gets the result of backslash-escaping newlines, carriage-returns and + * backslashes in `s`. + */ +bindingset[s] +private string escape(string s) { + result = + s.replaceAll("\\", "\\\\") + .replaceAll("\n", "\\n") + .replaceAll("\r", "\\r") + .replaceAll("\t", "\\t") +} + +/** + * Gets `str` with the last `i` characters moved to the front. + * + * We use this to adjust the pump string to match with the beginning of + * a RegExpTerm, so it doesn't start in the middle of a constant. + */ +bindingset[str, i] +private string rotate(string str, int i) { + result = str.suffix(str.length() - i) + str.prefix(str.length() - i) +} + +/** + * Holds if `term` may cause superlinear backtracking on strings containing many repetitions of `pump`. + * Gets the shortest string that causes superlinear backtracking. + */ +private predicate isReDoSAttackable(RegExpTerm term, string pump, State s) { + exists(int i, string c | s = Match(term, i) | + c = + min(string w | + any(ReDoSConfiguration conf).isReDoSCandidate(s, w) and + SuffixConstruction::reachesOnlyRejectableSuffixes(s, w) + | + w order by w.length(), w + ) and + pump = escape(rotate(c, i)) + ) +} + +/** + * Holds if the state `s` (represented by the term `t`) can have backtracking with repetitions of `pump`. + * + * `prefixMsg` contains a friendly message for a prefix that reaches `s` (or `prefixMsg` is the empty string if the prefix is empty or if no prefix could be found). + */ +predicate hasReDoSResult(RegExpTerm t, string pump, State s, string prefixMsg) { + isReDoSAttackable(t, pump, s) and + ( + prefixMsg = "starting with '" + escape(PrefixConstruction::prefix(s)) + "' and " and + not PrefixConstruction::prefix(s) = "" + or + PrefixConstruction::prefix(s) = "" and prefixMsg = "" + or + not exists(PrefixConstruction::prefix(s)) and prefixMsg = "" + ) +} diff --git a/java/ql/lib/semmle/code/java/security/performance/ReDoSUtilSpecific.qll b/java/ql/lib/semmle/code/java/security/performance/ReDoSUtilSpecific.qll new file mode 100644 index 00000000000..d72d6770848 --- /dev/null +++ b/java/ql/lib/semmle/code/java/security/performance/ReDoSUtilSpecific.qll @@ -0,0 +1,76 @@ +/** + * This module should provide a class hierarchy corresponding to a parse tree of regular expressions. + * This is the interface to the shared ReDoS library. + */ + +private import java +import semmle.code.FileSystem +import semmle.code.java.regex.RegexTreeView + +/** + * Holds if `term` is an escape class representing e.g. `\d`. + * `clazz` is which character class it represents, e.g. "d" for `\d`. + */ +predicate isEscapeClass(RegExpTerm term, string clazz) { + term.(RegExpCharacterClassEscape).getValue() = clazz + or + term.(RegExpNamedProperty).getBackslashEquivalent() = clazz +} + +/** + * Holds if `term` is a possessive quantifier, e.g. `a*+`. + */ +predicate isPossessive(RegExpQuantifier term) { term.isPossessive() } + +/** + * Holds if the regex that `term` is part of is used in a way that ignores any leading prefix of the input it's matched against. + */ +predicate matchesAnyPrefix(RegExpTerm term) { not term.getRegex().matchesFullString() } + +/** + * Holds if the regex that `term` is part of is used in a way that ignores any trailing suffix of the input it's matched against. + */ +predicate matchesAnySuffix(RegExpTerm term) { not term.getRegex().matchesFullString() } + +/** + * Holds if the regular expression should not be considered. + * + * We make the pragmatic performance optimization to ignore regular expressions in files + * that do not belong to the project code (such as installed dependencies). + */ +predicate isExcluded(RegExpParent parent) { + not exists(parent.getRegex().getLocation().getFile().getRelativePath()) + or + // Regexes with many occurrences of ".*" may cause the polynomial ReDoS computation to explode, so + // we explicitly exclude these. + strictcount(int i | exists(parent.getRegex().getText().regexpFind("\\.\\*", i, _)) | i) > 10 +} + +/** + * A module containing predicates for determining which flags a regular expression have. + */ +module RegExpFlags { + /** + * Holds if `root` has the `i` flag for case-insensitive matching. + */ + predicate isIgnoreCase(RegExpTerm root) { + root.isRootTerm() and + root.getLiteral().isIgnoreCase() + } + + /** + * Gets the flags for `root`, or the empty string if `root` has no flags. + */ + string getFlags(RegExpTerm root) { + root.isRootTerm() and + result = root.getLiteral().getFlags() + } + + /** + * Holds if `root` has the `s` flag for multi-line matching. + */ + predicate isDotAll(RegExpTerm root) { + root.isRootTerm() and + root.getLiteral().isDotAll() + } +} diff --git a/java/ql/lib/semmle/code/java/security/performance/SuperlinearBackTracking.qll b/java/ql/lib/semmle/code/java/security/performance/SuperlinearBackTracking.qll new file mode 100644 index 00000000000..4ba9520cdcc --- /dev/null +++ b/java/ql/lib/semmle/code/java/security/performance/SuperlinearBackTracking.qll @@ -0,0 +1,454 @@ +/** + * 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 + ")" + ) + } +} + +/** + * 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) +} + +private predicate hasSuffix(Trace suffix, Trace t, int i) { + // Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the + // recursive case, so instead we check it explicitly here. + t instanceof RelevantTrace and + i = 0 and + suffix = t + or + hasSuffix(Step(_, _, _, suffix), t, i - 1) +} + +pragma[noinline] +private predicate hasTuple(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace t, int i) { + hasSuffix(Step(s1, s2, s3, _), t, i) +} + +private class RelevantTrace extends Trace, Step { + RelevantTrace() { + exists(State pivot, State succ, StateTuple q | + isReachableFromStartTuple(pivot, succ, q, this, _) and + q = getAnEndTuple(pivot, succ) + ) + } + + pragma[noinline] + private string getAThreewayIntersect(int i) { + exists(InputSymbol s1, InputSymbol s2, InputSymbol s3 | + hasTuple(s1, s2, s3, this, i) and + result = getAThreewayIntersect(s1, s2, s3) + ) + } + + /** Gets a string corresponding to this trace. */ + // the pragma is needed for the case where `getAThreewayIntersect(s1, s2, s3)` has multiple values, + // not for recursion + language[monotonicAggregates] + string concretise() { + result = + strictconcat(int i | + hasTuple(_, _, _, this, i) + | + this.getAThreewayIntersect(i) order by i desc + ) + } +} + +/** + * 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, RelevantTrace t | + isReachableFromStartTuple(pivot, succ, q, t, _) and + q = getAnEndTuple(pivot, succ) and + pump = t.concretise() + ) +} + +/** + * 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 } +} diff --git a/java/ql/src/Security/CWE/CWE-730/PolynomialReDoS.qhelp b/java/ql/src/Security/CWE/CWE-730/PolynomialReDoS.qhelp new file mode 100644 index 00000000000..dbb1f4c37f5 --- /dev/null +++ b/java/ql/src/Security/CWE/CWE-730/PolynomialReDoS.qhelp @@ -0,0 +1,108 @@ + + + + + + + +

+ + Consider this use of a regular expression, which removes + all leading and trailing whitespace in a string: + +

+ + + Pattern.compile("^\\s+|\\s+$").matcher(text).replaceAll("") // BAD + + +

+ + The sub-expression "\\s+$" will match the + whitespace characters in text from left to right, but it + can start matching anywhere within a whitespace sequence. This is + problematic for strings that do not 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. + +

+ +

+ + This ultimately means that the time cost of trimming a + string is quadratic in the length of the string. So a string like + "a b" will take milliseconds to process, but a similar + string with a million spaces instead of just one will take several + minutes. + +

+ +

+ + 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 + ("^\\s+|(?<!\\s)\\s+$"), or just by using the built-in trim + method (text.trim()). + +

+ +

+ + Note that the sub-expression "^\\s+" is + not problematic as the ^ anchor restricts + when that sub-expression can start matching, and as the regular + expression engine matches from left to right. + +

+ + + + + +

+ + As a similar, but slightly subtler problem, consider the + regular expression that matches lines with numbers, possibly written + using scientific notation: +

+ + + "^0\\.\\d+E?\\d+$"" + + +

+ + The problem with this regular expression is in the + sub-expression \d+E?\d+ because the second + \d+ can start matching digits anywhere after the first + match of the first \d+ if there is no E in + the input string. + +

+ +

+ + This is problematic for strings that do not + 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. + +

+ +

+ + To make the processing faster, the regular expression + should be rewritten such that the two \d+ sub-expressions + do not have overlapping matches: "^0\\.\\d+(E\\d+)?$". + +

+ + + + + + diff --git a/java/ql/src/Security/CWE/CWE-730/PolynomialReDoS.ql b/java/ql/src/Security/CWE/CWE-730/PolynomialReDoS.ql new file mode 100644 index 00000000000..1a52173183f --- /dev/null +++ b/java/ql/src/Security/CWE/CWE-730/PolynomialReDoS.ql @@ -0,0 +1,24 @@ +/** + * @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 + * @security-severity 7.5 + * @precision high + * @id java/polynomial-redos + * @tags security + * external/cwe/cwe-730 + * external/cwe/cwe-400 + */ + +import java +import semmle.code.java.security.performance.PolynomialReDoSQuery +import DataFlow::PathGraph + +from DataFlow::PathNode source, DataFlow::PathNode sink, PolynomialBackTrackingTerm regexp +where hasPolynomialReDoSResult(source, sink, regexp) +select sink, 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" diff --git a/java/ql/src/Security/CWE/CWE-730/ReDoS.qhelp b/java/ql/src/Security/CWE/CWE-730/ReDoS.qhelp new file mode 100644 index 00000000000..08b67acb638 --- /dev/null +++ b/java/ql/src/Security/CWE/CWE-730/ReDoS.qhelp @@ -0,0 +1,34 @@ + + + + + + + +

+ Consider this regular expression: +

+ + ^_(__|.)+_$ + +

+ Its sub-expression "(__|.)+?" can match the string "__" either by the + first alternative "__" to the left of the "|" operator, or by two + repetitions of the second alternative "." to the right. Thus, a string consisting + of an odd number of underscores followed by some other character will cause the regular + expression engine to run for an exponential amount of time before rejecting the input. +

+

+ This problem can be avoided by rewriting the regular expression to remove the ambiguity between + the two branches of the alternative inside the repetition: +

+ + ^_(__|[^_])+_$ + + + + + + diff --git a/java/ql/src/Security/CWE/CWE-730/ReDoS.ql b/java/ql/src/Security/CWE/CWE-730/ReDoS.ql new file mode 100644 index 00000000000..c5d9661a63b --- /dev/null +++ b/java/ql/src/Security/CWE/CWE-730/ReDoS.ql @@ -0,0 +1,26 @@ +/** + * @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 + * @security-severity 7.5 + * @precision high + * @id java/redos + * @tags security + * external/cwe/cwe-730 + * external/cwe/cwe-400 + */ + +import java +import semmle.code.java.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 + "'." diff --git a/java/ql/src/Security/CWE/CWE-730/ReDoSIntroduction.inc.qhelp b/java/ql/src/Security/CWE/CWE-730/ReDoSIntroduction.inc.qhelp new file mode 100644 index 00000000000..f6e4dbd0a5f --- /dev/null +++ b/java/ql/src/Security/CWE/CWE-730/ReDoSIntroduction.inc.qhelp @@ -0,0 +1,61 @@ + + + +

+ + Some regular expressions take a long time to match certain + input strings to the point where the time it takes to match a string + of length n is proportional to nk or even + 2n. Such regular expressions can negatively affect + performance, or even allow a malicious user to perform a Denial of + Service ("DoS") attack by crafting an expensive input string for the + regular expression to match. + +

+ +

+ + The regular expression engine provided by Java uses a backtracking non-deterministic finite + automata to implement regular expression matching. While this approach + is space-efficient and allows supporting advanced features like + capture groups, it is not time-efficient in general. The worst-case + time complexity of such an automaton can be polynomial or even + exponential, meaning that for strings of a certain shape, increasing + the input length by ten characters may make the automaton about 1000 + times slower. + +

+ +

+ + Typically, a regular expression is affected by this + problem if it contains a repetition of the form r* or + r+ where the sub-expression r is ambiguous + in the sense that it can match some string in multiple ways. More + information about the precise circumstances can be found in the + references. + +

+ +

+ Note that Java versions 9 and above have some mitigations against ReDoS; however they aren't perfect + and more complex regular expressions can still be affected by this problem. +

+ + + + +

+ + Modify the regular expression to remove the ambiguity, or + ensure that the strings matched with the regular expression are short + enough that the time-complexity does not matter. + + Alternatively, an alternate regex library that guarantees linear time execution, such as Google's RE2J, may be used. + +

+ + + diff --git a/java/ql/src/Security/CWE/CWE-730/ReDoSReferences.inc.qhelp b/java/ql/src/Security/CWE/CWE-730/ReDoSReferences.inc.qhelp new file mode 100644 index 00000000000..2b3e5f17c62 --- /dev/null +++ b/java/ql/src/Security/CWE/CWE-730/ReDoSReferences.inc.qhelp @@ -0,0 +1,16 @@ + + + +
  • + OWASP: + Regular expression Denial of Service - ReDoS. +
    • +
  • Wikipedia: ReDoS.
    • +
  • Wikipedia: Time complexity.
    • +
  • James Kirrage, Asiri Rathnayake, Hayo Thielecke: + Static Analysis for Regular Expression Denial-of-Service Attack. +
    • +     +     diff --git a/java/ql/src/change-notes/2022-03-03-redos.md b/java/ql/src/change-notes/2022-03-03-redos.md new file mode 100644 index 00000000000..daf1dd51be1 --- /dev/null +++ b/java/ql/src/change-notes/2022-03-03-redos.md @@ -0,0 +1,6 @@ +--- +category: newQuery +--- + +* Two new queries "Inefficient regular expression" (`java/redos`) and "Polynomial regular expression used on uncontrolled data" (`java/polynomial-redos`) have been added. +These queries help find instances of Regular Expression Denial of Service vulnerabilities. \ No newline at end of file diff --git a/java/ql/test/library-tests/JDK/PrintAst.expected b/java/ql/test/library-tests/JDK/PrintAst.expected index e6f240b325e..8074ef1b965 100644 --- a/java/ql/test/library-tests/JDK/PrintAst.expected +++ b/java/ql/test/library-tests/JDK/PrintAst.expected @@ -73,6 +73,11 @@ jdk/StringMatch.java: # 5| 0: [MethodAccess] matches(...) # 5| -1: [VarAccess] STR # 5| 0: [StringLiteral] "[a-z]+" +# 5| 0: [RegExpPlus] [a-z]+ +# 5| 0: [RegExpCharacterClass] [a-z] +# 5| 0: [RegExpCharacterRange] a-z +# 5| 0: [RegExpConstant | RegExpNormalChar] a +# 5| 1: [RegExpConstant | RegExpNormalChar] z # 8| 5: [Method] b # 8| 3: [TypeAccess] void # 8| 5: [BlockStmt] { ... } diff --git a/java/ql/test/library-tests/regex/Test.java b/java/ql/test/library-tests/regex/Test.java index b351c31812a..fd9be63b68b 100644 --- a/java/ql/test/library-tests/regex/Test.java +++ b/java/ql/test/library-tests/regex/Test.java @@ -101,4 +101,4 @@ public class Test { } -} +} \ No newline at end of file diff --git a/java/ql/test/library-tests/regex/parser/RegexParseTests.expected b/java/ql/test/library-tests/regex/parser/RegexParseTests.expected new file mode 100644 index 00000000000..ad94d005289 --- /dev/null +++ b/java/ql/test/library-tests/regex/parser/RegexParseTests.expected @@ -0,0 +1,207 @@ +parseFailures +#select +| Test.java:5:10:5:17 | [A-Z\\d] | [RegExpCharacterClass] | +| Test.java:5:10:5:19 | [A-Z\\d]++ | [RegExpPlus] | +| Test.java:5:11:5:11 | A | [RegExpConstant,RegExpNormalChar] | +| Test.java:5:11:5:13 | A-Z | [RegExpCharacterRange] | +| Test.java:5:13:5:13 | Z | [RegExpConstant,RegExpNormalChar] | +| Test.java:5:14:5:16 | \\d | [RegExpCharacterClassEscape] | +| Test.java:6:10:6:42 | \\Q hello world [ *** \\Q ) ( \\E | [RegExpConstant,RegExpQuote] | +| Test.java:6:10:6:43 | \\Q hello world [ *** \\Q ) ( \\E+ | [RegExpPlus] | +| Test.java:7:10:7:23 | [\\Q hi ] \\E] | [RegExpCharacterClass] | +| Test.java:7:10:7:24 | [\\Q hi ] \\E]+ | [RegExpPlus] | +| Test.java:7:11:7:22 | \\Q hi ] \\E | [RegExpConstant,RegExpQuote] | +| Test.java:8:10:8:12 | []] | [RegExpCharacterClass] | +| Test.java:8:10:8:13 | []]+ | [RegExpPlus] | +| Test.java:8:11:8:11 | ] | [RegExpConstant,RegExpNormalChar] | +| Test.java:9:10:9:13 | [^]] | [RegExpCharacterClass] | +| Test.java:9:10:9:14 | [^]]+ | [RegExpPlus] | +| Test.java:9:12:9:12 | ] | [RegExpConstant,RegExpNormalChar] | +| Test.java:10:10:10:20 | [abc[defg]] | [RegExpCharacterClass] | +| Test.java:10:10:10:21 | [abc[defg]]+ | [RegExpPlus] | +| Test.java:10:11:10:11 | a | [RegExpConstant,RegExpNormalChar] | +| Test.java:10:12:10:12 | b | [RegExpConstant,RegExpNormalChar] | +| Test.java:10:13:10:13 | c | [RegExpConstant,RegExpNormalChar] | +| Test.java:10:14:10:14 | [ | [RegExpConstant,RegExpNormalChar] | +| Test.java:10:15:10:15 | d | [RegExpConstant,RegExpNormalChar] | +| Test.java:10:16:10:16 | e | [RegExpConstant,RegExpNormalChar] | +| Test.java:10:17:10:17 | f | [RegExpConstant,RegExpNormalChar] | +| Test.java:10:18:10:18 | g | [RegExpConstant,RegExpNormalChar] | +| Test.java:10:19:10:19 | ] | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:10:11:57 | [abc&&[\\W\\p{Lower}\\P{Space}\\N{degree sign}]] | [RegExpCharacterClass] | +| Test.java:11:10:11:69 | [abc&&[\\W\\p{Lower}\\P{Space}\\N{degree sign}]]\\b7\\b{g}8+ | [RegExpSequence] | +| Test.java:11:11:11:11 | a | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:12:11:12 | b | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:13:11:13 | c | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:14:11:14 | & | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:15:11:15 | & | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:16:11:16 | [ | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:17:11:19 | \\W | [RegExpCharacterClassEscape] | +| Test.java:11:20:11:29 | \\p{Lower} | [RegExpCharacterClassEscape] | +| Test.java:11:30:11:39 | \\P{Space} | [RegExpCharacterClassEscape] | +| Test.java:11:40:11:55 | \\N{degree sign} | [RegExpConstant,RegExpEscape] | +| Test.java:11:56:11:56 | ] | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:58:11:60 | \\b | [RegExpConstant,RegExpEscape] | +| Test.java:11:61:11:61 | 7 | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:62:11:67 | \\b{g} | [RegExpConstant,RegExpEscape] | +| Test.java:11:68:11:68 | 8 | [RegExpConstant,RegExpNormalChar] | +| Test.java:11:68:11:69 | 8+ | [RegExpPlus] | +| Test.java:12:10:12:13 | \\cA | [RegExpConstant,RegExpEscape] | +| Test.java:12:10:12:14 | \\cA+ | [RegExpPlus] | +| Test.java:13:10:13:13 | \\c( | [RegExpConstant,RegExpEscape] | +| Test.java:13:10:13:14 | \\c(+ | [RegExpPlus] | +| Test.java:14:10:14:14 | \\c\\ | [RegExpConstant,RegExpEscape] | +| Test.java:14:10:14:19 | \\c\\(ab)+ | [RegExpSequence] | +| Test.java:14:15:14:18 | (ab) | [RegExpGroup] | +| Test.java:14:15:14:19 | (ab)+ | [RegExpPlus] | +| Test.java:14:16:14:16 | a | [RegExpConstant,RegExpNormalChar] | +| Test.java:14:16:14:17 | ab | [RegExpSequence] | +| Test.java:14:17:14:17 | b | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:10:15:15 | (?>hi) | [RegExpGroup] | +| Test.java:15:10:15:45 | (?>hi)(?hell*?o*+)123\\k | [RegExpSequence] | +| Test.java:15:13:15:13 | h | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:13:15:14 | hi | [RegExpSequence] | +| Test.java:15:14:15:14 | i | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:16:15:33 | (?hell*?o*+) | [RegExpGroup] | +| Test.java:15:24:15:24 | h | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:24:15:32 | hell*?o*+ | [RegExpSequence] | +| Test.java:15:25:15:25 | e | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:26:15:26 | l | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:27:15:27 | l | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:27:15:29 | l*? | [RegExpStar] | +| Test.java:15:30:15:30 | o | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:30:15:32 | o*+ | [RegExpStar] | +| Test.java:15:34:15:34 | 1 | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:35:15:35 | 2 | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:36:15:36 | 3 | [RegExpConstant,RegExpNormalChar] | +| Test.java:15:37:15:45 | \\k | [RegExpBackRef] | +| Test.java:16:10:16:10 | a | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:10:16:11 | a+ | [RegExpPlus] | +| Test.java:16:10:16:108 | a+b*c?d{2}e{3,4}f{,5}g{6,}h+?i*?j??k{7}?l{8,9}?m{,10}?n{11,}?o++p*+q?+r{12}+s{13,14}+t{,15}+u{16,}+ | [RegExpSequence] | +| Test.java:16:12:16:12 | b | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:12:16:13 | b* | [RegExpStar] | +| Test.java:16:14:16:14 | c | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:14:16:15 | c? | [RegExpOpt] | +| Test.java:16:16:16:16 | d | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:16:16:19 | d{2} | [RegExpRange] | +| Test.java:16:20:16:20 | e | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:20:16:25 | e{3,4} | [RegExpRange] | +| Test.java:16:26:16:26 | f | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:26:16:30 | f{,5} | [RegExpRange] | +| Test.java:16:31:16:31 | g | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:31:16:35 | g{6,} | [RegExpRange] | +| Test.java:16:36:16:36 | h | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:36:16:38 | h+? | [RegExpPlus] | +| Test.java:16:39:16:39 | i | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:39:16:41 | i*? | [RegExpStar] | +| Test.java:16:42:16:42 | j | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:42:16:44 | j?? | [RegExpOpt] | +| Test.java:16:45:16:45 | k | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:45:16:49 | k{7}? | [RegExpQuantifier] | +| Test.java:16:50:16:50 | l | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:50:16:56 | l{8,9}? | [RegExpQuantifier] | +| Test.java:16:57:16:57 | m | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:57:16:63 | m{,10}? | [RegExpQuantifier] | +| Test.java:16:64:16:64 | n | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:64:16:70 | n{11,}? | [RegExpQuantifier] | +| Test.java:16:71:16:71 | o | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:71:16:73 | o++ | [RegExpPlus] | +| Test.java:16:74:16:74 | p | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:74:16:76 | p*+ | [RegExpStar] | +| Test.java:16:77:16:77 | q | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:77:16:79 | q?+ | [RegExpOpt] | +| Test.java:16:80:16:80 | r | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:80:16:85 | r{12}+ | [RegExpQuantifier] | +| Test.java:16:86:16:86 | s | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:86:16:94 | s{13,14}+ | [RegExpQuantifier] | +| Test.java:16:95:16:95 | t | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:95:16:101 | t{,15}+ | [RegExpQuantifier] | +| Test.java:16:102:16:102 | u | [RegExpConstant,RegExpNormalChar] | +| Test.java:16:102:16:108 | u{16,}+ | [RegExpQuantifier] | +| Test.java:17:10:17:13 | (?i) | [RegExpZeroWidthMatch] | +| Test.java:17:10:17:36 | (?i)(?=a)(?!b)(?<=c)(?hi)(?hell*?o*+)123\\k", + "a+b*c?d{2}e{3,4}f{,5}g{6,}h+?i*?j??k{7}?l{8,9}?m{,10}?n{11,}?o++p*+q?+r{12}+s{13,14}+t{,15}+u{16,}+", + "(?i)(?=a)(?!b)(?<=c)(?+()\\s-]+|\\*|\\[.*?\\])+)\\s*(,|$)", // $ hasExpRedos + + // NOT GOOD; attack: "'" + "\\a".repeat(100) + '"' + // Adapted from Prism (https://github.com/PrismJS/prism), which is licensed + // under the MIT license; see file Prism-LICENSE. + "(\"|')(\\\\?.)*?\\1", // $ hasExpRedos + + // NOT GOOD + "(b|a?b)*c", // $ hasExpRedos + + // NOT GOOD + "(a|aa?)*b", // $ hasExpRedos + + // GOOD + "(.|\\n)*!", + + // NOT GOOD; attack: "\n".repeat(100) + "." + "(?s)(.|\\n)*!", // $ hasExpRedos + + // GOOD + "([\\w.]+)*", + + // NOT GOOD + "(a|aa?)*b", // $ hasExpRedos + + // NOT GOOD + "(([\\s\\S]|[^a])*)\"", // $ hasExpRedos + + // GOOD - there is no witness in the end that could cause the regexp to not match + "([^\"']+)*", + + // NOT GOOD + "((.|[^a])*)\"", // $ hasExpRedos + + // GOOD + "((a|[^a])*)\"", + + // NOT GOOD + "((b|[^a])*)\"", // $ hasExpRedos + + // NOT GOOD + "((G|[^a])*)\"", // $ hasExpRedos + + // NOT GOOD + "(([0-9]|[^a])*)\"", // $ hasExpRedos + + // NOT GOOD + "(?:=(?:([!#\\$%&'\\*\\+\\-\\.\\^_`\\|~0-9A-Za-z]+)|\"((?:\\\\[\\x00-\\x7f]|[^\\x00-\\x08\\x0a-\\x1f\\x7f\"])*)\"))?", // $ MISSING: hasExpRedos + + // NOT GOOD + "\"((?:\\\\[\\x00-\\x7f]|[^\\x00-\\x08\\x0a-\\x1f\\x7f\"])*)\"", // $ MISSING: hasExpRedos + + // GOOD + "\"((?:\\\\[\\x00-\\x7f]|[^\\x00-\\x08\\x0a-\\x1f\\x7f\"\\\\])*)\"", + + // NOT GOOD + "(([a-z]|[d-h])*)\"", // $ hasExpRedos + + // NOT GOOD + "(([^a-z]|[^0-9])*)\"", // $ hasExpRedos + + // NOT GOOD + "((\\d|[0-9])*)\"", // $ hasExpRedos + + // NOT GOOD + "((\\s|\\s)*)\"", // $ hasExpRedos + + // NOT GOOD + "((\\w|G)*)\"", // $ hasExpRedos + + // GOOD + "((\\s|\\d)*)\"", + + // NOT GOOD + "((\\d|\\w)*)\"", // $ hasExpRedos + + // NOT GOOD + "((\\d|5)*)\"", // $ hasExpRedos + + // NOT GOOD + "((\\s|[\\f])*)\"", // $ hasExpRedos + + // NOT GOOD - but not detected (likely because \v is a character class in Java rather than a specific character in other langs) + "((\\s|[\\v]|\\\\v)*)\"", // $ MISSING: hasExpRedos + + // NOT GOOD + "((\\f|[\\f])*)\"", // $ hasExpRedos + + // NOT GOOD + "((\\W|\\D)*)\"", // $ hasExpRedos + + // NOT GOOD + "((\\S|\\w)*)\"", // $ hasExpRedos + + // NOT GOOD + "((\\S|[\\w])*)\"", // $ hasExpRedos + + // NOT GOOD + "((1s|[\\da-z])*)\"", // $ hasExpRedos + + // NOT GOOD + "((0|[\\d])*)\"", // $ hasExpRedos + + // NOT GOOD + "(([\\d]+)*)\"", // $ hasExpRedos + + // GOOD - there is no witness in the end that could cause the regexp to not match + "(\\d+(X\\d+)?)+", + + // GOOD - there is no witness in the end that could cause the regexp to not match + "([0-9]+(X[0-9]*)?)*", + + // GOOD + "^([^>]+)*(>|$)", + + // NOT GOOD + "^([^>a]+)*(>|$)", // $ hasExpRedos + + // NOT GOOD + "(\\n\\s*)+$", // $ hasExpRedos + + // NOT GOOD + "^(?:\\s+|#.*|\\(\\?#[^)]*\\))*(?:[?*+]|\\{\\d+(?:,\\d*)?})", // $ hasExpRedos + + // NOT GOOD + "\\{\\[\\s*([a-zA-Z]+)\\(([a-zA-Z]+)\\)((\\s*([a-zA-Z]+)\\: ?([ a-zA-Z{}]+),?)+)*\\s*\\]\\}", // $ hasExpRedos + + // NOT GOOD + "(a+|b+|c+)*c", // $ hasExpRedos + + // NOT GOOD + "(((a+a?)*)+b+)", // $ hasExpRedos + + // NOT GOOD + "(a+)+bbbb", // $ hasExpRedos + + // GOOD + "(a+)+aaaaa*a+", + + // NOT GOOD + "(a+)+aaaaa$", // $ hasExpRedos + + // GOOD + "(\\n+)+\\n\\n", + + // NOT GOOD + "(\\n+)+\\n\\n$", // $ hasExpRedos + + // NOT GOOD + "([^X]+)*$", // $ hasExpRedos + + // NOT GOOD + "(([^X]b)+)*$", // $ hasExpRedos + + // GOOD + "(([^X]b)+)*($|[^X]b)", + + // NOT GOOD + "(([^X]b)+)*($|[^X]c)", // $ hasExpRedos + + // GOOD + "((ab)+)*ababab", + + // GOOD + "((ab)+)*abab(ab)*(ab)+", + + // GOOD + "((ab)+)*", + + // NOT GOOD + "((ab)+)*$", // $ hasExpRedos + + // GOOD + "((ab)+)*[a1][b1][a2][b2][a3][b3]", + + // NOT GOOD + "([\\n\\s]+)*(.)", // $ hasExpRedos + + // GOOD - any witness passes through the accept state. + "(A*A*X)*", + + // GOOD + "([^\\\\\\]]+)*", + + // NOT GOOD + "(\\w*foobarbaz\\w*foobarbaz\\w*foobarbaz\\w*foobarbaz\\s*foobarbaz\\d*foobarbaz\\w*)+-", // $ hasExpRedos + + // NOT GOOD + "(.thisisagoddamnlongstringforstresstestingthequery|\\sthisisagoddamnlongstringforstresstestingthequery)*-", // $ hasExpRedos + + // NOT GOOD + "(thisisagoddamnlongstringforstresstestingthequery|this\\w+query)*-", // $ hasExpRedos + + // GOOD + "(thisisagoddamnlongstringforstresstestingthequery|imanotherbutunrelatedstringcomparedtotheotherstring)*-", + + // GOOD (but false positive caused by the extractor converting all four unpaired surrogates to \uFFFD) + "foo([\uDC66\uDC67]|[\uDC68\uDC69])*foo", // $ SPURIOUS: hasExpRedos + + // GOOD (but false positive caused by the extractor converting all four unpaired surrogates to \uFFFD) + "foo((\uDC66|\uDC67)|(\uDC68|\uDC69))*foo", // $ SPURIOUS: hasExpRedos + + // NOT GOOD (but cannot currently construct a prefix) + "a{2,3}(b+)+X", // $ hasExpRedos + + // NOT GOOD (and a good prefix test) + "^<(\\w+)((?:\\s+\\w+(?:\\s*=\\s*(?:(?:\"[^\"]*\")|(?:'[^']*')|[^>\\s]+))?)*)\\s*(\\/?)>", // $ hasExpRedos + + // GOOD + "(a+)*[\\s\\S][\\s\\S][\\s\\S]?", + + // GOOD - but we fail to see that repeating the attack string ends in the "accept any" state (due to not parsing the range `[\s\S]{2,3}`). + "(a+)*[\\s\\S]{2,3}", // $ SPURIOUS: hasExpRedos + + // GOOD - but we spuriously conclude that a rejecting suffix exists (due to not parsing the range `[\s\S]{2,}` when constructing the NFA). + "(a+)*([\\s\\S]{2,}|X)$", // $ SPURIOUS: hasExpRedos + + // GOOD + "(a+)*([\\s\\S]*|X)$", + + // NOT GOOD + "((a+)*$|[\\s\\S]+)", // $ hasExpRedos + + // GOOD - but still flagged. The only change compared to the above is the order of alternatives, which we don't model. + "([\\s\\S]+|(a+)*$)", // $ SPURIOUS: hasExpRedos + + // GOOD + "((;|^)a+)+$", + + // NOT GOOD (a good prefix test) + "(^|;)(0|1)(0|1)(0|1)(0|1)(0|1)(0|1)(0|1)(0|1)(0|1)(0|1)(0|1)(0|1)(0|1)(0|1)(e+)+f", // $ hasExpRedos + + // NOT GOOD + "^ab(c+)+$", // $ hasExpRedos + + // NOT GOOD + "(\\d(\\s+)*){20}", // $ hasExpRedos + + // GOOD - but we spuriously conclude that a rejecting suffix exists. + "(([^/]|X)+)(\\/[\\s\\S]*)*$", // $ SPURIOUS: hasExpRedos + + // GOOD - but we spuriously conclude that a rejecting suffix exists. + "^((x([^Y]+)?)*(Y|$))", // $ SPURIOUS: hasExpRedos + + // NOT GOOD + "(a*)+b", // $ hasExpRedos + + // NOT GOOD + "foo([\\w-]*)+bar", // $ hasExpRedos + + // NOT GOOD + "((ab)*)+c", // $ hasExpRedos + + // NOT GOOD + "(a?a?)*b", // $ hasExpRedos + + // GOOD + "(a?)*b", + + // NOT GOOD - but not detected + "(c?a?)*b", // $ MISSING: hasExpRedos + + // NOT GOOD + "(?:a|a?)+b", // $ hasExpRedos + + // NOT GOOD - but not detected. + "(a?b?)*$", // $ MISSING: hasExpRedos + + // NOT GOOD + "PRE(([a-c]|[c-d])T(e?e?e?e?|X))+(cTcT|cTXcTX$)", // $ hasExpRedos + + // NOT GOOD + "^((a)+\\w)+$", // $ hasExpRedos + + // NOT GOOD + "^(b+.)+$", // $ hasExpRedos + + // GOOD + "a*b", + + // All 4 bad combinations of nested * and + + "(a*)*b", // $ hasExpRedos + "(a+)*b", // $ hasExpRedos + "(a*)+b", // $ hasExpRedos + "(a+)+b", // $ hasExpRedos + + // GOOD + "(a|b)+", + "(?:[\\s;,\"'<>(){}|\\[\\]@=+*]|:(?![/\\\\]))+", + + "^((?:a{|-)|\\w\\{)+X$", // $ hasParseFailure + "^((?:a{0|-)|\\w\\{\\d)+X$", // $ hasParseFailure + "^((?:a{0,|-)|\\w\\{\\d,)+X$", // $ hasParseFailure + "^((?:a{0,2|-)|\\w\\{\\d,\\d)+X$", // $ hasParseFailure + + // GOOD + "^((?:a{0,2}|-)|\\w\\{\\d,\\d\\})+X$", + + // NOT GOOD + "X(\\u0061|a)*Y", // $ hasExpRedos + + // GOOD + "X(\\u0061|b)+Y", + + // NOT GOOD + "X(\\x61|a)*Y", // $ hasExpRedos + + // GOOD + "X(\\x61|b)+Y", + + // NOT GOOD + "X(\\x{061}|a)*Y", // $ hasExpRedos + + // GOOD + "X(\\x{061}|b)+Y", + + // NOT GOOD + "X(\\p{Digit}|7)*Y", // $ hasExpRedos + + // GOOD + "X(\\p{Digit}|b)+Y", + + // NOT GOOD + "X(\\P{Digit}|b)*Y", // $ hasExpRedos + + // GOOD + "X(\\P{Digit}|7)+Y", + + // NOT GOOD + "X(\\p{IsDigit}|7)*Y", // $ hasExpRedos + + // GOOD + "X(\\p{IsDigit}|b)+Y", + + // NOT GOOD - but not detected + "X(\\p{Alpha}|a)*Y", // $ MISSING: hasExpRedos + + // GOOD + "X(\\p{Alpha}|7)+Y", + + // GOOD + "(\"[^\"]*?\"|[^\"\\s]+)+(?=\\s*|\\s*$)", + + // BAD + "/(\"[^\"]*?\"|[^\"\\s]+)+(?=\\s*|\\s*$)X", // $ hasExpRedos + "/(\"[^\"]*?\"|[^\"\\s]+)+(?=X)", // $ hasExpRedos + + // BAD + "\\A(\\d|0)*x", // $ hasExpRedos + "(\\d|0)*\\Z", // $ hasExpRedos + "\\b(\\d|0)*x", // $ hasExpRedos + + // GOOD - possessive quantifiers don't backtrack + "(a*+)*+b", + "(a*)*+b", + "(a*+)*b", + + // BAD + "(a*)*b", // $ hasExpRedos + + // BAD - but not detected due to the way possessive quantifiers are approximated + "((aa|a*+)b)*c" // $ MISSING: hasExpRedos + }; + + void test() { + for (int i = 0; i < regs.length; i++) { + Pattern.compile(regs[i]); + } + } +} diff --git a/java/ql/test/query-tests/security/CWE-730/PolyRedosTest.java b/java/ql/test/query-tests/security/CWE-730/PolyRedosTest.java new file mode 100644 index 00000000000..44931190460 --- /dev/null +++ b/java/ql/test/query-tests/security/CWE-730/PolyRedosTest.java @@ -0,0 +1,84 @@ +import java.util.regex.Pattern; +import java.util.function.Predicate; +import javax.servlet.http.HttpServletRequest; +import com.google.common.base.Splitter; + +class PolyRedosTest { + void test(HttpServletRequest request) { + String tainted = request.getParameter("inp"); + String reg = "0\\.\\d+E?\\d+!"; + Predicate dummyPred = (s -> s.length() % 7 == 0); + + tainted.matches(reg); // $ hasPolyRedos + tainted.split(reg); // $ hasPolyRedos + tainted.split(reg, 7); // $ hasPolyRedos + tainted.replaceAll(reg, "a"); // $ hasPolyRedos + tainted.replaceFirst(reg, "a"); // $ hasPolyRedos + Pattern.matches(reg, tainted); // $ hasPolyRedos + Pattern.compile(reg).matcher(tainted).matches(); // $ hasPolyRedos + Pattern.compile(reg).split(tainted); // $ hasPolyRedos + Pattern.compile(reg, Pattern.DOTALL).split(tainted); // $ hasPolyRedos + Pattern.compile(reg).split(tainted, 7); // $ hasPolyRedos + Pattern.compile(reg).splitAsStream(tainted); // $ hasPolyRedos + Pattern.compile(reg).asPredicate().test(tainted); // $ hasPolyRedos + Pattern.compile(reg).asMatchPredicate().negate().and(dummyPred).or(dummyPred).test(tainted); // $ hasPolyRedos + Predicate.not(dummyPred.and(dummyPred.or(Pattern.compile(reg).asPredicate()))).test(tainted); // $ hasPolyRedos + + Splitter.on(Pattern.compile(reg)).split(tainted); // $ hasPolyRedos + Splitter.on(reg).split(tainted); + Splitter.onPattern(reg).split(tainted); // $ hasPolyRedos + Splitter.onPattern(reg).splitToList(tainted); // $ hasPolyRedos + Splitter.onPattern(reg).limit(7).omitEmptyStrings().trimResults().split(tainted); // $ hasPolyRedos + Splitter.onPattern(reg).withKeyValueSeparator(" => ").split(tainted); // $ hasPolyRedos + Splitter.on(";").withKeyValueSeparator(reg).split(tainted); + Splitter.on(";").withKeyValueSeparator(Splitter.onPattern(reg)).split(tainted); // $ hasPolyRedos + + } + + void test2(HttpServletRequest request) { + String tainted = request.getParameter("inp"); + + Pattern p1 = Pattern.compile(".*a"); + Pattern p2 = Pattern.compile(".*b"); + + p1.matcher(tainted).matches(); + p2.matcher(tainted).find(); // $ hasPolyRedos + } + + void test3(HttpServletRequest request) { + String tainted = request.getParameter("inp"); + + Pattern p1 = Pattern.compile("ab*b*"); + Pattern p2 = Pattern.compile("cd*d*"); + + p1.matcher(tainted).matches(); // $ hasPolyRedos + p2.matcher(tainted).find(); + } + + void test4(HttpServletRequest request) { + String tainted = request.getParameter("inp"); + + tainted.matches(".*a"); + tainted.replaceAll(".*b", "c"); // $ hasPolyRedos + } + + static Pattern p3 = Pattern.compile(".*a"); + static Pattern p4 = Pattern.compile(".*b"); + + + void test5(HttpServletRequest request) { + String tainted = request.getParameter("inp"); + + p3.asMatchPredicate().test(tainted); + p4.asPredicate().test(tainted); // $ hasPolyRedos + } + + void test6(HttpServletRequest request) { + Pattern p = Pattern.compile("^a*a*$"); + + p.matcher(request.getParameter("inp")).matches(); // $ hasPolyRedos + p.matcher(request.getHeader("If-None-Match")).matches(); + p.matcher(request.getRequestURI()).matches(); + p.matcher(request.getCookies()[0].getName()).matches(); + } +} \ No newline at end of file diff --git a/java/ql/test/query-tests/security/CWE-730/PolynomialReDoS.expected b/java/ql/test/query-tests/security/CWE-730/PolynomialReDoS.expected new file mode 100644 index 00000000000..e69de29bb2d diff --git a/java/ql/test/query-tests/security/CWE-730/PolynomialReDoS.ql b/java/ql/test/query-tests/security/CWE-730/PolynomialReDoS.ql new file mode 100644 index 00000000000..19096cf6f95 --- /dev/null +++ b/java/ql/test/query-tests/security/CWE-730/PolynomialReDoS.ql @@ -0,0 +1,19 @@ +import java +import TestUtilities.InlineExpectationsTest +import semmle.code.java.security.performance.PolynomialReDoSQuery + +class HasPolyRedos extends InlineExpectationsTest { + HasPolyRedos() { this = "HasPolyRedos" } + + override string getARelevantTag() { result = "hasPolyRedos" } + + override predicate hasActualResult(Location location, string element, string tag, string value) { + tag = "hasPolyRedos" and + exists(DataFlow::PathNode source, DataFlow::PathNode sink, PolynomialBackTrackingTerm regexp | + hasPolynomialReDoSResult(source, sink, regexp) and + location = sink.getNode().getLocation() and + element = sink.getNode().toString() and + value = "" + ) + } +} diff --git a/java/ql/test/query-tests/security/CWE-730/ReDoS.expected b/java/ql/test/query-tests/security/CWE-730/ReDoS.expected new file mode 100644 index 00000000000..e69de29bb2d diff --git a/java/ql/test/query-tests/security/CWE-730/ReDoS.ql b/java/ql/test/query-tests/security/CWE-730/ReDoS.ql new file mode 100644 index 00000000000..79cb8243cd7 --- /dev/null +++ b/java/ql/test/query-tests/security/CWE-730/ReDoS.ql @@ -0,0 +1,29 @@ +import java +import TestUtilities.InlineExpectationsTest +import semmle.code.java.security.performance.ExponentialBackTracking +import semmle.code.java.regex.regex + +class HasExpRedos extends InlineExpectationsTest { + HasExpRedos() { this = "HasExpRedos" } + + override string getARelevantTag() { result = ["hasExpRedos", "hasParseFailure"] } + + override predicate hasActualResult(Location location, string element, string tag, string value) { + tag = "hasExpRedos" and + exists(RegExpTerm t, string pump, State s, string prefixMsg | + hasReDoSResult(t, pump, s, prefixMsg) and + not t.getRegex().getAMode() = "VERBOSE" and + value = "" and + location = t.getLocation() and + element = t.toString() + ) + or + tag = "hasParseFailure" and + exists(Regex r | + r.failedToParse(_) and + value = "" and + location = r.getLocation() and + element = r.toString() + ) + } +} diff --git a/java/ql/test/query-tests/security/CWE-730/options b/java/ql/test/query-tests/security/CWE-730/options new file mode 100644 index 00000000000..2f7d22dc61c --- /dev/null +++ b/java/ql/test/query-tests/security/CWE-730/options @@ -0,0 +1 @@ +// semmle-extractor-options: --javac-args -cp ${testdir}/../../../stubs/servlet-api-2.4:${testdir}/../../../stubs/guava-30.0 \ No newline at end of file diff --git a/java/ql/test/stubs/guava-30.0/com/google/common/base/CharMatcher.java b/java/ql/test/stubs/guava-30.0/com/google/common/base/CharMatcher.java new file mode 100644 index 00000000000..bcc9a0f30b4 --- /dev/null +++ b/java/ql/test/stubs/guava-30.0/com/google/common/base/CharMatcher.java @@ -0,0 +1,53 @@ +// Generated automatically from com.google.common.base.CharMatcher for testing purposes + +package com.google.common.base; + +import com.google.common.base.Predicate; + +abstract public class CharMatcher implements Predicate +{ + protected CharMatcher(){} + public CharMatcher and(CharMatcher p0){ return null; } + public CharMatcher negate(){ return null; } + public CharMatcher or(CharMatcher p0){ return null; } + public CharMatcher precomputed(){ return null; } + public String collapseFrom(CharSequence p0, char p1){ return null; } + public String removeFrom(CharSequence p0){ return null; } + public String replaceFrom(CharSequence p0, CharSequence p1){ return null; } + public String replaceFrom(CharSequence p0, char p1){ return null; } + public String retainFrom(CharSequence p0){ return null; } + public String toString(){ return null; } + public String trimAndCollapseFrom(CharSequence p0, char p1){ return null; } + public String trimFrom(CharSequence p0){ return null; } + public String trimLeadingFrom(CharSequence p0){ return null; } + public String trimTrailingFrom(CharSequence p0){ return null; } + public abstract boolean matches(char p0); + public boolean apply(Character p0){ return false; } + public boolean matchesAllOf(CharSequence p0){ return false; } + public boolean matchesAnyOf(CharSequence p0){ return false; } + public boolean matchesNoneOf(CharSequence p0){ return false; } + public int countIn(CharSequence p0){ return 0; } + public int indexIn(CharSequence p0){ return 0; } + public int indexIn(CharSequence p0, int p1){ return 0; } + public int lastIndexIn(CharSequence p0){ return 0; } + public static CharMatcher any(){ return null; } + public static CharMatcher anyOf(CharSequence p0){ return null; } + public static CharMatcher ascii(){ return null; } + public static CharMatcher breakingWhitespace(){ return null; } + public static CharMatcher digit(){ return null; } + public static CharMatcher forPredicate(Predicate p0){ return null; } + public static CharMatcher inRange(char p0, char p1){ return null; } + public static CharMatcher invisible(){ return null; } + public static CharMatcher is(char p0){ return null; } + public static CharMatcher isNot(char p0){ return null; } + public static CharMatcher javaDigit(){ return null; } + public static CharMatcher javaIsoControl(){ return null; } + public static CharMatcher javaLetter(){ return null; } + public static CharMatcher javaLetterOrDigit(){ return null; } + public static CharMatcher javaLowerCase(){ return null; } + public static CharMatcher javaUpperCase(){ return null; } + public static CharMatcher none(){ return null; } + public static CharMatcher noneOf(CharSequence p0){ return null; } + public static CharMatcher singleWidth(){ return null; } + public static CharMatcher whitespace(){ return null; } +} diff --git a/java/ql/test/stubs/guava-30.0/com/google/common/base/Splitter.java b/java/ql/test/stubs/guava-30.0/com/google/common/base/Splitter.java index 521b6a605a5..0575f99cffd 100644 --- a/java/ql/test/stubs/guava-30.0/com/google/common/base/Splitter.java +++ b/java/ql/test/stubs/guava-30.0/com/google/common/base/Splitter.java @@ -1,48 +1,35 @@ -/* - * Copyright (C) 2009 The Guava Authors - * - * Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except - * in compliance with the License. You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software distributed under the License - * is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express - * or implied. See the License for the specific language governing permissions and limitations under - * the License. - */ +// Generated automatically from com.google.common.base.Splitter for testing purposes package com.google.common.base; -import java.util.Iterator; +import com.google.common.base.CharMatcher; import java.util.List; import java.util.Map; +import java.util.regex.Pattern; +import java.util.stream.Stream; -public final class Splitter { - - public static Splitter on(final String separator) { - return null; - } - - public Splitter omitEmptyStrings() { - return null; - } - - public Iterable split(final CharSequence sequence) { - return null; - } - - public List splitToList(CharSequence sequence) { - return null; - } - - public MapSplitter withKeyValueSeparator(String separator) { - return null; - } - - public static final class MapSplitter { - public Map split(CharSequence sequence) { - return null; +public class Splitter +{ + protected Splitter() {} + public Iterable split(CharSequence p0){ return null; } + public List splitToList(CharSequence p0){ return null; } + public Splitter limit(int p0){ return null; } + public Splitter omitEmptyStrings(){ return null; } + public Splitter trimResults(){ return null; } + public Splitter trimResults(CharMatcher p0){ return null; } + public Splitter.MapSplitter withKeyValueSeparator(Splitter p0){ return null; } + public Splitter.MapSplitter withKeyValueSeparator(String p0){ return null; } + public Splitter.MapSplitter withKeyValueSeparator(char p0){ return null; } + public Stream splitToStream(CharSequence p0){ return null; } + public static Splitter fixedLength(int p0){ return null; } + public static Splitter on(CharMatcher p0){ return null; } + public static Splitter on(Pattern p0){ return null; } + public static Splitter on(String p0){ return null; } + public static Splitter on(char p0){ return null; } + public static Splitter onPattern(String p0){ return null; } + static public class MapSplitter + { + protected MapSplitter() {} + public Map split(CharSequence p0){ return null; } } - } } diff --git a/javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtil.qll b/javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtil.qll index 6f695b5035b..8aa348bf62f 100644 --- a/javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtil.qll +++ b/javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtil.qll @@ -610,16 +610,23 @@ State after(RegExpTerm t) { or exists(RegExpGroup grp | t = grp.getAChild() | result = after(grp)) or - exists(EffectivelyStar star | t = star.getAChild() | result = before(star)) + exists(EffectivelyStar star | t = star.getAChild() | + not isPossessive(star) and + result = before(star) + ) or exists(EffectivelyPlus plus | t = plus.getAChild() | - result = before(plus) or + not isPossessive(plus) and + result = before(plus) + or result = after(plus) ) or exists(EffectivelyQuestion opt | t = opt.getAChild() | result = after(opt)) or - exists(RegExpRoot root | t = root | result = AcceptAnySuffix(root)) + exists(RegExpRoot root | t = root | + if matchesAnySuffix(root) then result = AcceptAnySuffix(root) else result = Accept(root) + ) } /** @@ -690,7 +697,7 @@ predicate delta(State q1, EdgeLabel lbl, State q2) { lbl = Epsilon() and q2 = Accept(root) ) or - exists(RegExpRoot root | q1 = Match(root, 0) | lbl = Any() and q2 = q1) + exists(RegExpRoot root | q1 = Match(root, 0) | matchesAnyPrefix(root) and lbl = Any() and q2 = q1) or exists(RegExpDollar dollar | q1 = before(dollar) | lbl = Epsilon() and q2 = Accept(getRoot(dollar)) diff --git a/javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtilSpecific.qll b/javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtilSpecific.qll index 4f247b0ce50..d363e25d83d 100644 --- a/javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtilSpecific.qll +++ b/javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtilSpecific.qll @@ -12,6 +12,24 @@ predicate isEscapeClass(RegExpTerm term, string clazz) { exists(RegExpCharacterClassEscape escape | term = escape | escape.getValue() = clazz) } +/** + * Holds if `term` is a possessive quantifier. + * As javascript's regexes do not support possessive quantifiers, this never holds, but is used by the shared library. + */ +predicate isPossessive(RegExpQuantifier term) { none() } + +/** + * Holds if the regex that `term` is part of is used in a way that ignores any leading prefix of the input it's matched against. + * Not yet implemented for Javascript. + */ +predicate matchesAnyPrefix(RegExpTerm term) { any() } + +/** + * Holds if the regex that `term` is part of is used in a way that ignores any trailing suffix of the input it's matched against. + * Not yet implemented for Javascript. + */ +predicate matchesAnySuffix(RegExpTerm term) { any() } + /** * Holds if the regular expression should not be considered. * diff --git a/python/ql/lib/semmle/python/security/performance/ReDoSUtil.qll b/python/ql/lib/semmle/python/security/performance/ReDoSUtil.qll index 6f695b5035b..8aa348bf62f 100644 --- a/python/ql/lib/semmle/python/security/performance/ReDoSUtil.qll +++ b/python/ql/lib/semmle/python/security/performance/ReDoSUtil.qll @@ -610,16 +610,23 @@ State after(RegExpTerm t) { or exists(RegExpGroup grp | t = grp.getAChild() | result = after(grp)) or - exists(EffectivelyStar star | t = star.getAChild() | result = before(star)) + exists(EffectivelyStar star | t = star.getAChild() | + not isPossessive(star) and + result = before(star) + ) or exists(EffectivelyPlus plus | t = plus.getAChild() | - result = before(plus) or + not isPossessive(plus) and + result = before(plus) + or result = after(plus) ) or exists(EffectivelyQuestion opt | t = opt.getAChild() | result = after(opt)) or - exists(RegExpRoot root | t = root | result = AcceptAnySuffix(root)) + exists(RegExpRoot root | t = root | + if matchesAnySuffix(root) then result = AcceptAnySuffix(root) else result = Accept(root) + ) } /** @@ -690,7 +697,7 @@ predicate delta(State q1, EdgeLabel lbl, State q2) { lbl = Epsilon() and q2 = Accept(root) ) or - exists(RegExpRoot root | q1 = Match(root, 0) | lbl = Any() and q2 = q1) + exists(RegExpRoot root | q1 = Match(root, 0) | matchesAnyPrefix(root) and lbl = Any() and q2 = q1) or exists(RegExpDollar dollar | q1 = before(dollar) | lbl = Epsilon() and q2 = Accept(getRoot(dollar)) diff --git a/python/ql/lib/semmle/python/security/performance/ReDoSUtilSpecific.qll b/python/ql/lib/semmle/python/security/performance/ReDoSUtilSpecific.qll index 4193fd5a1e5..bc495f88c3c 100644 --- a/python/ql/lib/semmle/python/security/performance/ReDoSUtilSpecific.qll +++ b/python/ql/lib/semmle/python/security/performance/ReDoSUtilSpecific.qll @@ -13,6 +13,24 @@ predicate isEscapeClass(RegExpTerm term, string clazz) { exists(RegExpCharacterClassEscape escape | term = escape | escape.getValue() = clazz) } +/** + * Holds if `term` is a possessive quantifier. + * As python's regexes do not support possessive quantifiers, this never holds, but is used by the shared library. + */ +predicate isPossessive(RegExpQuantifier term) { none() } + +/** + * Holds if the regex that `term` is part of is used in a way that ignores any leading prefix of the input it's matched against. + * Not yet implemented for Python. + */ +predicate matchesAnyPrefix(RegExpTerm term) { any() } + +/** + * Holds if the regex that `term` is part of is used in a way that ignores any trailing suffix of the input it's matched against. + * Not yet implemented for Python. + */ +predicate matchesAnySuffix(RegExpTerm term) { any() } + /** * Holds if the regular expression should not be considered. * diff --git a/ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtil.qll b/ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtil.qll index 6f695b5035b..8aa348bf62f 100644 --- a/ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtil.qll +++ b/ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtil.qll @@ -610,16 +610,23 @@ State after(RegExpTerm t) { or exists(RegExpGroup grp | t = grp.getAChild() | result = after(grp)) or - exists(EffectivelyStar star | t = star.getAChild() | result = before(star)) + exists(EffectivelyStar star | t = star.getAChild() | + not isPossessive(star) and + result = before(star) + ) or exists(EffectivelyPlus plus | t = plus.getAChild() | - result = before(plus) or + not isPossessive(plus) and + result = before(plus) + or result = after(plus) ) or exists(EffectivelyQuestion opt | t = opt.getAChild() | result = after(opt)) or - exists(RegExpRoot root | t = root | result = AcceptAnySuffix(root)) + exists(RegExpRoot root | t = root | + if matchesAnySuffix(root) then result = AcceptAnySuffix(root) else result = Accept(root) + ) } /** @@ -690,7 +697,7 @@ predicate delta(State q1, EdgeLabel lbl, State q2) { lbl = Epsilon() and q2 = Accept(root) ) or - exists(RegExpRoot root | q1 = Match(root, 0) | lbl = Any() and q2 = q1) + exists(RegExpRoot root | q1 = Match(root, 0) | matchesAnyPrefix(root) and lbl = Any() and q2 = q1) or exists(RegExpDollar dollar | q1 = before(dollar) | lbl = Epsilon() and q2 = Accept(getRoot(dollar)) diff --git a/ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtilSpecific.qll b/ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtilSpecific.qll index de125f4a9db..8d6b14607e0 100644 --- a/ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtilSpecific.qll +++ b/ruby/ql/lib/codeql/ruby/security/performance/ReDoSUtilSpecific.qll @@ -33,6 +33,24 @@ predicate isExcluded(RegExpParent parent) { parent.(RegExpTerm).getRegExp().(AST::RegExpLiteral).hasFreeSpacingFlag() // exclude free-spacing mode regexes } +/** + * Holds if `term` is a possessive quantifier. + * Not currently implemented, but is used by the shared library. + */ +predicate isPossessive(RegExpQuantifier term) { none() } + +/** + * Holds if the regex that `term` is part of is used in a way that ignores any leading prefix of the input it's matched against. + * Not yet implemented for Ruby. + */ +predicate matchesAnyPrefix(RegExpTerm term) { any() } + +/** + * Holds if the regex that `term` is part of is used in a way that ignores any trailing suffix of the input it's matched against. + * Not yet implemented for Ruby. + */ +predicate matchesAnySuffix(RegExpTerm term) { any() } + /** * A module containing predicates for determining which flags a regular expression have. */