|
| 1 | +/** |
| 2 | + * @name Potential double free |
| 3 | + * @description An allocated memory block is free multiple times. Behavior in such cases is undefined and can cause memory corruption. |
| 4 | + * @kind path-problem |
| 5 | + * @precision medium |
| 6 | + * @id cpp/double-free |
| 7 | + * @problem.severity warning |
| 8 | + * @security-severity 9.3 |
| 9 | + * @tags reliability |
| 10 | + * security |
| 11 | + * external/cwe/cwe-415 |
| 12 | + */ |
| 13 | + |
| 14 | +import cpp |
| 15 | +import semmle.code.cpp.dataflow.new.DataFlow |
| 16 | +import FlowAfterFree |
| 17 | +import DoubleFree::PathGraph |
| 18 | + |
| 19 | +predicate isFree(DataFlow::Node n, Expr e) { isFree(n, e, _) } |
| 20 | + |
| 21 | +/** |
| 22 | + * Holds if `fc` is a function call that is the result of expanding |
| 23 | + * the `ExFreePool` macro. |
| 24 | + */ |
| 25 | +predicate isExFreePoolCall(FunctionCall fc) { |
| 26 | + exists(MacroInvocation mi | |
| 27 | + mi.getMacroName() = "ExFreePool" and |
| 28 | + mi.getExpr() = fc |
| 29 | + ) |
| 30 | + or |
| 31 | + fc.getTarget().hasGlobalName("ExFreePool") |
| 32 | +} |
| 33 | + |
| 34 | +bindingset[dealloc1, e] |
| 35 | +predicate isExcludeFreePair(DeallocationExpr dealloc1, Expr e) { |
| 36 | + exists(DeallocationExpr dealloc2 | isFree(_, e, dealloc2) | |
| 37 | + dealloc1.(FunctionCall).getTarget().hasGlobalName("MmFreePagesFromMdl") and |
| 38 | + // From https://learn.microsoft.com/en-us/windows-hardware/drivers/ddi/wdm/nf-wdm-mmfreepagesfrommdl: |
| 39 | + // "After calling MmFreePagesFromMdl, the caller must also call ExFreePool |
| 40 | + // to release the memory that was allocated for the MDL structure." |
| 41 | + isExFreePoolCall(dealloc2) |
| 42 | + ) |
| 43 | +} |
| 44 | + |
| 45 | +module DoubleFree = FlowFromFree<isFree/2, isExcludeFreePair/2>; |
| 46 | + |
| 47 | +from DoubleFree::PathNode source, DoubleFree::PathNode sink, DeallocationExpr dealloc, Expr e2 |
| 48 | +where |
| 49 | + DoubleFree::flowPath(source, sink) and |
| 50 | + isFree(source.getNode(), _, dealloc) and |
| 51 | + isFree(sink.getNode(), e2) |
| 52 | +select sink.getNode(), source, sink, |
| 53 | + "Memory pointed to by '" + e2.toString() + "' may already have been freed by $@.", dealloc, |
| 54 | + dealloc.toString() |
0 commit comments