Further reorg of libraries and predicates to allow for more reusable and consistent libraries.

This commit is contained in:
Benjamin Rodes
2024-01-18 11:17:24 -05:00
parent 967526b285
commit 833ef9d6d6
4 changed files with 30 additions and 43 deletions

View File

@@ -22,29 +22,10 @@ import DoubleFree::PathGraph
*/
predicate isFree(DataFlow::Node n, Expr e) { isFree(_, n, e, _) }
/**
* `dealloc1` is a deallocation expression and `e` is an expression such
* that is deallocated by a deallocation expression, and the `(dealloc1, e)` pair
* should be excluded by the `FlowFromFree` library.
*
* Note that `e` is not necessarily the expression deallocated by `dealloc1`. It will
* be bound to the second deallocation as identified by the `FlowFromFree` library.
*/
bindingset[dealloc1, e]
predicate isExcludeFreePair(DeallocationExpr dealloc1, Expr e) {
exists(DeallocationExpr dealloc2 | isFree(_, _, e, dealloc2) |
dealloc1.(FunctionCall).getTarget().hasGlobalName("MmFreePagesFromMdl") and
// From https://learn.microsoft.com/en-us/windows-hardware/drivers/ddi/wdm/nf-wdm-mmfreepagesfrommdl:
// "After calling MmFreePagesFromMdl, the caller must also call ExFreePool
// to release the memory that was allocated for the MDL structure."
isExFreePoolCall(dealloc2, _)
)
}
module DoubleFreeParam implements FlowFromFreeParamSig {
predicate isSink = isFree/2;
predicate isExcluded = isExcludeFreePair/2;
predicate isExcluded = isExcludedMmFreePageFromMdl/2;
predicate sourceSinkIsRelated = defaultSourceSinkIsRelated/2;
}

View File

@@ -143,3 +143,22 @@ predicate defaultSourceSinkIsRelated(DataFlow::Node source, DataFlow::Node sink)
strictlyPostDominates(b2, i2, b1, i1)
)
}
/**
* `dealloc1` is a deallocation expression, `e` is an expression that dereferences a
* pointer, and the `(dealloc1, e)` pair should be excluded by the `FlowFromFree` library.
*
* Note that `e` is not necessarily the expression deallocated by `dealloc1`. It will
* be bound to the second deallocation as identified by the `FlowFromFree` library.
*
* From https://learn.microsoft.com/en-us/windows-hardware/drivers/ddi/wdm/nf-wdm-mmfreepagesfrommdl:
* "After calling MmFreePagesFromMdl, the caller must also call ExFreePool
* to release the memory that was allocated for the MDL structure."
*/
bindingset[dealloc1, e]
predicate isExcludedMmFreePageFromMdl(DeallocationExpr dealloc1, Expr e) {
exists(DeallocationExpr dealloc2 | isFree(_, _, e, dealloc2) |
dealloc1.(FunctionCall).getTarget().hasGlobalName("MmFreePagesFromMdl") and
isExFreePoolCall(dealloc2, _)
)
}

View File

@@ -18,6 +18,16 @@ import FlowAfterFree
import UseAfterFree
import UseAfterFreeTrace::PathGraph
module UseAfterFreeParam implements FlowFromFreeParamSig {
predicate isSink = isUse/2;
predicate isExcluded = isExcludedMmFreePageFromMdl/2;
predicate sourceSinkIsRelated = defaultSourceSinkIsRelated/2;
}
import UseAfterFreeParam
module UseAfterFreeTrace = FlowFromFree<UseAfterFreeParam>;
from UseAfterFreeTrace::PathNode source, UseAfterFreeTrace::PathNode sink, DeallocationExpr dealloc

View File

@@ -144,26 +144,3 @@ module IsUse {
}
import IsUse
/**
* `dealloc1` is a deallocation expression, `e` is an expression that dereferences a
* pointer, and the `(dealloc1, e)` pair should be excluded by the `FlowFromFree` library.
*/
bindingset[dealloc1, e]
predicate isExcludeFreeUsePair(DeallocationExpr dealloc1, Expr e) {
// From https://learn.microsoft.com/en-us/windows-hardware/drivers/ddi/wdm/nf-wdm-mmfreepagesfrommdl:
// "After calling MmFreePagesFromMdl, the caller must also call ExFreePool
// to release the memory that was allocated for the MDL structure."
dealloc1.(FunctionCall).getTarget().hasGlobalName("MmFreePagesFromMdl") and
isExFreePoolCall(_, e)
}
module UseAfterFreeParam implements FlowFromFreeParamSig {
predicate isSink = isUse/2;
predicate isExcluded = isExcludeFreeUsePair/2;
predicate sourceSinkIsRelated = defaultSourceSinkIsRelated/2;
}
import UseAfterFreeParam