Model generator

Author: hvitved

shared/dataflow/codeql/dataflow/DataFlow.qll

@@ -363,6 +363,11 @@ module Configs<LocationSig Location, InputSig<Location> Lang> {
      */
     predicate isSink(Node sink);
 
+    /**
+     * Holds if `sink` is a relevant data flow sink.
+     */
+    default predicate isSinkReverse(Node sink) { none() }
+
     /**
      * Holds if data flow through `node` is prohibited. This completely removes
      * `node` from the data flow graph.
@@ -465,6 +470,16 @@ module Configs<LocationSig Location, InputSig<Location> Lang> {
      */
     default predicate isSink(Node sink) { none() }
 
+    /**
+     * Holds if `sink` is a relevant data flow sink for any state.
+     */
+    default predicate isSinkReverse(Node sink) { none() }
+
+    /**
+     * Holds if `sink` is a relevant data flow sink accepting `state`.
+     */
+    default predicate isSinkReverse(Node sink, FlowState state) { none() }
+
     /**
      * Holds if data flow through `node` is prohibited. This completely removes
      * `node` from the data flow graph.

shared/dataflow/codeql/dataflow/TaintTracking.qll

@@ -179,6 +179,10 @@ module TaintFlowMake<
       Config::isSink(sink, state.getState())
     }
 
+    predicate isSinkReverse(DataFlowLang::Node sink, FlowState state) {
+      Config::isSinkReverse(sink, state.getState())
+    }
+
     predicate isBarrier(DataFlowLang::Node node, FlowState state) {
       Config::isBarrier(node, state.getState())
     }

shared/dataflow/codeql/dataflow/internal/ContentDataFlowImpl.qll

@@ -46,6 +46,11 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
      */
     predicate isSink(Node sink);
 
+    /**
+     * Holds if `sink` is a relevant data flow sink.
+     */
+    default predicate isSinkReverse(Node sink) { none() }
+
     /**
      * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
      */
@@ -98,6 +103,15 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
         )
       }
 
+      predicate isSinkReverse(Node sink, FlowState state) {
+        ContentConfig::isSinkReverse(sink) and
+        (
+          state instanceof InitState or
+          state instanceof StoreState or
+          state instanceof ReadState
+        )
+      }
+
       predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
         storeStep(node1, state1, _, node2, state2) or
         readStep(node1, state1, _, node2, state2) or
@@ -114,7 +128,35 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
       predicate includeHiddenNodes() { any() }
     }
 
-    private module Flow = GlobalWithState<FlowConfig>;
+    module Flow = GlobalWithState<FlowConfig>;
+
+    /**
+     * Holds if data stored inside `sourceAp` on `source` flows to `sinkAp` inside `sink`
+     * for this configuration. `preservesValue` indicates whether any of the additional
+     * flow steps defined by `isAdditionalFlowStep` are needed.
+     *
+     * For the source access path, `sourceAp`, the top of the stack represents the content
+     * that was last read from. That is, if `sourceAp` is `Field1.Field2` (with `Field1`
+     * being the top of the stack), then there is flow from `source.Field2.Field1`.
+     *
+     * For the sink access path, `sinkAp`, the top of the stack represents the content
+     * that was last stored into. That is, if `sinkAp` is `Field1.Field2` (with `Field1`
+     * being the top of the stack), then there is flow into `sink.Field1.Field2`.
+     */
+    predicate flowPath(
+      Flow::PathNode source, AccessPath sourceAp, Flow::PathNode sink, AccessPath sinkAp,
+      boolean preservesValue
+    ) {
+      Flow::flowPath(source, sink) and
+      nodeReaches(source, TAccessPathNil(), TAccessPathNil(), sink, sourceAp, sinkAp) and
+      (
+        sink.getState().(InitState).decode(preservesValue)
+        or
+        sink.getState().(ReadState).decode(_, preservesValue)
+        or
+        sink.getState().(StoreState).decode(_, preservesValue)
+      )
+    }
 
     /**
      * Holds if data stored inside `sourceAp` on `source` flows to `sinkAp` inside `sink`
@@ -133,16 +175,9 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
       Node source, AccessPath sourceAp, Node sink, AccessPath sinkAp, boolean preservesValue
     ) {
       exists(Flow::PathNode pathSource, Flow::PathNode pathSink |
-        Flow::flowPath(pathSource, pathSink) and
-        nodeReaches(pathSource, TAccessPathNil(), TAccessPathNil(), pathSink, sourceAp, sinkAp) and
+        flowPath(pathSource, sourceAp, pathSink, sinkAp, preservesValue) and
         source = pathSource.getNode() and
         sink = pathSink.getNode()
-      |
-        pathSink.getState().(InitState).decode(preservesValue)
-        or
-        pathSink.getState().(ReadState).decode(_, preservesValue)
-        or
-        pathSink.getState().(StoreState).decode(_, preservesValue)
       )
     }
 
@@ -359,6 +394,8 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
           or
           FlowConfig::isSink(node.getNode(), node.getState())
           or
+          FlowConfig::isSinkReverse(node.getNode(), node.getState())
+          or
           excludeStep(node, _)
           or
           Flow::PathGraph::subpaths(_, _, node, _)

shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll

@@ -40,6 +40,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
      */
     predicate isSink(Node sink);
 
