Skip to content

Commit 985650c

Browse files
MathiasVPMathiasVP
authored
Merge pull request github#13559 from MathiasVP/add-barrier-to-invalid-deref-query
C++: Add barriers to `cpp/invalid-pointer-deref`
2 parents 29f5c78 + ef383a1 commit 985650c

File tree

3 files changed

+300
-24
lines changed

3 files changed

+300
-24
lines changed

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

Lines changed: 129 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,8 @@ import cpp
1919
import semmle.code.cpp.ir.dataflow.internal.ProductFlow
2020
import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
2121
import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
22+
import semmle.code.cpp.ir.ValueNumbering
23+
import semmle.code.cpp.controlflow.IRGuards
2224
import semmle.code.cpp.ir.IR
2325
import codeql.util.Unit
2426

@@ -67,6 +69,86 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
6769
)
6870
}
6971

72+
/**
73+
* A module that encapsulates a barrier guard to remove false positives from flow like:
74+
* ```cpp
75+
* char *p = new char[size];
76+
* // ...
77+
* unsigned n = size;
78+
* // ...
79+
* if(n < size) {
80+
* use(*p[n]);
81+
* }
82+
* ```
83+
* In this case, the sink pair identified by the product flow library (without any additional barriers)
84+
* would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
85+
* instruction `pai` such that:
86+
* 1. The left-hand of `pai` flows from the allocation, and
87+
* 2. The right-hand of `pai` is non-strictly upper bounded by `n` (where `n` is the `n` in `p[n]`)
88+
* but because there's a strict comparison that compares `n` against the size of the allocation this
89+
* snippet is fine.
90+
*/
91+
module Barrier2 {
92+
private class FlowState2 = AllocToInvalidPointerConfig::FlowState2;
93+
94+
private module BarrierConfig2 implements DataFlow::ConfigSig {
95+
predicate isSource(DataFlow::Node source) {
96+
// The sources is the same as in the sources for the second
97+
// projection in the `AllocToInvalidPointerConfig` module.
98+
hasSize(_, source, _)
99+
}
100+
101+
additional predicate isSink(
102+
DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, FlowState2 state,
103+
boolean testIsTrue
104+
) {
105+
// The sink is any "large" side of a relational comparison.
106+
g.comparesLt(left.asOperand(), right.asOperand(), state, true, testIsTrue)
107+
}
108+
109+
predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
110+
}
111+
112+
private import DataFlow::Global<BarrierConfig2>
113+
114+
private FlowState2 getAFlowStateForNode(DataFlow::Node node) {
115+
exists(DataFlow::Node source |
116+
flow(source, node) and
117+
hasSize(_, source, result)
118+
)
119+
}
120+
121+
private predicate operandGuardChecks(
122+
IRGuardCondition g, Operand left, Operand right, FlowState2 state, boolean edge
123+
) {
124+
exists(DataFlow::Node nLeft, DataFlow::Node nRight, FlowState2 state0 |
125+
nRight.asOperand() = right and
126+
nLeft.asOperand() = left and
127+
BarrierConfig2::isSink(nLeft, nRight, g, state0, edge) and
128+
state = getAFlowStateForNode(nRight) and
129+
state0 <= state
130+
)
131+
}
132+
133+
Instruction getABarrierInstruction(FlowState2 state) {
134+
exists(IRGuardCondition g, ValueNumber value, Operand use, boolean edge |
135+
use = value.getAUse() and
136+
operandGuardChecks(pragma[only_bind_into](g), pragma[only_bind_into](use), _,
137+
pragma[only_bind_into](state), pragma[only_bind_into](edge)) and
138+
result = value.getAnInstruction() and
139+
g.controls(result.getBlock(), edge)
140+
)
141+
}
142+
143+
DataFlow::Node getABarrierNode(FlowState2 state) {
144+
result.asOperand() = getABarrierInstruction(state).getAUse()
145+
}
146+
147+
IRBlock getABarrierBlock(FlowState2 state) {
148+
result.getAnInstruction() = getABarrierInstruction(state)
149+
}
150+
}
151+
70152
/**
71153
* A product-flow configuration for flow from an (allocation, size) pair to a
72154
* pointer-arithmetic operation that is non-strictly upper-bounded by `allocation + size`.
@@ -111,15 +193,14 @@ module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
111193
exists(state1) and
112194
// We check that the delta computed by the range analysis matches the
113195
// state value that we set in `isSourcePair`.
114-
exists(int delta |
115-
isSinkImpl(_, sink1, sink2, delta) and
116-
state2 = delta
117-
)
196+
isSinkImpl(_, sink1, sink2, state2)
118197
}
119198

120199
predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() }
121200

122-
predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() }
201+
predicate isBarrier2(DataFlow::Node node, FlowState2 state) {
202+
node = Barrier2::getABarrierNode(state)
203+
}
123204

124205
predicate isBarrierIn1(DataFlow::Node node) { isSourcePair(node, _, _, _) }
125206

@@ -160,13 +241,40 @@ pragma[nomagic]
160241
predicate pointerAddInstructionHasBounds(
161242
PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
162243
) {
163-
exists(Instruction right |
244+
InterestingPointerAddInstruction::isInteresting(pragma[only_bind_into](pai)) and
245+
exists(Instruction right, Instruction instr2 |
164246
pai.getRight() = right and
165247
pai.getLeft() = sink1.asInstruction() and
166-
bounded1(right, sink2.asInstruction(), delta)
248+
instr2 = sink2.asInstruction() and
249+
bounded1(right, instr2, delta) and
250+
not right = Barrier2::getABarrierInstruction(delta) and
251+
not instr2 = Barrier2::getABarrierInstruction(delta)
167252
)
168253
}
169254

255+
module InterestingPointerAddInstruction {
256+
private module PointerAddInstructionConfig implements DataFlow::ConfigSig {
257+
predicate isSource(DataFlow::Node source) {
258+
// The sources is the same as in the sources for the second
259+
// projection in the `AllocToInvalidPointerConfig` module.
260+
hasSize(source.asConvertedExpr(), _, _)
261+
}
262+
263+
predicate isSink(DataFlow::Node sink) {
264+
sink.asInstruction() = any(PointerAddInstruction pai).getLeft()
265+
}
266+
}
267+
268+
private import DataFlow::Global<PointerAddInstructionConfig>
269+
270+
predicate isInteresting(PointerAddInstruction pai) {
271+
exists(DataFlow::Node n |
272+
n.asInstruction() = pai.getLeft() and
273+
flowTo(n)
274+
)
275+
}
276+
}
277+
170278
/**
171279
* Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
172280
* left operand of the pointer-arithmetic operation.
@@ -246,12 +354,21 @@ module InvalidPointerToDerefFlow = DataFlow::Global<InvalidPointerToDerefConfig>
246354
predicate invalidPointerToDerefSource(
247355
PointerArithmeticInstruction pai, DataFlow::Node source, int delta
248356
) {
249-
exists(AllocToInvalidPointerFlow::PathNode1 p, DataFlow::Node sink1 |
250-
pragma[only_bind_out](p.getNode()) = sink1 and
251-
AllocToInvalidPointerFlow::flowPath(_, _, pragma[only_bind_into](p), _) and
252-
isSinkImpl(pai, sink1, _, _) and
357+
exists(
358+
AllocToInvalidPointerFlow::PathNode1 p1, AllocToInvalidPointerFlow::PathNode2 p2,
359+
DataFlow::Node sink1, DataFlow::Node sink2, int delta0
360+
|
361+
pragma[only_bind_out](p1.getNode()) = sink1 and
362+
pragma[only_bind_out](p2.getNode()) = sink2 and
363+
AllocToInvalidPointerFlow::flowPath(_, _, pragma[only_bind_into](p1), pragma[only_bind_into](p2)) and
364+
// Note that `delta` is not necessarily equal to `delta0`:
365+
// `delta0` is the constant offset added to the size of the allocation, and
366+
// delta is the constant difference between the pointer-arithmetic instruction
367+
// and the instruction computing the address for which we will search for a dereference.
368+
isSinkImpl(pai, sink1, sink2, delta0) and
253369
bounded2(source.asInstruction(), pai, delta) and
254-
delta >= 0
370+
delta >= 0 and
371+
not source.getBasicBlock() = Barrier2::getABarrierBlock(delta0)
255372
)
256373
}
257374

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

Lines changed: 48 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -783,11 +783,24 @@ edges
783783
| test.cpp:407:7:407:8 | xs | test.cpp:407:3:407:18 | access to array |
784784
| test.cpp:407:7:407:8 | xs indirection | test.cpp:407:7:407:8 | xs |
785785
| test.cpp:417:16:417:33 | new[] | test.cpp:419:7:419:8 | xs |
786-
| test.cpp:419:7:419:8 | xs | test.cpp:419:7:419:11 | access to array |
787-
| test.cpp:419:7:419:11 | access to array | test.cpp:419:7:419:15 | Store: ... = ... |
788786
| test.cpp:427:14:427:27 | new[] | test.cpp:433:5:433:6 | xs |
789-
| test.cpp:433:5:433:6 | xs | test.cpp:433:5:433:17 | access to array |
790-
| test.cpp:433:5:433:17 | access to array | test.cpp:433:5:433:21 | Store: ... = ... |
787+
| test.cpp:439:14:439:27 | new[] | test.cpp:444:5:444:6 | xs |
788+
| test.cpp:450:14:450:27 | new[] | test.cpp:455:5:455:6 | xs |
789+
| test.cpp:455:5:455:6 | xs | test.cpp:455:5:455:15 | access to array |
790+
| test.cpp:455:5:455:15 | access to array | test.cpp:455:5:455:19 | Store: ... = ... |
791+
| test.cpp:461:14:461:27 | new[] | test.cpp:466:5:466:6 | xs |
792+
| test.cpp:466:5:466:6 | xs | test.cpp:466:5:466:15 | access to array |
793+
| test.cpp:466:5:466:15 | access to array | test.cpp:466:5:466:19 | Store: ... = ... |
794+
| test.cpp:472:14:472:27 | new[] | test.cpp:477:5:477:6 | xs |
795+
| test.cpp:483:14:483:27 | new[] | test.cpp:488:5:488:6 | xs |
796+
| test.cpp:494:14:494:31 | new[] | test.cpp:499:5:499:6 | xs |
797+
| test.cpp:505:14:505:31 | new[] | test.cpp:510:5:510:6 | xs |
798+
| test.cpp:516:14:516:31 | new[] | test.cpp:521:5:521:6 | xs |
799+
| test.cpp:527:14:527:31 | new[] | test.cpp:532:5:532:6 | xs |
800+
| test.cpp:538:14:538:31 | new[] | test.cpp:543:5:543:6 | xs |
801+
| test.cpp:549:14:549:31 | new[] | test.cpp:554:5:554:6 | xs |
802+
| test.cpp:554:5:554:6 | xs | test.cpp:554:5:554:15 | access to array |
803+
| test.cpp:554:5:554:15 | access to array | test.cpp:554:5:554:19 | Store: ... = ... |
791804
nodes
792805
| test.cpp:4:15:4:20 | call to malloc | semmle.label | call to malloc |
793806
| test.cpp:5:15:5:15 | p | semmle.label | p |
@@ -1151,12 +1164,36 @@ nodes
11511164
| test.cpp:407:7:407:8 | xs indirection | semmle.label | xs indirection |
11521165
| test.cpp:417:16:417:33 | new[] | semmle.label | new[] |
11531166
| test.cpp:419:7:419:8 | xs | semmle.label | xs |
1154-
| test.cpp:419:7:419:11 | access to array | semmle.label | access to array |
1155-
| test.cpp:419:7:419:15 | Store: ... = ... | semmle.label | Store: ... = ... |
11561167
| test.cpp:427:14:427:27 | new[] | semmle.label | new[] |
11571168
| test.cpp:433:5:433:6 | xs | semmle.label | xs |
1158-
| test.cpp:433:5:433:17 | access to array | semmle.label | access to array |
1159-
| test.cpp:433:5:433:21 | Store: ... = ... | semmle.label | Store: ... = ... |
1169+
| test.cpp:439:14:439:27 | new[] | semmle.label | new[] |
1170+
| test.cpp:444:5:444:6 | xs | semmle.label | xs |
1171+
| test.cpp:450:14:450:27 | new[] | semmle.label | new[] |
1172+
| test.cpp:455:5:455:6 | xs | semmle.label | xs |
1173+
| test.cpp:455:5:455:15 | access to array | semmle.label | access to array |
1174+
| test.cpp:455:5:455:19 | Store: ... = ... | semmle.label | Store: ... = ... |
1175+
| test.cpp:461:14:461:27 | new[] | semmle.label | new[] |
1176+
| test.cpp:466:5:466:6 | xs | semmle.label | xs |
1177+
| test.cpp:466:5:466:15 | access to array | semmle.label | access to array |
1178+
| test.cpp:466:5:466:19 | Store: ... = ... | semmle.label | Store: ... = ... |
1179+
| test.cpp:472:14:472:27 | new[] | semmle.label | new[] |
1180+
| test.cpp:477:5:477:6 | xs | semmle.label | xs |
1181+
| test.cpp:483:14:483:27 | new[] | semmle.label | new[] |
1182+
| test.cpp:488:5:488:6 | xs | semmle.label | xs |
1183+
| test.cpp:494:14:494:31 | new[] | semmle.label | new[] |
1184+
| test.cpp:499:5:499:6 | xs | semmle.label | xs |
1185+
| test.cpp:505:14:505:31 | new[] | semmle.label | new[] |
1186+
| test.cpp:510:5:510:6 | xs | semmle.label | xs |
1187+
| test.cpp:516:14:516:31 | new[] | semmle.label | new[] |
1188+
| test.cpp:521:5:521:6 | xs | semmle.label | xs |
1189+
| test.cpp:527:14:527:31 | new[] | semmle.label | new[] |
1190+
| test.cpp:532:5:532:6 | xs | semmle.label | xs |
1191+
| test.cpp:538:14:538:31 | new[] | semmle.label | new[] |
1192+
| test.cpp:543:5:543:6 | xs | semmle.label | xs |
1193+
| test.cpp:549:14:549:31 | new[] | semmle.label | new[] |
1194+
| test.cpp:554:5:554:6 | xs | semmle.label | xs |
1195+
| test.cpp:554:5:554:15 | access to array | semmle.label | access to array |
1196+
| test.cpp:554:5:554:19 | Store: ... = ... | semmle.label | Store: ... = ... |
11601197
subpaths
11611198
#select
11621199
| 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 |
@@ -1185,5 +1222,6 @@ subpaths
11851222
| test.cpp:384:13:384:16 | Load: * ... | test.cpp:377:14:377:27 | new[] | test.cpp:384:13:384:16 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:377:14:377:27 | new[] | new[] | test.cpp:378:20:378:23 | size | size |
11861223
| test.cpp:395:5:395:13 | Store: ... = ... | test.cpp:388:14:388:27 | new[] | test.cpp:395:5:395:13 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:388:14:388:27 | new[] | new[] | test.cpp:389:19:389:22 | size | size |
11871224
| test.cpp:407:3:407:22 | Store: ... = ... | test.cpp:404:12:404:25 | new[] | test.cpp:407:3:407:22 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:404:12:404:25 | new[] | new[] | test.cpp:407:10:407:17 | ... - ... | ... - ... |
1188-
| test.cpp:419:7:419:15 | Store: ... = ... | test.cpp:417:16:417:33 | new[] | test.cpp:419:7:419:15 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:417:16:417:33 | new[] | new[] | test.cpp:419:10:419:10 | i | i |
1189-
| test.cpp:433:5:433:21 | Store: ... = ... | test.cpp:427:14:427:27 | new[] | test.cpp:433:5:433:21 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:427:14:427:27 | new[] | new[] | test.cpp:433:8:433:16 | ... ++ | ... ++ |
1225+
| test.cpp:455:5:455:19 | Store: ... = ... | test.cpp:450:14:450:27 | new[] | test.cpp:455:5:455:19 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:450:14:450:27 | new[] | new[] | test.cpp:455:8:455:14 | src_pos | src_pos |
1226+
| test.cpp:466:5:466:19 | Store: ... = ... | test.cpp:461:14:461:27 | new[] | test.cpp:466:5:466:19 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:461:14:461:27 | new[] | new[] | test.cpp:466:8:466:14 | src_pos | src_pos |
1227+
| test.cpp:554:5:554:19 | Store: ... = ... | test.cpp:549:14:549:31 | new[] | test.cpp:554:5:554:19 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:549:14:549:31 | new[] | new[] | test.cpp:554:8:554:14 | src_pos | src_pos |

0 commit comments

Comments
 (0)