@@ -85,6 +85,9 @@ module Public {
85
85
/** Holds if this stack contains summary component `c`. */
86
86
predicate contains ( SummaryComponent c ) { c = this .drop ( _) .head ( ) }
87
87
88
+ /** Gets the bottom element of this stack. */
89
+ SummaryComponent bottom ( ) { result = this .drop ( this .length ( ) - 1 ) .head ( ) }
90
+
88
91
/** Gets a textual representation of this stack. */
89
92
string toString ( ) {
90
93
exists ( SummaryComponent head , SummaryComponentStack tail |
@@ -197,6 +200,8 @@ module Private {
197
200
or
198
201
tail .( RequiredSummaryComponentStack ) .required ( TParameterSummaryComponent ( _) ) and
199
202
head = thisParam ( )
203
+ or
204
+ derivedFluentFlowPush ( _, _, _, head , tail , _)
200
205
}
201
206
202
207
pragma [ nomagic]
@@ -210,7 +215,7 @@ module Private {
210
215
c .propagatesFlow ( output , input , preservesValue ) and
211
216
preservesValue = true and
212
217
isCallbackParameter ( input ) and
213
- isContentOfArgument ( output )
218
+ isContentOfArgument ( output , _ )
214
219
or
215
220
// flow from the receiver of a callback into the instance-parameter
216
221
exists ( SummaryComponentStack s , SummaryComponentStack callbackRef |
@@ -222,16 +227,81 @@ module Private {
222
227
output = TConsSummaryComponentStack ( thisParam ( ) , input ) and
223
228
preservesValue = true
224
229
)
230
+ or
231
+ exists ( SummaryComponentStack arg , SummaryComponentStack return |
232
+ derivedFluentFlow ( c , input , arg , return , preservesValue )
233
+ |
234
+ arg .length ( ) = 1 and
235
+ output = return
236
+ or
237
+ exists ( SummaryComponent head , SummaryComponentStack tail |
238
+ derivedFluentFlowPush ( c , input , arg , head , tail , 0 ) and
239
+ output = SummaryComponentStack:: push ( head , tail )
240
+ )
241
+ )
242
+ or
243
+ // Chain together summaries where values get passed into callbacks along the way
244
+ exists ( SummaryComponentStack mid , boolean preservesValue1 , boolean preservesValue2 |
245
+ c .propagatesFlow ( input , mid , preservesValue1 ) and
246
+ c .propagatesFlow ( mid , output , preservesValue2 ) and
247
+ mid .drop ( mid .length ( ) - 2 ) =
248
+ SummaryComponentStack:: push ( TParameterSummaryComponent ( _) ,
249
+ SummaryComponentStack:: singleton ( TArgumentSummaryComponent ( _) ) ) and
250
+ preservesValue = preservesValue1 .booleanAnd ( preservesValue2 )
251
+ )
252
+ }
253
+
254
+ /**
255
+ * Holds if `c` has a flow summary from `input` to `arg`, where `arg`
256
+ * writes to (contents of) the `i`th argument, and `c` has a
257
+ * value-preserving flow summary from the `i`th argument to a return value
258
+ * (`return`).
259
+ *
260
+ * In such a case, we derive flow from `input` to (contents of) the return
261
+ * value.
262
+ *
263
+ * As an example, this simplifies modeling of fluent methods:
264
+ * for `StringBuilder.append(x)` with a specified value flow from qualifier to
265
+ * return value and taint flow from argument 0 to the qualifier, then this
266
+ * allows us to infer taint flow from argument 0 to the return value.
267
+ */
268
+ pragma [ nomagic]
269
+ private predicate derivedFluentFlow (
270
+ SummarizedCallable c , SummaryComponentStack input , SummaryComponentStack arg ,
271
+ SummaryComponentStack return , boolean preservesValue
272
+ ) {
273
+ exists ( int i |
274
+ summary ( c , input , arg , preservesValue ) and
275
+ isContentOfArgument ( arg , i ) and
276
+ summary ( c , SummaryComponentStack:: singleton ( TArgumentSummaryComponent ( i ) ) , return , true ) and
277
+ return .bottom ( ) = TReturnSummaryComponent ( _)
278
+ )
279
+ }
280
+
281
+ pragma [ nomagic]
282
+ private predicate derivedFluentFlowPush (
283
+ SummarizedCallable c , SummaryComponentStack input , SummaryComponentStack arg ,
284
+ SummaryComponent head , SummaryComponentStack tail , int i
285
+ ) {
286
+ derivedFluentFlow ( c , input , arg , tail , _) and
287
+ head = arg .drop ( i ) .head ( ) and
288
+ i = arg .length ( ) - 2
289
+ or
290
+ exists ( SummaryComponent head0 , SummaryComponentStack tail0 |
291
+ derivedFluentFlowPush ( c , input , arg , head0 , tail0 , i + 1 ) and
292
+ head = arg .drop ( i ) .head ( ) and
293
+ tail = SummaryComponentStack:: push ( head0 , tail0 )
294
+ )
225
295
}
226
296
227
297
private predicate isCallbackParameter ( SummaryComponentStack s ) {
228
298
s .head ( ) = TParameterSummaryComponent ( _) and exists ( s .tail ( ) )
229
299
}
230
300
231
- private predicate isContentOfArgument ( SummaryComponentStack s ) {
232
- s .head ( ) = TContentSummaryComponent ( _) and isContentOfArgument ( s .tail ( ) )
301
+ private predicate isContentOfArgument ( SummaryComponentStack s , int i ) {
302
+ s .head ( ) = TContentSummaryComponent ( _) and isContentOfArgument ( s .tail ( ) , i )
233
303
or
234
- s = TSingletonSummaryComponentStack ( TArgumentSummaryComponent ( _ ) )
304
+ s = TSingletonSummaryComponentStack ( TArgumentSummaryComponent ( i ) )
235
305
}
236
306
237
307
private predicate outputState ( SummarizedCallable c , SummaryComponentStack s ) {
@@ -508,9 +578,14 @@ module Private {
508
578
* node, and back out to `p`.
509
579
*/
510
580
predicate summaryAllowParameterReturnInSelf ( ParamNode p ) {
511
- exists ( SummarizedCallable c , int i |
512
- c .clearsContent ( i , _) and
513
- p .isParameterOf ( c , i )
581
+ exists ( SummarizedCallable c , int i | p .isParameterOf ( c , i ) |
582
+ c .clearsContent ( i , _)
583
+ or
584
+ exists ( SummaryComponentStack inputContents , SummaryComponentStack outputContents |
585
+ summary ( c , inputContents , outputContents , _) and
586
+ inputContents .bottom ( ) = pragma [ only_bind_into ] ( TArgumentSummaryComponent ( i ) ) and
587
+ outputContents .bottom ( ) = pragma [ only_bind_into ] ( TArgumentSummaryComponent ( i ) )
588
+ )
514
589
)
515
590
}
516
591
@@ -534,22 +609,6 @@ module Private {
534
609
preservesValue = false and not summary ( c , inputContents , outputContents , true )
535
610
)
536
611
or
537
- // If flow through a method updates a parameter from some input A, and that
538
- // parameter also is returned through B, then we'd like a combined flow from A
539
- // to B as well. As an example, this simplifies modeling of fluent methods:
540
- // for `StringBuilder.append(x)` with a specified value flow from qualifier to
541
- // return value and taint flow from argument 0 to the qualifier, then this
542
- // allows us to infer taint flow from argument 0 to the return value.
543
- succ instanceof ParamNode and
544
- summaryPostUpdateNode ( pred , succ ) and
545
- preservesValue = true
546
- or
547
- // Similarly we would like to chain together summaries where values get passed
548
- // into callbacks along the way.
549
- pred instanceof ArgNode and
550
- summaryPostUpdateNode ( succ , pred ) and
551
- preservesValue = true
552
- or
553
612
exists ( SummarizedCallable c , int i |
554
613
pred .( ParamNode ) .isParameterOf ( c , i ) and
555
614
succ = summaryNode ( c , TSummaryNodeClearsContentState ( i , _) ) and
0 commit comments