Skip to content

Commit 82bbe67

Browse files
rdmarsh2rdmarsh2
authored
Merge pull request #10593 from MathiasVP/fix-fp-on-cwe-193
C++: Fix FPs on `cpp/invalid-pointer-deref`
2 parents df2b586 + 549eca1 commit 82bbe67

File tree

6 files changed

+86
-13
lines changed

6 files changed

+86
-13
lines changed

‎cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,46 @@ module ProductFlow {
4949
this.isSinkPair(sink1, sink2)
5050
}
5151

52+
/**
53+
* Holds if data flow through `node` is prohibited through the first projection of the product
54+
* dataflow graph when the flow state is `state`.
55+
*/
56+
predicate isBarrier1(DataFlow::Node node, DataFlow::FlowState state) {
57+
this.isBarrier1(node) and state = ""
58+
}
59+
60+
/**
61+
* Holds if data flow through `node` is prohibited through the second projection of the product
62+
* dataflow graph when the flow state is `state`.
63+
*/
64+
predicate isBarrier2(DataFlow::Node node, DataFlow::FlowState state) {
65+
this.isBarrier2(node) and state = ""
66+
}
67+
68+
/**
69+
* Holds if data flow through `node` is prohibited through the first projection of the product
70+
* dataflow graph.
71+
*/
72+
predicate isBarrier1(DataFlow::Node node) { none() }
73+
74+
/**
75+
* Holds if data flow through `node` is prohibited through the second projection of the product
76+
* dataflow graph.
77+
*/
78+
predicate isBarrier2(DataFlow::Node node) { none() }
79+
80+
/**
81+
* Holds if data flow out of `node` is prohibited in the first projection of the product
82+
* dataflow graph.
83+
*/
84+
predicate isBarrierOut1(DataFlow::Node node) { none() }
85+
86+
/**
87+
* Holds if data flow out of `node` is prohibited in the second projection of the product
88+
* dataflow graph.
89+
*/
90+
predicate isBarrierOut2(DataFlow::Node node) { none() }
91+
5292
predicate hasFlowPath(
5393
DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode sink1,
5494
DataFlow2::PathNode sink2
@@ -70,6 +110,14 @@ module ProductFlow {
70110
override predicate isSink(DataFlow::Node sink, string state) {
71111
exists(Configuration conf | conf.isSinkPair(sink, state, _, _))
72112
}
113+
114+
override predicate isBarrier(DataFlow::Node node, string state) {
115+
exists(Configuration conf | conf.isBarrier1(node, state))
116+
}
117+
118+
override predicate isBarrierOut(DataFlow::Node node) {
119+
exists(Configuration conf | conf.isBarrierOut1(node))
120+
}
73121
}
74122

75123
class Conf2 extends DataFlow2::Configuration {
@@ -87,6 +135,14 @@ module ProductFlow {
87135
conf.isSinkPair(sink1, _, sink, state) and any(Conf1 c).hasFlow(_, sink1)
88136
)
89137
}
138+
139+
override predicate isBarrier(DataFlow::Node node, string state) {
140+
exists(Configuration conf | conf.isBarrier2(node, state))
141+
}
142+
143+
override predicate isBarrierOut(DataFlow::Node node) {
144+
exists(Configuration conf | conf.isBarrierOut2(node))
145+
}
90146
}
91147
}
92148

‎cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -416,6 +416,21 @@ class SsaPhiNode extends Node, TSsaPhiNode {
416416
final override Location getLocationImpl() { result = phi.getBasicBlock().getLocation() }
417417

418418
override string toStringImpl() { result = "Phi" }
419+
420+
/**
421+
* Gets a node that is used as input to this phi node.
422+
* `fromBackEdge` is true if data flows along a back-edge,
423+
* and `false` otherwise.
424+
*/
425+
final Node getAnInput(boolean fromBackEdge) {
426+
localFlowStep(result, this) and
427+
if phi.getBasicBlock().dominates(getBasicBlock(result))
428+
then fromBackEdge = true
429+
else fromBackEdge = false
430+
}
431+
432+
/** Gets a node that is used as input to this phi node. */
433+
final Node getAnInput() { result = this.getAnInput(_) }
419434
}
420435

