C++: stitch paths and ignore cast arrays in constant off-by-one query

cpp/ql/src/experimental/Security/CWE/CWE-193/ConstantSizeArrayOffByOne.ql

@@ -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 PointerArithmeticToDerefFlow::PathGraph
+import FieldAddressToDerefFlow::PathGraph
 
 pragma[nomagic]
 Instruction getABoundIn(SemBound b, IRFunction func) {
@@ -42,21 +42,6 @@ bindingset[b]
 pragma[inline_late]
 predicate bounded2(Instruction i, Instruction b, int delta) { boundedImpl(i, b, delta) }
 
-module FieldAddressToPointerArithmeticConfig implements DataFlow::ConfigSig {
-  predicate isSource(DataFlow::Node source) { isFieldAddressSource(_, source) }
-
-  predicate isSink(DataFlow::Node sink) {
-    exists(PointerAddInstruction pai | pai.getLeft() = sink.asInstruction())
-  }
-}
-
-module FieldAddressToPointerArithmeticFlow =
-  DataFlow::Global<FieldAddressToPointerArithmeticConfig>;
-
-predicate isFieldAddressSource(Field f, DataFlow::Node source) {
-  source.asInstruction().(FieldAddressInstruction).getField() = f
-}
-
 bindingset[delta]
 predicate isInvalidPointerDerefSinkImpl(
   int delta, Instruction i, AddressOperand addr, string operation
@@ -93,38 +78,90 @@ predicate isInvalidPointerDerefSink2(DataFlow::Node sink, Instruction i, string
   )
 }
 
-predicate isConstantSizeOverflowSource(Field f, PointerAddInstruction pai, int delta) {
-  exists(int size, int bound, DataFlow::Node source, DataFlow::InstructionNode sink |
-    FieldAddressToPointerArithmeticFlow::flow(source, sink) and
-    isFieldAddressSource(f, source) and
-    pai.getLeft() = sink.asInstruction() and
-    f.getUnspecifiedType().(ArrayType).getArraySize() = size and
-    semBounded(getSemanticExpr(pai.getRight()), any(SemZeroBound b), bound, true, _) and
-    delta = bound - size and
-    delta >= 0 and
-    size != 0 and
-    size != 1
-  )
+predicate pointerArithOverflow0(
+  PointerArithmeticInstruction pai, Field f, int size, int bound, int delta
+) {
+  pai.getElementSize() = f.getUnspecifiedType().(ArrayType).getBaseType().getSize() and
+  f.getUnspecifiedType().(ArrayType).getArraySize() = size and
+  semBounded(getSemanticExpr(pai.getRight()), any(SemZeroBound b), bound, true, _) and
+  delta = bound - size and
+  delta >= 0 and
+  size != 0 and
+  size != 1
 }
 
 module PointerArithmeticToDerefConfig implements DataFlow::ConfigSig {
   predicate isSource(DataFlow::Node source) {
-    isConstantSizeOverflowSource(_, source.asInstruction(), _)
+    pointerArithOverflow0(source.asInstruction(), _, _, _, _)
   }
 
-  pragma[inline]
+  predicate isBarrierIn(DataFlow::Node node) { isSource(node) }
+
+  predicate isBarrierOut(DataFlow::Node node) { isSink(node) }
+
   predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink1(sink, _, _) }
 }
 
 module PointerArithmeticToDerefFlow = DataFlow::Global<PointerArithmeticToDerefConfig>;
 
+predicate pointerArithOverflow(
+  PointerArithmeticInstruction pai, Field f, int size, int bound, int delta
+) {
+  pointerArithOverflow0(pai, f, size, bound, delta) and
+  PointerArithmeticToDerefFlow::flow(DataFlow::instructionNode(pai), _)
+}
+
+module FieldAddressToDerefConfig implements DataFlow::StateConfigSig {
+  newtype FlowState =
+    additional TArray(Field f) { pointerArithOverflow(_, f, _, _, _) } or
+    additional TOverflowArithmetic(PointerArithmeticInstruction pai) {
+      pointerArithOverflow(pai, _, _, _, _)
+    }
+
+  predicate isSource(DataFlow::Node source, FlowState state) {
+    exists(Field f |
+      source.asInstruction().(FieldAddressInstruction).getField() = f and
+      state = TArray(f)
+    )
+  }
+
+  predicate isSink(DataFlow::Node sink, FlowState state) {
+    exists(DataFlow::Node pai |
+      state = TOverflowArithmetic(pai.asInstruction()) and
+      PointerArithmeticToDerefFlow::flow(pai, sink)
+    )
+  }
+
+  predicate isBarrier(DataFlow::Node node, FlowState state) { none() }
+
+  predicate isBarrierIn(DataFlow::Node node) { isSource(node, _) }
+
+  predicate isBarrierOut(DataFlow::Node node) { isSink(node, _) }
+
+  predicate isAdditionalFlowStep(
+    DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2
+  ) {
+    exists(PointerArithmeticInstruction pai, Field f |
+      state1 = TArray(f) and
+      state2 = TOverflowArithmetic(pai) and
+      pai.getLeft() = node1.asInstruction() and
+      node2.asInstruction() = pai and
+      pointerArithOverflow(pai, f, _, _, _)
+    )
+  }
+}
+
+module FieldAddressToDerefFlow = DataFlow::GlobalWithState<FieldAddressToDerefConfig>;
+
 from
-  Field f, PointerArithmeticToDerefFlow::PathNode source,
-  PointerArithmeticToDerefFlow::PathNode sink, Instruction deref, string operation, int delta
+  Field f, FieldAddressToDerefFlow::PathNode source, PointerArithmeticInstruction pai,
+  FieldAddressToDerefFlow::PathNode sink, Instruction deref, string operation, int delta
 where
-  PointerArithmeticToDerefFlow::flowPath(source, sink) and
+  FieldAddressToDerefFlow::flowPath(source, sink) and
   isInvalidPointerDerefSink2(sink.getNode(), deref, operation) and
-  isConstantSizeOverflowSource(f, source.getNode().asInstruction(), delta)
-select source, source, sink,
+  source.getState() = FieldAddressToDerefConfig::TArray(f) and
+  sink.getState() = FieldAddressToDerefConfig::TOverflowArithmetic(pai) and
+  pointerArithOverflow(pai, f, _, _, 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

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected

@@ -1,37 +1,46 @@
 edges
-| test.cpp:66:32:66:32 | p | test.cpp:66:32:66:32 | p |
-| test.cpp:66:32:66:32 | p | test.cpp:67:5:67:6 | * ... |
-| test.cpp:66:32:66:32 | p | test.cpp:67:6:67:6 | p |
+| test.cpp:35:10:35:12 | buf | test.cpp:35:5:35:22 | access to array |
+| test.cpp:36:10:36:12 | buf | test.cpp:36:5:36:24 | access to array |
+| test.cpp:43:14:43:16 | buf | test.cpp:43:9:43:19 | access to array |
+| test.cpp:49:10:49:12 | buf | test.cpp:49:5:49:22 | access to array |
+| test.cpp:50:10:50:12 | buf | test.cpp:50:5:50:24 | access to array |
+| test.cpp:57:14:57:16 | buf | test.cpp:57:9:57:19 | access to array |
+| test.cpp:61:14:61:16 | buf | test.cpp:61:9:61:19 | access to array |
+| test.cpp:70:33:70:33 | p | test.cpp:72:5:72:15 | access to array |
 | test.cpp:77:26:77:44 | & ... | test.cpp:66:32:66:32 | p |
-| test.cpp:77:26:77:44 | & ... | test.cpp:66:32:66:32 | p |
-| test.cpp:77:27:77:44 | access to array | test.cpp:77:26:77:44 | & ... |
+| 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 |
 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 |
 | test.cpp:36:5:36:24 | access to array | semmle.label | access to array |
+| test.cpp:36:10:36:12 | buf | semmle.label | buf |
 | test.cpp:43:9:43:19 | access to array | semmle.label | access to array |
+| test.cpp:43:14:43:16 | buf | semmle.label | buf |
 | test.cpp:49:5:49:22 | access to array | semmle.label | access to array |
+| test.cpp:49:10:49:12 | buf | semmle.label | buf |
 | test.cpp:50:5:50:24 | access to array | semmle.label | access to array |
+| test.cpp:50:10:50:12 | buf | semmle.label | buf |
 | test.cpp:57:9:57:19 | access to array | semmle.label | access to array |
+| test.cpp:57:14:57:16 | buf | semmle.label | buf |
 | test.cpp:61:9:61:19 | access to array | semmle.label | access to array |
+| test.cpp:61:14:61:16 | buf | semmle.label | buf |
 | test.cpp:66:32:66:32 | p | semmle.label | p |
-| test.cpp:66:32:66:32 | p | semmle.label | p |
-| test.cpp:66:32:66:32 | p | semmle.label | p |
-| test.cpp:67:5:67:6 | * ... | semmle.label | * ... |
-| test.cpp:67:6:67:6 | p | semmle.label | p |
+| test.cpp:70:33:70:33 | p | semmle.label | p |
 | test.cpp:72:5:72:15 | access to array | semmle.label | access to array |
 | test.cpp:77:26:77:44 | & ... | semmle.label | & ... |
-| test.cpp:77:27:77:44 | access to array | semmle.label | access to array |
+| 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 |
 subpaths
 #select
-| test.cpp:35:5:35:22 | access to array | test.cpp:35:5:35:22 | access to array | 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 |
-| test.cpp:36:5:36:24 | access to array | test.cpp:36:5:36:24 | access to array | test.cpp:36:5:36:24 | access to array | This pointer arithmetic may have an off-by-2 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:36:5:36:28 | Store: ... = ... | write |
-| test.cpp:43:9:43:19 | access to array | test.cpp:43:9:43:19 | access to array | test.cpp:43:9:43:19 | 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:43:9:43:23 | Store: ... = ... | write |
-| test.cpp:49:5:49:22 | access to array | test.cpp:49:5:49:22 | access to array | test.cpp:49:5:49:22 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:19:9:19:11 | buf | buf | test.cpp:49:5:49:26 | Store: ... = ... | write |
-| test.cpp:50:5:50:24 | access to array | test.cpp:50:5:50:24 | access to array | test.cpp:50:5:50:24 | 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:50:5:50:28 | Store: ... = ... | write |
-| test.cpp:57:9:57:19 | access to array | test.cpp:57:9:57:19 | access to array | test.cpp:57:9:57:19 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:19:9:19:11 | buf | buf | test.cpp:57:9:57:23 | Store: ... = ... | write |
-| test.cpp:61:9:61:19 | access to array | test.cpp:61:9:61:19 | access to array | 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 | access to array | test.cpp:72:5:72:15 | access to array | 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 | access to array | test.cpp:77:27:77:44 | access to array | 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:77:27:77:44 | access to array | test.cpp:77:27:77:44 | access to array | 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:77:27:77:44 | access to array | test.cpp:77:27:77:44 | access to array | test.cpp:67:5:67:6 | * ... | 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:77:27:77:44 | access to array | test.cpp:77:27:77:44 | access to array | test.cpp:67:6:67:6 | 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: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 |
+| test.cpp:36:5:36:24 | PointerAdd: access to array | test.cpp:36:10:36:12 | buf | test.cpp:36:5:36:24 | access to array | This pointer arithmetic may have an off-by-2 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:36:5:36:28 | Store: ... = ... | write |
+| test.cpp:43:9:43:19 | PointerAdd: access to array | test.cpp:43:14:43:16 | buf | test.cpp:43:9:43:19 | 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:43:9:43:23 | Store: ... = ... | write |
+| test.cpp:49:5:49:22 | PointerAdd: access to array | test.cpp:49:10:49:12 | buf | test.cpp:49:5:49:22 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:19:9:19:11 | buf | buf | test.cpp:49:5:49:26 | Store: ... = ... | write |
+| test.cpp:50:5:50:24 | PointerAdd: access to array | test.cpp:50:10:50:12 | buf | test.cpp:50:5:50:24 | 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:50:5:50:28 | Store: ... = ... | write |
+| test.cpp:57:9:57:19 | PointerAdd: access to array | test.cpp:57:14:57:16 | buf | test.cpp:57:9:57:19 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:19:9:19:11 | buf | buf | test.cpp:57:9:57:23 | Store: ... = ... | write |
+| 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 |

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp

@@ -79,6 +79,15 @@ void testInterproc(BigArray *arr) {
     addToPointerAndAssign(arr->buf);
 }
 
+#define MAX_SIZE_BYTES 4096
+
+void testCharIndex(BigArray *arr) {
+    char *charBuf = (char*) arr->buf;
+
+    charBuf[MAX_SIZE_BYTES - 1] = 0; // GOOD
+    charBuf[MAX_SIZE_BYTES] = 0; // BAD [FALSE NEGATIVE]
+}
+
 void testEqRefinement() {
     int arr[MAX_SIZE];