|
4 | 4 | */
|
5 | 5 |
|
6 | 6 | import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
|
7 |
| -import experimental.semmle.code.cpp.rangeanalysis.Bound |
| 7 | +import experimental.semmle.code.cpp.semantic.SemanticBound |
8 | 8 | import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
|
9 | 9 | import semmle.code.cpp.ir.IR
|
10 | 10 | import experimental.semmle.code.cpp.ir.dataflow.DataFlow
|
| 11 | +import experimental.semmle.code.cpp.ir.dataflow.DataFlow2 |
| 12 | + |
| 13 | +pragma[nomagic] |
| 14 | +Instruction getABoundIn(SemBound b, IRFunction func) { |
| 15 | + result = b.getExpr(0) and |
| 16 | + result.getEnclosingIRFunction() = func |
| 17 | +} |
| 18 | + |
| 19 | +/** |
| 20 | + * Holds if `i <= b + delta`. |
| 21 | + */ |
| 22 | +pragma[nomagic] |
| 23 | +predicate bounded(Instruction i, Instruction b, int delta) { |
| 24 | + exists(SemBound bound, IRFunction func | |
| 25 | + semBounded(getSemanticExpr(i), bound, delta, true, _) and |
| 26 | + b = getABoundIn(bound, func) and |
| 27 | + i.getEnclosingIRFunction() = func |
| 28 | + ) |
| 29 | +} |
| 30 | + |
| 31 | +class FieldAddressToPointerArithmeticConf extends DataFlow::Configuration { |
| 32 | + FieldAddressToPointerArithmeticConf() { this = "FieldAddressToPointerArithmeticConf" } |
| 33 | + |
| 34 | + override predicate isSource(DataFlow::Node source) { isFieldAddressSource(_, source) } |
| 35 | + |
| 36 | + override predicate isSink(DataFlow::Node sink) { |
| 37 | + exists(PointerAddInstruction pai | pai.getLeft() = sink.asInstruction()) |
| 38 | + } |
| 39 | +} |
| 40 | + |
| 41 | +predicate isFieldAddressSource(Field f, DataFlow::Node source) { |
| 42 | + source.asInstruction().(FieldAddressInstruction).getField() = f |
| 43 | +} |
| 44 | + |
| 45 | +/** |
| 46 | + * Holds if `sink` is a sink for `InvalidPointerToDerefConf` and `i` is a `StoreInstruction` that |
| 47 | + * writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that |
| 48 | + * reads from an address that non-strictly upper-bounds `sink`. |
| 49 | + */ |
| 50 | +predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string operation) { |
| 51 | + exists(AddressOperand addr, int delta | |
| 52 | + bounded(addr.getDef(), sink.asInstruction(), delta) and |
| 53 | + delta >= 0 and |
| 54 | + i.getAnOperand() = addr |
| 55 | + | |
| 56 | + i instanceof StoreInstruction and |
| 57 | + operation = "write" |
| 58 | + or |
| 59 | + i instanceof LoadInstruction and |
| 60 | + operation = "read" |
| 61 | + ) |
| 62 | +} |
| 63 | + |
| 64 | +predicate isConstantSizeOverflowSource(Field f, PointerAddInstruction pai, int delta) { |
| 65 | + exists( |
| 66 | + int size, int bound, SemZeroBound b, FieldAddressToPointerArithmeticConf conf, |
| 67 | + DataFlow::Node source, DataFlow::InstructionNode sink |
| 68 | + | |
| 69 | + conf.hasFlow(source, sink) and |
| 70 | + isFieldAddressSource(f, source) and |
| 71 | + pai.getLeft() = sink.asInstruction() and |
| 72 | + f.getUnspecifiedType().(ArrayType).getArraySize() = size and |
| 73 | + semBounded(getSemanticExpr(pai.getRight()), b, bound, true, _) and |
| 74 | + delta = bound - size and |
| 75 | + delta >= 0 and |
| 76 | + size != 0 and |
| 77 | + size != 1 |
| 78 | + ) |
| 79 | +} |
| 80 | + |
| 81 | +class PointerArithmeticToDerefConf extends DataFlow2::Configuration { |
| 82 | + PointerArithmeticToDerefConf() { this = "PointerArithmeticToDerefConf" } |
| 83 | + |
| 84 | + override predicate isSource(DataFlow::Node source) { |
| 85 | + isConstantSizeOverflowSource(_, source.asInstruction(), _) |
| 86 | + } |
| 87 | + |
| 88 | + override predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _) } |
| 89 | +} |
11 | 90 |
|
12 | 91 | from
|
13 |
| - FieldAddressInstruction fai, PointerArithmeticInstruction pai, AddressOperand ao, ZeroBound b, |
14 |
| - int delta, int size |
| 92 | + Field f, DataFlow::Node source, DataFlow::Node sink, |
| 93 | + Instruction deref, |
| 94 | + PointerArithmeticToDerefConf conf, string operation, int delta |
15 | 95 | where
|
16 |
| - size = fai.getField().getUnspecifiedType().(ArrayType).getArraySize() and |
17 |
| - DataFlow::localInstructionFlow(fai, pai.getLeft()) and |
18 |
| - DataFlow::localInstructionFlow(pai, ao.getAnyDef()) and |
19 |
| - semBounded(getSemanticExpr(pai.getRight()), b, delta, true, _) and |
20 |
| - delta >= size and |
21 |
| - size != 0 and // sometimes 0 or 1 is used for a variable-size array |
22 |
| - size != 1 |
23 |
| -select pai, "This pointer may have an off-by-" + (delta - size + 1) + " error allowing it to overrun $@", |
24 |
| - fai.getField(), fai.getField().toString() |
| 96 | + conf.hasFlow(source, sink) and |
| 97 | + isInvalidPointerDerefSink(sink, deref, operation) and |
| 98 | + isConstantSizeOverflowSource(f, source.asInstruction(), delta) |
| 99 | +select source, |
| 100 | + "This pointer arithmetic may have an off-by-" + (delta + 1) + " error allowing it to overrun $@ at this $@", |
| 101 | + f, f.getName(), deref, operation |
0 commit comments