Skip to content

Commit 65a4f36

Browse files
aschackmullaschackmull
authored
Merge pull request github#6767 from aschackmull/dataflow/callback-postupdate
Dataflow: Support side-effects for callbacks in summaries.
2 parents ce27acd + 99ba80d commit 65a4f36

File tree

7 files changed

+231
-64
lines changed

7 files changed

+231
-64
lines changed

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll

Lines changed: 78 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -186,10 +186,17 @@ module Private {
186186
TArgumentSummaryComponent(int i) { parameterPosition(i) } or
187187
TReturnSummaryComponent(ReturnKind rk)
188188

189+
private TSummaryComponent thisParam() {
190+
result = TParameterSummaryComponent(instanceParameterPosition())
191+
}
192+
189193
newtype TSummaryComponentStack =
190194
TSingletonSummaryComponentStack(SummaryComponent c) or
191195
TConsSummaryComponentStack(SummaryComponent head, SummaryComponentStack tail) {
192196
tail.(RequiredSummaryComponentStack).required(head)
197+
or
198+
tail.(RequiredSummaryComponentStack).required(TParameterSummaryComponent(_)) and
199+
head = thisParam()
193200
}
194201

195202
pragma[nomagic]
@@ -198,21 +205,63 @@ module Private {
198205
boolean preservesValue
199206
) {
200207
c.propagatesFlow(input, output, preservesValue)
208+
or
209+
// observe side effects of callbacks on input arguments
210+
c.propagatesFlow(output, input, preservesValue) and
211+
preservesValue = true and
212+
isCallbackParameter(input) and
213+
isContentOfArgument(output)
214+
or
215+
// flow from the receiver of a callback into the instance-parameter
216+
exists(SummaryComponentStack s, SummaryComponentStack callbackRef |
217+
c.propagatesFlow(s, _, _) or c.propagatesFlow(_, s, _)
218+
|
219+
callbackRef = s.drop(_) and
220+
(isCallbackParameter(callbackRef) or callbackRef.head() = TReturnSummaryComponent(_)) and
221+
input = callbackRef.tail() and
222+
output = TConsSummaryComponentStack(thisParam(), input) and
223+
preservesValue = true
224+
)
225+
}
226+
227+
private predicate isCallbackParameter(SummaryComponentStack s) {
228+
s.head() = TParameterSummaryComponent(_) and exists(s.tail())
229+
}
230+
231+
private predicate isContentOfArgument(SummaryComponentStack s) {
232+
s.head() = TContentSummaryComponent(_) and isContentOfArgument(s.tail())
233+
or
234+
s = TSingletonSummaryComponentStack(TArgumentSummaryComponent(_))
235+
}
236+
237+
private predicate outputState(SummarizedCallable c, SummaryComponentStack s) {
238+
summary(c, _, s, _)
239+
or
240+
exists(SummaryComponentStack out |
241+
outputState(c, out) and
242+
out.head() = TContentSummaryComponent(_) and
243+
s = out.tail()
244+
)
245+
or
246+
// Add the argument node corresponding to the requested post-update node
247+
inputState(c, s) and isCallbackParameter(s)
248+
}
249+
250+
private predicate inputState(SummarizedCallable c, SummaryComponentStack s) {
251+
summary(c, s, _, _)
252+
or
253+
exists(SummaryComponentStack inp | inputState(c, inp) and s = inp.tail())
254+
or
255+
exists(SummaryComponentStack out |
256+
outputState(c, out) and
257+
out.head() = TParameterSummaryComponent(_) and
258+
s = out.tail()
259+
)
201260
}
202261

203262
private newtype TSummaryNodeState =
204-
TSummaryNodeInputState(SummaryComponentStack s) {
205-
exists(SummaryComponentStack input |
206-
summary(_, input, _, _) and
207-
s = input.drop(_)
208-
)
209-
} or
210-
TSummaryNodeOutputState(SummaryComponentStack s) {
211-
exists(SummaryComponentStack output |
212-
summary(_, _, output, _) and
213-
s = output.drop(_)
214-
)
215-
}
263+
TSummaryNodeInputState(SummaryComponentStack s) { inputState(_, s) } or
264+
TSummaryNodeOutputState(SummaryComponentStack s) { outputState(_, s) }
216265

217266
/**
218267
* A state used to break up (complex) flow summaries into atomic flow steps.
@@ -238,20 +287,14 @@ module Private {
238287
pragma[nomagic]
239288
predicate isInputState(SummarizedCallable c, SummaryComponentStack s) {
240289
this = TSummaryNodeInputState(s) and
241-
exists(SummaryComponentStack input |
242-
summary(c, input, _, _) and
243-
s = input.drop(_)
244-
)
290+
inputState(c, s)
245291
}
246292

247293
/** Holds if this state is a valid output state for `c`. */
248294
pragma[nomagic]
249295
predicate isOutputState(SummarizedCallable c, SummaryComponentStack s) {
250296
this = TSummaryNodeOutputState(s) and
251-
exists(SummaryComponentStack output |
252-
summary(c, _, output, _) and
253-
s = output.drop(_)
254-
)
297+
outputState(c, s)
255298
}
256299

257300
/** Gets a textual representation of this state. */
@@ -331,19 +374,12 @@ module Private {
331374
receiver = summaryNodeInputState(c, s.drop(1))
332375
}
333376

334-
private Node pre(Node post) {
335-
summaryPostUpdateNode(post, result)
336-
or
337-
not summaryPostUpdateNode(post, _) and
338-
result = post
339-
}
340-
341377
private predicate callbackInput(
342378
SummarizedCallable c, SummaryComponentStack s, Node receiver, int i
343379
) {
344380
any(SummaryNodeState state).isOutputState(c, s) and
345381
s.head() = TParameterSummaryComponent(i) and
346-
receiver = pre(summaryNodeOutputState(c, s.drop(1)))
382+
receiver = summaryNodeInputState(c, s.drop(1))
347383
}
348384

349385
/** Holds if a call targeting `receiver` should be synthesized inside `c`. */
@@ -395,7 +431,7 @@ module Private {
395431
or
396432
exists(int i | head = TParameterSummaryComponent(i) |
397433
result =
398-
getCallbackParameterType(getNodeType(summaryNodeOutputState(pragma[only_bind_out](c),
434+
getCallbackParameterType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
399435
s.drop(1))), i)
400436
)
401437
)
@@ -421,10 +457,16 @@ module Private {
421457
}
422458

423459
/** Holds if summary node `post` is a post-update node with pre-update node `pre`. */
424-
predicate summaryPostUpdateNode(Node post, ParamNode pre) {
460+
predicate summaryPostUpdateNode(Node post, Node pre) {
425461
exists(SummarizedCallable c, int i |
426462
isParameterPostUpdate(post, c, i) and
427-
pre.isParameterOf(c, i)
463+
pre.(ParamNode).isParameterOf(c, i)
464+
)
465+
or
466+
exists(SummarizedCallable callable, SummaryComponentStack s |
467+
callbackInput(callable, s, _, _) and
468+
pre = summaryNodeOutputState(callable, s) and
469+
post = summaryNodeInputState(callable, s)
428470
)
429471
}
430472

@@ -462,7 +504,11 @@ module Private {
462504
// for `StringBuilder.append(x)` with a specified value flow from qualifier to
463505
// return value and taint flow from argument 0 to the qualifier, then this
464506
// allows us to infer taint flow from argument 0 to the return value.
465-
summaryPostUpdateNode(pred, succ) and preservesValue = true
507+
succ instanceof ParamNode and summaryPostUpdateNode(pred, succ) and preservesValue = true
508+
or
509+
// Similarly we would like to chain together summaries where values get passed
510+
// into callbacks along the way.
511+
pred instanceof ArgNode and summaryPostUpdateNode(succ, pred) and preservesValue = true
466512
}
467513

468514
/**

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImplSpecific.qll

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,9 @@ private import semmle.code.csharp.dataflow.ExternalFlow
1616
/** Holds is `i` is a valid parameter position. */
1717
predicate parameterPosition(int i) { i in [-1 .. any(Parameter p).getPosition()] }
1818

19+
/** Gets the parameter position of the instance parameter. */
20+
int instanceParameterPosition() { none() } // disables implicit summary flow to `this` for callbacks
21+
1922
/** Gets the synthesized summary data-flow node for the given values. */
2023
Node summaryNode(SummarizedCallable c, SummaryNodeState state) { result = TSummaryNode(c, state) }
2124

‎csharp/ql/test/library-tests/dataflow/external-models/ExternalFlow.expected

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,9 @@ edges
4545
| ExternalFlow.cs:91:30:91:30 | SSA def(i) : Int32 | ExternalFlow.cs:92:18:92:18 | (...) ... |
4646
| ExternalFlow.cs:121:46:121:46 | s : Object | ExternalFlow.cs:60:35:60:35 | o : Object |
4747
| ExternalFlow.cs:123:34:123:41 | elements [element] : Object | ExternalFlow.cs:72:23:72:23 | o : Object |
48+
| ExternalFlow.cs:123:34:123:41 | elements [element] : Object | ExternalFlow.cs:72:23:72:23 | o : Object |
49+
| ExternalFlow.cs:123:34:123:41 | elements [element] : Object | ExternalFlow.cs:123:34:123:41 | elements [element] : Object |
50+
| ExternalFlow.cs:123:34:123:41 | elements [element] : Object | ExternalFlow.cs:123:34:123:41 | elements [element] : Object |
4851
nodes
4952
| ExternalFlow.cs:9:27:9:38 | object creation of type Object : Object | semmle.label | object creation of type Object : Object |
5053
| ExternalFlow.cs:10:18:10:33 | call to method StepArgRes | semmle.label | call to method StepArgRes |
@@ -106,6 +109,7 @@ nodes
106109
| ExternalFlow.cs:92:18:92:18 | (...) ... | semmle.label | (...) ... |
107110
| ExternalFlow.cs:121:46:121:46 | s : Object | semmle.label | s : Object |
108111
| ExternalFlow.cs:123:34:123:41 | elements [element] : Object | semmle.label | elements [element] : Object |
112+
| ExternalFlow.cs:123:34:123:41 | elements [element] : Object | semmle.label | elements [element] : Object |
109113
subpaths
110114
invalidModelRow
111115
#select

‎java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll

Lines changed: 78 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -186,10 +186,17 @@ module Private {
186186
TArgumentSummaryComponent(int i) { parameterPosition(i) } or
187187
TReturnSummaryComponent(ReturnKind rk)
188188

189+
private TSummaryComponent thisParam() {
190+
result = TParameterSummaryComponent(instanceParameterPosition())
191+
}
192+
189193
newtype TSummaryComponentStack =
190194
TSingletonSummaryComponentStack(SummaryComponent c) or
191195
TConsSummaryComponentStack(SummaryComponent head, SummaryComponentStack tail) {
192196
tail.(RequiredSummaryComponentStack).required(head)
197+
or
198+
tail.(RequiredSummaryComponentStack).required(TParameterSummaryComponent(_)) and
199+
head = thisParam()
193200
}
194201

195202
pragma[nomagic]
@@ -198,21 +205,63 @@ module Private {
198205
boolean preservesValue
199206
) {
200207
c.propagatesFlow(input, output, preservesValue)
208+
or
209+
// observe side effects of callbacks on input arguments
210+
c.propagatesFlow(output, input, preservesValue) and
211+
preservesValue = true and
212+
isCallbackParameter(input) and
213+
isContentOfArgument(output)
214+
or
215+
// flow from the receiver of a callback into the instance-parameter
216+
exists(SummaryComponentStack s, SummaryComponentStack callbackRef |
217+
c.propagatesFlow(s, _, _) or c.propagatesFlow(_, s, _)
218+
|
219+
callbackRef = s.drop(_) and
220+
(isCallbackParameter(callbackRef) or callbackRef.head() = TReturnSummaryComponent(_)) and
221+
input = callbackRef.tail() and
222+
output = TConsSummaryComponentStack(thisParam(), input) and
223+
preservesValue = true
224+
)
225+
}
226+
227+
private predicate isCallbackParameter(SummaryComponentStack s) {
228+
s.head() = TParameterSummaryComponent(_) and exists(s.tail())
229+
}
230+
231+
private predicate isContentOfArgument(SummaryComponentStack s) {
232+
s.head() = TContentSummaryComponent(_) and isContentOfArgument(s.tail())
233+
or
234+
s = TSingletonSummaryComponentStack(TArgumentSummaryComponent(_))
235+
}
236+
237+
private predicate outputState(SummarizedCallable c, SummaryComponentStack s) {
238+
summary(c, _, s, _)
239+
or
240+
exists(SummaryComponentStack out |
241+
outputState(c, out) and
242+
out.head() = TContentSummaryComponent(_) and
243+
s = out.tail()
244+
)
245+
or
246+
// Add the argument node corresponding to the requested post-update node
247+
inputState(c, s) and isCallbackParameter(s)
248+
}
249+
250+
private predicate inputState(SummarizedCallable c, SummaryComponentStack s) {
251+
summary(c, s, _, _)
252+
or
253+
exists(SummaryComponentStack inp | inputState(c, inp) and s = inp.tail())
254+
or
255+
exists(SummaryComponentStack out |
256+
outputState(c, out) and
257+
out.head() = TParameterSummaryComponent(_) and
258+
s = out.tail()
259+
)
201260
}
202261

203262
private newtype TSummaryNodeState =
204-
TSummaryNodeInputState(SummaryComponentStack s) {
205-
exists(SummaryComponentStack input |
206-
summary(_, input, _, _) and
207-
s = input.drop(_)
208-
)
209-
} or
210-
TSummaryNodeOutputState(SummaryComponentStack s) {
211-
exists(SummaryComponentStack output |
212-
summary(_, _, output, _) and
213-
s = output.drop(_)
214-
)
215-
}
263+
TSummaryNodeInputState(SummaryComponentStack s) { inputState(_, s) } or
264+
TSummaryNodeOutputState(SummaryComponentStack s) { outputState(_, s) }
216265

217266
/**
218267
* A state used to break up (complex) flow summaries into atomic flow steps.
@@ -238,20 +287,14 @@ module Private {
238287
pragma[nomagic]
239288
predicate isInputState(SummarizedCallable c, SummaryComponentStack s) {
240289
this = TSummaryNodeInputState(s) and
241-
exists(SummaryComponentStack input |
242-
summary(c, input, _, _) and
243-
s = input.drop(_)
244-
)
290+
inputState(c, s)
245291
}
246292

247293
/** Holds if this state is a valid output state for `c`. */
248294
pragma[nomagic]
249295
predicate isOutputState(SummarizedCallable c, SummaryComponentStack s) {
250296
this = TSummaryNodeOutputState(s) and
251-
exists(SummaryComponentStack output |
252-
summary(c, _, output, _) and
253-
s = output.drop(_)
254-
)
297+
outputState(c, s)
255298
}
256299

257300
/** Gets a textual representation of this state. */
@@ -331,19 +374,12 @@ module Private {
331374
receiver = summaryNodeInputState(c, s.drop(1))
332375
}
333376

334-
private Node pre(Node post) {
335-
summaryPostUpdateNode(post, result)
336-
or
337-
not summaryPostUpdateNode(post, _) and
338-
result = post
339-
}
340-
341377
private predicate callbackInput(
342378
SummarizedCallable c, SummaryComponentStack s, Node receiver, int i
343379
) {
344380
any(SummaryNodeState state).isOutputState(c, s) and
345381
s.head() = TParameterSummaryComponent(i) and
346-
receiver = pre(summaryNodeOutputState(c, s.drop(1)))
382+
receiver = summaryNodeInputState(c, s.drop(1))
347383
}
348384

349385
/** Holds if a call targeting `receiver` should be synthesized inside `c`. */
@@ -395,7 +431,7 @@ module Private {
395431
or
396432
exists(int i | head = TParameterSummaryComponent(i) |
397433
result =
398-
getCallbackParameterType(getNodeType(summaryNodeOutputState(pragma[only_bind_out](c),
434+
getCallbackParameterType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
399435
s.drop(1))), i)
400436
)
401437
)
@@ -421,10 +457,16 @@ module Private {
421457
}
422458

423459
/** Holds if summary node `post` is a post-update node with pre-update node `pre`. */
424-
predicate summaryPostUpdateNode(Node post, ParamNode pre) {
460+
predicate summaryPostUpdateNode(Node post, Node pre) {
425461
exists(SummarizedCallable c, int i |
426462
isParameterPostUpdate(post, c, i) and
427-
pre.isParameterOf(c, i)
463+
pre.(ParamNode).isParameterOf(c, i)
464+
)
465+
or
466+
exists(SummarizedCallable callable, SummaryComponentStack s |
467+
callbackInput(callable, s, _, _) and
468+
pre = summaryNodeOutputState(callable, s) and
469+
post = summaryNodeInputState(callable, s)
428470
)
429471
}
430472

@@ -462,7 +504,11 @@ module Private {
462504
// for `StringBuilder.append(x)` with a specified value flow from qualifier to
463505
// return value and taint flow from argument 0 to the qualifier, then this
464506
// allows us to infer taint flow from argument 0 to the return value.
465-
summaryPostUpdateNode(pred, succ) and preservesValue = true
507+
succ instanceof ParamNode and summaryPostUpdateNode(pred, succ) and preservesValue = true
508+
or
509+
// Similarly we would like to chain together summaries where values get passed
510+
// into callbacks along the way.
511+
pred instanceof ArgNode and summaryPostUpdateNode(succ, pred) and preservesValue = true
466512
}
467513

468514
/**

0 commit comments

Comments
 (0)