Skip to content

Commit 13b8249

Browse files
hvitvedhvitved
committed
Model generator
1 parent 28ccac4 commit 13b8249

File tree

5 files changed

+208
-22
lines changed

5 files changed

+208
-22
lines changed

‎shared/dataflow/codeql/dataflow/DataFlow.qll‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -363,6 +363,11 @@ module Configs<LocationSig Location, InputSig<Location> Lang>{
363363
*/
364364
predicateisSink(Nodesink);
365365

366+
/**
367+
* Holds if `sink` is a relevant data flow sink.
368+
*/
369+
defaultpredicateisSinkReverse(Nodesink){none()}
370+
366371
/**
367372
* Holds if data flow through `node` is prohibited. This completely removes
368373
* `node` from the data flow graph.
@@ -465,6 +470,16 @@ module Configs<LocationSig Location, InputSig<Location> Lang>{
465470
*/
466471
defaultpredicateisSink(Nodesink){none()}
467472

473+
/**
474+
* Holds if `sink` is a relevant data flow sink for any state.
475+
*/
476+
defaultpredicateisSinkReverse(Nodesink){none()}
477+
478+
/**
479+
* Holds if `sink` is a relevant data flow sink accepting `state`.
480+
*/
481+
defaultpredicateisSinkReverse(Nodesink,FlowStatestate){none()}
482+
468483
/**
469484
* Holds if data flow through `node` is prohibited. This completely removes
470485
* `node` from the data flow graph.

‎shared/dataflow/codeql/dataflow/TaintTracking.qll‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -179,6 +179,10 @@ module TaintFlowMake<
179179
Config::isSink(sink,state.getState())
180180
}
181181

182+
predicateisSinkReverse(DataFlowLang::Nodesink,FlowStatestate){
183+
Config::isSinkReverse(sink,state.getState())
184+
}
185+
182186
predicateisBarrier(DataFlowLang::Nodenode,FlowStatestate){
183187
Config::isBarrier(node,state.getState())
184188
}

‎shared/dataflow/codeql/dataflow/internal/ContentDataFlowImpl.qll‎

Lines changed: 46 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,11 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang>{
4646
*/
4747
predicateisSink(Nodesink);
4848

49+
/**
50+
* Holds if `sink` is a relevant data flow sink.
51+
*/
52+
defaultpredicateisSinkReverse(Nodesink){none()}
53+
4954
/**
5055
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
5156
*/
@@ -98,6 +103,15 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang>{
98103
)
99104
}
100105

