DataFlow: Bugfix in flow state for value preservation.

This commit is contained in:
Michael Nebel
2024-08-28 14:40:04 +02:00
parent 3a864d3de2
commit 6d346dbedd

View File

@@ -51,6 +51,11 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
*/ */
default predicate isAdditionalFlowStep(Node node1, Node node2) { none() } default predicate isAdditionalFlowStep(Node node1, Node node2) { none() }
/**
* Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow steps.
*/
default predicate isAdditionalTaintStep(Node node1, Node node2) { none() }
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
default predicate isBarrier(Node node) { none() } default predicate isBarrier(Node node) { none() }
@@ -101,7 +106,7 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) { predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
storeStep(node1, state1, _, node2, state2) or storeStep(node1, state1, _, node2, state2) or
readStep(node1, state1, _, node2, state2) or readStep(node1, state1, _, node2, state2) or
additionalStep(node1, state1, node2, state2) additionalTaintStep(node1, state1, node2, state2)
} }
predicate isAdditionalFlowStep = ContentConfig::isAdditionalFlowStep/2; predicate isAdditionalFlowStep = ContentConfig::isAdditionalFlowStep/2;
@@ -229,8 +234,8 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
) )
} }
private predicate additionalStep(Node node1, State state1, Node node2, State state2) { private predicate additionalTaintStep(Node node1, State state1, Node node2, State state2) {
ContentConfig::isAdditionalFlowStep(node1, node2) and ContentConfig::isAdditionalTaintStep(node1, node2) and
( (
state1 instanceof InitState and state1 instanceof InitState and
state2.(InitState).decode(false) state2.(InitState).decode(false)
@@ -302,12 +307,16 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
// relation, when flow can reach a sink without going back out // relation, when flow can reach a sink without going back out
Flow::PathGraph::subpaths(pred, succ, _, _) and Flow::PathGraph::subpaths(pred, succ, _, _) and
not reachesSink(succ) not reachesSink(succ)
or )
or
exists(Node predNode, State predState, Node succNode, State succState |
succNodeAndState(pred, predNode, predState, succ, succNode, succState)
|
// needed to record store steps // needed to record store steps
storeStep(pred.getNode(), pred.getState(), _, succ.getNode(), succ.getState()) storeStep(predNode, predState, _, succNode, succState)
or or
// needed to record read steps // needed to record read steps
readStep(pred.getNode(), pred.getState(), _, succ.getNode(), succ.getState()) readStep(predNode, predState, _, succNode, succState)
) )
} }