mirror of
https://github.com/github/codeql.git
synced 2026-04-26 09:15:12 +02:00
Merge pull request #13559 from MathiasVP/add-barrier-to-invalid-deref-query
C++: Add barriers to `cpp/invalid-pointer-deref`
This commit is contained in:
Mathias Vorreiter Pedersen
@@ -19,6 +19,8 @@ import cpp
|
||||
import semmle.code.cpp.ir.dataflow.internal.ProductFlow
|
||||
import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
|
||||
import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
|
||||
import semmle.code.cpp.ir.ValueNumbering
|
||||
import semmle.code.cpp.controlflow.IRGuards
|
||||
import semmle.code.cpp.ir.IR
|
||||
import codeql.util.Unit
|
||||
|
||||
@@ -67,6 +69,86 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* A module that encapsulates a barrier guard to remove false positives from flow like:
|
||||
* ```cpp
|
||||
* char *p = new char[size];
|
||||
* // ...
|
||||
* unsigned n = size;
|
||||
* // ...
|
||||
* if(n < size) {
|
||||
* use(*p[n]);
|
||||
* }
|
||||
* ```
|
||||
* In this case, the sink pair identified by the product flow library (without any additional barriers)
|
||||
* would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
|
||||
* instruction `pai` such that:
|
||||
* 1. The left-hand of `pai` flows from the allocation, and
|
||||
* 2. The right-hand of `pai` is non-strictly upper bounded by `n` (where `n` is the `n` in `p[n]`)
|
||||
* but because there's a strict comparison that compares `n` against the size of the allocation this
|
||||
* snippet is fine.
|
||||
*/
|
||||
module Barrier2 {
|
||||
private class FlowState2 = AllocToInvalidPointerConfig::FlowState2;
|
||||
|
||||
private module BarrierConfig2 implements DataFlow::ConfigSig {
|
||||
predicate isSource(DataFlow::Node source) {
|
||||
// The sources is the same as in the sources for the second
|
||||
// projection in the `AllocToInvalidPointerConfig` module.
|
||||
hasSize(_, source, _)
|
||||
}
|
||||
|
||||
additional predicate isSink(
|
||||
DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, FlowState2 state,
|
||||
boolean testIsTrue
|
||||
) {
|
||||
// The sink is any "large" side of a relational comparison.
|
||||
g.comparesLt(left.asOperand(), right.asOperand(), state, true, testIsTrue)
|
||||
}
|
||||
|
||||
predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
|
||||
}
|
||||
|
||||
private import DataFlow::Global<BarrierConfig2>
|
||||
|
||||
private FlowState2 getAFlowStateForNode(DataFlow::Node node) {
|
||||
exists(DataFlow::Node source |
|
||||
flow(source, node) and
|
||||
hasSize(_, source, result)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate operandGuardChecks(
|
||||
IRGuardCondition g, Operand left, Operand right, FlowState2 state, boolean edge
|
||||
) {
|
||||
exists(DataFlow::Node nLeft, DataFlow::Node nRight, FlowState2 state0 |
|
||||
nRight.asOperand() = right and
|
||||
nLeft.asOperand() = left and
|
||||
BarrierConfig2::isSink(nLeft, nRight, g, state0, edge) and
|
||||
state = getAFlowStateForNode(nRight) and
|
||||
state0 <= state
|
||||
)
|
||||
}
|
||||
|
||||
Instruction getABarrierInstruction(FlowState2 state) {
|
||||
exists(IRGuardCondition g, ValueNumber value, Operand use, boolean edge |
|
||||
use = value.getAUse() and
|
||||
operandGuardChecks(pragma[only_bind_into](g), pragma[only_bind_into](use), _,
|
||||
pragma[only_bind_into](state), pragma[only_bind_into](edge)) and
|
||||
result = value.getAnInstruction() and
|
||||
g.controls(result.getBlock(), edge)
|
||||
)
|
||||
}
|
||||
|
||||
DataFlow::Node getABarrierNode(FlowState2 state) {
|
||||
result.asOperand() = getABarrierInstruction(state).getAUse()
|
||||
}
|
||||
|
||||
IRBlock getABarrierBlock(FlowState2 state) {
|
||||
result.getAnInstruction() = getABarrierInstruction(state)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A product-flow configuration for flow from an (allocation, size) pair to a
|
||||
* pointer-arithmetic operation that is non-strictly upper-bounded by `allocation + size`.
|
||||
@@ -111,15 +193,14 @@ module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
|
||||
exists(state1) and
|
||||
// We check that the delta computed by the range analysis matches the
|
||||
// state value that we set in `isSourcePair`.
|
||||
exists(int delta |
|
||||
isSinkImpl(_, sink1, sink2, delta) and
|
||||
state2 = delta
|
||||
)
|
||||
isSinkImpl(_, sink1, sink2, state2)
|
||||
}
|
||||
|
||||
predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() }
|
||||
|
||||
predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() }
|
||||
predicate isBarrier2(DataFlow::Node node, FlowState2 state) {
|
||||
node = Barrier2::getABarrierNode(state)
|
||||
}
|
||||
|
||||
predicate isBarrierIn1(DataFlow::Node node) { isSourcePair(node, _, _, _) }
|
||||
|
||||
@@ -160,13 +241,40 @@ pragma[nomagic]
|
||||
predicate pointerAddInstructionHasBounds(
|
||||
PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
|
||||
) {
|
||||
exists(Instruction right |
|
||||
InterestingPointerAddInstruction::isInteresting(pragma[only_bind_into](pai)) and
|
||||
exists(Instruction right, Instruction instr2 |
|
||||
pai.getRight() = right and
|
||||
pai.getLeft() = sink1.asInstruction() and
|
||||
bounded1(right, sink2.asInstruction(), delta)
|
||||
instr2 = sink2.asInstruction() and
|
||||
bounded1(right, instr2, delta) and
|
||||
not right = Barrier2::getABarrierInstruction(delta) and
|
||||
not instr2 = Barrier2::getABarrierInstruction(delta)
|
||||
)
|
||||
}
|
||||
|
||||
module InterestingPointerAddInstruction {
|
||||
private module PointerAddInstructionConfig implements DataFlow::ConfigSig {
|
||||
predicate isSource(DataFlow::Node source) {
|
||||
// The sources is the same as in the sources for the second
|
||||
// projection in the `AllocToInvalidPointerConfig` module.
|
||||
hasSize(source.asConvertedExpr(), _, _)
|
||||
}
|
||||
|
||||
predicate isSink(DataFlow::Node sink) {
|
||||
sink.asInstruction() = any(PointerAddInstruction pai).getLeft()
|
||||
}
|
||||
}
|
||||
|
||||
private import DataFlow::Global<PointerAddInstructionConfig>
|
||||
|
||||
predicate isInteresting(PointerAddInstruction pai) {
|
||||
exists(DataFlow::Node n |
|
||||
n.asInstruction() = pai.getLeft() and
|
||||
flowTo(n)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
|
||||
* left operand of the pointer-arithmetic operation.
|
||||
@@ -246,12 +354,21 @@ module InvalidPointerToDerefFlow = DataFlow::Global<InvalidPointerToDerefConfig>
|
||||
predicate invalidPointerToDerefSource(
|
||||
PointerArithmeticInstruction pai, DataFlow::Node source, int delta
|
||||
) {
|
||||
exists(AllocToInvalidPointerFlow::PathNode1 p, DataFlow::Node sink1 |
|
||||
pragma[only_bind_out](p.getNode()) = sink1 and
|
||||
AllocToInvalidPointerFlow::flowPath(_, _, pragma[only_bind_into](p), _) and
|
||||
isSinkImpl(pai, sink1, _, _) and
|
||||
exists(
|
||||
AllocToInvalidPointerFlow::PathNode1 p1, AllocToInvalidPointerFlow::PathNode2 p2,
|
||||
DataFlow::Node sink1, DataFlow::Node sink2, int delta0
|
||||
|
|
||||
pragma[only_bind_out](p1.getNode()) = sink1 and
|
||||
pragma[only_bind_out](p2.getNode()) = sink2 and
|
||||
AllocToInvalidPointerFlow::flowPath(_, _, pragma[only_bind_into](p1), pragma[only_bind_into](p2)) and
|
||||
// Note that `delta` is not necessarily equal to `delta0`:
|
||||
// `delta0` is the constant offset added to the size of the allocation, and
|
||||
// delta is the constant difference between the pointer-arithmetic instruction
|
||||
// and the instruction computing the address for which we will search for a dereference.
|
||||
isSinkImpl(pai, sink1, sink2, delta0) and
|
||||
bounded2(source.asInstruction(), pai, delta) and
|
||||
delta >= 0
|
||||
delta >= 0 and
|
||||
not source.getBasicBlock() = Barrier2::getABarrierBlock(delta0)
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
@@ -783,11 +783,24 @@ edges
|
||||
| test.cpp:407:7:407:8 | xs | test.cpp:407:3:407:18 | access to array |
|
||||
| test.cpp:407:7:407:8 | xs indirection | test.cpp:407:7:407:8 | xs |
|
||||
| test.cpp:417:16:417:33 | new[] | test.cpp:419:7:419:8 | xs |
|
||||
| test.cpp:419:7:419:8 | xs | test.cpp:419:7:419:11 | access to array |
|
||||
| test.cpp:419:7:419:11 | access to array | test.cpp:419:7:419:15 | Store: ... = ... |
|
||||
| test.cpp:427:14:427:27 | new[] | test.cpp:433:5:433:6 | xs |
|
||||
| test.cpp:433:5:433:6 | xs | test.cpp:433:5:433:17 | access to array |
|
||||
| test.cpp:433:5:433:17 | access to array | test.cpp:433:5:433:21 | Store: ... = ... |
|
||||
| test.cpp:439:14:439:27 | new[] | test.cpp:444:5:444:6 | xs |
|
||||
| test.cpp:450:14:450:27 | new[] | test.cpp:455:5:455:6 | xs |
|
||||
| test.cpp:455:5:455:6 | xs | test.cpp:455:5:455:15 | access to array |
|
||||
| test.cpp:455:5:455:15 | access to array | test.cpp:455:5:455:19 | Store: ... = ... |
|
||||
| test.cpp:461:14:461:27 | new[] | test.cpp:466:5:466:6 | xs |
|
||||
| test.cpp:466:5:466:6 | xs | test.cpp:466:5:466:15 | access to array |
|
||||
| test.cpp:466:5:466:15 | access to array | test.cpp:466:5:466:19 | Store: ... = ... |
|
||||
| test.cpp:472:14:472:27 | new[] | test.cpp:477:5:477:6 | xs |
|
||||
| test.cpp:483:14:483:27 | new[] | test.cpp:488:5:488:6 | xs |
|
||||
| test.cpp:494:14:494:31 | new[] | test.cpp:499:5:499:6 | xs |
|
||||
| test.cpp:505:14:505:31 | new[] | test.cpp:510:5:510:6 | xs |
|
||||
| test.cpp:516:14:516:31 | new[] | test.cpp:521:5:521:6 | xs |
|
||||
| test.cpp:527:14:527:31 | new[] | test.cpp:532:5:532:6 | xs |
|
||||
| test.cpp:538:14:538:31 | new[] | test.cpp:543:5:543:6 | xs |
|
||||
| test.cpp:549:14:549:31 | new[] | test.cpp:554:5:554:6 | xs |
|
||||
| test.cpp:554:5:554:6 | xs | test.cpp:554:5:554:15 | access to array |
|
||||
| test.cpp:554:5:554:15 | access to array | test.cpp:554:5:554:19 | Store: ... = ... |
|
||||
nodes
|
||||
| test.cpp:4:15:4:20 | call to malloc | semmle.label | call to malloc |
|
||||
| test.cpp:5:15:5:15 | p | semmle.label | p |
|
||||
@@ -1151,12 +1164,36 @@ nodes
|
||||
| test.cpp:407:7:407:8 | xs indirection | semmle.label | xs indirection |
|
||||
| test.cpp:417:16:417:33 | new[] | semmle.label | new[] |
|
||||
| test.cpp:419:7:419:8 | xs | semmle.label | xs |
|
||||
| test.cpp:419:7:419:11 | access to array | semmle.label | access to array |
|
||||
| test.cpp:419:7:419:15 | Store: ... = ... | semmle.label | Store: ... = ... |
|
||||
| test.cpp:427:14:427:27 | new[] | semmle.label | new[] |
|
||||
| test.cpp:433:5:433:6 | xs | semmle.label | xs |
|
||||
| test.cpp:433:5:433:17 | access to array | semmle.label | access to array |
|
||||
| test.cpp:433:5:433:21 | Store: ... = ... | semmle.label | Store: ... = ... |
|
||||
| test.cpp:439:14:439:27 | new[] | semmle.label | new[] |
|
||||
| test.cpp:444:5:444:6 | xs | semmle.label | xs |
|
||||
| test.cpp:450:14:450:27 | new[] | semmle.label | new[] |
|
||||
| test.cpp:455:5:455:6 | xs | semmle.label | xs |
|
||||
| test.cpp:455:5:455:15 | access to array | semmle.label | access to array |
|
||||
| test.cpp:455:5:455:19 | Store: ... = ... | semmle.label | Store: ... = ... |
|
||||
| test.cpp:461:14:461:27 | new[] | semmle.label | new[] |
|
||||
| test.cpp:466:5:466:6 | xs | semmle.label | xs |
|
||||
| test.cpp:466:5:466:15 | access to array | semmle.label | access to array |
|
||||
| test.cpp:466:5:466:19 | Store: ... = ... | semmle.label | Store: ... = ... |
|
||||
| test.cpp:472:14:472:27 | new[] | semmle.label | new[] |
|
||||
| test.cpp:477:5:477:6 | xs | semmle.label | xs |
|
||||
| test.cpp:483:14:483:27 | new[] | semmle.label | new[] |
|
||||
| test.cpp:488:5:488:6 | xs | semmle.label | xs |
|
||||
| test.cpp:494:14:494:31 | new[] | semmle.label | new[] |
|
||||
| test.cpp:499:5:499:6 | xs | semmle.label | xs |
|
||||
| test.cpp:505:14:505:31 | new[] | semmle.label | new[] |
|
||||
| test.cpp:510:5:510:6 | xs | semmle.label | xs |
|
||||
| test.cpp:516:14:516:31 | new[] | semmle.label | new[] |
|
||||
| test.cpp:521:5:521:6 | xs | semmle.label | xs |
|
||||
| test.cpp:527:14:527:31 | new[] | semmle.label | new[] |
|
||||
| test.cpp:532:5:532:6 | xs | semmle.label | xs |
|
||||
| test.cpp:538:14:538:31 | new[] | semmle.label | new[] |
|
||||
| test.cpp:543:5:543:6 | xs | semmle.label | xs |
|
||||
| test.cpp:549:14:549:31 | new[] | semmle.label | new[] |
|
||||
| test.cpp:554:5:554:6 | xs | semmle.label | xs |
|
||||
| test.cpp:554:5:554:15 | access to array | semmle.label | access to array |
|
||||
| test.cpp:554:5:554:19 | Store: ... = ... | semmle.label | Store: ... = ... |
|
||||
subpaths
|
||||
#select
|
||||
| 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
|
||||
| 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 |
|
||||
| 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 |
|
||||
| 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 | ... - ... | ... - ... |
|
||||
| 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 |
|
||||
| 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 | ... ++ | ... ++ |
|
||||
| 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 |
|
||||
| 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 |
|
||||
| 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 |
|
||||
|
||||
@@ -416,7 +416,7 @@ void test30(int *size)
|
||||
new_size = tmp_size + 1;
|
||||
char *xs = new char[new_size];
|
||||
for (int i = 0; i < new_size; i++) {
|
||||
xs[i] = 0; // GOOD [FALSE POSITIVE]
|
||||
xs[i] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
*size = new_size;
|
||||
@@ -430,6 +430,127 @@ void test31(unsigned size, unsigned src_pos)
|
||||
}
|
||||
unsigned dst_pos = src_pos;
|
||||
if(dst_pos < size - 3) {
|
||||
xs[dst_pos++] = 0; // GOOD [FALSE POSITIVE]
|
||||
xs[dst_pos++] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple1(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos < size) {
|
||||
xs[src_pos] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple2(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos < size + 1) {
|
||||
xs[src_pos] = 0; // BAD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple3(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos - 1 < size) {
|
||||
xs[src_pos] = 0; // BAD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple4(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos < size - 1) {
|
||||
xs[src_pos] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple5(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos + 1 < size) {
|
||||
xs[src_pos] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple1_plus1(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size + 1];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos < size) {
|
||||
xs[src_pos] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple2_plus1(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size + 1];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos < size + 1) {
|
||||
xs[src_pos] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple3_plus1(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size + 1];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos - 1 < size) {
|
||||
xs[src_pos] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple4_plus1(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size + 1];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos < size - 1) {
|
||||
xs[src_pos] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple5_plus1(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size + 1];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos + 1 < size) {
|
||||
xs[src_pos] = 0; // GOOD
|
||||
}
|
||||
}
|
||||
|
||||
void test31_simple1_sub1(unsigned size, unsigned src_pos)
|
||||
{
|
||||
char *xs = new char[size - 1];
|
||||
if (src_pos > size) {
|
||||
src_pos = size;
|
||||
}
|
||||
if(src_pos < size) {
|
||||
xs[src_pos] = 0; // BAD
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user