+    /**
+     * Holds if `sink` is a relevant data flow sink accepting `state`.
+     */
+    predicate isSinkReverse(Node sink, FlowState state);
+
+    /**
+     * Holds if `sink` is a relevant data flow sink for any state.
+     */
+    predicate isSinkReverse(Node sink);
+
     /**
      * Holds if data flow through `node` is prohibited. This completely removes
      * `node` from the data flow graph.
@@ -149,6 +159,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
 
     predicate isSink(Node sink, FlowState state) { Config::isSink(sink) and exists(state) }
 
+    predicate isSinkReverse(Node sink, FlowState state) {
+      Config::isSinkReverse(sink) and exists(state)
+    }
+
     predicate isBarrier(Node node, FlowState state) { none() }
 
     predicate isBarrierIn(Node node, FlowState state) { none() }
@@ -192,18 +206,32 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
         else any()
       }
 
+      pragma[nomagic]
+      private predicate isFilteredSinkReverse(Node sink) {
+        (
+          Config::isSinkReverse(sink, _) or
+          Config::isSinkReverse(sink)
+        ) and
+        if Config::observeDiffInformedIncrementalMode()
+        then AlertFiltering::filterByLocation(sink.getLocation())
+        else any()
+      }
+
       private predicate hasFilteredSource() { isFilteredSource(_) }
 
       private predicate hasFilteredSink() { isFilteredSink(_) }
 
+      private predicate hasFilteredSinkReverse() { isFilteredSinkReverse(_) }
+
       predicate isRelevantSource(Node source, FlowState state) {
         // If there are filtered sinks, we need to pass through all sources to preserve all alerts
         // with filtered sinks. Otherwise the only alerts of interest are those with filtered
         // sources, so we can perform the source filtering right here.
         Config::isSource(source, state) and
         (
           isFilteredSource(source) or
-          hasFilteredSink()
+          hasFilteredSink() or
+          hasFilteredSinkReverse()
         )
       }
 
@@ -218,6 +246,17 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
         )
       }
 
+      predicate isRelevantSinkReverse(Node sink, FlowState state) {
+        // If there are filtered sources, we need to pass through all sinks to preserve all alerts
+        // with filtered sources. Otherwise the only alerts of interest are those with filtered
+        // sinks, so we can perform the sink filtering right here.
+        Config::isSinkReverse(sink, state) and
+        (
+          isFilteredSinkReverse(sink) or
+          hasFilteredSource()
+        )
+      }
+
       predicate isRelevantSink(Node sink) {
         // If there are filtered sources, we need to pass through all sinks to preserve all alerts
         // with filtered sources. Otherwise the only alerts of interest are those with filtered
@@ -229,12 +268,30 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
         )
       }
 
+      predicate isRelevantSinkReverse(Node sink) {
+        // If there are filtered sources, we need to pass through all sinks to preserve all alerts
+        // with filtered sources. Otherwise the only alerts of interest are those with filtered
+        // sinks, so we can perform the sink filtering right here.
+        Config::isSinkReverse(sink) and
+        (
+          isFilteredSinkReverse(sink) or
+          hasFilteredSource()
+        )
+      }
+
       bindingset[source, sink]
       pragma[inline_late]
       predicate isRelevantSourceSinkPair(Node source, Node sink) {
         isFilteredSource(source) or
         isFilteredSink(sink)
       }
+
+      bindingset[source, sink]
+      pragma[inline_late]
+      predicate isRelevantSourceSinkPairReverse(Node source, Node sink) {
+        isFilteredSource(source) or
+        isFilteredSinkReverse(sink)
+      }
     }
 
     private import SourceSinkFiltering
@@ -258,19 +315,28 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
 
     private predicate outBarrier(NodeEx node) {
       exists(Node n |
-        [node.asNodeOrImplicitRead(), node.asNodeReverse(_)] = n and
+        node.asNodeOrImplicitRead() = n and
         Config::isBarrierOut(n)
       |
         isRelevantSink(n, _)
         or
         isRelevantSink(n)
       )
+      or
+      exists(Node n |
+        node.asNodeReverse(_) = n and
+        Config::isBarrierOut(n)
+      |
+        isRelevantSinkReverse(n, _)
+        or
+        isRelevantSinkReverse(n)
+      )
     }
 
     pragma[nomagic]
     private predicate outBarrier(NodeEx node, FlowState state) {
       exists(Node n |
-        [node.asNodeOrImplicitRead(), node.asNodeReverse(_)] = n and
+        node.asNodeOrImplicitRead() = n and
         Config::isBarrierOut(n, state)
       |
         isRelevantSink(n, state)
@@ -321,6 +387,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
       not stateBarrier(node, state)
     }
 
+    pragma[nomagic]
+    private predicate sinkNodeWithStateReverse(NodeEx node, FlowState state) {
+      isRelevantSinkReverse(node.asNodeReverse(_), state) and
+      not fullBarrier(node) and
+      not stateBarrier(node, state)
+    }
+
     /** Provides the relevant barriers for a step from `node1` to `node2`. */
     bindingset[node1, node2]
     private predicate stepFilter(NodeEx node1, NodeEx node2) {
@@ -707,6 +780,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
         fwdFlow(node) and
         fwdFlowState(state) and
         sinkNodeWithState(node, state)
+        or
+        fwdFlow(pragma[only_bind_into](node)) and
+        fwdFlowState(state) and
+        isRelevantSinkReverse(node.asNodeReverse(_))
+        or
+        fwdFlow(node) and
+        fwdFlowState(state) and
+        sinkNodeWithState(node, state)
+        or
+        fwdFlow(node) and
+        fwdFlowState(state) and
+        sinkNodeWithStateReverse(node, state)
       }
 
       /**
@@ -1025,7 +1110,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
 
     private predicate sinkModel(NodeEx node, string model) {
       sinkNode(node, _) and
-      exists(Node n | n = node.asNodeOrImplicitRead() |
+      exists(Node n | n = [node.asNodeOrImplicitRead(), node.asNodeReverse(_)] |
         knownSinkModel(n, model)
         or
         not knownSinkModel(n, _) and model = ""
@@ -2995,6 +3080,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
                 (isRelevantSink(n) or isRelevantSink(n, _)) and
                 result.asNode() = n
               )
+              or
+              exists(Node n |
+                node.asNodeReverse(_) = n and
+                (isRelevantSinkReverse(n) or isRelevantSinkReverse(n, _)) and
+                result = node
+              )
             }
 
             override PathNodeImpl getASuccessorImpl(string label) {
@@ -3489,6 +3580,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
               /** Gets the underlying `Node`. */
               final Node getNode() { super.getNodeEx().projectToNode() = result }
 