106+
predicateisSinkReverse(Nodesink,FlowStatestate){
107+
ContentConfig::isSinkReverse(sink)and
108+
(
109+
stateinstanceofInitStateor
110+
stateinstanceofStoreStateor
111+
stateinstanceofReadState
112+
)
113+
}
114+
101115
predicateisAdditionalFlowStep(Nodenode1,FlowStatestate1,Nodenode2,FlowStatestate2){
102116
storeStep(node1,state1, _,node2,state2)or
103117
readStep(node1,state1, _,node2,state2)or
@@ -114,7 +128,35 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang>{
114128
predicateincludeHiddenNodes(){any()}
115129
}
116130

117-
privatemodule Flow = GlobalWithState<FlowConfig>;
131+
module Flow = GlobalWithState<FlowConfig>;
132+
133+
/**
134+
* Holds if data stored inside `sourceAp` on `source` flows to `sinkAp` inside `sink`
135+
* for this configuration. `preservesValue` indicates whether any of the additional
136+
* flow steps defined by `isAdditionalFlowStep` are needed.
137+
*
138+
* For the source access path, `sourceAp`, the top of the stack represents the content
139+
* that was last read from. That is, if `sourceAp` is `Field1.Field2` (with `Field1`
140+
* being the top of the stack), then there is flow from `source.Field2.Field1`.
141+
*
142+
* For the sink access path, `sinkAp`, the top of the stack represents the content
143+
* that was last stored into. That is, if `sinkAp` is `Field1.Field2` (with `Field1`
144+
* being the top of the stack), then there is flow into `sink.Field1.Field2`.
145+
*/
146+
predicateflowPath(
147+
Flow::PathNodesource,AccessPathsourceAp, Flow::PathNodesink,AccessPathsinkAp,
148+
booleanpreservesValue
149+
){
150+
Flow::flowPath(source,sink)and
151+
nodeReaches(source,TAccessPathNil(),TAccessPathNil(),sink,sourceAp,sinkAp)and
152+
(
153+
sink.getState().(InitState).decode(preservesValue)
154+
or
155+
sink.getState().(ReadState).decode(_,preservesValue)
156+
or
157+
sink.getState().(StoreState).decode(_,preservesValue)
158+
)
159+
}
118160

119161
/**
120162
* Holds if data stored inside `sourceAp` on `source` flows to `sinkAp` inside `sink`
@@ -133,16 +175,9 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang>{
133175
Nodesource,AccessPathsourceAp,Nodesink,AccessPathsinkAp,booleanpreservesValue
134176
){
135177
exists(Flow::PathNodepathSource, Flow::PathNodepathSink|
136-
Flow::flowPath(pathSource,pathSink)and
137-
nodeReaches(pathSource,TAccessPathNil(),TAccessPathNil(),pathSink,sourceAp,sinkAp)and
178+
flowPath(pathSource,sourceAp,pathSink,sinkAp,preservesValue)and
138179
source=pathSource.getNode()and
139180
sink=pathSink.getNode()
140-
|
141-
pathSink.getState().(InitState).decode(preservesValue)
142-
or
143-
pathSink.getState().(ReadState).decode(_,preservesValue)
144-
or
145-
pathSink.getState().(StoreState).decode(_,preservesValue)
146181
)
147182
}
148183

@@ -359,6 +394,8 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang>{
359394
or
360395
FlowConfig::isSink(node.getNode(),node.getState())
361396
or
397+
FlowConfig::isSinkReverse(node.getNode(),node.getState())
398+
or
362399
excludeStep(node, _)
363400
or
364401
Flow::PathGraph::subpaths(_, _,node, _)

‎shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll‎

Lines changed: 109 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
4040
*/
4141
predicateisSink(Nodesink);
4242

43+
/**
44+
* Holds if `sink` is a relevant data flow sink accepting `state`.
45+
*/
46+
predicateisSinkReverse(Nodesink,FlowStatestate);
47+
48+
/**
49+
* Holds if `sink` is a relevant data flow sink for any state.
50+
*/
51+
predicateisSinkReverse(Nodesink);
52+
4353
/**
4454
* Holds if data flow through `node` is prohibited. This completely removes
4555
* `node` from the data flow graph.
@@ -149,6 +159,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
149159

150160
predicateisSink(Nodesink,FlowStatestate){ Config::isSink(sink)andexists(state)}
151161

162+
predicateisSinkReverse(Nodesink,FlowStatestate){
163+
Config::isSinkReverse(sink)andexists(state)
164+
}
165+
152166
predicateisBarrier(Nodenode,FlowStatestate){none()}
153167

154168
predicateisBarrierIn(Nodenode,FlowStatestate){none()}
@@ -192,18 +206,32 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
192206
elseany()
193207
}
194208

209+
pragma[nomagic]
210+
privatepredicateisFilteredSinkReverse(Nodesink){
211+
(
212+
Config::isSinkReverse(sink, _)or
213+
Config::isSinkReverse(sink)
214+
)and
215+
if Config::observeDiffInformedIncrementalMode()
216+
then AlertFiltering::filterByLocation(sink.getLocation())
217+
elseany()
218+
}
219+
195220
privatepredicatehasFilteredSource(){isFilteredSource(_)}
196221

197222
privatepredicatehasFilteredSink(){isFilteredSink(_)}
198223

224+
privatepredicatehasFilteredSinkReverse(){isFilteredSinkReverse(_)}
225+
199226
predicateisRelevantSource(Nodesource,FlowStatestate){
200227
// If there are filtered sinks, we need to pass through all sources to preserve all alerts
201228
// with filtered sinks. Otherwise the only alerts of interest are those with filtered
202229
// sources, so we can perform the source filtering right here.
203230
Config::isSource(source,state)and
204231
(
205232
isFilteredSource(source)or
206-
hasFilteredSink()
233+
hasFilteredSink()or
234+
hasFilteredSinkReverse()
207235
)
208236
}
209237

@@ -218,6 +246,17 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
218246
)
219247
}
220248

249+
predicateisRelevantSinkReverse(Nodesink,FlowStatestate){
250+
// If there are filtered sources, we need to pass through all sinks to preserve all alerts
251+
// with filtered sources. Otherwise the only alerts of interest are those with filtered
252+
// sinks, so we can perform the sink filtering right here.
253+
Config::isSinkReverse(sink,state)and
254+
(
255+
isFilteredSinkReverse(sink)or
256+
hasFilteredSource()
257+
)
258+
}
259+
221260
predicateisRelevantSink(Nodesink){
222261
// If there are filtered sources, we need to pass through all sinks to preserve all alerts
223262
// with filtered sources. Otherwise the only alerts of interest are those with filtered
@@ -229,12 +268,30 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
229268
)
230269
}
231270

271+
predicateisRelevantSinkReverse(Nodesink){
272+
// If there are filtered sources, we need to pass through all sinks to preserve all alerts
273+
// with filtered sources. Otherwise the only alerts of interest are those with filtered
274+
// sinks, so we can perform the sink filtering right here.
275+
Config::isSinkReverse(sink)and
276+
(
277+
isFilteredSinkReverse(sink)or
278+
hasFilteredSource()
279+
)
280+
}
281+
232282
bindingset[source, sink]
233283
pragma[inline_late]
234284
predicateisRelevantSourceSinkPair(Nodesource,Nodesink){
235285
isFilteredSource(source)or
236286
isFilteredSink(sink)
237287
}
288+
289+
bindingset[source, sink]
290+
pragma[inline_late]
291+
predicateisRelevantSourceSinkPairReverse(Nodesource,Nodesink){
292+
isFilteredSource(source)or
293+
isFilteredSinkReverse(sink)
294+
}
238295
}
239296

240297
privateimport SourceSinkFiltering
@@ -258,19 +315,28 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
258315

259316
privatepredicateoutBarrier(NodeExnode){
260317
exists(Noden|
261-
[node.asNodeOrImplicitRead(),node.asNodeReverse(_)]=nand
318+
node.asNodeOrImplicitRead()=nand
262319
Config::isBarrierOut(n)
263320
|
264321
isRelevantSink(n, _)
265322
or
266323
isRelevantSink(n)
267324
)
325+
or
326+
exists(Noden|
327+
node.asNodeReverse(_)=nand
328+
Config::isBarrierOut(n)
329+
|
330+
isRelevantSinkReverse(n, _)
331+
or
332+
isRelevantSinkReverse(n)
333+
)
268334
}
269335

270336
pragma[nomagic]
271337
privatepredicateoutBarrier(NodeExnode,FlowStatestate){
272338
exists(Noden|
273-
[node.asNodeOrImplicitRead(),node.asNodeReverse(_)]=nand
339+
node.asNodeOrImplicitRead()=nand
274340
Config::isBarrierOut(n,state)
275341
|
276342
isRelevantSink(n,state)
@@ -321,6 +387,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
321387
notstateBarrier(node,state)
322388
}
323389

390+
pragma[nomagic]
391+
privatepredicatesinkNodeWithStateReverse(NodeExnode,FlowStatestate){
392+
isRelevantSinkReverse(node.asNodeReverse(_),state)and
393+
notfullBarrier(node)and
394+
notstateBarrier(node,state)
395+
}
396+
324397
/** Provides the relevant barriers for a step from `node1` to `node2`. */
325398
bindingset[node1, node2]
326399
privatepredicatestepFilter(NodeExnode1,NodeExnode2){
@@ -707,6 +780,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
707780
fwdFlow(node)and
708781
fwdFlowState(state)and
709782
sinkNodeWithState(node,state)
783+
or
784+
fwdFlow(pragma[only_bind_into](node))and
785+
fwdFlowState(state)and
786+
isRelevantSinkReverse(node.asNodeReverse(_))
787+
or
788+
fwdFlow(node)and
789+
fwdFlowState(state)and
790+
sinkNodeWithState(node,state)
791+
or
792+
fwdFlow(node)and
793+
fwdFlowState(state)and
794+
sinkNodeWithStateReverse(node,state)
710795
}
711796

712797
/**
@@ -1025,7 +1110,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
10251110

10261111
privatepredicatesinkModel(NodeExnode,stringmodel){
10271112
sinkNode(node, _)and
1028-
exists(Noden|n=node.asNodeOrImplicitRead()|
1113+
exists(Noden|n=[node.asNodeOrImplicitRead(),node.asNodeReverse(_)]|
10291114
knownSinkModel(n,model)
10301115
or
10311116
notknownSinkModel(n, _)andmodel=""
@@ -3021,6 +3106,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
30213106
(isRelevantSink(n)orisRelevantSink(n, _))and
30223107
result.asNode()=n
30233108
)
3109+
or
3110+
exists(Noden|
3111+
node.asNodeReverse(_)=nand
3112+
(isRelevantSinkReverse(n)orisRelevantSinkReverse(n, _))and
3113+
result=node
3114+
)
30243115
}
30253116

30263117
overridePathNodeImplgetASuccessorImpl(stringlabel){
@@ -3520,6 +3611,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
35203611
/** Gets the underlying `Node`. */
35213612
finalNodegetNode(){super.getNodeEx().projectToNode()=result}
35223613

3614+
/** Gets the underlying `Node`, but only when it represents a reverse-flow node. */
3615+
finalNodegetNodeReverse(){super.getNodeEx().asNodeReverse(_)=result}
3616+
35233617
/** Gets the parameter node through which data is returned, if any. */
35243618
finalParameterNodeasParameterReturnNode(){
35253619
result=super.getNodeEx().asNodeReverse(_)
@@ -4869,7 +4963,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
48694963
privatepredicateinterestingCallableSink(DataFlowCallablec){
48704964
exists(Noden|c=getNodeEnclosingCallable(n)|
48714965
isRelevantSink(n, _)or
4872-
isRelevantSink(n)
4966+
isRelevantSink(n)or
4967+
isRelevantSinkReverse(n, _)or
4968+
isRelevantSinkReverse(n)
48734969
)
48744970
or
48754971
exists(DataFlowCallablemid|interestingCallableSink(mid)andcallableStep(c,mid))
@@ -4905,7 +5001,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
49055001
ce1=TCallable(getNodeEnclosingCallable(n))
49065002
|
49075003
isRelevantSink(n, _)or
4908-
isRelevantSink(n)
5004+
isRelevantSink(n)or
5005+
isRelevantSinkReverse(n, _)or
5006+
isRelevantSinkReverse(n)
49095007
)
49105008
}
49115009

@@ -4973,6 +5071,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang>{
49735071
relevantState(state)and
49745072
notfullBarrier(node)and
49755073
notstateBarrier(node,state)
5074+
or
5075+
isRelevantSinkReverse(node.asNodeReverse(_))and
5076+
relevantState(state)and
5077+
notfullBarrier(node)and
5078+
notstateBarrier(node,state)
49765079
}
49775080

49785081
privatenewtypeTSummaryCtx1=

0 commit comments

Comments
(0)