Merge pull request #227 from xiemaisi/js/taint-kinds

JavaScript: Add support for state-based taint tracking.
2026-04-29 18:55:14 +02:00 · 2018-10-08 15:09:12 +01:00
parent 2904ebb8a3 335adee69c
commit d2af4ab94a
15 changed files with 290 additions and 144 deletions
--- a/javascript/ql/src/Security/CWE-078/CommandInjection.ql
+++ b/javascript/ql/src/Security/CWE-078/CommandInjection.ql
@@ -17,5 +17,8 @@ import semmle.javascript.security.dataflow.CommandInjection::CommandInjection

 from Configuration cfg, DataFlow::Node source, DataFlow::Node sink, DataFlow::Node highlight
 where cfg.hasFlow(source, sink) and
-      if cfg.isSink(sink, _) then cfg.isSink(sink, highlight) else highlight = sink
+      if cfg.isSinkWithHighlight(sink, _) then
+        cfg.isSinkWithHighlight(sink, highlight)
+      else
+        highlight = sink
 select highlight, "This command depends on $@.", source, "a user-provided value"
--- a/javascript/ql/src/semmle/javascript/dataflow/Configuration.qll
+++ b/javascript/ql/src/semmle/javascript/dataflow/Configuration.qll
@@ -88,15 +88,35 @@ abstract class Configuration extends string {
  /**
   * Holds if `source` is a relevant data flow source for this configuration.
   */
-  abstract predicate isSource(DataFlow::Node source);
+  predicate isSource(DataFlow::Node source) {
+    none()
+  }
+
+  /**
+   * Holds if `source` is a source of flow labelled with `lbl` that is relevant
+   * for this configuration.
+   */
+  predicate isSource(DataFlow::Node source, FlowLabel lbl) {
+    none()
+  }

  /**
   * Holds if `sink` is a relevant data flow sink for this configuration.
   */
-  abstract predicate isSink(DataFlow::Node sink);
+  predicate isSink(DataFlow::Node sink) {
+    none()
+  }

  /**
-   * Holds if `source -> sink` should be considered as a flow edge
+   * Holds if `sink` is a sink of flow labelled with `lbl` that is relevant
+   * for this configuration.
+   */
+  predicate isSink(DataFlow::Node sink, FlowLabel lbl) {
+    none()
+  }
+
+  /**
+   * Holds if `src -> trg` should be considered as a flow edge
   * in addition to standard data flow edges.
   */
  predicate isAdditionalFlowStep(DataFlow::Node src, DataFlow::Node trg) { none() }
@@ -105,7 +125,7 @@ abstract class Configuration extends string {
   * INTERNAL: This predicate should not normally be used outside the data flow
   * library.
   *
-   * Holds if `source -> sink` should be considered as a flow edge
+   * Holds if `src -> trg` should be considered as a flow edge
   * in addition to standard data flow edges, with `valuePreserving`
   * indicating whether the step preserves values or just taintedness.
   */
@@ -113,6 +133,14 @@ abstract class Configuration extends string {
    isAdditionalFlowStep(src, trg) and valuePreserving = true
  }

+  /**
+   * Holds if `src -> trg` is a flow edge converting flow with label `inlbl` to
+   * flow with label `outlbl`.
+   */
+  predicate isAdditionalFlowStep(DataFlow::Node src, DataFlow::Node trg, FlowLabel inlbl, FlowLabel outlbl) {
+    none()
+  }
+
  /**
   * Holds if the intermediate flow node `node` is prohibited.
   */
@@ -128,6 +156,11 @@ abstract class Configuration extends string {
   */
  predicate isBarrier(DataFlow::Node src, DataFlow::Node trg) { none() }

+  /**
+   * Holds if flow with label `lbl` cannot flow from `src` to `trg`.
+   */
+  predicate isBarrier(DataFlow::Node src, DataFlow::Node trg, FlowLabel lbl) { none() }
+
  /**
   * Holds if data flow node `guard` can act as a barrier when appearing
   * in a condition.
@@ -142,7 +175,7 @@ abstract class Configuration extends string {
   * Holds if data may flow from `source` to `sink` for this configuration.
   */
  predicate hasFlow(DataFlow::Node source, DataFlow::Node sink) {
-    isSource(_, this) and isSink(_, this) and
+    isSource(_, this, _) and isSink(_, this, _) and
    exists (SourcePathNode flowsource, SinkPathNode flowsink |
      hasPathFlow(flowsource, flowsink) and
      source = flowsource.getNode() and
@@ -176,6 +209,44 @@ abstract class Configuration extends string {
  }
 }

+/**
+ * A label describing the kind of information tracked by a flow configuration.
+ *
+ * There are two standard labels "data" and "taint", the former describing values
+ * that directly originate from a flow source, the latter values that are derived
+ * from a flow source via one or more transformations (such as string operations).
+ */
+abstract class FlowLabel extends string {
+  bindingset[this] FlowLabel() { any() }
+}
+
+/**
+ * A kind of taint tracked by a taint-tracking configuration.
+ *
+ * This is an alias of `FlowLabel`, so the two types can be used interchangeably.
+ */
+class TaintKind = FlowLabel;
+
+/**
+ * A standard flow label, that is, either `FlowLabel::data()` or `FlowLabel::taint()`.
+ */
+private class StandardFlowLabel extends FlowLabel {
+  StandardFlowLabel() { this = "data" or this = "taint" }
+}
+
+module FlowLabel {
+  /**
+   * Gets the standard flow label for describing values that directly originate from a flow source.
+   */
+  FlowLabel data() { result = "data" }
+
+  /**
+   * Gets the standard flow label for describing values that are influenced ("tainted") by a flow
+   * source, but not necessarily directly derived from it.
+   */
+  FlowLabel taint() { result = "taint" }
+}
+
 /**
 * A node that can act as a barrier when appearing in a condition.
 *
@@ -353,26 +424,27 @@ private predicate basicFlowStep(DataFlow::Node pred, DataFlow::Node succ, PathSu
  isRelevantForward(pred, cfg) and
  (
   // Local flow
-   exists (boolean valuePreserving |
-     localFlowStep(pred, succ, cfg, valuePreserving) and
-     summary = PathSummary::level(valuePreserving)
+   exists (FlowLabel predlbl, FlowLabel succlbl |
+     localFlowStep(pred, succ, cfg, predlbl, succlbl) and
+     not cfg.isBarrier(pred, succ, predlbl) and
+     summary = MkPathSummary(false, false, predlbl, succlbl)
   )
   or
   // Flow through properties of objects
   propertyFlowStep(pred, succ) and
-   summary = PathSummary::level(true)
+   summary = PathSummary::level()
   or
   // Flow through global variables
   globalFlowStep(pred, succ) and
-   summary = PathSummary::level(true)
+   summary = PathSummary::level()
   or
   // Flow into function
   callStep(pred, succ) and
-   summary = PathSummary::call(true)
+   summary = PathSummary::call()
   or
   // Flow out of function
   returnStep(pred, succ) and
-   summary = PathSummary::return(true)
+   summary = PathSummary::return()
  )
 }

@@ -393,15 +465,21 @@ private predicate exploratoryFlowStep(DataFlow::Node pred, DataFlow::Node succ,
 /**
 * Holds if `nd` is a source node for configuration `cfg`.
 */
-private predicate isSource(DataFlow::Node nd, DataFlow::Configuration cfg) {
-  cfg.isSource(nd) or nd.(AdditionalSource).isSourceFor(cfg)
+private predicate isSource(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLabel lbl) {
+  (cfg.isSource(nd) or nd.(AdditionalSource).isSourceFor(cfg)) and
+  lbl = FlowLabel::data()
+  or
+  cfg.isSource(nd, lbl)
 }

 /**
 * Holds if `nd` is a sink node for configuration `cfg`.
 */
-private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg) {
-  cfg.isSink(nd) or nd.(AdditionalSink).isSinkFor(cfg)
+private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLabel lbl) {
+  (cfg.isSink(nd) or nd.(AdditionalSink).isSinkFor(cfg)) and
+  lbl = any(StandardFlowLabel f)
+  or
+  cfg.isSink(nd, lbl)
 }

 /**
@@ -410,7 +488,7 @@ private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg) {
 * No call/return matching is done, so this is a relatively coarse over-approximation.
 */
 private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration cfg) {
-  isSource(nd, cfg)
+  isSource(nd, cfg, _)
  or
  exists (DataFlow::Node mid |
    isRelevantForward(mid, cfg) and exploratoryFlowStep(mid, nd, cfg)
@@ -424,7 +502,7 @@ private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration c
 */
 private predicate isRelevant(DataFlow::Node nd, DataFlow::Configuration cfg) {
  isRelevantForward(nd, cfg) and
-  isSink(nd, cfg)
+  isSink(nd, cfg, _)
  or
  exists (DataFlow::Node mid |
    isRelevant(mid, cfg) and
@@ -472,7 +550,7 @@ private predicate reachableFromInput(Function f, DataFlow::Node invk,
                                     DataFlow::Node input, DataFlow::Node nd,
                                     DataFlow::Configuration cfg, PathSummary summary) {
  callInputStep(f, invk, input, nd, cfg) and
-  summary = PathSummary::empty()
+  summary = PathSummary::level()
  or
  exists (DataFlow::Node mid, PathSummary oldSummary, PathSummary newSummary |
    reachableFromInput(f, invk, input, mid, cfg, oldSummary) and
@@ -487,11 +565,12 @@ private predicate reachableFromInput(Function f, DataFlow::Node invk,
 * configuration `cfg`, possibly through callees.
 */
 private predicate flowThroughCall(DataFlow::Node input, DataFlow::Node invk,
-                                  DataFlow::Configuration cfg, boolean valuePreserving) {
+                                  DataFlow::Configuration cfg, PathSummary summary) {
  exists (Function f, DataFlow::ValueNode ret |
    ret.asExpr() = f.getAReturnedExpr() and
    calls(invk, f) and // Do not consider partial calls
-    reachableFromInput(f, invk, input, ret, cfg, PathSummary::level(valuePreserving))
+    reachableFromInput(f, invk, input, ret, cfg, summary) and
+    not cfg.isBarrier(ret, invk)
  )
 }

@@ -502,7 +581,7 @@ private predicate flowThroughCall(DataFlow::Node input, DataFlow::Node invk,
 private predicate storeStep(DataFlow::Node pred, DataFlow::SourceNode succ, string prop,
                            DataFlow::Configuration cfg, PathSummary summary) {
  basicStoreStep(pred, succ, prop) and
-  summary = PathSummary::level(true)
+  summary = PathSummary::level()
  or
  exists (Function f, DataFlow::Node mid, DataFlow::SourceNode base |
    // `f` stores its parameter `pred` in property `prop` of a value that it returns,
@@ -526,8 +605,7 @@ private predicate reachableFromStoreBase(string prop, DataFlow::Node rhs, DataFl
  exists (DataFlow::Node mid, PathSummary oldSummary, PathSummary newSummary |
    reachableFromStoreBase(prop, rhs, mid, cfg, oldSummary) and
    flowStep(mid, cfg, nd, newSummary) and
-    newSummary.valuePreserving() = true and
-    summary = oldSummary.append(newSummary)
+    summary = oldSummary.appendValuePreserving(newSummary)
  )
 }

@@ -557,10 +635,7 @@ private predicate flowStep(DataFlow::Node pred, DataFlow::Configuration cfg,
   or
   // Flow through a function that returns a value that depends on one of its arguments
   // or a captured variable
-   exists (boolean valuePreserving |
-     flowThroughCall(pred, succ, cfg, valuePreserving) and
-     summary = PathSummary::level(valuePreserving)
-   )
+   flowThroughCall(pred, succ, cfg, summary)
   or
   // Flow through a property write/read pair
   flowThroughProperty(pred, succ, cfg, summary)
@@ -588,9 +663,11 @@ private predicate flowsTo(PathNode flowsource, DataFlow::Node source,
 */
 private predicate reachableFromSource(DataFlow::Node nd, DataFlow::Configuration cfg,
                                      PathSummary summary) {
-  isSource(nd, cfg) and
-  not cfg.isBarrier(nd) and
-  summary = PathSummary::empty()
+  exists (FlowLabel lbl |
+    isSource(nd, cfg, lbl) and
+    not cfg.isBarrier(nd) and
+    summary = MkPathSummary(false, false, lbl, lbl)
+  )
  or
  exists (DataFlow::Node pred, PathSummary oldSummary, PathSummary newSummary |
    reachableFromSource(pred, cfg, oldSummary) and
@@ -601,21 +678,18 @@ private predicate reachableFromSource(DataFlow::Node nd, DataFlow::Configuration

 /**
 * Holds if `nd` can be reached from a source under `cfg`, and in turn a sink is
- * reachable from `nd`. The path from the source to `nd` is summarized by `summary1`,
- * the path from `nd` to the sink is summarized by `summary2`.
+ * reachable from `nd`, where the path from the source to `nd` is summarized by `summary`.
 */
 private predicate onPath(DataFlow::Node nd, DataFlow::Configuration cfg,
-                         PathSummary summary1, PathSummary summary2) {
-  reachableFromSource(nd, cfg, summary1) and
-  isSink(nd, cfg) and
-  not cfg.isBarrier(nd) and
-  summary2 = PathSummary::empty()
+                         PathSummary summary) {
+  reachableFromSource(nd, cfg, summary) and
+  isSink(nd, cfg, summary.getEndLabel()) and
+  not cfg.isBarrier(nd)
  or
-  exists (DataFlow::Node mid, PathSummary newSummary, PathSummary oldSummary |
-    onPath(mid, cfg, _, oldSummary) and
-    flowStep(nd, cfg, mid, newSummary) and
-    reachableFromSource(nd, cfg, summary1) and
-    summary2 = oldSummary.prepend(newSummary)
+  exists (DataFlow::Node mid, PathSummary stepSummary |
+    reachableFromSource(nd, cfg, summary) and
+    flowStep(nd, cfg, mid, stepSummary) and
+    onPath(mid, cfg, summary.append(stepSummary))
  )
 }

@@ -624,7 +698,7 @@ private predicate onPath(DataFlow::Node nd, DataFlow::Configuration cfg,
 */
 private newtype TPathNode =
  MkPathNode(DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary) {
-    onPath(nd, cfg, summary, _)
+    onPath(nd, cfg, summary)
  }

 /**
@@ -693,7 +767,7 @@ class PathNode extends TPathNode {
 */
 class SourcePathNode extends PathNode {
  SourcePathNode() {
-    isSource(nd, cfg)
+    isSource(nd, cfg, _)
  }
 }

@@ -702,7 +776,7 @@ class SourcePathNode extends PathNode {
 */
 class SinkPathNode extends PathNode {
  SinkPathNode() {
-    isSink(nd, cfg)
+    isSink(nd, cfg, _)
  }
 }

--- a/javascript/ql/src/semmle/javascript/dataflow/TaintTracking.qll
+++ b/javascript/ql/src/semmle/javascript/dataflow/TaintTracking.qll
@@ -38,7 +38,9 @@ module TaintTracking {
     * The smaller this predicate is, the faster `hasFlow()` will converge.
     */
    // overridden to provide taint-tracking specific qldoc
-    abstract override predicate isSource(DataFlow::Node source);
+    override predicate isSource(DataFlow::Node source) {
+      super.isSource(source)
+    }

    /**
     * Holds if `sink` is a relevant taint sink.
@@ -46,7 +48,9 @@ module TaintTracking {
     * The smaller this predicate is, the faster `hasFlow()` will converge.
     */
    // overridden to provide taint-tracking specific qldoc
-    abstract override predicate isSink(DataFlow::Node sink);
+    override predicate isSink(DataFlow::Node sink) {
+      super.isSink(sink)
+    }

    /** Holds if the intermediate node `node` is a taint sanitizer. */
    predicate isSanitizer(DataFlow::Node node) {
@@ -58,6 +62,11 @@ module TaintTracking {
      none()
    }

+    /** Holds if the edge from `source` to `sink` is a taint sanitizer for data labelled with `lbl`. */
+    predicate isSanitizer(DataFlow::Node source, DataFlow::Node sink, DataFlow::FlowLabel lbl) {
+      none()
+    }
+
    /**
     * Holds if data flow node `guard` can act as a sanitizer when appearing
     * in a condition.
@@ -82,6 +91,12 @@ module TaintTracking {
      isSanitizer(source, sink)
    }

+    final
+    override predicate isBarrier(DataFlow::Node source, DataFlow::Node sink, DataFlow::FlowLabel lbl) {
+      super.isBarrier(source, sink, lbl) or
+      isSanitizer(source, sink, lbl)
+    }
+
    final
    override predicate isBarrierGuard(DataFlow::BarrierGuardNode guard) {
      super.isBarrierGuard(guard) or
--- a/javascript/ql/src/semmle/javascript/dataflow/TrackedNodes.qll
+++ b/javascript/ql/src/semmle/javascript/dataflow/TrackedNodes.qll
@@ -70,23 +70,23 @@ private module NodeTracking {
    (
     // Local flow
     localFlowStep(pred, succ) and
-     summary = PathSummary::level(true)
+     summary = PathSummary::level()
     or
     // Flow through properties of objects
     propertyFlowStep(pred, succ) and
-     summary = PathSummary::level(true)
+     summary = PathSummary::level()
     or
     // Flow through global variables
     globalFlowStep(pred, succ) and
-     summary = PathSummary::level(true)
+     summary = PathSummary::level()
     or
     // Flow into function
     callStep(pred, succ) and
-     summary = PathSummary::call(true)
+     summary = PathSummary::call()
     or
     // Flow out of function
     returnStep(pred, succ) and
-     summary = PathSummary::return(true)
+     summary = PathSummary::return()
    )
  }

@@ -138,7 +138,7 @@ private module NodeTracking {
                                       DataFlow::Node input, DataFlow::Node nd,
                                       PathSummary summary) {
    callInputStep(f, invk, input, nd) and
-    summary = PathSummary::empty()
+    summary = PathSummary::level()
    or
    exists (DataFlow::Node mid, PathSummary oldSummary, PathSummary newSummary |
      reachableFromInput(f, invk, input, mid, oldSummary) and
@@ -165,7 +165,7 @@ private module NodeTracking {
  private predicate storeStep(DataFlow::Node pred, DataFlow::SourceNode succ, string prop,
                              PathSummary summary) {
    basicStoreStep(pred, succ, prop) and
-    summary = PathSummary::level(true)
+    summary = PathSummary::level()
    or
    exists (Function f, DataFlow::Node mid, DataFlow::SourceNode base |
      // `f` stores its parameter `pred` in property `prop` of a value that it returns,
@@ -214,7 +214,7 @@ private module NodeTracking {
    // Flow through a function that returns a value that depends on one of its arguments
    // or a captured variable
    flowThroughCall(pred, succ) and
-    summary = PathSummary::level(true)
+    summary = PathSummary::level()
    or
    // Flow through a property write/read pair
    flowThroughProperty(pred, succ, summary)
@@ -226,7 +226,7 @@ private module NodeTracking {
   */
  predicate flowsTo(TrackedNode source, DataFlow::Node nd, PathSummary summary) {
    source = nd and
-    summary = PathSummary::empty()
+    summary = PathSummary::level()
    or
    exists (DataFlow::Node pred, PathSummary oldSummary, PathSummary newSummary |
      flowsTo(source, pred, oldSummary) and
--- a/javascript/ql/src/semmle/javascript/dataflow/internal/FlowSteps.qll
+++ b/javascript/ql/src/semmle/javascript/dataflow/internal/FlowSteps.qll
@@ -5,6 +5,7 @@
 */

 import javascript
+import semmle.javascript.dataflow.Configuration

 /**
 * Holds if flow should be tracked through properties of `obj`.
@@ -66,12 +67,20 @@ predicate returnExpr(Function f, DataFlow::Node source, DataFlow::Node sink) {
 */
 pragma[inline]
 predicate localFlowStep(DataFlow::Node pred, DataFlow::Node succ,
-                        DataFlow::Configuration configuration, boolean valuePreserving) {
- pred = succ.getAPredecessor() and valuePreserving = true
- or
- any(DataFlow::AdditionalFlowStep afs).step(pred, succ) and valuePreserving = true
- or
- configuration.isAdditionalFlowStep(pred, succ, valuePreserving)
+                        DataFlow::Configuration configuration,
+                        FlowLabel predlbl, FlowLabel succlbl) {
+  pred = succ.getAPredecessor() and predlbl = succlbl
+  or
+  any(DataFlow::AdditionalFlowStep afs).step(pred, succ) and predlbl = succlbl
+  or
+  exists (boolean vp | configuration.isAdditionalFlowStep(pred, succ, vp) |
+    if vp = false and (predlbl = FlowLabel::data() or predlbl = FlowLabel::taint()) then
+      succlbl = FlowLabel::taint()
+    else
+      predlbl = succlbl
+  )
+  or
+  configuration.isAdditionalFlowStep(pred, succ, predlbl, succlbl)
 }

 /**
@@ -240,17 +249,15 @@ class Boolean extends boolean {
 */
 newtype TPathSummary =
  /** A summary of an inter-procedural data flow path. */
-  MkPathSummary(Boolean hasReturn, Boolean hasCall, Boolean valuePreserving)
+  MkPathSummary(Boolean hasReturn, Boolean hasCall, FlowLabel start, FlowLabel end)

 /**
 * A summary of an inter-procedural data flow path.
 *
- * The summary keeps track of whether the path contains any call steps from an argument
- * of a function call to the corresponding parameter, and/or any return steps from the
- * `return` statement of a function to a call of that function.
- *
- * Additionally, it records and whether each step on the path preserves the value of its
- * input node (and not just its taintedness).
+ * The summary includes a start flow label and an end flow label, and keeps track of
+ * whether the path contains any call steps from an argument of a function call to the
+ * corresponding parameter, and/or any return steps from the `return` statement of a
+ * function to a call of that function.
 *
 * We only want to build properly matched call/return sequences, so if a path has both
 * call steps and return steps, all return steps must precede all call steps.
@@ -258,10 +265,11 @@ newtype TPathSummary =
 class PathSummary extends TPathSummary {
  Boolean hasReturn;
  Boolean hasCall;
-  Boolean valuePreserving;
+  FlowLabel start;
+  FlowLabel end;

  PathSummary() {
-    this = MkPathSummary(hasReturn, hasCall, valuePreserving)
+    this = MkPathSummary(hasReturn, hasCall, start, end)
  }

  /** Indicates whether the path represented by this summary contains any return steps. */
@@ -274,12 +282,9 @@ class PathSummary extends TPathSummary {
    result = hasCall
  }

-  /**
-   * Indicates whether the path represented by this summary preserves the value of
-   * its start node or only its taintedness.
-   */
-  boolean valuePreserving() {
-    result = valuePreserving
+  /** Gets the flow label describing the value at the end of this flow path. */
+  FlowLabel getEndLabel() {
+    result = end
  }

  /**
@@ -289,11 +294,30 @@ class PathSummary extends TPathSummary {
   * a `call` step in order to maintain well-formedness.
   */
  PathSummary append(PathSummary that) {
-    result = MkPathSummary(this.hasReturn().booleanOr(that.hasReturn()),
-                           this.hasCall().booleanOr(that.hasCall()),
-                           this.valuePreserving().booleanAnd(that.valuePreserving())) and
-    // avoid constructing invalid paths
-    not (this.hasCall() = true and that.hasReturn() = true)
+    exists (Boolean hasReturn2, Boolean hasCall2, FlowLabel end2 |
+      that = MkPathSummary(hasReturn2, hasCall2, end, end2) |
+      result = MkPathSummary(hasReturn.booleanOr(hasReturn2),
+                             hasCall.booleanOr(hasCall2),
+                             start, end2) and
+      // avoid constructing invalid paths
+      not (hasCall = true and hasReturn2 = true)
+    )
+  }
+
+  /**
+   * Gets the summary for the path obtained by appending `that` to `this`, where
+   * `that` must be a path mapping `data` to `data` (in other words, it must be
+   * a value-preserving path).
+   */
+  PathSummary appendValuePreserving(PathSummary that) {
+    exists (Boolean hasReturn2, Boolean hasCall2 |
+      that = MkPathSummary(hasReturn2, hasCall2, FlowLabel::data(), FlowLabel::data()) |
+      result = MkPathSummary(hasReturn.booleanOr(hasReturn2),
+                             hasCall.booleanOr(hasCall2),
+                             start, end) and
+      // avoid constructing invalid paths
+      not (hasCall = true and hasReturn2 = true)
+    )
  }

  /**
@@ -308,43 +332,37 @@ class PathSummary extends TPathSummary {
    exists (string withReturn, string withCall |
      (if hasReturn = true then withReturn = "with" else withReturn = "without") and
      (if hasCall = true then withCall = "with" else withCall = "without") |
-      result = "forward path " + withReturn + " return steps and " + withCall + " call steps"
+      result = "path " + withReturn + " return steps and " + withCall + " call steps " +
+               "transforming " + start + " into " + end
    )
  }
 }

 module PathSummary {
-  /**
-   * Gets a summary describing an empty path.
-   */
-  PathSummary empty() {
-    result = level(true)
-  }
-
  /**
   * Gets a summary describing a path without any calls or returns.
-   * `valuePreserving` indicates whether the path preserves the value of its
-   * start node or only its taintedness.
   */
-  PathSummary level(Boolean valuePreserving) {
-    result = MkPathSummary(false, false, valuePreserving)
+  PathSummary level() {
+    exists (FlowLabel lbl |
+      result = MkPathSummary(false, false, lbl, lbl)
+    )
  }

  /**
   * Gets a summary describing a path with one or more calls, but no returns.
-   * `valuePreserving` indicates whether the path preserves the value of its
-   * start node or only its taintedness.
   */
-  PathSummary call(Boolean valuePreserving) {
-    result = MkPathSummary(false, true, valuePreserving)
+  PathSummary call() {
+    exists (FlowLabel lbl |
+      result = MkPathSummary(false, true, lbl, lbl)
+    )
  }

  /**
   * Gets a summary describing a path with one or more returns, but no calls.
-   * `valuePreserving` indicates whether the path preserves the value of its
-   * start node or only its taintedness.
   */
-  PathSummary return(Boolean valuePreserving) {
-    result = MkPathSummary(true, false, valuePreserving)
+  PathSummary return() {
+    exists (FlowLabel lbl |
+      result = MkPathSummary(true, false, lbl, lbl)
+    )
  }
 }
--- a/javascript/ql/src/semmle/javascript/security/dataflow/ClientSideUrlRedirect.qll
+++ b/javascript/ql/src/semmle/javascript/security/dataflow/ClientSideUrlRedirect.qll
@@ -23,6 +23,14 @@ module ClientSideUrlRedirect {
   */
  abstract class Sanitizer extends DataFlow::Node { }

+  /**
+   * A flow label for values that represent the URL of the current document, and
+   * hence are only partially user-controlled.
+   */
+  class DocumentUrl extends DataFlow::FlowLabel {
+    DocumentUrl() { this = "document.url" }
+  }
+
  /**
   * A taint-tracking configuration for reasoning about unvalidated URL redirections.
   */
@@ -35,19 +43,29 @@ module ClientSideUrlRedirect {
      source instanceof Source
    }

+    override predicate isSource(DataFlow::Node source, DataFlow::FlowLabel lbl) {
+      isDocumentURL(source.asExpr()) and
+      lbl instanceof DocumentUrl
+    }
+
    override predicate isSink(DataFlow::Node sink) {
      sink instanceof Sink
    }

    override predicate isSanitizer(DataFlow::Node node) {
      super.isSanitizer(node) or
-      isSafeLocationProperty(node.asExpr()) or
      node instanceof Sanitizer
    }

    override predicate isSanitizer(DataFlow::Node source, DataFlow::Node sink) {
      sanitizingPrefixEdge(source, sink)
    }
+
+    override predicate isAdditionalFlowStep(DataFlow::Node pred, DataFlow::Node succ, DataFlow::FlowLabel f, DataFlow::FlowLabel g) {
+      queryAccess(pred, succ) and
+      f instanceof DocumentUrl and
+      g = DataFlow::FlowLabel::taint()
+    }
  }

  /** A source of remote user input, considered as a flow source for unvalidated URL redirects. */
@@ -84,35 +102,6 @@ module ClientSideUrlRedirect {
    )
  }

-  /**
-   * A taint tracking configuration for identifying accesses of the query string of the current URL.
-   */
-  private class LocationHrefDataFlowConfiguration extends TaintTracking::Configuration {
-    LocationHrefDataFlowConfiguration() {
-      this = "LocationHrefDataFlowConfiguration"
-    }
-
-    override predicate isSource(DataFlow::Node source) {
-      isDocumentURL(source.asExpr())
-    }
-
-    override predicate isSink(DataFlow::Node sink) {
-      queryAccess(sink, _)
-    }
-  }
-
-  /**
-   * An access of the query string of the current URL.
-   */
-  class LocationSearchSource extends Source {
-    LocationSearchSource() {
-      exists(LocationHrefDataFlowConfiguration cfg, DataFlow::Node nd |
-        cfg.hasFlow(_, nd) and
-        queryAccess(nd, this)
-      )
-    }
-  }
-
  /**
   * A sink which is used to set the window location.
   */
--- a/javascript/ql/src/semmle/javascript/security/dataflow/CommandInjection.qll
+++ b/javascript/ql/src/semmle/javascript/security/dataflow/CommandInjection.qll
@@ -37,14 +37,14 @@ module CommandInjection {
     * Holds if `sink` is a data flow sink for command-injection vulnerabilities, and
     * the alert should be placed at the node `highlight`.
     */
-    predicate isSink(DataFlow::Node sink, DataFlow::Node highlight) {
+    predicate isSinkWithHighlight(DataFlow::Node sink, DataFlow::Node highlight) {
      sink instanceof Sink and highlight = sink
      or
      indirectCommandInjection(sink, highlight)
    }

    override predicate isSink(DataFlow::Node sink) {
-      isSink(sink, _)
+      isSinkWithHighlight(sink, _)
    }

    override predicate isSanitizer(DataFlow::Node node) {