Skip to content

C++: Suggestions to #15343 #39

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Jan 17, 2024
Merged

C++: Suggestions to #15343 #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
fb9f848
C++: Change the interface of 'FlowAfterFree' so that the module it takes
MathiasVP Jan 16, 2024
5a72d91
C++: Add another predicate to the module signature.
MathiasVP Jan 16, 2024
32caf64
C++: Convert the use-after-free and double-free libraries to use new …
MathiasVP Jan 16, 2024
ddc87ac
C++: Accept test changes.
MathiasVP Jan 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 12 additions & 20 deletions cpp/ql/src/Critical/DoubleFree.ql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@

import cpp
import semmle.code.cpp.dataflow.new.DataFlow
import semmle.code.cpp.ir.IR
import FlowAfterFree
import DoubleFree::PathGraph

Expand Down Expand Up @@ -42,28 +41,21 @@ predicate isExcludeFreePair(DeallocationExpr dealloc1, Expr e) {
)
}

module DoubleFree = FlowFromFree<isFree/2, isExcludeFreePair/2>;
module DoubleFreeParam implements FlowFromFreeParamSig {
predicate isSink = isFree/2;

/*
* In order to reduce false positives, the set of sinks is restricted to only those
* that satisfy at least one of the following two criteria:
* 1. The source dominates the sink, or
* 2. The sink post-dominates the source.
*/
predicate isExcluded = isExcludeFreePair/2;

predicate sourceSinkIsRelated = defaultSourceSinkIsRelated/2;
}

from
DoubleFree::PathNode source, DoubleFree::PathNode sink, DeallocationExpr dealloc, Expr e2,
DataFlow::Node srcNode, DataFlow::Node sinkNode
module DoubleFree = FlowFromFree<DoubleFreeParam>;

from DoubleFree::PathNode source, DoubleFree::PathNode sink, DeallocationExpr dealloc, Expr e2
where
DoubleFree::flowPath(source, sink) and
source.getNode() = srcNode and
sink.getNode() = sinkNode and
isFree(srcNode, _, _, dealloc) and
isFree(sinkNode, e2) and
(
sinkStrictlyPostDominatesSource(srcNode, sinkNode) or
sourceStrictlyDominatesSink(srcNode, sinkNode)
)
select sinkNode, source, sink,
isFree(source.getNode(), _, _, dealloc) and
isFree(sink.getNode(), e2)
select sink.getNode(), source, sink,
"Memory pointed to by '" + e2.toString() + "' may already have been freed by $@.", dealloc,
dealloc.toString()
78 changes: 46 additions & 32 deletions cpp/ql/src/Critical/FlowAfterFree.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,6 @@ import cpp
import semmle.code.cpp.dataflow.new.DataFlow
private import semmle.code.cpp.ir.IR

/**
* Signature for a predicate that holds if `n.asExpr() = e` and `n` is a sink in
* the `FlowFromFreeConfig` module.
*/
private signature predicate isSinkSig(DataFlow::Node n, Expr e);

/**
* Holds if `dealloc` is a deallocation expression and `e` is an expression such
* that `isFree(_, e)` holds for some `isFree` predicate satisfying `isSinkSig`,
* and this source-sink pair should be excluded from the analysis.
*/
bindingset[dealloc, e]
private signature predicate isExcludedSig(DeallocationExpr dealloc, Expr e);

/**
* Holds if `(b1, i1)` strictly post-dominates `(b2, i2)`
*/
Expand All @@ -38,27 +24,38 @@ predicate strictlyDominates(IRBlock b1, int i1, IRBlock b2, int i2) {
b1.strictlyDominates(b2)
}

