From 3c110f2eb80ea316e3b9f0e60feba02e65abf983 Mon Sep 17 00:00:00 2001 From: Alex Eyers-Taylor Date: Fri, 19 Sep 2025 15:56:02 +0100 Subject: [PATCH] DataFlow: Add code for merging base with overlay. --- shared/dataflow/codeql/dataflow/DataFlow.qll | 77 +++++++- .../codeql/dataflow/TaintTracking.qll | 177 +++++++++++++++++- .../codeql/dataflow/internal/DataFlowImpl.qll | 52 ++++- 3 files changed, 296 insertions(+), 10 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/DataFlow.qll b/shared/dataflow/codeql/dataflow/DataFlow.qll index f2fd4979c57..94bae26e7aa 100644 --- a/shared/dataflow/codeql/dataflow/DataFlow.qll +++ b/shared/dataflow/codeql/dataflow/DataFlow.qll @@ -657,7 +657,7 @@ private module PathGraphSigMod { } } -module DataFlowMake Lang> { +module DataFlowMakeCore Lang> { private import Lang private import internal.DataFlowImpl::MakeImpl private import internal.DataFlowImplStage1::MakeImplStage1 @@ -1099,6 +1099,13 @@ module DataFlowMake Lang> { // Re-export the PathGraph so the user can import a single module and get both PathNode and the query predicates import PathGraph } +} + +module DataFlowMake Lang> { + import DataFlowMakeCore + private import Lang + private import internal.DataFlowImpl::MakeImpl + private import internal.DataFlowImplStage1::MakeImplStage1 /** * Constructs a global data flow computation. @@ -1157,3 +1164,71 @@ module DataFlowMake Lang> { import Flow } } + +module DataFlowMakeOverlay Lang> { + import DataFlowMakeCore + private import Lang + private import internal.DataFlowImpl::MakeImpl + private import internal.DataFlowImplStage1::MakeImplStage1 + + /** + * Constructs a global data flow computation. + */ + module Global implements GlobalFlowSig { + private module C implements FullStateConfigSig { + import DefaultState + import Config + + predicate accessPathLimit = Config::accessPathLimit/0; + + predicate isAdditionalFlowStep(Node node1, Node node2, string model) { + Config::isAdditionalFlowStep(node1, node2) and model = "Config" + } + + predicate observeOverlayInformedIncrementalMode() { + not Config::observeDiffInformedIncrementalMode() + } + } + + private module Stage1 = ImplStage1; + + import Stage1::PartialFlow + + private module Flow = OverlayImpl; + + import Flow + } + + /** + * Constructs a global data flow computation using flow state. + */ + module GlobalWithState implements GlobalFlowSig { + private module C implements FullStateConfigSig { + import Config + + predicate accessPathLimit = Config::accessPathLimit/0; + + predicate isAdditionalFlowStep(Node node1, Node node2, string model) { + Config::isAdditionalFlowStep(node1, node2) and model = "Config" + } + + predicate isAdditionalFlowStep( + Node node1, FlowState state1, Node node2, FlowState state2, string model + ) { + Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config" + } + + predicate observeOverlayInformedIncrementalMode() { + not Config::observeDiffInformedIncrementalMode() + } + } + + private module Stage1 = ImplStage1; + + import Stage1::PartialFlow + + private module Flow = OverlayImpl; + + import Flow + } +} diff --git a/shared/dataflow/codeql/dataflow/TaintTracking.qll b/shared/dataflow/codeql/dataflow/TaintTracking.qll index 1f6cabbbba1..cb4fad7c8ce 100644 --- a/shared/dataflow/codeql/dataflow/TaintTracking.qll +++ b/shared/dataflow/codeql/dataflow/TaintTracking.qll @@ -47,16 +47,16 @@ signature module InputSig Lang> { /** * Construct the modules for taint-tracking analyses. */ -module TaintFlowMake< +private module TaintFlowMakeCore< LocationSig Location, DF::InputSig DataFlowLang, InputSig TaintTrackingLang> { - private import TaintTrackingLang - private import DF::DataFlowMake as DataFlow - private import MakeImpl as DataFlowInternal - private import MakeImplStage1 as DataFlowInternalStage1 + import TaintTrackingLang + import DF::DataFlowMakeCore as DataFlow + import MakeImpl as DataFlowInternal + import MakeImplStage1 as DataFlowInternalStage1 - private module AddTaintDefaults implements + module AddTaintDefaults implements DataFlowInternal::FullStateConfigSig { import Config @@ -85,7 +85,7 @@ module TaintFlowMake< signature int speculationLimitSig(); - private module AddSpeculativeTaintSteps< + module AddSpeculativeTaintSteps< DataFlowInternal::FullStateConfigSig Config, speculationLimitSig/0 speculationLimit> implements DataFlowInternal::FullStateConfigSig { @@ -153,6 +153,13 @@ module TaintFlowMake< state1.getState() = state2.getState() } } +} + +module TaintFlowMake< + LocationSig Location, DF::InputSig DataFlowLang, + InputSig TaintTrackingLang> +{ + private import TaintFlowMakeCore /** * Constructs a global taint tracking computation. @@ -288,7 +295,161 @@ module TaintFlowMake< import Stage1::PartialFlow - private module Flow = DataFlowInternal::Impl; + private module Flow = DataFlowInternal::OverlayImpl; + + import Flow + } +} + +module TaintFlowMakeOverlay< + LocationSig Location, DF::InputSig DataFlowLang, + InputSig TaintTrackingLang> +{ + private import TaintFlowMakeCore + + /** + * Constructs a global taint tracking computation. + */ + module Global implements DataFlow::GlobalFlowSig { + private module Config0 implements DataFlowInternal::FullStateConfigSig { + import DataFlowInternal::DefaultState + import Config + + predicate isAdditionalFlowStep( + DataFlowLang::Node node1, DataFlowLang::Node node2, string model + ) { + Config::isAdditionalFlowStep(node1, node2) and model = "Config" + } + + predicate observeOverlayInformedIncrementalMode() { + not Config::observeDiffInformedIncrementalMode() + } + } + + private module C implements DataFlowInternal::FullStateConfigSig { + import AddTaintDefaults + } + + private module Stage1 = DataFlowInternalStage1::ImplStage1; + + import Stage1::PartialFlow + + private module Flow = DataFlowInternal::OverlayImpl; + + import Flow + } + + /** + * Constructs a global taint tracking computation using flow state. + */ + module GlobalWithState implements DataFlow::GlobalFlowSig { + private module Config0 implements DataFlowInternal::FullStateConfigSig { + import Config + + predicate isAdditionalFlowStep( + DataFlowLang::Node node1, DataFlowLang::Node node2, string model + ) { + Config::isAdditionalFlowStep(node1, node2) and model = "Config" + } + + predicate isAdditionalFlowStep( + DataFlowLang::Node node1, FlowState state1, DataFlowLang::Node node2, FlowState state2, + string model + ) { + Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config" + } + + predicate observeOverlayInformedIncrementalMode() { + not Config::observeDiffInformedIncrementalMode() + } + } + + private module C implements DataFlowInternal::FullStateConfigSig { + import AddTaintDefaults + } + + private module Stage1 = DataFlowInternalStage1::ImplStage1; + + import Stage1::PartialFlow + + private module Flow = DataFlowInternal::OverlayImpl; + + import Flow + } + + /** + * Constructs a global taint tracking computation that also allows a given + * maximum number of speculative taint steps. + */ + module SpeculativeGlobal + implements DataFlow::GlobalFlowSig + { + private module Config0 implements DataFlowInternal::FullStateConfigSig { + import DataFlowInternal::DefaultState + import Config + + predicate isAdditionalFlowStep( + DataFlowLang::Node node1, DataFlowLang::Node node2, string model + ) { + Config::isAdditionalFlowStep(node1, node2) and model = "Config" + } + + predicate observeOverlayInformedIncrementalMode() { + not Config::observeDiffInformedIncrementalMode() + } + } + + private module C implements DataFlowInternal::FullStateConfigSig { + import AddTaintDefaults> + } + + private module Stage1 = DataFlowInternalStage1::ImplStage1; + + import Stage1::PartialFlow + + private module Flow = DataFlowInternal::Impl; + + import Flow + } + + /** + * Constructs a global taint tracking computation using flow state that also + * allows a given maximum number of speculative taint steps. + */ + module SpeculativeGlobalWithState< + DataFlow::StateConfigSig Config, speculationLimitSig/0 speculationLimit> implements + DataFlow::GlobalFlowSig + { + private module Config0 implements DataFlowInternal::FullStateConfigSig { + import Config + + predicate isAdditionalFlowStep( + DataFlowLang::Node node1, DataFlowLang::Node node2, string model + ) { + Config::isAdditionalFlowStep(node1, node2) and model = "Config" + } + + predicate isAdditionalFlowStep( + DataFlowLang::Node node1, FlowState state1, DataFlowLang::Node node2, FlowState state2, + string model + ) { + Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config" + } + + predicate observeOverlayInformedIncrementalMode() { + not Config::observeDiffInformedIncrementalMode() + } + } + + private module C implements DataFlowInternal::FullStateConfigSig { + import AddTaintDefaults> + } + + private module Stage1 = DataFlowInternalStage1::ImplStage1; + + import Stage1::PartialFlow + + private module Flow = DataFlowInternal::OverlayImpl; import Flow } diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index c21858cc167..81ac268b8b3 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -15,7 +15,7 @@ private import DataFlowImplStage1 module MakeImpl Lang> { private import Lang - private import DataFlowMake + private import DataFlowMakeCore private import MakeImplStage1 private import DataFlowImplCommon::MakeImplCommon private import DataFlowImplCommonPublic @@ -179,6 +179,56 @@ module MakeImpl Lang> { } } + /** + * Constructs a data flow computation given a full input configuration, and + * an initial stage 1 pruning with merging of overlay and base results. + */ + module OverlayImpl Stage1> { + module Base = Impl; + + import Base + + /** + * Holds if data can flow from `source` to `sink`. + * + * This is a local predicate that only has results local to the overlay/base database. + */ + predicate flowLocal(Node source, Node sink) = forceLocal(Base::flow/2)(source, sink) + + /** + * Holds if data can flow from `source` to `sink`. + */ + predicate flow(Node source, Node sink) { + Base::flow(source, sink) + or + // If we are overlay informed (i.e. we are not diff-informed), we + // merge in the local results which includes the base database results. + flowLocal(source, sink) and Config::observeOverlayInformedIncrementalMode() + } + + /** + * Holds if data can flow from some source to `sink`. + * This predicate that only has results local to the overlay/base database. + */ + predicate flowToLocal(Node sink) = forceLocal(Base::flowTo/1)(sink) + + /** + * Holds if data can flow from some source to `sink`. + */ + predicate flowTo(Node sink) { + Base::flowTo(sink) + or + // If we are overlay informed (i.e. we are not diff-informed), we + // merge in the local results which includes the base database results. + flowToLocal(sink) and Config::observeOverlayInformedIncrementalMode() + } + + /** + * Holds if data can flow from some source to `sink`. + */ + predicate flowToExpr(Lang::DataFlowExpr sink) { flowTo(exprNode(sink)) } + } + /** * Constructs a data flow computation given a full input configuration, and * an initial stage 1 pruning.