Skip to content

Commit

Permalink
Data flow: Use stage path graph in store/load matching
Browse files Browse the repository at this point in the history
  • Loading branch information
@hvitved
hvitved committed Aug 20, 2024
1 parent 1211318 commit 2a9f751
Show file tree
Hide file tree
Showing 2 changed files with 331 additions and 141 deletions.
169 changes: 104 additions & 65 deletions shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1719,7 +1719,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
Typ t1, Ap ap1, Typ t2, Ap ap2, Content c, NodeEx node1, NodeEx node2, FlowState state,
Cc cc, ParamNodeOption summaryCtx, TypOption argT, ApOption argAp
) {
fwdFlowRead0(t1, ap1, c, node1, node2, state, cc, summaryCtx, argT, argAp) and
fwdFlowRead0(pragma[only_bind_into](t1), pragma[only_bind_into](ap1),
pragma[only_bind_into](c), node1, node2, state, cc, summaryCtx, argT, argAp) and
(
exists(NodeEx storeSource |
fwdFlowConsCandStoreReadMatchingEnabled(storeSource, t1, ap1, c, t2, ap2) and
Expand Down Expand Up @@ -2646,7 +2647,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
abstract Location getLocation();

/** Gets the corresponding `Node`, if any. */
Node getNode() { none() }
NodeEx getNodeEx() { none() }

/** Gets the summary context. */
ParamNodeOption getSummaryCtx() { none() }

/** Gets the access path. */
Ap getAp() { none() }

/** Gets the corresponding `Node`, if any. */
final Node getNode() { result = this.getNodeEx().asNode() }

predicate isSource() { none() }

Expand Down Expand Up @@ -2690,7 +2700,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {

override Location getLocation() { result = node.getLocation() }

override Node getNode() { result = node.asNode() }
override NodeEx getNodeEx() { result = node }

override ParamNodeOption getSummaryCtx() { result = summaryCtx }

override Ap getAp() { result = ap }

override predicate isSource() {
sourceNode(node, state) and
Expand Down Expand Up @@ -2728,8 +2742,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap,
boolean allowsFlowThrough
) {
exists(ApApprox apa, boolean allowsFlowThrough0 |
FwdFlowIn<FwdFlowInNoRestriction>::fwdFlowIn(_, arg, _, p, state, outercc, innercc,
exists(DataFlowCall call, ApApprox apa, boolean allowsFlowThrough0 |
callEdgeArgParam(call, _, arg, p, _, ap) and
FwdFlowIn<FwdFlowInNoRestriction>::fwdFlowIn(call, arg, _, p, state, outercc, innercc,
summaryCtx, argT, argAp, t, ap, apa, _, allowsFlowThrough0) and
if PrevStage::parameterMayFlowThrough(p, apa)
then allowsFlowThrough = allowsFlowThrough0
Expand All @@ -2744,6 +2759,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
RetNodeEx ret, ParamNodeEx innerSummaryCtx, Typ innerArgT, Ap innerArgAp,
ApApprox innerArgApa
) {
callEdgeReturn(call, _, ret, _, _, _, ap) and
callMayFlowThroughRev(call) and
returnMayFlowThrough(ret, _, _, _) and
matchesCall(ccc, call) and
fwdFlowThrough0(call, arg, cc, state, ccc, summaryCtx, argT, argAp, t, ap, apa, ret,
innerSummaryCtx, innerArgT, innerArgAp, innerArgApa)
}
Expand Down Expand Up @@ -2797,6 +2816,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow,
ApApprox innerArgApa, ApApprox apa
|
callEdgeReturn(call, _, ret, _, node, allowsFieldFlow, ap) and
fwdFlowThroughStep1(pn1, pn2, pn3, call, cc, state, ccc, summaryCtx, argT, argAp, t,
ap, apa, ret, innerArgApa) and
flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow, innerArgApa, apa) and
Expand All @@ -2818,31 +2838,70 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
localStep(mid, state0, node, state, false, t, localCc, label) and
ap instanceof ApNil
)
or
// store
exists(NodeEx mid, Content c, Typ t0, Ap ap0 |
}

private predicate storeStep(
StagePathNode pn1, Content c, NodeEx node, FlowState state, Cc cc,
ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, string label
) {
exists(NodeEx mid, Typ t0, Ap ap0 |
pn1 = TStagePathNodeMid(mid, state, cc, summaryCtx, argT, argAp, t0, ap0) and
fwdFlowStore(mid, t0, ap0, c, t, node, state, cc, summaryCtx, argT, argAp) and
storeStepCand(mid, ap0, c, node, _,
any(DataFlowType containerType | t = getTyp(containerType))) and
ap = apCons(c, t0, ap0) and
label = ""
)
or
// read
}

private predicate readStep(
StagePathNode pn1, Content c, NodeEx node, FlowState state, Cc cc,
ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, string label
) {
exists(NodeEx mid, Typ t0, Ap ap0 |
pn1 = TStagePathNodeMid(mid, state, cc, summaryCtx, argT, argAp, t0, ap0) and
fwdFlowRead(t0, ap0, t, ap, _, mid, node, state, cc, summaryCtx, argT, argAp) and
fwdFlowRead(t0, ap0, t, ap, c, mid, node, state, cc, summaryCtx, argT, argAp) and
readStepCand(mid, c, node) and
label = ""
)
}

private predicate localStep(StagePathNode pn1, StagePathNode pn2, string label) {
predicate localStep(StagePathNode pn1, StagePathNode pn2, string label) {
exists(
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
ApOption argAp, Typ t0, Ap ap
|
localStep(pn1, node, state, cc, summaryCtx, argT, argAp, t0, ap, label) and
pn2 = typeStrengthenToStagePathNode(node, state, cc, summaryCtx, argT, argAp, t0, ap)
)
}

predicate storeStep(StagePathNode pn1, Content c, StagePathNode pn2, string label) {
exists(
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
ApOption argAp, Typ t0, Ap ap
|
storeStep(pn1, c, node, state, cc, summaryCtx, argT, argAp, t0, ap, label) and
pn2 = typeStrengthenToStagePathNode(node, state, cc, summaryCtx, argT, argAp, t0, ap)
)
}

predicate readStep(StagePathNode pn1, Content c, StagePathNode pn2, string label) {
exists(
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
ApOption argAp, Typ t0, Ap ap
|
readStep(pn1, c, node, state, cc, summaryCtx, argT, argAp, t0, ap, label) and
pn2 = typeStrengthenToStagePathNode(node, state, cc, summaryCtx, argT, argAp, t0, ap)
)
}

private predicate localScopeStep(StagePathNode pn1, StagePathNode pn2, string label) {

Check warning

Code scanning / CodeQL

Dead code Warning

This code is never used, and it's not publicly exported.
localStep(pn1, pn2, label)
or
storeStep(pn1, _, pn2, label)
or
readStep(pn1, _, pn2, label)
or
summaryStep(pn1, pn2, label)
}
Expand All @@ -2854,7 +2913,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
or
exists(StagePathNode mid, string l1, string l2 |
summaryLabel(pn1, mid, l1) and
localStep(mid, pn2, l2) and
localScopeStep(mid, pn2, l2) and
summaryLabel = mergeLabels(l1, l2)
)
}
Expand Down Expand Up @@ -2917,16 +2976,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
or
// flow out of a callable
exists(RetNodeEx ret, CcNoCall innercc, boolean allowsFieldFlow, ApApprox apa |
exists(
DataFlowCall call, RetNodeEx ret, CcNoCall innercc, boolean allowsFieldFlow,

Check warning

Code scanning / CodeQL

Omittable 'exists' variable Warning

This exists variable can be omitted by using a don't-care expression
in this argument
Loading
.
ApApprox apa
|
pn1 = TStagePathNodeMid(ret, state, innercc, summaryCtx, argT, argAp, t, ap) and
fwdFlowIntoRet(ret, state, innercc, summaryCtx, argT, argAp, t, ap, apa) and
fwdFlowOutValidEdge(_, ret, innercc, _, node, cc, apa, allowsFieldFlow) and
callEdgeReturn(call, _, ret, _, node, allowsFieldFlow, ap) and
label = "" and
if allowsFieldFlow = false then ap instanceof ApNil else any()
)
}

private predicate nonLocalStep(StagePathNode pn1, StagePathNode pn2, string label) {
predicate nonLocalStep(StagePathNode pn1, StagePathNode pn2, string label) {
exists(
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
ApOption argAp, Typ t0, Ap ap
Expand All @@ -2951,7 +3014,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
query predicate edges(StagePathNode pn1, StagePathNode pn2, string key, string val) {
key = "provenance" and
(
localStep(pn1, pn2, val)
localScopeStep(pn1, pn2, val)
or
nonLocalStep(pn1, pn2, val)
or
Expand Down Expand Up @@ -3417,73 +3480,49 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {

predicate enableStoreReadMatching() { any() }

private class NodeExAlias = NodeEx;
final private class NodeExAlias = NodeEx;

final private class ArgNodeExAlias = ArgNodeEx;

final private class ParamNodeExAlias = ParamNodeEx;

private module StoreReadMatchingInput implements StoreReadMatchingInputSig {
class NodeEx = NodeExAlias;

predicate nodeRange(NodeEx node, boolean fromArg) {
exists(PrevStage::Ap ap |
PrevStage::revFlowAp(node, ap) and
(
ap = true
or
PrevStage::storeStepCand(node, ap, _, _, _, _)
or
PrevStage::readStepCand(_, _, node)
)
|
exists(PrevStage::Cc cc | PrevStage::fwdFlow(node, _, cc, _, _, _, _, ap, _) |
PrevStage::instanceofCcCall(cc) and
fromArg = true
or
PrevStage::instanceofCcNoCall(cc) and
fromArg = false
)
)
}
class ArgNodeEx = ArgNodeExAlias;

predicate localValueStep(NodeEx node1, NodeEx node2) {
exists(FlowState state, PrevStage::ApOption returnAp |
PrevStage::revFlow(node1, pragma[only_bind_into](state), _,
pragma[only_bind_into](returnAp), true) and
PrevStage::revFlow(node2, pragma[only_bind_into](state), _,
pragma[only_bind_into](returnAp), true) and
Stage2Param::localStep(node1, state, node2, state, true, _, _, _)
)
}
class ParamNodeEx = ParamNodeExAlias;

predicate jumpValueStep = jumpStepEx/2;
class PathNode = PrevStage::Graph::StagePathNode;

pragma[nomagic]
private predicate flowThroughOutOfCall(RetNodeEx ret, NodeEx out) {
exists(DataFlowCall call, CcCall ccc, ReturnKindExt kind |
PrevStage::callEdgeReturn(call, _, ret, kind, out, true, true) and
PrevStage::callMayFlowThroughRev(call) and
PrevStage::returnMayFlowThrough(ret, _, true, kind) and
matchesCall(ccc, call)
)
predicate localStep(PathNode node1, PathNode node2) {
PrevStage::Graph::localStep(node1, node2, _)
}

predicate callEdgeArgParam(NodeEx arg, NodeEx param) {
PrevStage::callEdgeArgParam(_, _, arg, param, true, true)
predicate nonLocalStep(PathNode node1, PathNode node2) {
PrevStage::Graph::nonLocalStep(node1, node2, _)
}

predicate callEdgeReturn(NodeEx ret, NodeEx out, boolean mayFlowThrough) {
PrevStage::callEdgeReturn(_, _, ret, _, out, true, true) and
if flowThroughOutOfCall(ret, out) then mayFlowThrough = true else mayFlowThrough = false
}
predicate subpaths = PrevStage::Graph::subpaths/4;

predicate readContentStep = PrevStage::readStepCand/3;
predicate readContentStep(PathNode node1, Content c, PathNode node2) {
PrevStage::Graph::readStep(node1, c, node2, _)
}

predicate storeContentStep(NodeEx node1, Content c, NodeEx node2) {
PrevStage::storeStepCand(node1, _, c, node2, _, _)
predicate storeContentStep(PathNode node1, Content c, PathNode node2) {
PrevStage::Graph::storeStep(node1, c, node2, _)
}

predicate accessPathConfigLimit = Config::accessPathLimit/0;
}

predicate storeMayReachRead = StoreReadMatching<StoreReadMatchingInput>::storeMayReachRead/3;
predicate storeMayReachRead(NodeEx storeSource, Content c, NodeEx readTarget) {
exists(StoreReadMatchingInput::PathNode pn1, StoreReadMatchingInput::PathNode pn2 |
StoreReadMatching<StoreReadMatchingInput>::storeMayReachRead(pn1, c, pn2) and
storeSource = pn1.getNodeEx() and
readTarget = pn2.getNodeEx()
)
}
}

private module Stage3 = MkStage<Stage2>::Stage<Stage3Param>;
Expand Down
Loading

0 comments on commit 2a9f751

Please sign in to comment.