Skip to content

Commit 9abd225

Browse files
aschackmullaschackmull
authored
Merge pull request #9381 from aschackmull/redos/perf
ReDoS: Improve performance in ExponentialBackTracking.qll.
2 parents 4f3751d + e36c59b commit 9abd225

File tree

4 files changed

+96
-84
lines changed

4 files changed

+96
-84
lines changed

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

Lines changed: 24 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -141,26 +141,28 @@ private class StatePair extends TStatePair {
141141
}
142142

143143
/**
144-
* Holds for all constructed state pairs.
144+
* Holds for `(fork, fork)` state pairs when `isFork(fork, _, _, _, _)` holds.
145145
*
146-
* Used in `statePairDist`
146+
* Used in `statePairDistToFork`
147147
*/
148-
private predicate isStatePair(StatePair p) { any() }
148+
private predicate isStatePairFork(StatePair p) {
149+
exists(State fork | p = MkStatePair(fork, fork) and isFork(fork, _, _, _, _))
150+
}
149151

150152
/**
151153
* Holds if there are transitions from the components of `q` to the corresponding
152154
* components of `r`.
153155
*
154-
* Used in `statePairDist`
156+
* Used in `statePairDistToFork`
155157
*/
156-
private predicate delta2(StatePair q, StatePair r) { step(q, _, _, r) }
158+
private predicate reverseStep(StatePair r, StatePair q) { step(q, _, _, r) }
157159

158160
/**
159161
* Gets the minimum length of a path from `q` to `r` in the
160162
* product automaton.
161163
*/
162-
private int statePairDist(StatePair q, StatePair r) =
163-
shortestDistances(isStatePair/1, delta2/2)(q, r, result)
164+
private int statePairDistToFork(StatePair q, StatePair r) =
165+
shortestDistances(isStatePairFork/1, reverseStep/2)(r, q, result)
164166