421436
/**

‎cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -301,7 +301,12 @@ private predicate defToNode(Node nodeFrom, Def def) {
301301
nodeHasInstruction(nodeFrom, def.getDefiningInstruction(), def.getIndirectionIndex())
302302
}
303303

304-
private predicate nodeToDefOrUse(Node nodeFrom, SsaDefOrUse defOrUse) {
304+
/**
305+
* INTERNAL: Do not use.
306+
*
307+
* Holds if `nodeFrom` is the node that correspond to the definition or use `defOrUse`.
308+
*/
309+
predicate nodeToDefOrUse(Node nodeFrom, SsaDefOrUse defOrUse) {
305310
// Node -> Def
306311
defToNode(nodeFrom, defOrUse)
307312
or

‎cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,10 @@ class AllocToInvalidPointerConf extends ProductFlow::Configuration {
128128
state2 = delta.toString()
129129
)
130130
}
131+
132+
override predicate isBarrierOut2(DataFlow::Node node) {
133+
node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
134+
}
131135
}
132136

133137
pragma[nomagic]
@@ -154,11 +158,11 @@ predicate pointerAddInstructionHasOperands(
154158
*/
155159
pragma[nomagic]
156160
predicate pointerAddInstructionHasBounds(
157-
PointerAddInstruction pai, DataFlow::Node sink1, Instruction sink2, int delta
161+
PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
158162
) {
159163
exists(Instruction right |
160164
pointerAddInstructionHasOperands(pai, sink1.asInstruction(), right) and
161-
bounded(right, sink2, delta)
165+
bounded(right, sink2.asInstruction(), delta)
162166
)
163167
}
164168

@@ -171,7 +175,7 @@ predicate pointerAddInstructionHasBounds(
171175
predicate isSinkImpl(
172176
PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
173177
) {
174-
pointerAddInstructionHasBounds(pai, sink1, sink2.asInstruction(), delta)
178+
pointerAddInstructionHasBounds(pai, sink1, sink2, delta)
175179
}
176180

177181
/**

‎cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/InvalidPointerDeref.expected

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -678,12 +678,6 @@ edges
678678
| test.cpp:213:6:213:6 | Load | test.cpp:213:5:213:13 | Store: ... = ... |
679679
| test.cpp:213:6:213:6 | Load | test.cpp:213:5:213:13 | Store: ... = ... |
680680
| test.cpp:221:17:221:22 | call to malloc | test.cpp:222:5:222:5 | Load |
681-
| test.cpp:222:5:222:5 | Load | test.cpp:222:5:222:12 | access to array |
682-
| test.cpp:222:5:222:5 | Load | test.cpp:222:5:222:12 | access to array |
683-
| test.cpp:222:5:222:5 | Load | test.cpp:222:5:222:12 | access to array |
684-
| test.cpp:222:5:222:5 | Load | test.cpp:222:5:222:12 | access to array |
685-
| test.cpp:222:5:222:12 | access to array | test.cpp:222:5:222:18 | Store: ... = ... |
686-
| test.cpp:222:5:222:12 | access to array | test.cpp:222:5:222:18 | Store: ... = ... |
687681
#select
688682
| test.cpp:6:14:6:15 | Load: * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:6:14:6:15 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size |
689683
| test.cpp:8:14:8:21 | Load: * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:8:14:8:21 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size |
@@ -702,4 +696,3 @@ edges
702696
| test.cpp:171:9:171:14 | Store: ... = ... | test.cpp:143:18:143:23 | call to malloc | test.cpp:171:9:171:14 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:143:18:143:23 | call to malloc | call to malloc | test.cpp:144:29:144:32 | size | size |
703697
| test.cpp:201:5:201:19 | Store: ... = ... | test.cpp:194:23:194:28 | call to malloc | test.cpp:201:5:201:19 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:194:23:194:28 | call to malloc | call to malloc | test.cpp:195:21:195:23 | len | len |
704698
| test.cpp:213:5:213:13 | Store: ... = ... | test.cpp:205:23:205:28 | call to malloc | test.cpp:213:5:213:13 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:205:23:205:28 | call to malloc | call to malloc | test.cpp:206:21:206:23 | len | len |
705-
| test.cpp:222:5:222:18 | Store: ... = ... | test.cpp:221:17:221:22 | call to malloc | test.cpp:222:5:222:18 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:221:17:221:22 | call to malloc | call to malloc | test.cpp:222:7:222:11 | ... - ... | ... - ... |

‎cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -219,6 +219,6 @@ void test14(unsigned long n, char *p) {
219219
while (unknown()) {
220220
n++;
221221
p = (char *)malloc(n);
222-
p[n - 1] = 'a'; // GOOD [FALSE POSITIVE]
222+
p[n - 1] = 'a'; // GOOD
223223
}
224-
}
224+
}

0 commit comments

Comments
 (0)