predicate sinkStrictlyPostDominatesSource(DataFlow::Node source, DataFlow::Node sink) {
exists(IRBlock b1, int i1, IRBlock b2, int i2 |
source.hasIndexInBlock(b1, i1) and
sink.hasIndexInBlock(b2, i2) and
strictlyPostDominates(b2, i2, b1, i1)
)
}
signature module FlowFromFreeParamSig {
/**
* Signature for a predicate that holds if `n.asExpr() = e` and `n` is a sink in
* the `FlowFromFreeConfig` module.
*/
predicate isSink(DataFlow::Node n, Expr e);

predicate sourceStrictlyDominatesSink(DataFlow::Node source, DataFlow::Node sink) {
exists(IRBlock b1, int i1, IRBlock b2, int i2 |
source.hasIndexInBlock(b1, i1) and
sink.hasIndexInBlock(b2, i2) and
strictlyDominates(b1, i1, b2, i2)
)
/**
* Holds if `dealloc` is a deallocation expression and `e` is an expression such
* that `isFree(_, e)` holds for some `isFree` predicate satisfying `isSinkSig`,
* and this source-sink pair should be excluded from the analysis.
*/
bindingset[dealloc, e]
predicate isExcluded(DeallocationExpr dealloc, Expr e);

/**
* Holds if `sink` should be considered a `sink` when the source of flow is `source`.
*/
bindingset[source, sink]
default predicate sourceSinkIsRelated(DataFlow::Node source, DataFlow::Node sink) { any() }
}

/**
* Constructs a `FlowFromFreeConfig` module that can be used to find flow between
* a pointer being freed by some deallocation function, and a user-specified sink.
*
* In order to reduce false positives, the set of sinks is restricted to only those
* that satisfy at least one of the following two criteria:
* 1. The source dominates the sink, or
* 2. The sink post-dominates the source.
*/
module FlowFromFree<isSinkSig/2 isASink, isExcludedSig/2 isExcluded> {
module FlowFromFree<FlowFromFreeParamSig P> {
module FlowFromFreeConfig implements DataFlow::StateConfigSig {
class FlowState instanceof Expr {
FlowState() { isFree(_, _, this, _) }
Expand All @@ -70,11 +67,12 @@ module FlowFromFree<isSinkSig/2 isASink, isExcludedSig/2 isExcluded> {

pragma[inline]
predicate isSink(DataFlow::Node sink, FlowState state) {
exists(Expr e, DeallocationExpr dealloc |
isASink(sink, e) and
isFree(_, _, state, dealloc) and
exists(Expr e, DataFlow::Node source, DeallocationExpr dealloc |
P::isSink(sink, e) and
isFree(source, _, state, dealloc) and
e != state and
not isExcluded(dealloc, e)
not P::isExcluded(dealloc, e) and
P::sourceSinkIsRelated(source, sink)
)
}

Expand Down Expand Up @@ -129,3 +127,19 @@ predicate isExFreePoolCall(FunctionCall fc, Expr e) {
fc.getTarget().hasGlobalName("ExFreePool")
)
}

/**
* Holds if either `source` strictly dominates `sink`, or `sink` strictly
* post-dominates `source`.
*/
bindingset[source, sink]
predicate defaultSourceSinkIsRelated(DataFlow::Node source, DataFlow::Node sink) {
exists(IRBlock b1, int i1, IRBlock b2, int i2 |
source.hasIndexInBlock(b1, i1) and
sink.hasIndexInBlock(b2, i2)
|
strictlyDominates(b1, i1, b2, i2)
or
strictlyPostDominates(b2, i2, b1, i1)
)
}
29 changes: 11 additions & 18 deletions cpp/ql/src/Critical/UseAfterFree.ql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,26 +173,19 @@ predicate isExcludeFreeUsePair(DeallocationExpr dealloc1, Expr e) {
isExFreePoolCall(_, e)
}

module UseAfterFree = FlowFromFree<isUse/2, isExcludeFreeUsePair/2>;
module UseAfterFreeParam implements FlowFromFreeParamSig {
predicate isSink = isUse/2;

/*
* In order to reduce false positives, the set of sinks is restricted to only those
* that satisfy at least one of the following two criteria:
* 1. The source dominates the sink, or
* 2. The sink post-dominates the source.
*/
predicate isExcluded = isExcludeFreeUsePair/2;

predicate sourceSinkIsRelated = defaultSourceSinkIsRelated/2;
}

from
UseAfterFree::PathNode source, UseAfterFree::PathNode sink, DeallocationExpr dealloc,
DataFlow::Node srcNode, DataFlow::Node sinkNode
module UseAfterFree = FlowFromFree<UseAfterFreeParam>;

from UseAfterFree::PathNode source, UseAfterFree::PathNode sink, DeallocationExpr dealloc
where
UseAfterFree::flowPath(source, sink) and
source.getNode() = srcNode and
sink.getNode() = sinkNode and
isFree(srcNode, _, _, dealloc) and
(
sinkStrictlyPostDominatesSource(srcNode, sinkNode) or
sourceStrictlyDominatesSink(srcNode, sinkNode)
)
select sinkNode, source, sink, "Memory may have been previously freed by $@.", dealloc,
isFree(source.getNode(), _, _, dealloc)
select sink.getNode(), source, sink, "Memory may have been previously freed by $@.", dealloc,
dealloc.toString()
2 changes: 0 additions & 2 deletions cpp/ql/test/query-tests/Critical/MemoryFreed/DoubleFree.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ edges
| test_free.cpp:11:10:11:10 | pointer to free output argument | test_free.cpp:14:10:14:10 | a |
| test_free.cpp:30:10:30:10 | pointer to free output argument | test_free.cpp:31:27:31:27 | a |
| test_free.cpp:35:10:35:10 | pointer to free output argument | test_free.cpp:37:27:37:27 | a |
| test_free.cpp:42:27:42:27 | pointer to free output argument | test_free.cpp:44:27:44:27 | a |
| test_free.cpp:42:27:42:27 | pointer to free output argument | test_free.cpp:46:10:46:10 | a |
| test_free.cpp:44:27:44:27 | pointer to free output argument | test_free.cpp:46:10:46:10 | a |
| test_free.cpp:50:27:50:27 | pointer to free output argument | test_free.cpp:51:10:51:10 | a |
Expand All @@ -20,7 +19,6 @@ nodes
| test_free.cpp:35:10:35:10 | pointer to free output argument | semmle.label | pointer to free output argument |
| test_free.cpp:37:27:37:27 | a | semmle.label | a |
| test_free.cpp:42:27:42:27 | pointer to free output argument | semmle.label | pointer to free output argument |
| test_free.cpp:44:27:44:27 | a | semmle.label | a |
| test_free.cpp:44:27:44:27 | pointer to free output argument | semmle.label | pointer to free output argument |
| test_free.cpp:46:10:46:10 | a | semmle.label | a |
| test_free.cpp:46:10:46:10 | a | semmle.label | a |
Expand Down
2 changes: 0 additions & 2 deletions cpp/ql/test/query-tests/Critical/MemoryFreed/UseAfterFree.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
edges
| test_free.cpp:11:10:11:10 | pointer to free output argument | test_free.cpp:12:5:12:5 | a |
| test_free.cpp:11:10:11:10 | pointer to free output argument | test_free.cpp:13:5:13:6 | * ... |
| test_free.cpp:42:27:42:27 | pointer to free output argument | test_free.cpp:43:22:43:22 | a |
| test_free.cpp:42:27:42:27 | pointer to free output argument | test_free.cpp:45:5:45:5 | a |
| test_free.cpp:44:27:44:27 | pointer to free output argument | test_free.cpp:45:5:45:5 | a |
| test_free.cpp:69:10:69:10 | pointer to free output argument | test_free.cpp:71:9:71:9 | a |
Expand All @@ -28,7 +27,6 @@ nodes
| test_free.cpp:12:5:12:5 | a | semmle.label | a |
| test_free.cpp:13:5:13:6 | * ... | semmle.label | * ... |
| test_free.cpp:42:27:42:27 | pointer to free output argument | semmle.label | pointer to free output argument |
| test_free.cpp:43:22:43:22 | a | semmle.label | a |
| test_free.cpp:44:27:44:27 | pointer to free output argument | semmle.label | pointer to free output argument |
| test_free.cpp:45:5:45:5 | a | semmle.label | a |
| test_free.cpp:45:5:45:5 | a | semmle.label | a |
Expand Down