+              /** Gets the underlying `Node`, but only when it represents a reverse-flow node. */
+              final Node getNodeReverse() { super.getNodeEx().asNodeReverse(_) = result }
+
               /** Gets the parameter node through which data is returned, if any. */
               final ParameterNode asParameterReturnNode() {
                 result = super.getNodeEx().asNodeReverse(_)
@@ -4838,7 +4932,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
       private predicate interestingCallableSink(DataFlowCallable c) {
         exists(Node n | c = getNodeEnclosingCallable(n) |
           isRelevantSink(n, _) or
-          isRelevantSink(n)
+          isRelevantSink(n) or
+          isRelevantSinkReverse(n, _) or
+          isRelevantSinkReverse(n)
         )
         or
         exists(DataFlowCallable mid | interestingCallableSink(mid) and callableStep(c, mid))
@@ -4874,7 +4970,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
           ce1 = TCallable(getNodeEnclosingCallable(n))
         |
           isRelevantSink(n, _) or
-          isRelevantSink(n)
+          isRelevantSink(n) or
+          isRelevantSinkReverse(n, _) or
+          isRelevantSinkReverse(n)
         )
       }
 
@@ -4942,6 +5040,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
         relevantState(state) and
         not fullBarrier(node) and
         not stateBarrier(node, state)
+        or
+        isRelevantSinkReverse(node.asNodeReverse(_)) and
+        relevantState(state) and
+        not fullBarrier(node) and
+        not stateBarrier(node, state)
       }
 
       private newtype TSummaryCtx1 =