165167
/**
166168
* Holds if there are transitions from `q` to `r1` and from `q` to `r2`
@@ -255,14 +257,7 @@ private predicate step(StatePair q, InputSymbol s1, InputSymbol s2, State r1, St
255257

256258
private newtype TTrace =
257259
Nil() or
258-
Step(InputSymbol s1, InputSymbol s2, TTrace t) {
259-
exists(StatePair p |
260-
isReachableFromFork(_, p, t, _) and
261-
step(p, s1, s2, _)
262-
)
263-
or
264-
t = Nil() and isFork(_, s1, s2, _, _)
265-
}
260+
Step(InputSymbol s1, InputSymbol s2, TTrace t) { isReachableFromFork(_, _, s1, s2, t, _) }
266261

267262
/**
268263
* A list of pairs of input symbols that describe a path in the product automaton
@@ -284,20 +279,28 @@ private class Trace extends TTrace {
284279
* a path from `r` back to `(fork, fork)` with `rem` steps.
285280
*/
286281
private predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) {
282+
exists(InputSymbol s1, InputSymbol s2, Trace v |
283+
isReachableFromFork(fork, r, s1, s2, v, rem) and
284+
w = Step(s1, s2, v)
285+
)
286+
}
287+
288+
private predicate isReachableFromFork(
289+
State fork, StatePair r, InputSymbol s1, InputSymbol s2, Trace v, int rem
290+
) {
287291
// base case
288-
exists(InputSymbol s1, InputSymbol s2, State q1, State q2 |
292+
exists(State q1, State q2 |
289293
isFork(fork, s1, s2, q1, q2) and
290294
r = MkStatePair(q1, q2) and
291-
w = Step(s1, s2, Nil()) and
292-
rem = statePairDist(r, MkStatePair(fork, fork))
295+
v = Nil() and
296+
rem = statePairDistToFork(r, MkStatePair(fork, fork))
293297
)
294298
or
295299
// recursive case
296-
exists(StatePair p, Trace v, InputSymbol s1, InputSymbol s2 |
300+
exists(StatePair p |
297301
isReachableFromFork(fork, p, v, rem + 1) and
298302
step(p, s1, s2, r) and
299-
w = Step(s1, s2, v) and
300-
rem >= statePairDist(r, MkStatePair(fork, fork))
303+
rem = statePairDistToFork(r, MkStatePair(fork, fork))
301304
)
302305
}
303306

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

Lines changed: 24 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -141,26 +141,28 @@ private class StatePair extends TStatePair {
141141
}
142142

143143
/**
144-
* Holds for all constructed state pairs.
144+
* Holds for `(fork, fork)` state pairs when `isFork(fork, _, _, _, _)` holds.
145145
*
146-
* Used in `statePairDist`
146+
* Used in `statePairDistToFork`
147147
*/
148-
private predicate isStatePair(StatePair p) { any() }
148+
private predicate isStatePairFork(StatePair p) {
149+
exists(State fork | p = MkStatePair(fork, fork) and isFork(fork, _, _, _, _))
150+
}
149151

150152
/**
151153
* Holds if there are transitions from the components of `q` to the corresponding
152154
* components of `r`.
153155
*
154-
* Used in `statePairDist`
156+
* Used in `statePairDistToFork`
155157
*/
156-
private predicate delta2(StatePair q, StatePair r) { step(q, _, _, r) }
158+
private predicate reverseStep(StatePair r, StatePair q) { step(q, _, _, r) }
157159

158160
/**
159161
* Gets the minimum length of a path from `q` to `r` in the
160162
* product automaton.
161163
*/
162-
private int statePairDist(StatePair q, StatePair r) =
163-
shortestDistances(isStatePair/1, delta2/2)(q, r, result)
164+
private int statePairDistToFork(StatePair q, StatePair r) =
165+
shortestDistances(isStatePairFork/1, reverseStep/2)(r, q, result)
164166

165167
/**
166168
* Holds if there are transitions from `q` to `r1` and from `q` to `r2`
@@ -255,14 +257,7 @@ private predicate step(StatePair q, InputSymbol s1, InputSymbol s2, State r1, St
255257

256258
private newtype TTrace =
257259
Nil() or
258-
Step(InputSymbol s1, InputSymbol s2, TTrace t) {
259-
exists(StatePair p |
260-
isReachableFromFork(_, p, t, _) and
261-
step(p, s1, s2, _)
262-
)
263-
or
264-
t = Nil() and isFork(_, s1, s2, _, _)
265-
}
260+
Step(InputSymbol s1, InputSymbol s2, TTrace t) { isReachableFromFork(_, _, s1, s2, t, _) }
266261

267262
/**
268263
* A list of pairs of input symbols that describe a path in the product automaton
@@ -284,20 +279,28 @@ private class Trace extends TTrace {
284279
* a path from `r` back to `(fork, fork)` with `rem` steps.
285280
*/
286281
private predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) {
282+
exists(InputSymbol s1, InputSymbol s2, Trace v |
283+
isReachableFromFork(fork, r, s1, s2, v, rem) and
284+
w = Step(s1, s2, v)
285+
)
286+
}
287+
288+
private predicate isReachableFromFork(
289+
State fork, StatePair r, InputSymbol s1, InputSymbol s2, Trace v, int rem
290+
) {
287291
// base case
288-
exists(InputSymbol s1, InputSymbol s2, State q1, State q2 |
292+
exists(State q1, State q2 |
289293
isFork(fork, s1, s2, q1, q2) and
290294
r = MkStatePair(q1, q2) and
291-
w = Step(s1, s2, Nil()) and
292-
rem = statePairDist(r, MkStatePair(fork, fork))
295+
v = Nil() and
296+
rem = statePairDistToFork(r, MkStatePair(fork, fork))
293297
)
294298
or
295299
// recursive case
296-
exists(StatePair p, Trace v, InputSymbol s1, InputSymbol s2 |
300+
exists(StatePair p |
297301
isReachableFromFork(fork, p, v, rem + 1) and
298302
step(p, s1, s2, r) and
299-
w = Step(s1, s2, v) and
300-
rem >= statePairDist(r, MkStatePair(fork, fork))
303+
rem = statePairDistToFork(r, MkStatePair(fork, fork))
301304
)
302305
}
303306

‎python/ql/lib/semmle/python/security/performance/ExponentialBackTracking.qll‎

Lines changed: 24 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -141,26 +141,28 @@ private class StatePair extends TStatePair {
141141
}
142142

143143
/**
144-
* Holds for all constructed state pairs.
144+
* Holds for `(fork, fork)` state pairs when `isFork(fork, _, _, _, _)` holds.
145145
*
146-
* Used in `statePairDist`
146+
* Used in `statePairDistToFork`
147147
*/
148-
private predicate isStatePair(StatePair p) { any() }
148+
private predicate isStatePairFork(StatePair p) {
149+
exists(State fork | p = MkStatePair(fork, fork) and isFork(fork, _, _, _, _))
150+
}
149151

150152
/**
151153
* Holds if there are transitions from the components of `q` to the corresponding
152154
* components of `r`.
153155
*
154-
* Used in `statePairDist`
156+
* Used in `statePairDistToFork`
155157
*/
156-
private predicate delta2(StatePair q, StatePair r) { step(q, _, _, r) }
158+
private predicate reverseStep(StatePair r, StatePair q) { step(q, _, _, r) }
157159

158160
/**
159161
* Gets the minimum length of a path from `q` to `r` in the
160162
* product automaton.
161163
*/
162-
private int statePairDist(StatePair q, StatePair r) =
163-
shortestDistances(isStatePair/1, delta2/2)(q, r, result)
164+
private int statePairDistToFork(StatePair q, StatePair r) =
165+
shortestDistances(isStatePairFork/1, reverseStep/2)(r, q, result)
164166

165167
/**
166168
* Holds if there are transitions from `q` to `r1` and from `q` to `r2`
@@ -255,14 +257,7 @@ private predicate step(StatePair q, InputSymbol s1, InputSymbol s2, State r1, St
255257

256258
private newtype TTrace =
257259
Nil() or
258-
Step(InputSymbol s1, InputSymbol s2, TTrace t) {
259-
exists(StatePair p |
260-
isReachableFromFork(_, p, t, _) and
261-
step(p, s1, s2, _)
262-
)
263-
or
264-
t = Nil() and isFork(_, s1, s2, _, _)
265-
}
260+
Step(InputSymbol s1, InputSymbol s2, TTrace t) { isReachableFromFork(_, _, s1, s2, t, _) }
266261

267262
/**
268263
* A list of pairs of input symbols that describe a path in the product automaton
@@ -284,20 +279,28 @@ private class Trace extends TTrace {
284279
* a path from `r` back to `(fork, fork)` with `rem` steps.
285280
*/
286281
private predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) {
282+
exists(InputSymbol s1, InputSymbol s2, Trace v |
283+
isReachableFromFork(fork, r, s1, s2, v, rem) and
284+
w = Step(s1, s2, v)
285+
)
286+
}
287+
288+
private predicate isReachableFromFork(
289+
State fork, StatePair r, InputSymbol s1, InputSymbol s2, Trace v, int rem
290+
) {
287291
// base case
288-
exists(InputSymbol s1, InputSymbol s2, State q1, State q2 |
292+
exists(State q1, State q2 |
289293
isFork(fork, s1, s2, q1, q2) and
290294
r = MkStatePair(q1, q2) and
291-
w = Step(s1, s2, Nil()) and
292-
rem = statePairDist(r, MkStatePair(fork, fork))
295+
v = Nil() and
296+
rem = statePairDistToFork(r, MkStatePair(fork, fork))
293297
)
294298
or
295299
// recursive case
296-
exists(StatePair p, Trace v, InputSymbol s1, InputSymbol s2 |
300+
exists(StatePair p |
297301
isReachableFromFork(fork, p, v, rem + 1) and
298302
step(p, s1, s2, r) and
299-
w = Step(s1, s2, v) and
300-
rem >= statePairDist(r, MkStatePair(fork, fork))
303+
rem = statePairDistToFork(r, MkStatePair(fork, fork))
301304
)
302305
}
303306

‎ruby/ql/lib/codeql/ruby/security/performance/ExponentialBackTracking.qll‎

Lines changed: 24 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -141,26 +141,28 @@ private class StatePair extends TStatePair {
141141
}
142142

143143
/**
144-
* Holds for all constructed state pairs.
144+
* Holds for `(fork, fork)` state pairs when `isFork(fork, _, _, _, _)` holds.
145145
*
146-
* Used in `statePairDist`
146+
* Used in `statePairDistToFork`
147147
*/
148-
private predicate isStatePair(StatePair p) { any() }
148+
private predicate isStatePairFork(StatePair p) {
149+
exists(State fork | p = MkStatePair(fork, fork) and isFork(fork, _, _, _, _))
150+
}
149151

150152
/**
151153
* Holds if there are transitions from the components of `q` to the corresponding
152154
* components of `r`.
153155
*
154-
* Used in `statePairDist`
156+
* Used in `statePairDistToFork`
155157
*/
156-
private predicate delta2(StatePair q, StatePair r) { step(q, _, _, r) }
158+
private predicate reverseStep(StatePair r, StatePair q) { step(q, _, _, r) }
157159

158160
/**
159161
* Gets the minimum length of a path from `q` to `r` in the
160162
* product automaton.
161163
*/
162-
private int statePairDist(StatePair q, StatePair r) =
163-
shortestDistances(isStatePair/1, delta2/2)(q, r, result)
164+
private int statePairDistToFork(StatePair q, StatePair r) =
165+
shortestDistances(isStatePairFork/1, reverseStep/2)(r, q, result)
164166

165167
/**
166168
* Holds if there are transitions from `q` to `r1` and from `q` to `r2`
@@ -255,14 +257,7 @@ private predicate step(StatePair q, InputSymbol s1, InputSymbol s2, State r1, St
255257

256258
private newtype TTrace =
257259
Nil() or
258-
Step(InputSymbol s1, InputSymbol s2, TTrace t) {
259-
exists(StatePair p |
260-
isReachableFromFork(_, p, t, _) and
261-
step(p, s1, s2, _)
262-
)
263-
or
264-
t = Nil() and isFork(_, s1, s2, _, _)
265-
}
260+
Step(InputSymbol s1, InputSymbol s2, TTrace t) { isReachableFromFork(_, _, s1, s2, t, _) }
266261

267262
/**
268263
* A list of pairs of input symbols that describe a path in the product automaton
@@ -284,20 +279,28 @@ private class Trace extends TTrace {
284279
* a path from `r` back to `(fork, fork)` with `rem` steps.
285280
*/
286281
private predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) {
282+
exists(InputSymbol s1, InputSymbol s2, Trace v |
283+
isReachableFromFork(fork, r, s1, s2, v, rem) and
284+
w = Step(s1, s2, v)
285+
)
286+
}
287+
288+
private predicate isReachableFromFork(
289+
State fork, StatePair r, InputSymbol s1, InputSymbol s2, Trace v, int rem
290+
) {
287291
// base case
288-
exists(InputSymbol s1, InputSymbol s2, State q1, State q2 |
292+
exists(State q1, State q2 |
289293
isFork(fork, s1, s2, q1, q2) and
290294
r = MkStatePair(q1, q2) and
291-
w = Step(s1, s2, Nil()) and
292-
rem = statePairDist(r, MkStatePair(fork, fork))
295+
v = Nil() and
296+
rem = statePairDistToFork(r, MkStatePair(fork, fork))
293297
)
294298
or
295299
// recursive case
296-
exists(StatePair p, Trace v, InputSymbol s1, InputSymbol s2 |
300+
exists(StatePair p |
297301
isReachableFromFork(fork, p, v, rem + 1) and
298302
step(p, s1, s2, r) and
299-
w = Step(s1, s2, v) and
300-
rem >= statePairDist(r, MkStatePair(fork, fork))
303+
rem = statePairDistToFork(r, MkStatePair(fork, fork))
301304
)
302305
}
303306

0 commit comments

Comments
 (0)