Dataflow: Add speculative flow modules.

This commit is contained in:
Anders Schack-Mulligen
2024-09-19 10:32:46 +02:00
parent c80627a3d3
commit 7d123296f8

View File

@@ -29,6 +29,12 @@ signature module InputSig<LocationSig Location, DF::InputSig<Location> 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<Config>
}
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<DataFlow::ConfigSig Config, speculationLimitSig/0 speculationLimit>
implements DataFlow::GlobalFlowSig
{
private module Config0 implements DataFlowInternal::FullStateConfigSig {
import DataFlowInternal::DefaultState<Config>
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<AddSpeculativeTaintSteps<Config0, speculationLimit/0>>
}
import DataFlowInternal::Impl<C>
}
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<AddSpeculativeTaintSteps<Config0, speculationLimit/0>>
}
import DataFlowInternal::Impl<C>
}
}