2
2
* @name Use of expired stack-address
3
3
* @description Accessing the stack-allocated memory of a function
4
4
* after it has returned can lead to memory corruption.
5
- * @kind problem
5
+ * @kind path- problem
6
6
* @problem.severity error
7
7
* @security-severity 9.3
8
8
* @precision high
@@ -178,13 +178,10 @@ predicate blockStoresToAddress(
178
178
globalAddress = globalAddress ( store .getDestinationAddress ( ) )
179
179
}
180
180
181
- predicate blockLoadsFromAddress (
182
- IRBlock block , int index , LoadInstruction load , TGlobalAddress globalAddress
183
- ) {
184
- block .getInstruction ( index ) = load and
185
- globalAddress = globalAddress ( load .getSourceAddress ( ) )
186
- }
187
-
181
+ /**
182
+ * Holds if `globalAddress` evaluates to the address of `var` (which escaped through `store` before
183
+ * returning through `call`) when control reaches `block`.
184
+ */
188
185
predicate globalAddressPointsToStack (
189
186
StoreInstruction store , StackVariable var , CallInstruction call , IRBlock block ,
190
187
TGlobalAddress globalAddress , boolean isCallBlock , boolean isStoreBlock
@@ -203,21 +200,127 @@ predicate globalAddressPointsToStack(
203
200
)
204
201
or
205
202
isCallBlock = false and
206
- exists ( IRBlock mid |
207
- mid .immediatelyDominates ( block ) and
208
- // Only recurse if there is no store to `globalAddress` in `mid`.
209
- globalAddressPointsToStack ( store , var , call , mid , globalAddress , _, false )
203
+ step ( store , var , call , globalAddress , _, block )
204
+ )
205
+ }
206
+
207
+ pragma [ inline]
208
+ int getInstructionIndex ( Instruction instr , IRBlock block ) { block .getInstruction ( result ) = instr }
209
+
210
+ predicate step (
211
+ StoreInstruction store , StackVariable var , CallInstruction call , TGlobalAddress globalAddress ,
212
+ IRBlock pred , IRBlock succ
213
+ ) {
214
+ exists ( boolean isCallBlock , boolean isStoreBlock |
215
+ // Only recurse if there is no store to `globalAddress` in `mid`.
216
+ globalAddressPointsToStack ( store , var , call , pred , globalAddress , isCallBlock , isStoreBlock )
217
+ |
218
+ // Post domination ensures that `block` is always executed after `mid`
219
+ // Domination ensures that `mid` is always executed before `block`
220
+ isStoreBlock = false and
221
+ succ .immediatelyPostDominates ( pred ) and
222
+ pred .immediatelyDominates ( succ )
223
+ or
224
+ exists ( CallInstruction anotherCall , int anotherCallIndex |
225
+ anotherCall = pred .getInstruction ( anotherCallIndex ) and
226
+ succ .getFirstInstruction ( ) instanceof EnterFunctionInstruction and
227
+ succ .getEnclosingFunction ( ) = anotherCall .getStaticCallTarget ( ) and
228
+ ( if isCallBlock = true then getInstructionIndex ( call , _) < anotherCallIndex else any ( ) ) and
229
+ (
230
+ if isStoreBlock = true
231
+ then
232
+ forex ( int storeIndex | blockStoresToAddress ( pred , storeIndex , _, globalAddress ) |
233
+ anotherCallIndex < storeIndex
234
+ )
235
+ else any ( )
236
+ )
210
237
)
211
238
)
212
239
}
213
240
241
+ newtype TPathElement =
242
+ TStore ( StoreInstruction store ) { globalAddressPointsToStack ( store , _, _, _, _, _, _) } or
243
+ TCall ( CallInstruction call , IRBlock block ) {
244
+ globalAddressPointsToStack ( _, _, call , block , _, _, _)
245
+ } or
246
+ TMid ( IRBlock block ) { step ( _, _, _, _, _, block ) } or
247
+ TSink ( LoadInstruction load , IRBlock block ) {
248
+ exists ( TGlobalAddress address |
249
+ globalAddressPointsToStack ( _, _, _, block , address , _, _) and
250
+ block .getAnInstruction ( ) = load and
251
+ globalAddress ( load .getSourceAddress ( ) ) = address
252
+ )
253
+ }
254
+
255
+ class PathElement extends TPathElement {
256
+ StoreInstruction asStore ( ) { this = TStore ( result ) }
257
+
258
+ CallInstruction asCall ( IRBlock block ) { this = TCall ( result , block ) }
259
+
260
+ predicate isCall ( IRBlock block ) { exists ( this .asCall ( block ) ) }
261
+
262
+ IRBlock asMid ( ) { this = TMid ( result ) }
263
+
264
+ LoadInstruction asSink ( IRBlock block ) { this = TSink ( result , block ) }
265
+
266
+ predicate isSink ( IRBlock block ) { exists ( this .asSink ( block ) ) }
267
+
268
+ string toString ( ) {
269
+ result = [ asStore ( ) .toString ( ) , asCall ( _) .toString ( ) , asMid ( ) .toString ( ) , asSink ( _) .toString ( ) ]
270
+ }
271
+
272
+ predicate hasLocationInfo (
273
+ string filepath , int startline , int startcolumn , int endline , int endcolumn
274
+ ) {
275
+ this .asStore ( )
276
+ .getLocation ( )
277
+ .hasLocationInfo ( filepath , startline , startcolumn , endline , endcolumn )
278
+ or
279
+ this .asCall ( _)
280
+ .getLocation ( )
281
+ .hasLocationInfo ( filepath , startline , startcolumn , endline , endcolumn )
282
+ or
283
+ this .asMid ( ) .getLocation ( ) .hasLocationInfo ( filepath , startline , startcolumn , endline , endcolumn )
284
+ or
285
+ this .asSink ( _)
286
+ .getLocation ( )
287
+ .hasLocationInfo ( filepath , startline , startcolumn , endline , endcolumn )
288
+ }
289
+ }
290
+
291
+ predicate isSink ( LoadInstruction load , IRBlock block , int index , TGlobalAddress globalAddress ) {
292
+ block .getInstruction ( index ) = load and
293
+ globalAddress ( load .getSourceAddress ( ) ) = globalAddress
294
+ }
295
+
296
+ query predicate edges ( PathElement pred , PathElement succ ) {
297
+ // Store -> caller
298
+ globalAddressPointsToStack ( pred .asStore ( ) , _, succ .asCall ( _) , _, _, _, _)
299
+ or
300
+ // Call -> basic block
301
+ pred .isCall ( succ .asMid ( ) )
302
+ or
303
+ // Special case for when the caller goes directly to the load with no steps
304
+ // across basic blocks (i.e., caller -> sink)
305
+ exists ( IRBlock block |
306
+ pred .isCall ( block ) and
307
+ succ .isSink ( block )
308
+ )
309
+ or
310
+ // Basic block -> basic block
311
+ step ( _, _, _, _, pred .asMid ( ) , succ .asMid ( ) )
312
+ or
313
+ // Basic block -> load
314
+ succ .isSink ( pred .asMid ( ) )
315
+ }
316
+
214
317
from
215
318
StoreInstruction store , StackVariable var , LoadInstruction load , CallInstruction call ,
216
- IRBlock block , boolean isCallBlock , TGlobalAddress address , boolean isStoreBlock
319
+ IRBlock block , boolean isCallBlock , TGlobalAddress address , boolean isStoreBlock ,
320
+ PathElement source , PathElement sink , int loadIndex
217
321
where
218
322
globalAddressPointsToStack ( store , var , call , block , address , isCallBlock , isStoreBlock ) and
219
- block .getAnInstruction ( ) = load and
220
- globalAddress ( load .getSourceAddress ( ) ) = address and
323
+ isSink ( load , block , loadIndex , address ) and
221
324
(
222
325
// We know that we have a sequence:
223
326
// (1) store to `address` -> (2) return from `f` -> (3) load from `address`.
@@ -226,22 +329,20 @@ where
226
329
if isCallBlock = true
227
330
then
228
331
// If so, the load must happen after the call.
229
- exists ( int callIndex , int loadIndex |
230
- blockLoadsFromAddress ( _, loadIndex , load , _) and
231
- block .getInstruction ( callIndex ) = call and
232
- callIndex < loadIndex
332
+ getInstructionIndex ( call , _) < loadIndex
333
+ else any ( )
334
+ ) and
335
+ (
336
+ // If there is a store to the address we need to make sure that the load we found was
337
+ // before that store (So that the load doesn't read an overwritten value).
338
+ if isStoreBlock = true
339
+ then
340
+ forex ( int storeIndex | blockStoresToAddress ( block , storeIndex , _, address ) |
341
+ loadIndex < storeIndex
233
342
)
234
343
else any ( )
235
344
) and
236
- // If there is a store to the address we need to make sure that the load we found was
237
- // before that store (So that the load doesn't read an overwritten value).
238
- if isStoreBlock = true
239
- then
240
- exists ( int storeIndex , int loadIndex |
241
- blockStoresToAddress ( block , storeIndex , _, address ) and
242
- block .getInstruction ( loadIndex ) = load and
243
- loadIndex < storeIndex
244
- )
245
- else any ( )
246
- select load , "Stack variable $@ escapes $@ and is used after it has expired." , var , var .toString ( ) ,
247
- store , "here"
345
+ source .asStore ( ) = store and
346
+ sink .asSink ( _) = load
347
+ select sink , source , sink , "Stack variable $@ escapes $@ and is used after it has expired." , var ,
348
+ var .toString ( ) , store , "here"
0 commit comments