Merge pull request #13116 from rdmarsh2/rdmarsh2/cpp/cobo-array-vars

C++: include stack-allocated arrays in off-by-one query
This commit is contained in:
Robert Marsh
2023-06-26 15:26:45 -04:00
committed by GitHub
3 changed files with 108 additions and 37 deletions

View File

@@ -14,7 +14,7 @@ import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysi
import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
import semmle.code.cpp.ir.IR
import semmle.code.cpp.ir.dataflow.DataFlow
import FieldAddressToDerefFlow::PathGraph
import ArrayAddressToDerefFlow::PathGraph
pragma[nomagic]
Instruction getABoundIn(SemBound b, IRFunction func) {
@@ -78,28 +78,45 @@ predicate isInvalidPointerDerefSink2(DataFlow::Node sink, Instruction i, string
)
}
predicate arrayTypeCand(ArrayType arrayType) {
any(Variable v).getUnspecifiedType() = arrayType and
exists(arrayType.getArraySize())
}
pragma[nomagic]
predicate arrayTypeHasSizes(ArrayType arr, int baseTypeSize, int arraySize) {
arrayTypeCand(arr) and
arr.getBaseType().getSize() = baseTypeSize and
arr.getArraySize() = arraySize
}
predicate pointerArithOverflow0(
PointerArithmeticInstruction pai, Field f, int size, int bound, int delta
) {
not f.getNamespace() instanceof StdNamespace and
arrayTypeHasSizes(f.getUnspecifiedType(), pai.getElementSize(), size) and
semBounded(getSemanticExpr(pai.getRight()), any(SemZeroBound b), bound, true, _) and
delta = bound - size and
delta >= 0 and
size != 0 and
size != 1
bindingset[pai]
pragma[inline_late]
predicate constantUpperBounded(PointerArithmeticInstruction pai, int delta) {
semBounded(getSemanticExpr(pai.getRight()), any(SemZeroBound b), delta, true, _)
}
bindingset[pai, size]
predicate pointerArithOverflow0Impl(PointerArithmeticInstruction pai, int size, int delta) {
exists(int bound |
constantUpperBounded(pai, bound) and
delta = bound - size and
delta >= 0 and
size != 0 and
size != 1
)
}
pragma[nomagic]
predicate pointerArithOverflow0(PointerArithmeticInstruction pai, int delta) {
exists(int size |
arrayTypeHasSizes(_, pai.getElementSize(), size) and
pointerArithOverflow0Impl(pai, size, delta)
)
}
module PointerArithmeticToDerefConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) {
pointerArithOverflow0(source.asInstruction(), _, _, _, _)
}
predicate isSource(DataFlow::Node source) { pointerArithOverflow0(source.asInstruction(), _) }
predicate isBarrierIn(DataFlow::Node node) { isSource(node) }
@@ -110,25 +127,38 @@ module PointerArithmeticToDerefConfig implements DataFlow::ConfigSig {
module PointerArithmeticToDerefFlow = DataFlow::Global<PointerArithmeticToDerefConfig>;
predicate pointerArithOverflow(
PointerArithmeticInstruction pai, Field f, int size, int bound, int delta
) {
pointerArithOverflow0(pai, f, size, bound, delta) and
predicate pointerArithOverflow(PointerArithmeticInstruction pai, int delta) {
pointerArithOverflow0(pai, delta) and
PointerArithmeticToDerefFlow::flow(DataFlow::instructionNode(pai), _)
}
module FieldAddressToDerefConfig implements DataFlow::StateConfigSig {
bindingset[v]
predicate finalPointerArithOverflow(Variable v, PointerArithmeticInstruction pai, int delta) {
exists(int size |
arrayTypeHasSizes(pragma[only_bind_out](v.getUnspecifiedType()), pai.getElementSize(), size) and
pointerArithOverflow0Impl(pai, size, delta)
)
}
predicate isSourceImpl(DataFlow::Node source, Variable v) {
(
source.asInstruction().(FieldAddressInstruction).getField() = v
or
source.asInstruction().(VariableAddressInstruction).getAstVariable() = v
) and
arrayTypeCand(v.getUnspecifiedType())
}
module ArrayAddressToDerefConfig implements DataFlow::StateConfigSig {
newtype FlowState =
additional TArray(Field f) { pointerArithOverflow(_, f, _, _, _) } or
additional TArray() or
additional TOverflowArithmetic(PointerArithmeticInstruction pai) {
pointerArithOverflow(pai, _, _, _, _)
pointerArithOverflow(pai, _)
}
predicate isSource(DataFlow::Node source, FlowState state) {
exists(Field f |
source.asInstruction().(FieldAddressInstruction).getField() = f and
state = TArray(f)
)
isSourceImpl(source, _) and
state = TArray()
}
predicate isSink(DataFlow::Node sink, FlowState state) {
@@ -147,27 +177,27 @@ module FieldAddressToDerefConfig implements DataFlow::StateConfigSig {
predicate isAdditionalFlowStep(
DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2
) {
exists(PointerArithmeticInstruction pai, Field f |
state1 = TArray(f) and
exists(PointerArithmeticInstruction pai |
state1 = TArray() and
state2 = TOverflowArithmetic(pai) and
pai.getLeft() = node1.asInstruction() and
node2.asInstruction() = pai and
pointerArithOverflow(pai, f, _, _, _)
pointerArithOverflow(pai, _)
)
}
}
module FieldAddressToDerefFlow = DataFlow::GlobalWithState<FieldAddressToDerefConfig>;
module ArrayAddressToDerefFlow = DataFlow::GlobalWithState<ArrayAddressToDerefConfig>;
from
Field f, FieldAddressToDerefFlow::PathNode source, PointerArithmeticInstruction pai,
FieldAddressToDerefFlow::PathNode sink, Instruction deref, string operation, int delta
Variable v, ArrayAddressToDerefFlow::PathNode source, PointerArithmeticInstruction pai,
ArrayAddressToDerefFlow::PathNode sink, Instruction deref, string operation, int delta
where
FieldAddressToDerefFlow::flowPath(source, sink) and
ArrayAddressToDerefFlow::flowPath(pragma[only_bind_into](source), pragma[only_bind_into](sink)) and
isInvalidPointerDerefSink2(sink.getNode(), deref, operation) and
source.getState() = FieldAddressToDerefConfig::TArray(f) and
sink.getState() = FieldAddressToDerefConfig::TOverflowArithmetic(pai) and
pointerArithOverflow(pai, f, _, _, delta)
pragma[only_bind_out](sink.getState()) = ArrayAddressToDerefConfig::TOverflowArithmetic(pai) and
isSourceImpl(source.getNode(), v) and
finalPointerArithOverflow(v, pai, delta)
select pai, source, sink,
"This pointer arithmetic may have an off-by-" + (delta + 1) +
" error allowing it to overrun $@ at this $@.", f, f.getName(), deref, operation
" error allowing it to overrun $@ at this $@.", v, v.getName(), deref, operation

View File

@@ -11,6 +11,13 @@ edges
| test.cpp:77:32:77:34 | buf | test.cpp:77:26:77:44 | & ... |
| test.cpp:79:27:79:34 | buf | test.cpp:70:33:70:33 | p |
| test.cpp:79:32:79:34 | buf | test.cpp:79:27:79:34 | buf |
| test.cpp:85:34:85:36 | buf | test.cpp:87:5:87:31 | access to array |
| test.cpp:85:34:85:36 | buf | test.cpp:88:5:88:27 | access to array |
| test.cpp:128:9:128:11 | arr | test.cpp:128:9:128:14 | access to array |
| test.cpp:134:25:134:27 | arr | test.cpp:136:9:136:16 | ... += ... |
| test.cpp:136:9:136:16 | ... += ... | test.cpp:138:13:138:15 | arr |
| test.cpp:143:18:143:21 | asdf | test.cpp:134:25:134:27 | arr |
| test.cpp:143:18:143:21 | asdf | test.cpp:143:18:143:21 | asdf |
nodes
| test.cpp:35:5:35:22 | access to array | semmle.label | access to array |
| test.cpp:35:10:35:12 | buf | semmle.label | buf |
@@ -33,6 +40,16 @@ nodes
| test.cpp:77:32:77:34 | buf | semmle.label | buf |
| test.cpp:79:27:79:34 | buf | semmle.label | buf |
| test.cpp:79:32:79:34 | buf | semmle.label | buf |
| test.cpp:85:34:85:36 | buf | semmle.label | buf |
| test.cpp:87:5:87:31 | access to array | semmle.label | access to array |
| test.cpp:88:5:88:27 | access to array | semmle.label | access to array |
| test.cpp:128:9:128:11 | arr | semmle.label | arr |
| test.cpp:128:9:128:14 | access to array | semmle.label | access to array |
| test.cpp:134:25:134:27 | arr | semmle.label | arr |
| test.cpp:136:9:136:16 | ... += ... | semmle.label | ... += ... |
| test.cpp:138:13:138:15 | arr | semmle.label | arr |
| test.cpp:143:18:143:21 | asdf | semmle.label | asdf |
| test.cpp:143:18:143:21 | asdf | semmle.label | asdf |
subpaths
#select
| test.cpp:35:5:35:22 | PointerAdd: access to array | test.cpp:35:10:35:12 | buf | test.cpp:35:5:35:22 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:35:5:35:26 | Store: ... = ... | write |
@@ -44,3 +61,5 @@ subpaths
| test.cpp:61:9:61:19 | PointerAdd: access to array | test.cpp:61:14:61:16 | buf | test.cpp:61:9:61:19 | access to array | This pointer arithmetic may have an off-by-2 error allowing it to overrun $@ at this $@. | test.cpp:19:9:19:11 | buf | buf | test.cpp:61:9:61:23 | Store: ... = ... | write |
| test.cpp:72:5:72:15 | PointerAdd: access to array | test.cpp:79:32:79:34 | buf | test.cpp:72:5:72:15 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:72:5:72:19 | Store: ... = ... | write |
| test.cpp:77:27:77:44 | PointerAdd: access to array | test.cpp:77:32:77:34 | buf | test.cpp:66:32:66:32 | p | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:67:5:67:10 | Store: ... = ... | write |
| test.cpp:128:9:128:14 | PointerAdd: access to array | test.cpp:128:9:128:11 | arr | test.cpp:128:9:128:14 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:125:11:125:13 | arr | arr | test.cpp:128:9:128:18 | Store: ... = ... | write |
| test.cpp:136:9:136:16 | PointerAdd: ... += ... | test.cpp:143:18:143:21 | asdf | test.cpp:138:13:138:15 | arr | This pointer arithmetic may have an off-by-2 error allowing it to overrun $@ at this $@. | test.cpp:142:10:142:13 | asdf | asdf | test.cpp:138:12:138:15 | Load: * ... | read |

View File

@@ -85,7 +85,7 @@ void testCharIndex(BigArray *arr) {
char *charBuf = (char*) arr->buf;
charBuf[MAX_SIZE_BYTES - 1] = 0; // GOOD
charBuf[MAX_SIZE_BYTES] = 0; // BAD [FALSE NEGATIVE]
charBuf[MAX_SIZE_BYTES] = 0; // BAD
}
void testEqRefinement() {
@@ -120,3 +120,25 @@ void testEqRefinement2() {
}
}
}
void testStackAllocated() {
char *arr[MAX_SIZE];
for(int i = 0; i <= MAX_SIZE; i++) {
arr[i] = 0; // BAD
}
}
int strncmp(const char*, const char*, int);
char testStrncmp2(char *arr) {
if(strncmp(arr, "<test>", 6) == 0) {
arr += 6;
}
return *arr; // GOOD [FALSE POSITIVE]
}
void testStrncmp1() {
char asdf[5];
testStrncmp2(asdf);
}