@@ -55,23 +55,33 @@ DataFlow::Node stringSink() {
55
55
/** Gets a node where regular expressions that flow to the node are used. */
56
56
DataFlow:: Node regSink ( ) { result = any ( RegexExecution exec ) .getRegex ( ) }
57
57
58
- private signature module ReachInputSig {
59
- DataFlow:: LocalSourceNode start ( TypeTracker t ) ;
58
+ private signature module TypeTrackInputSig {
59
+ DataFlow:: LocalSourceNode start ( TypeTracker t , DataFlow :: Node start ) ;
60
60
61
- DataFlow:: Node end ( ) ;
61
+ predicate end ( DataFlow:: Node n ) ;
62
62
63
- predicate additionalStep ( DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo ) ;
63
+ predicate additionalStep ( DataFlow:: Node nodeFrom , DataFlow:: LocalSourceNode nodeTo ) ;
64
64
}
65
65
66
- private module Reach< ReachInputSig Input> {
66
+ /**
67
+ * Provides a version of type tracking where we first prune for reachable nodes,
68
+ * before doing the type tracking computation.
69
+ */
70
+ private module TypeTrack< TypeTrackInputSig Input> {
71
+ private predicate additionalStep (
72
+ DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo
73
+ ) {
74
+ Input:: additionalStep ( nodeFrom .getALocalUse ( ) , nodeTo )
75
+ }
76
+
67
77
/** Gets a node that is forwards reachable by type-tracking. */
68
78
pragma [ nomagic]
69
79
private DataFlow:: LocalSourceNode forward ( TypeTracker t ) {
70
- result = Input:: start ( t )
80
+ result = Input:: start ( t , _ )
71
81
or
72
82
exists ( TypeTracker t2 | result = forward ( t2 ) .track ( t2 , t ) )
73
83
or
74
- exists ( TypeTracker t2 | t2 = t .continue ( ) | Input :: additionalStep ( forward ( t2 ) , result ) )
84
+ exists ( TypeTracker t2 | t2 = t .continue ( ) | additionalStep ( forward ( t2 ) , result ) )
75
85
}
76
86
77
87
bindingset [ result , tbt]
@@ -90,11 +100,11 @@ private module Reach<ReachInputSig Input> {
90
100
result = forwardLateInline ( t ) and
91
101
(
92
102
t .start ( ) and
93
- result . flowsTo ( Input:: end ( ) )
103
+ Input:: end ( result . getALocalUse ( ) )
94
104
or
95
105
exists ( TypeBackTracker t2 | result = backwards ( t2 ) .backtrack ( t2 , t ) )
96
106
or
97
- exists ( TypeBackTracker t2 | t2 = t .continue ( ) | Input :: additionalStep ( result , backwards ( t2 ) ) )
107
+ exists ( TypeBackTracker t2 | t2 = t .continue ( ) | additionalStep ( result , backwards ( t2 ) ) )
98
108
)
99
109
}
100
110
@@ -110,13 +120,13 @@ private module Reach<ReachInputSig Input> {
110
120
111
121
/** Holds if `n` is forwards and backwards reachable with type tracker `t`. */
112
122
pragma [ nomagic]
113
- predicate reached ( DataFlow:: LocalSourceNode n , TypeTracker t ) {
123
+ private predicate reached ( DataFlow:: LocalSourceNode n , TypeTracker t ) {
114
124
n = forward ( t ) and
115
125
n = backwardsInlineLate ( t )
116
126
}
117
127
118
128
pragma [ nomagic]
119
- TypeTracker stepReached (
129
+ private TypeTracker stepReached (
120
130
TypeTracker t , DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo
121
131
) {
122
132
exists ( StepSummary summary |
@@ -126,11 +136,20 @@ private module Reach<ReachInputSig Input> {
126
136
result = t .append ( summary )
127
137
)
128
138
or
129
- Input :: additionalStep ( nodeFrom , nodeTo ) and
139
+ additionalStep ( nodeFrom , nodeTo ) and
130
140
reached ( nodeFrom , pragma [ only_bind_into ] ( t ) ) and
131
141
reached ( nodeTo , pragma [ only_bind_into ] ( t ) ) and
132
142
result = t .continue ( )
133
143
}
144
+
145
+ /** Gets a node that has been tracked from the start node `start`. */
146
+ DataFlow:: LocalSourceNode track ( DataFlow:: Node start , TypeTracker t ) {
147
+ t .start ( ) and
148
+ result = Input:: start ( t , start ) and
149
+ reached ( result , t )
150
+ or
151
+ exists ( TypeTracker t2 | t = stepReached ( t2 , track ( start , t2 ) , result ) )
152
+ }
134
153
}
135
154
136
155
/** Holds if `inputStr` is compiled to a regular expression that is returned at `call`. */
@@ -143,47 +162,40 @@ private predicate regFromString(DataFlow::LocalSourceNode inputStr, DataFlow::Ca
143
162
)
144
163
}
145
164
146
- private module StringReachInput implements ReachInputSig {
147
- DataFlow:: LocalSourceNode start ( TypeTracker t ) { result = strStart ( ) and t .start ( ) }
165
+ private module StringTypeTrackInput implements TypeTrackInputSig {
166
+ DataFlow:: LocalSourceNode start ( TypeTracker t , DataFlow:: Node start ) {
167
+ start = strStart ( ) and t .start ( ) and result = start
168
+ }
148
169
149
- DataFlow:: Node end ( ) {
150
- result = stringSink ( ) or
151
- regFromString ( result , _)
170
+ predicate end ( DataFlow:: Node n ) {
171
+ n = stringSink ( ) or
172
+ regFromString ( n , _)
152
173
}
153
174
154
- predicate additionalStep ( DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo ) {
155
- exists ( DataFlow:: Node mid | nodeFrom .flowsTo ( mid ) |
156
- // include taint flow through `String` summaries
157
- TaintTrackingPrivate:: summaryThroughStepTaint ( mid , nodeTo , any ( String:: SummarizedCallable c ) )
158
- or
159
- // string concatenations, and
160
- exists ( CfgNodes:: ExprNodes:: OperationCfgNode op |
161
- op = nodeTo .asExpr ( ) and
162
- op .getAnOperand ( ) = mid .asExpr ( ) and
163
- op .getExpr ( ) .( Ast:: BinaryOperation ) .getOperator ( ) = "+"
164
- )
165
- or
166
- // string interpolations
167
- mid .asExpr ( ) = nodeTo .asExpr ( ) .( CfgNodes:: ExprNodes:: StringlikeLiteralCfgNode ) .getAComponent ( )
175
+ predicate additionalStep ( DataFlow:: Node nodeFrom , DataFlow:: LocalSourceNode nodeTo ) {
176
+ // include taint flow through `String` summaries
177
+ TaintTrackingPrivate:: summaryThroughStepTaint ( nodeFrom , nodeTo ,
178
+ any ( String:: SummarizedCallable c ) )
179
+ or
180
+ // string concatenations, and
181
+ exists ( CfgNodes:: ExprNodes:: OperationCfgNode op |
182
+ op = nodeTo .asExpr ( ) and
183
+ op .getAnOperand ( ) = nodeFrom .asExpr ( ) and
184
+ op .getExpr ( ) .( Ast:: BinaryOperation ) .getOperator ( ) = "+"
168
185
)
186
+ or
187
+ // string interpolations
188
+ nodeFrom .asExpr ( ) =
189
+ nodeTo .asExpr ( ) .( CfgNodes:: ExprNodes:: StringlikeLiteralCfgNode ) .getAComponent ( )
169
190
}
170
191
}
171
192
172
- private module StringReach = Reach< StringReachInput > ;
173
-
174
193
/**
175
194
* Gets a node that has been tracked from the string constant `start` to some node.
176
195
* This is used to figure out where `start` is evaluated as a regular expression against an input string,
177
196
* or where `start` is compiled into a regular expression.
178
197
*/
179
- private DataFlow:: LocalSourceNode trackStrings ( DataFlow:: Node start , TypeTracker t ) {
180
- t .start ( ) and
181
- start = result and
182
- result = strStart ( ) and
183
- StringReach:: reached ( result , t )
184
- or
185
- exists ( TypeTracker t2 | t = StringReach:: stepReached ( t2 , trackStrings ( start , t2 ) , result ) )
186
- }
198
+ private predicate trackStrings = TypeTrack< StringTypeTrackInput > :: track / 2 ;
187
199
188
200
/** Holds if `strConst` flows to a regex compilation (tracked by `t`), where the resulting regular expression is stored in `reg`. */
189
201
pragma [ nomagic]
@@ -192,39 +204,25 @@ private predicate regFromStringStart(DataFlow::Node strConst, TypeTracker t, Dat
192
204
exists ( t .continue ( ) )
193
205
}
194
206
195
- private module RegReachInput implements ReachInputSig {
196
- DataFlow:: LocalSourceNode start ( TypeTracker t ) {
197
- result = regStart ( ) and
198
- t .start ( )
207
+ private module RegTypeTrackInput implements TypeTrackInputSig {
208
+ DataFlow:: LocalSourceNode start ( TypeTracker t , DataFlow:: Node start ) {
209
+ start = regStart ( ) and
210
+ t .start ( ) and
211
+ result = start
199
212
or
200
- regFromStringStart ( _ , t , result )
213
+ regFromStringStart ( start , t , result )
201
214
}
202
215
203
- DataFlow:: Node end ( ) { result = regSink ( ) }
216
+ predicate end ( DataFlow:: Node n ) { n = regSink ( ) }
204
217
205
- predicate additionalStep ( DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo ) {
206
- none ( )
207
- }
218
+ predicate additionalStep ( DataFlow:: Node nodeFrom , DataFlow:: LocalSourceNode nodeTo ) { none ( ) }
208
219
}
209
220
210
- private module RegReach = Reach< RegReachInput > ;
211
-
212
221
/**
213
222
* Gets a node that has been tracked from the regular expression `start` to some node.
214
223
* This is used to figure out where `start` is executed against an input string.
215
224
*/
216
- private DataFlow:: LocalSourceNode trackRegs ( DataFlow:: Node start , TypeTracker t ) {
217
- RegReach:: reached ( result , t ) and
218
- (
219
- t .start ( ) and
220
- start = result and
221
- result = regStart ( )
222
- or
223
- regFromStringStart ( start , t , result )
224
- )
225
- or
226
- exists ( TypeTracker t2 | t = RegReach:: stepReached ( t2 , trackRegs ( start , t2 ) , result ) )
227
- }
225
+ private predicate trackRegs = TypeTrack< RegTypeTrackInput > :: track / 2 ;
228
226
229
227
/** Gets a node that references a regular expression. */
230
228
private DataFlow:: LocalSourceNode trackRegexpType ( TypeTracker t ) {
0 commit comments