22 * @name Use of expired stack-address
33 * @description Accessing the stack-allocated memory of a function
44 * after it has returned can lead to memory corruption.
5- * @kind problem
5+ * @kind path- problem
66 * @problem.severity error
77 * @security-severity 9.3
88 * @precision high
@@ -178,13 +178,10 @@ predicate blockStoresToAddress(
178178 globalAddress = globalAddress ( store .getDestinationAddress ( ) )
179179}
180180
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+ */
188185predicate globalAddressPointsToStack (
189186 StoreInstruction store , StackVariable var , CallInstruction call , IRBlock block ,
190187 TGlobalAddress globalAddress , boolean isCallBlock , boolean isStoreBlock
@@ -203,21 +200,127 @@ predicate globalAddressPointsToStack(
203200 )
204201 or
205202 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+ )
210237 )
211238 )
212239}
213240
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+
214317from
215318 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
217321where
218322 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
221324 (
222325 // We know that we have a sequence:
223326 // (1) store to `address` -> (2) return from `f` -> (3) load from `address`.
@@ -226,22 +329,20 @@ where
226329 if isCallBlock = true
227330 then
228331 // 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
233342 )
234343 else any ( )
235344 ) 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