make ReDoSPruning into a parameterized module

Author: erik-krogh

java/ql/lib/semmle/code/java/security/performance/ExponentialBackTracking.qll

@@ -364,11 +364,5 @@ private predicate isPumpable(State fork, string w) {
   )
 }
 
-/**
- * An instantiation of `ReDoSConfiguration` for exponential backtracking.
- */
-class ExponentialReDoSConfiguration extends ReDoSConfiguration {
-  ExponentialReDoSConfiguration() { this = "ExponentialReDoSConfiguration" }
-
-  override predicate isReDoSCandidate(State state, string pump) { isPumpable(state, pump) }
-}
+/** Holds if `state` has exponential ReDoS */
+predicate hasReDoSResult = ReDoSPruning<isPumpable/2>::hasReDoSResult/4;

java/ql/lib/semmle/code/java/security/performance/ReDoSUtil.qll

@@ -838,38 +838,32 @@ predicate isStartState(State state) {
 }
 
 /**
- * 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.
+ * Holds if `state` is a candidate for ReDoS with string `pump`.
  */
-abstract class ReDoSConfiguration extends string {
-  bindingset[this]
-  ReDoSConfiguration() { any() }
+signature predicate isCandidateSig(State state, string pump);
 
-  /**
-   * 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);
-}
-
-module ReDoSPruning {
+/**
+ * A module for pruning candidate ReDoS states.
+ * The candidates are specified by the `isCandidate` signature predicate.
+ * The candidates are checked for rejecting suffixes and deduplicated,
+ * and the resulting ReDoS states are read by the `hasReDoSResult` predicate.
+ */
+module ReDoSPruning<isCandidateSig/2 isCandidate> {
   /**
    * 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
+    isCandidate(state, pump) and
     (
-      not any(ReDoSConfiguration conf).isReDoSCandidate(epsilonSucc+(state), _)
+      not isCandidate(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
+          isCandidate(s, _) and
           s.getRepr() instanceof InfiniteRepetitionQuantifier
         |
           s order by l.getStartLine(), l.getStartColumn(), l.getEndColumn(), l.getEndLine()
@@ -887,8 +881,11 @@ module ReDoSPruning {
     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()
+          max(State s, Location l |
+            s = stateInPumpableRegexp() and
+            isStartState(s) and
+            getRoot(s.getRepr()) = root and
+            l = s.getRepr().getLocation()
           |
             s
             order by
@@ -957,14 +954,10 @@ module ReDoSPruning {
         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()))
-      }
+    /** Gets a state within a regular expression that has a pumpable state. */
+    pragma[noinline]
+    State stateInPumpableRegexp() {
+      exists(State s | isReDoSCandidate(s, _) | getRoot(s.getRepr()) = getRoot(result.getRepr()))
     }
   }
 
@@ -1002,26 +995,32 @@ module ReDoSPruning {
      * 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)
+    private predicate isLikelyRejectable(State s) {
+      s = stateInPumpableRegexp() and
+      (
+        // 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(_) }
+    predicate isRejectState(State s) {
+      s = stateInPumpableRegexp() and 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) {
+    predicate hasEdgeToLikelyRejectable(State s) {
+      s = stateInPumpableRegexp() and
       // 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) |
@@ -1036,7 +1035,8 @@ module ReDoSPruning {
      * and `s` has not been found to be rejectable by `hasRejectEdge` or `isRejectState`.
      */
     pragma[noinline]
-    private string hasEdgeToLikelyRejectableHelper(StateInPumpableRegexp s) {
+    private string hasEdgeToLikelyRejectableHelper(State s) {
+      s = stateInPumpableRegexp() and
       not hasRejectEdge(s) and
       not isRejectState(s) and
       deltaClosedChar(s, result, _)
@@ -1047,7 +1047,9 @@ module ReDoSPruning {
      * 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) {
+    predicate deltaClosedChar(State prev, string char, State next) {
+      prev = stateInPumpableRegexp() and
+      next = stateInPumpableRegexp() and
       deltaClosed(prev, getAnInputSymbolMatchingRelevant(char), next)
     }
 
@@ -1148,7 +1150,7 @@ module ReDoSPruning {
     exists(int i, string c | s = Match(term, i) |
       c =
         min(string w |
-          any(ReDoSConfiguration conf).isReDoSCandidate(s, w) and
+          isCandidate(s, w) and
           SuffixConstruction::reachesOnlyRejectableSuffixes(s, w)
         |
           w order by w.length(), w
@@ -1173,28 +1175,28 @@ module ReDoSPruning {
       not exists(PrefixConstruction::prefix(s)) and prefixMsg = ""
     )
   }
-}
 
-/**
- * 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 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)
+  /**
+   * 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)
+  }
 }

java/ql/lib/semmle/code/java/security/performance/SuperlinearBackTracking.qll

@@ -42,15 +42,6 @@ import ReDoSUtil
  * 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.
  */
@@ -386,12 +377,17 @@ predicate isPumpable(State pivot, State succ, string pump) {
   )
 }
 
+/**
+ * Holds if states starting in `state` can have polynomial backtracking with the string `pump`.
+ */
+predicate isReDoSCandidate(State state, string pump) { isPumpable(_, state, pump) }
+
 /**
  * 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 |
-    ReDoSPruning::hasReDoSResult(t, pump, s, prefixMsg) and
+    ReDoSPruning<isReDoSCandidate/2>::hasReDoSResult(t, pump, s, prefixMsg) and
     isPumpable(pivot, s, _) and
     prev = pivot.getRepr()
   )

java/ql/test/query-tests/security/CWE-730/ReDoS.ql

@@ -11,7 +11,7 @@ class HasExpRedos extends InlineExpectationsTest {
   override predicate hasActualResult(Location location, string element, string tag, string value) {
     tag = "hasExpRedos" and
     exists(RegExpTerm t, string pump, State s, string prefixMsg |
-      ReDoSPruning::hasReDoSResult(t, pump, s, prefixMsg) and
+      hasReDoSResult(t, pump, s, prefixMsg) and
       not t.getRegex().getAMode() = "VERBOSE" and
       value = "" and
       location = t.getLocation() and

javascript/ql/lib/semmle/javascript/security/performance/ExponentialBackTracking.qll

@@ -364,11 +364,5 @@ private predicate isPumpable(State fork, string w) {
   )
 }
 
-/**
- * An instantiation of `ReDoSConfiguration` for exponential backtracking.
- */
-class ExponentialReDoSConfiguration extends ReDoSConfiguration {
-  ExponentialReDoSConfiguration() { this = "ExponentialReDoSConfiguration" }
-
-  override predicate isReDoSCandidate(State state, string pump) { isPumpable(state, pump) }
-}
+/** Holds if `state` has exponential ReDoS */
+predicate hasReDoSResult = ReDoSPruning<isPumpable/2>::hasReDoSResult/4;