diff --git a/shared/dataflow/codeql/dataflow/TaintTracking.qll b/shared/dataflow/codeql/dataflow/TaintTracking.qll index a769b858028..beec8f38499 100644 --- a/shared/dataflow/codeql/dataflow/TaintTracking.qll +++ b/shared/dataflow/codeql/dataflow/TaintTracking.qll @@ -29,6 +29,12 @@ signature module InputSig Lang> { */ bindingset[node] predicate defaultImplicitTaintRead(Lang::Node node, Lang::ContentSet c); + + /** + * Holds if the additional step from `src` to `sink` should be considered in + * speculative taint flow exploration. + */ + predicate speculativeTaintStep(Lang::Node src, Lang::Node sink); } /** @@ -130,4 +136,124 @@ module TaintFlowMake< { import GlobalWithState } + + signature int speculationLimitSig(); + + private module AddSpeculativeTaintSteps< + DataFlowInternal::FullStateConfigSig Config, speculationLimitSig/0 speculationLimit> implements + DataFlowInternal::FullStateConfigSig + { + import Config + + private predicate relevantState(Config::FlowState state) { + Config::isSource(_, state) + or + exists(Config::FlowState state0 | + relevantState(state0) and Config::isAdditionalFlowStep(_, state0, _, state, _) + ) + } + + private newtype TFlowState = + TMkFlowState(Config::FlowState state, int spec) { + relevantState(state) and spec = [0 .. speculationLimit()] + } + + class FlowState extends TFlowState { + private Config::FlowState state; + private int spec; + + FlowState() { this = TMkFlowState(state, spec) } + + string toString() { result = "FlowState" } + + Config::FlowState getState() { result = state } + + int getSpec() { result = spec } + } + + predicate isSource(DataFlowLang::Node source, FlowState state) { + Config::isSource(source, state.getState()) and state.getSpec() = 0 + } + + predicate isSink(DataFlowLang::Node sink, FlowState state) { + Config::isSink(sink, state.getState()) + } + + predicate isBarrier(DataFlowLang::Node node, FlowState state) { + Config::isBarrier(node, state.getState()) + } + + predicate isBarrierIn(DataFlowLang::Node node, FlowState state) { + Config::isBarrierIn(node, state.getState()) + } + + predicate isBarrierOut(DataFlowLang::Node node, FlowState state) { + Config::isBarrierOut(node, state.getState()) + } + + predicate isAdditionalFlowStep( + DataFlowLang::Node node1, FlowState state1, DataFlowLang::Node node2, FlowState state2, + string model + ) { + Config::isAdditionalFlowStep(node1, state1.getState(), node2, state2.getState(), model) and + state1.getSpec() = state2.getSpec() + or + speculativeTaintStep(node1, node2) and + not defaultAdditionalTaintStep(node1, node2, _) and + not Config::isAdditionalFlowStep(node1, _, node2, _, _) and + not Config::isAdditionalFlowStep(node1, node2, _) and + model = "Speculative" and + state1.getSpec() + 1 = state2.getSpec() and + state1.getState() = state2.getState() + } + } + + module SpeculativeFlow + 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" + } + } + + private module C implements DataFlowInternal::FullStateConfigSig { + import AddTaintDefaults> + } + + import DataFlowInternal::Impl + } + + module SpeculativeFlowWithState< + 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" + } + } + + private module C implements DataFlowInternal::FullStateConfigSig { + import AddTaintDefaults> + } + + import DataFlowInternal::Impl + } }