Skip to content

Commit 05d9e40

Browse files
hvitvedhvitved
committed
Model generator
1 parent 2542539 commit 05d9e40

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
predicate isSink(Node sink);
365365

366+
/**
367+
* Holds if `sink` is a relevant data flow sink.
368+
*/
369+
default predicate isSinkReverse(Node sink) { 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
default predicate isSink(Node sink) { none() }
467472

473+
/**
474+
* Holds if `sink` is a relevant data flow sink for any state.
475+
*/
476+
default predicate isSinkReverse(Node sink) { none() }
477+
478+
/**
479+
* Holds if `sink` is a relevant data flow sink accepting `state`.
480+
*/
481+
default predicate isSinkReverse(Node sink, FlowState state) { 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+
predicate isSinkReverse(DataFlowLang::Node sink, FlowState state) {
183+
Config::isSinkReverse(sink, state.getState())
184+
}
185+
182186
predicate isBarrier(DataFlowLang::Node node, FlowState state) {
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
predicate isSink(Node sink);
4848

49+
/**
50+
* Holds if `sink` is a relevant data flow sink.
51+
*/
52+
default predicate isSinkReverse(Node sink) { 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+
predicate isSinkReverse(Node sink, FlowState state) {
107+
ContentConfig::isSinkReverse(sink) and
108+
(
109+
state instanceof InitState or
110+
state instanceof StoreState or
111+
state instanceof ReadState
112+
)
113+
}
114+
101115
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
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
predicate includeHiddenNodes() { any() }
115129
}
116130

117-
private module 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+
predicate flowPath(
147+
Flow::PathNode source, AccessPath sourceAp, Flow::PathNode sink, AccessPath sinkAp,
148+
boolean preservesValue
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
Node source, AccessPath sourceAp, Node sink, AccessPath sinkAp, boolean preservesValue
134176
) {
135177
exists(Flow::PathNode pathSource, Flow::PathNode pathSink |
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
predicate isSink(Node sink);
4242

43+
/**
44+
* Holds if `sink` is a relevant data flow sink accepting `state`.
45+
*/
46+
predicate isSinkReverse(Node sink, FlowState state);
47+
48+
/**
49+
* Holds if `sink` is a relevant data flow sink for any state.
50+
*/
51+
predicate isSinkReverse(Node sink);
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
predicate isSink(Node sink, FlowState state) { Config::isSink(sink) and exists(state) }
151161

162+
predicate isSinkReverse(Node sink, FlowState state) {
163+
Config::isSinkReverse(sink) and exists(state)
164+
}
165+
152166
predicate isBarrier(Node node, FlowState state) { none() }
153167

154168
predicate isBarrierIn(Node node, FlowState state) { none() }
@@ -192,18 +206,32 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
192206
else any()
193207
}
194208

209+
pragma[nomagic]
210+
private predicate isFilteredSinkReverse(Node sink) {
211+
(
212+
Config::isSinkReverse(sink, _) or
213+
Config::isSinkReverse(sink)
214+
) and
215+
if Config::observeDiffInformedIncrementalMode()
216+
then AlertFiltering::filterByLocation(sink.getLocation())
217+
else any()
218+
}
219+
195220
private predicate hasFilteredSource() { isFilteredSource(_) }
196221

197222
private predicate hasFilteredSink() { isFilteredSink(_) }
198223

224+
private predicate hasFilteredSinkReverse() { isFilteredSinkReverse(_) }
225+
199226
predicate isRelevantSource(Node source, FlowState state) {
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+
predicate isRelevantSinkReverse(Node sink, FlowState state) {
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
predicate isRelevantSink(Node sink) {
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+
predicate isRelevantSinkReverse(Node sink) {
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
predicate isRelevantSourceSinkPair(Node source, Node sink) {
235285
isFilteredSource(source) or
236286
isFilteredSink(sink)
237287
}
288+
289+
bindingset[source, sink]
290+
pragma[inline_late]
291+
predicate isRelevantSourceSinkPairReverse(Node source, Node sink) {
292+
isFilteredSource(source) or
293+
isFilteredSinkReverse(sink)
294+
}
238295
}
239296

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

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

270336
pragma[nomagic]
271337
private predicate outBarrier(NodeEx node, FlowState state) {
272338
exists(Node n |
273-
[node.asNodeOrImplicitRead(), node.asNodeReverse(_)] = n and
339+
node.asNodeOrImplicitRead() = n and
274340
Config::isBarrierOut(n, state)
275341
|
276342
isRelevantSink(n, state)
@@ -321,6 +387,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
321387
not stateBarrier(node, state)
322388
}
323389

390+
pragma[nomagic]
391+
private predicate sinkNodeWithStateReverse(NodeEx node, FlowState state) {
392+
isRelevantSinkReverse(node.asNodeReverse(_), state) and
393+
not fullBarrier(node) and
394+
not stateBarrier(node, state)
395+
}
396+
324397
/** Provides the relevant barriers for a step from `node1` to `node2`. */
325398
bindingset[node1, node2]
326399
private predicate stepFilter(NodeEx node1, NodeEx node2) {
@@ -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
private predicate sinkModel(NodeEx node, string model) {
10271112
sinkNode(node, _) and
1028-
exists(Node n | n = node.asNodeOrImplicitRead() |
1113+
exists(Node n | n = [node.asNodeOrImplicitRead(), node.asNodeReverse(_)] |
10291114
knownSinkModel(n, model)
10301115
or
10311116
not knownSinkModel(n, _) and model = ""
@@ -2996,6 +3081,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
29963081
(isRelevantSink(n) or isRelevantSink(n, _)) and
29973082
result.asNode() = n
29983083
)
3084+
or
3085+
exists(Node n |
3086+
node.asNodeReverse(_) = n and
3087+
(isRelevantSinkReverse(n) or isRelevantSinkReverse(n, _)) and
3088+
result = node
3089+
)
29993090
}
30003091

30013092
override PathNodeImpl getASuccessorImpl(string label) {
@@ -3492,6 +3583,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
34923583
/** Gets the underlying `Node`. */
34933584
final Node getNode() { super.getNodeEx().projectToNode() = result }
34943585

3586+
/** Gets the underlying `Node`, but only when it represents a reverse-flow node. */
3587+
final Node getNodeReverse() { super.getNodeEx().asNodeReverse(_) = result }
3588+
34953589
/** Gets the parameter node through which data is returned, if any. */
34963590
final ParameterNode asParameterReturnNode() {
34973591
result = super.getNodeEx().asNodeReverse(_)
@@ -4841,7 +4935,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
48414935
private predicate interestingCallableSink(DataFlowCallable c) {
48424936
exists(Node n | c = getNodeEnclosingCallable(n) |
48434937
isRelevantSink(n, _) or
4844-
isRelevantSink(n)
4938+
isRelevantSink(n) or
4939+
isRelevantSinkReverse(n, _) or
4940+
isRelevantSinkReverse(n)
48454941
)
48464942
or
48474943
exists(DataFlowCallable mid | interestingCallableSink(mid) and callableStep(c, mid))
@@ -4877,7 +4973,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
48774973
ce1 = TCallable(getNodeEnclosingCallable(n))
48784974
|
48794975
isRelevantSink(n, _) or
4880-
isRelevantSink(n)
4976+
isRelevantSink(n) or
4977+
isRelevantSinkReverse(n, _) or
4978+
isRelevantSinkReverse(n)
48814979
)
48824980
}
48834981

@@ -4945,6 +5043,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
49455043
relevantState(state) and
49465044
not fullBarrier(node) and
49475045
not stateBarrier(node, state)
5046+
or
5047+
isRelevantSinkReverse(node.asNodeReverse(_)) and
5048+
relevantState(state) and
5049+
not fullBarrier(node) and
5050+
not stateBarrier(node, state)
49485051
}
49495052

49505053
private newtype TSummaryCtx1 =

0 commit comments

Comments
 (0)