From 29ac38c84faaf48b22575711971e18838276e7e3 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Mon, 17 Jun 2024 22:30:57 +0200 Subject: [PATCH] refactor --- .../codeql/dataflow/internal/DataFlowImpl.qll | 488 ++++++------------ .../dataflow/internal/DataFlowImplCommon.qll | 338 ++++++++++++ 2 files changed, 487 insertions(+), 339 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 5012df8e6861a..67582ad4cab89 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -553,6 +553,8 @@ module MakeImpl Lang> { private module Stage1 implements StageSig { class Ap = Unit; + Content getAHeadContent(Ap ap) { any() } + private class Cc = boolean; /* Begin: Stage 1 logic. */ @@ -1019,10 +1021,6 @@ module MakeImpl Lang> { callEdgeReturn(call, c, _, _, _, _, _) } - predicate storeMayReachRead(NodeEx storeSource, Content c, NodeEx readTarget) { none() } - - predicate storeMayReachReadEnabled() { none() } - additional predicate stats( boolean fwd, int nodes, int fields, int conscand, int states, int tuples, int calledges ) { @@ -1283,7 +1281,11 @@ module MakeImpl Lang> { } private signature module StageSig { - class Ap; + class Ap { + string toString(); + } + + Content getAHeadContent(Ap ap); predicate revFlow(NodeEx node); @@ -1318,10 +1320,6 @@ module MakeImpl Lang> { predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c); predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c); - - predicate storeMayReachRead(NodeEx storeSource, Content c, NodeEx readTarget); - - default predicate storeMayReachReadEnabled() { any() } } private module MkStage { @@ -1338,6 +1336,8 @@ module MakeImpl Lang> { class ApNil extends Ap; + Content getAHeadContent(Ap ap); + bindingset[result, ap] ApApprox getApprox(Ap ap); @@ -1410,11 +1410,12 @@ module MakeImpl Lang> { bindingset[cc] LocalCc getLocalCc(Cc cc); + predicate localValueStep(NodeEx node1, NodeEx node2, LocalCc lcc); + bindingset[node1, state1] bindingset[node2, state2] - predicate localStep( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc + predicate localTaintStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, Typ t, LocalCc lcc ); bindingset[node, state, t0, ap] @@ -1424,6 +1425,8 @@ module MakeImpl Lang> { predicate typecheckStore(Typ typ, DataFlowType contentType); default predicate enableTypeFlow() { any() } + + default predicate enableStoreReadMatching() { any() } } module Stage implements StageSig { @@ -1452,6 +1455,46 @@ module MakeImpl Lang> { ) } + private class NodeExAlias = NodeEx; + + private module StoreReadMatchingInput implements StoreReadMatchingInputSig { + class NodeEx = NodeExAlias; + + final private class ApApproxFinal = PrevStage::Ap; + + class Ap extends ApApproxFinal { + Content getHead() { result = PrevStage::getAHeadContent(this) } + } + + predicate revFlow(NodeEx node, Ap ap) { + enableStoreReadMatching() and PrevStage::revFlowAp(node, ap) + } + + predicate localValueStep(NodeEx node1, NodeEx node2) { localValueStep(node1, node2, _) } + + predicate jumpValueStep(NodeEx node1, NodeEx node2) { jumpStepEx(node1, node2) } + + predicate callEdgeArgParam(NodeEx arg, NodeEx param, Ap ap) { + PrevStage::callEdgeArgParam(_, _, arg, param, true, ap) + } + + predicate callEdgeReturn(NodeEx ret, NodeEx out, Ap ap) { + PrevStage::callEdgeReturn(_, _, ret, _, out, true, ap) + } + + predicate readContentStep(NodeEx node1, Content c, NodeEx node2) { + PrevStage::readStepCand(node1, c, node2) + } + + predicate storeContentStep(NodeEx node1, Content c, NodeEx node2) { + PrevStage::storeStepCand(node1, _, c, node2, _, _) + } + + int accessPathConfigLimit() { result = Config::accessPathLimit() } + } + + private import StoreReadMatching + /** * Holds if `node` is reachable with access path `ap` from a source. * @@ -1486,7 +1529,22 @@ module MakeImpl Lang> { private predicate storeMayReachReadInlineLate( NodeEx storeSource, Content c, NodeEx readTarget ) { - PrevStage::storeMayReachRead(storeSource, c, readTarget) + storeMayReachRead(storeSource, c, readTarget) + } + + bindingset[node1, state1] + bindingset[node2, state2] + private predicate localStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, + Typ t, LocalCc lcc + ) { + localValueStep(node1, node2, lcc) and + state1 = state2 and + preservesValue = true and + t = getNodeTyp(node1) + or + localTaintStep(node1, state1, node2, state2, t, lcc) and + preservesValue = false } pragma[nomagic] @@ -1533,11 +1591,11 @@ module MakeImpl Lang> { apa = getApprox(ap) | exists(NodeEx storeSource | - fwdFlowConsCandStoreMayReachReadEnabled(storeSource, t0, ap0, c, t, ap) and + fwdFlowConsCandStoreReadMatchingEnabled(storeSource, t0, ap0, c, t, ap) and storeMayReachReadInlineLate(storeSource, c, node) ) or - fwdFlowConsCandStoreMayReachReadDisabled(t0, ap0, c, t, ap) + fwdFlowConsCandStoreReadMatchingDisabled(t0, ap0, c, t, ap) ) or // flow into a callable @@ -1598,7 +1656,8 @@ module MakeImpl Lang> { fwdFlow(node1, state, cc, summaryCtx, argT, argAp, t1, ap1, apa1) and PrevStage::storeStepCand(node1, apa1, c, node2, contentType, containerType) and t2 = getTyp(containerType) and - typecheckStore(t1, contentType) + typecheckStore(t1, contentType) and + if enableStoreReadMatching() then storeMayReachRead(node1, c, _) else any() ) } @@ -1607,20 +1666,19 @@ module MakeImpl Lang> { * store of `c` on a container of type `t2` resulting in access path * `cons`. `storeSource` is a relevant store source. * - * This predicate is only evaluated when `PrevStage::storeMayReachReadEnabled()` - * holds. + * This predicate is only evaluated when `enableStoreReadMatching()` holds. */ pragma[nomagic] - private predicate fwdFlowConsCandStoreMayReachReadEnabled( + private predicate fwdFlowConsCandStoreReadMatchingEnabled( NodeEx storeSource, Typ t2, Ap cons, Content c, Typ t1, Ap tail ) { - PrevStage::storeMayReachReadEnabled() and + enableStoreReadMatching() and fwdFlowStore(storeSource, t1, tail, c, t2, _, _, _, _, _, _) and cons = apCons(c, t1, tail) or exists(Typ t0 | typeStrengthen(t0, cons, t2) and - fwdFlowConsCandStoreMayReachReadEnabled(storeSource, t0, cons, c, t1, tail) + fwdFlowConsCandStoreReadMatchingEnabled(storeSource, t0, cons, c, t1, tail) ) } @@ -1629,27 +1687,28 @@ module MakeImpl Lang> { * store of `c` on a container of type `t2` resulting in access path * `cons`. * - * This predicate is only evaluated when `PrevStage::storeMayReachReadEnabled()` + * This predicate is only evaluated when `enableStoreReadMatching()` * doesn't hold. */ pragma[nomagic] - private predicate fwdFlowConsCandStoreMayReachReadDisabled( + private predicate fwdFlowConsCandStoreReadMatchingDisabled( Typ t2, Ap cons, Content c, Typ t1, Ap tail ) { - not PrevStage::storeMayReachReadEnabled() and + not enableStoreReadMatching() and fwdFlowStore(_, t1, tail, c, t2, _, _, _, _, _, _) and cons = apCons(c, t1, tail) or exists(Typ t0 | typeStrengthen(t0, cons, t2) and - fwdFlowConsCandStoreMayReachReadDisabled(t0, cons, c, t1, tail) + fwdFlowConsCandStoreReadMatchingDisabled(t0, cons, c, t1, tail) ) } pragma[nomagic] private predicate readStepCand(NodeEx node1, ApHeadContent apc, Content c, NodeEx node2) { PrevStage::readStepCand(node1, c, node2) and - apc = projectToHeadContent(c) + apc = projectToHeadContent(c) and + if enableStoreReadMatching() then storeMayReachRead(_, c, node2) else any() } bindingset[node1, apc] @@ -2095,11 +2154,11 @@ module MakeImpl Lang> { private predicate readStepFwd(NodeEx n1, Ap ap1, Content c, NodeEx n2, Ap ap2) { exists(Typ t1 | fwdFlowRead(t1, ap1, c, n1, n2, _, _, _, _, _) | exists(NodeEx storeSource | - fwdFlowConsCandStoreMayReachReadEnabled(storeSource, t1, ap1, c, _, ap2) and + fwdFlowConsCandStoreReadMatchingEnabled(storeSource, t1, ap1, c, _, ap2) and storeMayReachReadInlineLate(storeSource, c, n2) ) or - fwdFlowConsCandStoreMayReachReadDisabled(t1, ap1, c, _, ap2) + fwdFlowConsCandStoreReadMatchingDisabled(t1, ap1, c, _, ap2) ) } @@ -2221,7 +2280,7 @@ module MakeImpl Lang> { storeMayReachReadInlineLate(node, c, readTarget) ) or - revFlowConsCandStoreMayReachReadDisabled(ap0, c, ap) + revFlowConsCandStoreReadMatchingDisabled(ap0, c, ap) ) or // read @@ -2300,8 +2359,8 @@ module MakeImpl Lang> { * resulting in access path `cons`. */ pragma[nomagic] - private predicate revFlowConsCandStoreMayReachReadDisabled(Ap cons, Content c, Ap tail) { - not PrevStage::storeMayReachReadEnabled() and + private predicate revFlowConsCandStoreReadMatchingDisabled(Ap cons, Content c, Ap tail) { + not enableStoreReadMatching() and revFlowConsCand(_, cons, c, tail) } @@ -2422,7 +2481,7 @@ module MakeImpl Lang> { } pragma[nomagic] - private predicate storeStepCand0( + predicate storeStepCand( NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType, DataFlowType containerType ) { @@ -2434,7 +2493,7 @@ module MakeImpl Lang> { } pragma[nomagic] - private predicate readStepCand0(NodeEx node1, Content c, NodeEx node2) { + predicate readStepCand(NodeEx node1, Content c, NodeEx node2) { exists(Ap ap1, Ap ap2 | revFlow(node2, _, _, _, pragma[only_bind_into](ap2)) and readStepFwd(node1, ap1, c, node2, ap2) and @@ -2458,7 +2517,9 @@ module MakeImpl Lang> { exists(NodeEx storeSource, Ap ap2 | revFlowStore(ap2, c, ap, t, storeSource, _, _, _, _) and revFlowConsCand(readTarget, ap2, c, ap) and - storeMayReachRead(storeSource, c, readTarget) + if enableStoreReadMatching() + then storeMayReachRead(storeSource, c, readTarget) + else any() ) } @@ -2561,289 +2622,6 @@ module MakeImpl Lang> { callEdgeReturn(call, c, _, _, _, _, _) } - /** - * Provides logic for computing compatible and (likely) reachable store-read pairs. - * - * In order to determine whether a store can reach a compatible read, we first compute - * the set of contents that may be both stored and read. - * - * The implementation is based on `doublyBoundedFastTC`, and in order to avoid poor - * performance through recursion, we unroll the recursion manually 4 times, in order to - * be able to handle access paths of maximum length 5. - */ - private module StoreReadReachability { - final private class ApFinal = Ap; - - private class ApCons extends ApFinal { - ApCons() { not this instanceof ApNil } - } - - pragma[nomagic] - private predicate valueStep(NodeEx node1, NodeEx node2, ApCons ap) { - exists(FlowState state, ApOption returnAp1, ApOption returnAp2 | - revFlow(node1, pragma[only_bind_into](state), _, returnAp1, pragma[only_bind_into](ap)) and - revFlow(node2, pragma[only_bind_into](state), _, returnAp2, pragma[only_bind_into](ap)) - | - localStep(node1, state, node2, state, true, _, _) and - returnAp1 = returnAp2 - or - jumpStepEx(node1, node2) - or - callEdgeArgParam(_, _, node1, node2, _, ap) - or - callEdgeReturn(_, _, node1, _, node2, _, ap) - ) - } - - private signature module StoreReachesReadInputSig { - int iteration(); - - predicate storeMayReachReadDelta(NodeEx storeSource, Content c, NodeEx readTarget); - - predicate storeMayReachReadPrev(NodeEx storeSource, Content c, NodeEx readTarget); - } - - private signature class UsesPrevDeltaInfoSig { - string toString(); - - boolean toBoolean(); - } - - private module StoreReachesRead< - StoreReachesReadInputSig Prev, UsesPrevDeltaInfoSig UsesPrevDeltaInfo> implements - StoreReachesReadInputSig - { - int iteration() { result = Prev::iteration() + 1 } - - private predicate enabled() { Config::accessPathLimit() > Prev::iteration() } - - private newtype TNodeOrContent = - TNodeOrContentNode( - NodeEx n, FlowState state, ApCons ap, UsesPrevDeltaInfo usesPrevDelta - ) { - enabled() and - revFlow(n, state, _, _, ap) - } or - TNodeOrContentContentStart(Content c) { enabled() and readStepCand0(_, c, _) } or - TNodeOrContentContentEnd(Content c) { enabled() and readStepCand0(_, c, _) } - - private class NodeOrContent extends TNodeOrContent { - NodeEx asNodeEx(FlowState state, Ap ap, UsesPrevDeltaInfo usesPrevDelta) { - this = TNodeOrContentNode(result, state, ap, usesPrevDelta) - } - - Content asContentStart() { this = TNodeOrContentContentStart(result) } - - Content asContentEnd() { this = TNodeOrContentContentEnd(result) } - - string toString() { - result = this.asContentStart().toString() - or - result = this.asContentEnd().toString() - or - result = this.asNodeEx(_, _, _).toString() - } - } - - pragma[nomagic] - private predicate step(NodeOrContent node1, NodeOrContent node2) { - exists( - NodeEx n1, NodeEx n2, FlowState state, Ap ap, UsesPrevDeltaInfo usesPrevDelta1, - UsesPrevDeltaInfo usesPrevDelta2 - | - n1 = - node1 - .asNodeEx(pragma[only_bind_into](state), pragma[only_bind_into](ap), - usesPrevDelta1) and - n2 = - node2 - .asNodeEx(pragma[only_bind_into](state), pragma[only_bind_into](ap), - usesPrevDelta2) - | - valueStep(n1, n2, ap) and - pragma[only_bind_into](pragma[only_bind_out](usesPrevDelta2)) = - pragma[only_bind_into](pragma[only_bind_out](usesPrevDelta1)) - or - Prev::storeMayReachReadDelta(n1, _, n2) and usesPrevDelta2.toBoolean() = true - or - Prev::storeMayReachReadPrev(n1, _, n2) and - pragma[only_bind_into](pragma[only_bind_out](usesPrevDelta2)) = - pragma[only_bind_into](pragma[only_bind_out](usesPrevDelta1)) - ) - or - exists(NodeEx n2, Content c, ApCons ap2, UsesPrevDeltaInfo usesPrevDelta2 | - n2 = node2.asNodeEx(_, ap2, usesPrevDelta2) and - c = node1.asContentStart() and - projectToHeadContent(c) = getHeadContent(ap2) and - storeStepCand0(_, _, c, n2, _, _) and - usesPrevDelta2.toBoolean() = false - ) - or - exists(NodeEx n1, Content c, ApCons ap1, UsesPrevDeltaInfo usesPrevDelta1 | - n1 = node1.asNodeEx(_, ap1, usesPrevDelta1) and - c = node2.asContentEnd() and - projectToHeadContent(c) = getHeadContent(ap1) and - readStepCand0(n1, c, _) and - usesPrevDelta1.toBoolean() = true - ) - } - - private predicate contentIsStored(NodeOrContent c) { - storeStepCand0(_, _, c.asContentStart(), _, _, _) - } - - private predicate contentIsRead(NodeOrContent c) { - readStepCand0(_, c.asContentEnd(), _) - } - - private predicate contentReachesReadTc(NodeOrContent node1, NodeOrContent node2) = - doublyBoundedFastTC(step/2, contentIsStored/1, contentIsRead/1)(node1, node2) - - pragma[nomagic] - private predicate contentId(NodeOrContent c1, NodeOrContent c2, Content c) { - c1.asContentStart() = c and - c2.asContentEnd() = c - } - - additional predicate contentIsReadAndStored(Content c) { - exists(NodeOrContent n1, NodeOrContent n2 | - contentReachesReadTc(n1, n2) and - contentId(n1, n2, c) - ) - } - - private predicate isStoreTarget(NodeOrContent node) { - exists(Content c, Ap ap, UsesPrevDeltaInfo usesPrevDelta | - contentIsReadAndStored(c) and - storeStepCand0(_, _, c, node.asNodeEx(_, ap, usesPrevDelta), _, _) and - projectToHeadContent(c) = getHeadContent(ap) and - usesPrevDelta.toBoolean() = false - ) - } - - private predicate isReadSource(NodeOrContent node) { - exists(Content c, Ap ap, UsesPrevDeltaInfo usesPrevDelta | - contentIsReadAndStored(c) and - readStepCand0(node.asNodeEx(_, ap, usesPrevDelta), c, _) and - projectToHeadContent(c) = getHeadContent(ap) and - usesPrevDelta.toBoolean() = true - ) - } - - private predicate storeMayReachReadTc(NodeOrContent node1, NodeOrContent node2) = - doublyBoundedFastTC(step/2, isStoreTarget/1, isReadSource/1)(node1, node2) - - pragma[nomagic] - private predicate storeStepCandIsReadAndStored( - NodeEx node1, Content c, NodeOrContent node2 - ) { - exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta | - contentIsReadAndStored(c) and - storeStepCand0(node1, _, c, node2.asNodeEx(_, ap, usesPrevDelta), _, _) and - projectToHeadContent(c) = getHeadContent(ap) and - usesPrevDelta.toBoolean() = false - ) - } - - pragma[nomagic] - private predicate readStepCandIsReadAndStored( - NodeOrContent node1, Content c, NodeEx node2 - ) { - exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta | - contentIsReadAndStored(c) and - readStepCand0(node1.asNodeEx(_, ap, usesPrevDelta), c, node2) and - projectToHeadContent(c) = getHeadContent(ap) and - usesPrevDelta.toBoolean() = true - ) - } - - pragma[nomagic] - predicate storeMayReachReadPrev(NodeEx storeSource, Content c, NodeEx readTarget) { - Prev::storeMayReachReadPrev(storeSource, c, readTarget) - or - Prev::storeMayReachReadDelta(storeSource, c, readTarget) - } - - pragma[nomagic] - predicate storeMayReachReadDelta(NodeEx storeSource, Content c, NodeEx readTarget) { - exists(NodeOrContent storeTarget, NodeOrContent readSource | - storeMayReachReadTc(storeTarget, readSource) and - storeStepCandIsReadAndStored(storeSource, c, storeTarget) and - readStepCandIsReadAndStored(readSource, c, readTarget) - ) and - not Prev::storeMayReachReadPrev(storeSource, c, readTarget) - } - } - - module Iteration0 implements StoreReachesReadInputSig { - int iteration() { result = 0 } - - predicate storeMayReachReadDelta(NodeEx node1, Content c, NodeEx node2) { none() } - - predicate storeMayReachReadPrev(NodeEx node1, Content c, NodeEx node2) { none() } - } - - private class UsesPrevDeltaInfoUnit extends Unit { - boolean toBoolean() { result = [false, true] } - } - - private module StoreReachesRead1 implements StoreReachesReadInputSig { - private module M = StoreReachesRead; - - import M - - predicate storeMayReachReadDelta(NodeEx storeSource, Content c, NodeEx readTarget) { - M::storeMayReachReadDelta(storeSource, c, readTarget) - or - // special case only needed for the first iteration: a store immediately followed by a read - exists(NodeEx storeTargetReadSource | - StoreReachesRead1::contentIsReadAndStored(c) and - storeStepCand0(storeSource, _, c, storeTargetReadSource, _, _) and - readStepCand0(storeTargetReadSource, c, readTarget) - ) - } - } - - private class UsesPrevDeltaInfoBoolean extends Boolean { - boolean toBoolean() { result = this } - } - - private module StoreReachesRead2 = - StoreReachesRead; - - private module StoreReachesRead3 = - StoreReachesRead; - - private module StoreReachesRead4 = - StoreReachesRead; - - private module StoreReachesRead5 = - StoreReachesRead; - - predicate storeMayReachRead(NodeEx storeSource, Content c, NodeEx readTarget) { - StoreReachesRead5::storeMayReachReadDelta(storeSource, c, readTarget) - or - StoreReachesRead5::storeMayReachReadPrev(storeSource, c, readTarget) - } - } - - predicate storeMayReachRead = StoreReadReachability::storeMayReachRead/3; - - pragma[nomagic] - predicate storeStepCand( - NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType, - DataFlowType containerType - ) { - storeStepCand0(node1, ap1, c, node2, contentType, containerType) and - storeMayReachRead(node1, c, _) - } - - pragma[nomagic] - predicate readStepCand(NodeEx node1, Content c, NodeEx node2) { - readStepCand0(node1, c, node2) and - storeMayReachRead(_, c, node2) - } - additional predicate stats( boolean fwd, int nodes, int fields, int conscand, int states, int tuples, int calledges, int tfnodes, int tftuples @@ -2941,6 +2719,8 @@ module MakeImpl Lang> { ApNil() { this = false } } + Content getAHeadContent(Ap ap) { ap = true and exists(result) } + bindingset[result, ap] PrevStage::Ap getApprox(Ap ap) { any() } @@ -2970,22 +2750,20 @@ module MakeImpl Lang> { import CachedCallContextSensitivity import NoLocalCallContext + predicate localValueStep(NodeEx node1, NodeEx node2, LocalCc lcc) { + localFlowStepNodeCand1(node1, node2, _) and + exists(lcc) + } + bindingset[node1, state1] bindingset[node2, state2] - predicate localStep( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc + predicate localTaintStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, Typ t, LocalCc lcc ) { ( - preservesValue = true and - localFlowStepNodeCand1(node1, node2, _) and - state1 = state2 - or - preservesValue = false and additionalLocalFlowStepNodeCand1(node1, node2, _) and state1 = state2 or - preservesValue = false and additionalLocalStateStep(node1, state1, node2, state2) ) and exists(t) and @@ -3019,6 +2797,8 @@ module MakeImpl Lang> { predicate typecheckStore(Typ typ, DataFlowType contentType) { any() } predicate enableTypeFlow() { none() } + + predicate enableStoreReadMatching() { none() } } private module Stage2 = MkStage::Stage; @@ -3219,6 +2999,8 @@ module MakeImpl Lang> { class Ap = ApproxAccessPathFront; + Content getAHeadContent(Ap ap) { result = ap.getAHead() } + class ApNil = ApproxAccessPathFrontNil; PrevStage::Ap getApprox(Ap ap) { result = ap.toBoolNonEmpty() } @@ -3256,11 +3038,15 @@ module MakeImpl Lang> { import CallContextSensitivity import NoLocalCallContext - predicate localStep( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc + predicate localValueStep(NodeEx node1, NodeEx node2, LocalCc lcc) { + localFlowBigStep(node1, _, node2, _, true, _, _, _) and + exists(lcc) + } + + predicate localTaintStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, Typ t, LocalCc lcc ) { - localFlowBigStep(node1, state1, node2, state2, preservesValue, t, _, _) and + localFlowBigStep(node1, state1, node2, state2, false, t, _, _) and exists(lcc) } @@ -3320,6 +3106,8 @@ module MakeImpl Lang> { class ApNil = AccessPathFrontNil; + Content getAHeadContent(Ap ap) { result = ap.getHead() } + PrevStage::Ap getApprox(Ap ap) { result = ap.toApprox() } Typ getTyp(DataFlowType t) { result = t } @@ -3343,11 +3131,20 @@ module MakeImpl Lang> { import BooleanCallContext pragma[nomagic] - predicate localStep( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc + predicate localValueStep(NodeEx node1, NodeEx node2, LocalCc lcc) { + exists(FlowState state | + localFlowBigStep(node1, _, node2, _, true, _, _, _) and + PrevStage::revFlow(node1, pragma[only_bind_into](state), _) and + PrevStage::revFlow(node2, pragma[only_bind_into](state), _) and + exists(lcc) + ) + } + + pragma[nomagic] + predicate localTaintStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, Typ t, LocalCc lcc ) { - localFlowBigStep(node1, state1, node2, state2, preservesValue, t, _, _) and + localFlowBigStep(node1, state1, node2, state2, false, t, _, _) and PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and PrevStage::revFlow(node2, pragma[only_bind_into](state2), _) and exists(lcc) @@ -3606,6 +3403,8 @@ module MakeImpl Lang> { class Ap = AccessPathApprox; + Content getAHeadContent(Ap ap) { result = ap.getHead() } + class ApNil = AccessPathApproxNil; pragma[nomagic] @@ -3643,13 +3442,24 @@ module MakeImpl Lang> { import CallContextSensitivity import LocalCallContext - predicate localStep( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc + pragma[nomagic] + predicate localValueStep(NodeEx node1, NodeEx node2, LocalCc lcc) { + exists(FlowState state | + localFlowBigStep(node1, _, node2, _, true, _, _, _) and + PrevStage::revFlow(node1, pragma[only_bind_into](state), _) and + PrevStage::revFlow(node2, pragma[only_bind_into](state), _) and + exists(lcc) + ) + } + + pragma[nomagic] + predicate localTaintStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, Typ t, LocalCc lcc ) { - localFlowBigStep(node1, state1, node2, state2, preservesValue, t, lcc, _) and + localFlowBigStep(node1, state1, node2, state2, false, t, _, _) and PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and - PrevStage::revFlow(node2, pragma[only_bind_into](state2), _) + PrevStage::revFlow(node2, pragma[only_bind_into](state2), _) and + exists(lcc) } bindingset[node, state, t0, ap] diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll index 3023450d083a7..9ec260d156254 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll @@ -2351,4 +2351,342 @@ module MakeImplCommon Lang> { this = TAccessPathFrontSome(any(AccessPathFront apf | result = apf.toString())) } } + + signature module StoreReadMatchingInputSig { + class NodeEx { + string toString(); + } + + class Ap { + string toString(); + + Content getHead(); + } + + predicate revFlow(NodeEx node, Ap ap); + + predicate localValueStep(NodeEx node1, NodeEx node2); + + predicate jumpValueStep(NodeEx node1, NodeEx node2); + + predicate callEdgeArgParam(NodeEx arg, NodeEx param, Ap ap); + + predicate callEdgeReturn(NodeEx ret, NodeEx out, Ap ap); + + predicate readContentStep(NodeEx node1, Content c, NodeEx node2); + + predicate storeContentStep(NodeEx node1, Content c, NodeEx node2); + + int accessPathConfigLimit(); + } + + /** + * Provides logic for computing compatible and (likely) matching store-read pairs. + * + * In order to determine whether a store can be matched with a compatible read, we + * check whether the target of a store may reach the source of a read, using simple + * data flow. + * + * The implementation is based on `doublyBoundedFastTC`, and in order to avoid poor + * performance through recursion, we unroll the recursion manually 4 times, in order to + * be able to handle access paths of maximum length 5. + * + * Additionally, in order to speed up the join with `doublyBoundedFastTC`, we first + * compute three pruning steps: + * + * 1. Which contents may have matching read-store pairs (called `contentIsReadAndStored` below). + * 2. Which store targets may have a matching read (called `storeMayReachARead` below). + * 3. Which reads may have a matching store (called `aStoreMayReachRead` below). + */ + module StoreReadMatching { + private import Input + + final private class ApFinal = Ap; + + private class ApCons extends ApFinal { + ApCons() { exists(this.getHead()) } + } + + pragma[nomagic] + private predicate valueStep(NodeEx node1, NodeEx node2) { + exists(ApCons ap | + revFlow(node1, pragma[only_bind_into](ap)) and + revFlow(node2, pragma[only_bind_into](ap)) + | + localValueStep(node1, node2) + or + jumpValueStep(node1, node2) + or + callEdgeArgParam(node1, node2, ap) + or + callEdgeReturn(node1, node2, ap) + ) + } + + private signature module StoreReachesReadInputSig { + int iteration(); + + predicate storeMayReachReadDelta(NodeEx storeSource, Content c, NodeEx readTarget); + + predicate storeMayReachReadPrev(NodeEx storeSource, Content c, NodeEx readTarget); + } + + private signature class UsesPrevDeltaInfoSig { + string toString(); + + boolean toBoolean(); + } + + private module StoreReachesRead< + StoreReachesReadInputSig Prev, UsesPrevDeltaInfoSig UsesPrevDeltaInfo> implements + StoreReachesReadInputSig + { + int iteration() { result = Prev::iteration() + 1 } + + private predicate enabled() { accessPathConfigLimit() > Prev::iteration() } + + private newtype TNodeOrContent = + TNodeOrContentNode(NodeEx n, ApCons ap, UsesPrevDeltaInfo usesPrevDelta) { + enabled() and + revFlow(n, ap) + } or + TNodeOrContentContentStart(Content c) { enabled() and storeContentStep(_, c, _) } or + TNodeOrContentContentEnd(Content c) { enabled() and readContentStep(_, c, _) } + + private class NodeOrContent extends TNodeOrContent { + NodeEx asNodeEx(Ap ap, UsesPrevDeltaInfo usesPrevDelta) { + this = TNodeOrContentNode(result, ap, usesPrevDelta) + } + + Content asContentStart() { this = TNodeOrContentContentStart(result) } + + Content asContentEnd() { this = TNodeOrContentContentEnd(result) } + + string toString() { + result = this.asContentStart().toString() + or + result = this.asContentEnd().toString() + or + result = this.asNodeEx(_, _).toString() + } + } + + pragma[nomagic] + private predicate step(NodeOrContent node1, NodeOrContent node2) { + exists( + NodeEx n1, NodeEx n2, Ap ap, UsesPrevDeltaInfo usesPrevDelta1, + UsesPrevDeltaInfo usesPrevDelta2 + | + n1 = node1.asNodeEx(pragma[only_bind_into](ap), usesPrevDelta1) and + n2 = node2.asNodeEx(pragma[only_bind_into](ap), usesPrevDelta2) + | + valueStep(n1, n2) and + pragma[only_bind_into](pragma[only_bind_out](usesPrevDelta2)) = + pragma[only_bind_into](pragma[only_bind_out](usesPrevDelta1)) + or + Prev::storeMayReachReadDelta(n1, _, n2) and usesPrevDelta2.toBoolean() = true + or + Prev::storeMayReachReadPrev(n1, _, n2) and + pragma[only_bind_into](pragma[only_bind_out](usesPrevDelta2)) = + pragma[only_bind_into](pragma[only_bind_out](usesPrevDelta1)) + ) + or + exists(NodeEx n2, Content c, ApCons ap2, UsesPrevDeltaInfo usesPrevDelta2 | + n2 = node2.asNodeEx(ap2, usesPrevDelta2) and + c = node1.asContentStart() and + c = ap2.getHead() and + storeContentStep(_, c, n2) and + usesPrevDelta2.toBoolean() = false + ) + or + exists(NodeEx n1, Content c, ApCons ap1, UsesPrevDeltaInfo usesPrevDelta1 | + n1 = node1.asNodeEx(ap1, usesPrevDelta1) and + c = node2.asContentEnd() and + c = ap1.getHead() and + readContentStep(n1, c, _) and + usesPrevDelta1.toBoolean() = true + ) + } + + private predicate contentIsStored(NodeOrContent c) { + storeContentStep(_, c.asContentStart(), _) + } + + private predicate contentIsRead(NodeOrContent c) { readContentStep(_, c.asContentEnd(), _) } + + private predicate contentReachesReadTc(NodeOrContent node1, NodeOrContent node2) = + doublyBoundedFastTC(step/2, contentIsStored/1, contentIsRead/1)(node1, node2) + + pragma[nomagic] + private predicate contentIsReadAndStoredJoin(NodeOrContent c1, NodeOrContent c2, Content c) { + c1.asContentStart() = c and + c2.asContentEnd() = c + } + + additional predicate contentIsReadAndStored(Content c) { + exists(NodeOrContent n1, NodeOrContent n2 | + contentReachesReadTc(n1, n2) and + contentIsReadAndStoredJoin(n1, n2, c) + ) + } + + private predicate isStoreTarget0(NodeOrContent node, Content c) { + exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta | + contentIsReadAndStored(c) and + storeContentStep(_, c, node.asNodeEx(ap, usesPrevDelta)) and + c = ap.getHead() and + usesPrevDelta.toBoolean() = false + ) + } + + private predicate isStoreTarget(NodeOrContent node) { isStoreTarget0(node, _) } + + private predicate isReadSource0(NodeOrContent node, Content c) { + exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta | + contentIsReadAndStored(c) and + readContentStep(node.asNodeEx(ap, usesPrevDelta), c, _) and + c = ap.getHead() and + usesPrevDelta.toBoolean() = true + ) + } + + private predicate isReadSource(NodeOrContent node) { isReadSource0(node, _) } + + private predicate storeMayReachAReadTc(NodeOrContent node1, NodeOrContent node2) = + doublyBoundedFastTC(step/2, isStoreTarget/1, contentIsRead/1)(node1, node2) + + pragma[nomagic] + private predicate storeMayReachAReadJoin(NodeOrContent n1, NodeOrContent n2, Content c) { + isStoreTarget0(n1, c) and + n2.asContentEnd() = c + } + + private predicate storeMayReachARead(NodeOrContent node1, Content c) { + exists(NodeOrContent node2 | + storeMayReachAReadTc(node1, node2) and + storeMayReachAReadJoin(node1, node2, c) + ) + } + + private predicate aStoreMayReachReadTc(NodeOrContent node1, NodeOrContent node2) = + doublyBoundedFastTC(step/2, contentIsStored/1, isReadSource/1)(node1, node2) + + pragma[nomagic] + private predicate aStoreMayReachReadJoin(NodeOrContent n1, NodeOrContent n2, Content c) { + n1.asContentStart() = c and + isReadSource0(n2, c) + } + + additional predicate aStoreMayReachRead(NodeOrContent node2, Content c) { + exists(NodeOrContent node1 | + aStoreMayReachReadTc(node1, node2) and + aStoreMayReachReadJoin(node1, node2, c) + ) + } + + private predicate isStoreTargetPruned(NodeOrContent node) { + isStoreTarget(node) and + storeMayReachARead(node, _) + } + + private predicate isReadSourcePruned(NodeOrContent node) { + isReadSource(node) and + aStoreMayReachRead(node, _) + } + + private predicate storeMayReachReadTc(NodeOrContent node1, NodeOrContent node2) = + doublyBoundedFastTC(step/2, isStoreTargetPruned/1, isReadSourcePruned/1)(node1, node2) + + pragma[nomagic] + private predicate storeMayReachReadDeltaJoinLeft(NodeEx node1, Content c, NodeOrContent node2) { + exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta | + storeMayReachARead(node2, c) and + storeContentStep(node1, c, node2.asNodeEx(ap, usesPrevDelta)) and + c = ap.getHead() and + usesPrevDelta.toBoolean() = false + ) + } + + pragma[nomagic] + private predicate storeMayReachReadDeltaJoinRight(NodeOrContent node1, Content c, NodeEx node2) { + exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta | + aStoreMayReachRead(node1, c) and + readContentStep(node1.asNodeEx(ap, usesPrevDelta), c, node2) and + c = ap.getHead() and + usesPrevDelta.toBoolean() = true + ) + } + + pragma[nomagic] + predicate storeMayReachReadDelta(NodeEx storeSource, Content c, NodeEx readTarget) { + exists(NodeOrContent storeTarget, NodeOrContent readSource | + storeMayReachReadTc(storeTarget, readSource) and + storeMayReachReadDeltaJoinLeft(storeSource, c, storeTarget) and + storeMayReachReadDeltaJoinRight(readSource, c, readTarget) + ) and + not Prev::storeMayReachReadPrev(storeSource, c, readTarget) + } + + pragma[nomagic] + predicate storeMayReachReadPrev(NodeEx storeSource, Content c, NodeEx readTarget) { + Prev::storeMayReachReadPrev(storeSource, c, readTarget) + or + Prev::storeMayReachReadDelta(storeSource, c, readTarget) + } + } + + module Iteration0 implements StoreReachesReadInputSig { + int iteration() { result = 0 } + + predicate storeMayReachReadDelta(NodeEx node1, Content c, NodeEx node2) { none() } + + predicate storeMayReachReadPrev(NodeEx node1, Content c, NodeEx node2) { none() } + } + + // in the first iteration there is no previous delta to use + private class UsesPrevDeltaInfoUnit extends Unit { + boolean toBoolean() { result = [false, true] } + } + + private module StoreReachesRead1 implements StoreReachesReadInputSig { + private module M = StoreReachesRead; + + import M + + predicate storeMayReachReadDelta(NodeEx storeSource, Content c, NodeEx readTarget) { + M::storeMayReachReadDelta(storeSource, c, readTarget) + or + // special case only needed for the first iteration: a store immediately followed by a read + exists(NodeEx storeTargetReadSource | + StoreReachesRead1::contentIsReadAndStored(c) and + storeContentStep(storeSource, c, storeTargetReadSource) and + readContentStep(storeTargetReadSource, c, readTarget) + ) + } + } + + private import codeql.util.Boolean + + private class UsesPrevDeltaInfoBoolean extends Boolean { + boolean toBoolean() { result = this } + } + + private module StoreReachesRead2 = + StoreReachesRead; + + private module StoreReachesRead3 = + StoreReachesRead; + + private module StoreReachesRead4 = + StoreReachesRead; + + private module StoreReachesRead5 = + StoreReachesRead; + + predicate storeMayReachRead(NodeEx storeSource, Content c, NodeEx readTarget) { + StoreReachesRead5::storeMayReachReadDelta(storeSource, c, readTarget) + or + StoreReachesRead5::storeMayReachReadPrev(storeSource, c, readTarget) + } + } }