Merge pull request #10609 from MathiasVP/overrun-write-only-flag-overrunning-write

Robert Marsh · web-flow · commit 9b03e1c0b1b7 · 2022-09-29T10:03:05.000-04:00
C++: Make `OverrunWriteProductFlow` raise alerts on overflows
diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll b/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll
@@ -20,7 +20,8 @@ module ProductFlow {
      * `source1` and `source2` must belong to the same callable.
      */
     predicate isSourcePair(
-      DataFlow::Node source1, string state1, DataFlow::Node source2, string state2
+      DataFlow::Node source1, DataFlow::FlowState state1, DataFlow::Node source2,
+      DataFlow::FlowState state2
     ) {
       state1 = "" and
       state2 = "" and
@@ -89,6 +90,49 @@ module ProductFlow {
      */
     predicate isBarrierOut2(DataFlow::Node node) { none() }
 
+    /*
+     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
+     * the first projection of the product dataflow graph.
+     */
+
+    predicate isAdditionalFlowStep1(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+    /**
+     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
+     * the first projection of the product dataflow graph.
+     *
+     * This step is only applicable in `state1` and updates the flow state to `state2`.
+     */
+    predicate isAdditionalFlowStep1(
+      DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+      DataFlow::FlowState state2
+    ) {
+      state1 instanceof DataFlow::FlowStateEmpty and
+      state2 instanceof DataFlow::FlowStateEmpty and
+      this.isAdditionalFlowStep1(node1, node2)
+    }
+
+    /**
+     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
+     * the second projection of the product dataflow graph.
+     */
+    predicate isAdditionalFlowStep2(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+    /**
+     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
+     * the second projection of the product dataflow graph.
+     *
+     * This step is only applicable in `state1` and updates the flow state to `state2`.
+     */
+    predicate isAdditionalFlowStep2(
+      DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+      DataFlow::FlowState state2
+    ) {
+      state1 instanceof DataFlow::FlowStateEmpty and
+      state2 instanceof DataFlow::FlowStateEmpty and
+      this.isAdditionalFlowStep2(node1, node2)
+    }
+
     predicate hasFlowPath(
       DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode sink1,
       DataFlow2::PathNode sink2
@@ -103,54 +147,69 @@ module ProductFlow {
     class Conf1 extends DataFlow::Configuration {
       Conf1() { this = "Conf1" }
 
-      override predicate isSource(DataFlow::Node source, string state) {
+      override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) {
         exists(Configuration conf | conf.isSourcePair(source, state, _, _))
       }
 
-      override predicate isSink(DataFlow::Node sink, string state) {
+      override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) {
         exists(Configuration conf | conf.isSinkPair(sink, state, _, _))
       }
 
-      override predicate isBarrier(DataFlow::Node node, string state) {
+      override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
         exists(Configuration conf | conf.isBarrier1(node, state))
       }
 
       override predicate isBarrierOut(DataFlow::Node node) {
         exists(Configuration conf | conf.isBarrierOut1(node))
       }
+
+      override predicate isAdditionalFlowStep(
+        DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+        DataFlow::FlowState state2
+      ) {
+        exists(Configuration conf | conf.isAdditionalFlowStep1(node1, state1, node2, state2))
+      }
     }
 
     class Conf2 extends DataFlow2::Configuration {
       Conf2() { this = "Conf2" }
 
-      override predicate isSource(DataFlow::Node source, string state) {
-        exists(Configuration conf, DataFlow::Node source1 |
-          conf.isSourcePair(source1, _, source, state) and
-          any(Conf1 c).hasFlow(source1, _)
+      override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) {
+        exists(Configuration conf, DataFlow::PathNode source1 |
+          conf.isSourcePair(source1.getNode(), source1.getState(), source, state) and
+          any(Conf1 c).hasFlowPath(source1, _)
         )
       }
 
-      override predicate isSink(DataFlow::Node sink, string state) {
-        exists(Configuration conf, DataFlow::Node sink1 |
-          conf.isSinkPair(sink1, _, sink, state) and any(Conf1 c).hasFlow(_, sink1)
+      override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) {
+        exists(Configuration conf, DataFlow::PathNode sink1 |
+          conf.isSinkPair(sink1.getNode(), sink1.getState(), sink, state) and
+          any(Conf1 c).hasFlowPath(_, sink1)
         )
       }
 
-      override predicate isBarrier(DataFlow::Node node, string state) {
+      override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
         exists(Configuration conf | conf.isBarrier2(node, state))
       }
 
       override predicate isBarrierOut(DataFlow::Node node) {
         exists(Configuration conf | conf.isBarrierOut2(node))
       }
+
+      override predicate isAdditionalFlowStep(
+        DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+        DataFlow::FlowState state2
+      ) {
+        exists(Configuration conf | conf.isAdditionalFlowStep2(node1, state1, node2, state2))
+      }
     }
   }
 
   private predicate reachableInterprocEntry(
     Configuration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
     DataFlow::PathNode node1, DataFlow2::PathNode node2
   ) {
-    conf.isSourcePair(node1.getNode(), _, node2.getNode(), _) and
+    conf.isSourcePair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState()) and
     node1 = source1 and
     node2 = source2
     or
@@ -213,7 +272,7 @@ module ProductFlow {
   ) {
     exists(DataFlow::PathNode mid1, DataFlow2::PathNode mid2 |
       reachableInterprocEntry(conf, source1, source2, mid1, mid2) and
-      conf.isSinkPair(sink1.getNode(), _, sink2.getNode(), _) and
+      conf.isSinkPair(sink1.getNode(), sink1.getState(), sink2.getNode(), sink2.getState()) and
       localPathStep1*(mid1, sink1) and
       localPathStep2*(mid2, sink2)
     )
diff --git a/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.cpp b/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.cpp
@@ -0,0 +1,9 @@
+int f(char * s, unsigned size) {
+	char* buf = (char*)malloc(size);
+
+	strncpy(buf, s, size + 1); // wrong: copy may exceed size of buf
+
+	for (int i = 0; i <= size; i++) { // wrong: upper limit that is higher than size of buf
+		cout << buf[i];
+	}
+}
diff --git a/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.qhelp b/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.qhelp
@@ -0,0 +1,29 @@
+<!DOCTYPE qhelp PUBLIC
+  "-//Semmle//qhelp//EN"
+  "qhelp.dtd">
+<qhelp>
+<overview>
+<p>You must ensure that you do not exceed the size of an allocation during write and read operations.
+If an operation attempts to write to or access an element that is outside the range of the allocation then this results in a buffer overflow.
+Buffer overflows can lead to anything from a segmentation fault to a security vulnerability.
+</p>
+
+</overview>
+<recommendation>
+<p>
+Check the offsets and sizes used in the highlighted operations to ensure that a buffer overflow will not occur.
+</p>
+
+</recommendation>
+<example><sample src="OverrunWriteProductFlow.cpp" />
+
+
+
+</example>
+<references>
+
+<li>I. Gerg. <em>An Overview and Example of the Buffer-Overflow Exploit</em>. IANewsletter vol 7 no 4. 2005.</li>
+<li>M. Donaldson. <em>Inside the Buffer Overflow Attack: Mechanism, Method &amp; Prevention</em>. SANS Institute InfoSec Reading Room. 2002.</li>
+
+</references>
+</qhelp>
diff --git a/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql b/cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql
@@ -1,42 +1,131 @@
 /**
  * @name Overrunning write
- * @description TODO
+ * @description Exceeding the size of a static array during write or access operations
+ *              may result in a buffer overflow.
  * @kind path-problem
  * @problem.severity error
  * @id cpp/overrun-write
  * @tags reliability
  *       security
+ *       external/cwe/cwe-119
+ *       external/cwe/cwe-131
  */
 
 import cpp
 import experimental.semmle.code.cpp.dataflow.ProductFlow
 import semmle.code.cpp.ir.IR
-import semmle.code.cpp.valuenumbering.GlobalValueNumbering
 import semmle.code.cpp.models.interfaces.Allocation
 import semmle.code.cpp.models.interfaces.ArrayFunction
+import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
+import experimental.semmle.code.cpp.semantic.SemanticBound
+import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
 import DataFlow::PathGraph
 
+pragma[nomagic]
+Instruction getABoundIn(SemBound b, IRFunction func) {
+  result = b.getExpr(0) and
+  result.getEnclosingIRFunction() = func
+}
+
+/**
+ * Holds if `i <= b + delta`.
+ */
+pragma[nomagic]
+predicate bounded(Instruction i, Instruction b, int delta) {
+  exists(SemBound bound, IRFunction func |
+    semBounded(getSemanticExpr(i), bound, delta, true, _) and
+    b = getABoundIn(bound, func) and
+    i.getEnclosingIRFunction() = func
+  )
+}
+
+VariableAccess getAVariableAccess(Expr e) { e.getAChild*() = result }
+
+/**
+ * Holds if `(n, state)` pair represents the source of flow for the size
+ * expression associated with `alloc`.
+ */
+predicate hasSize(AllocationExpr alloc, DataFlow::Node n, string state) {
+  exists(VariableAccess va, Expr size, int delta |
+    size = alloc.getSizeExpr() and
+    // Get the unique variable in a size expression like `x` in `malloc(x + 1)`.
+    va = unique( | | getAVariableAccess(size)) and
+    // Compute `delta` as the constant difference between `x` and `x + 1`.
+    bounded(any(Instruction instr | instr.getUnconvertedResultExpression() = size),
+      any(LoadInstruction load | load.getUnconvertedResultExpression() = va), delta) and
+    n.asConvertedExpr() = va.getFullyConverted() and
+    state = delta.toString()
+  )
+}
+
+predicate isSinkPairImpl(
+  CallInstruction c, DataFlow::Node bufSink, DataFlow::Node sizeSink, int delta, Expr eBuf
+) {
+  exists(int bufIndex, int sizeIndex, Instruction sizeInstr, Instruction bufInstr |
+    bufInstr = bufSink.asInstruction() and
+    c.getArgument(bufIndex) = bufInstr and
+    sizeInstr = sizeSink.asInstruction() and
+    c.getStaticCallTarget().(ArrayFunction).hasArrayWithVariableSize(bufIndex, sizeIndex) and
+    bounded(c.getArgument(sizeIndex), sizeInstr, delta) and
+    eBuf = bufInstr.getUnconvertedResultExpression()
+  )
+}
+
 class StringSizeConfiguration extends ProductFlow::Configuration {
   StringSizeConfiguration() { this = "StringSizeConfiguration" }
 
-  override predicate isSourcePair(DataFlow::Node bufSource, DataFlow::Node sizeSource) {
-    bufSource.asConvertedExpr().(AllocationExpr).getSizeExpr() = sizeSource.asConvertedExpr()
+  override predicate isSourcePair(
+    DataFlow::Node bufSource, DataFlow::FlowState state1, DataFlow::Node sizeSource,
+    DataFlow::FlowState state2
+  ) {
+    // In the case of an allocation like
+    // ```cpp
+    // malloc(size + 1);
+    // ```
+    // we use `state2` to remember that there was an offset (in this case an offset of `1`) added
+    // to the size of the allocation. This state is then checked in `isSinkPair`.
+    state1 instanceof DataFlow::FlowStateEmpty and
+    hasSize(bufSource.asConvertedExpr(), sizeSource, state2)
+  }
+
+  override predicate isSinkPair(
+    DataFlow::Node bufSink, DataFlow::FlowState state1, DataFlow::Node sizeSink,
+    DataFlow::FlowState state2
+  ) {
+    state1 instanceof DataFlow::FlowStateEmpty and
+    state2 = [-32 .. 32].toString() and // An arbitrary bound because we need to bound `state2`
+    exists(int delta |
+      isSinkPairImpl(_, bufSink, sizeSink, delta, _) and
+      delta > state2.toInt()
+    )
   }
 
-  override predicate isSinkPair(DataFlow::Node bufSink, DataFlow::Node sizeSink) {
-    exists(CallInstruction c, int bufIndex, int sizeIndex |
-      c.getStaticCallTarget().(ArrayFunction).hasArrayWithVariableSize(bufIndex, sizeIndex) and
-      c.getArgument(bufIndex) = bufSink.asInstruction() and
-      c.getArgument(sizeIndex) = sizeSink.asInstruction()
+  override predicate isAdditionalFlowStep2(
+    DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+    DataFlow::FlowState state2
+  ) {
+    exists(AddInstruction add, Operand op, int delta, int s1, int s2 |
+      s1 = [-32 .. 32] and // An arbitrary bound because we need to bound `state`
+      state1 = s1.toString() and
+      state2 = s2.toString() and
+      add.hasOperands(node1.asOperand(), op) and
+      semBounded(op.getDef(), any(SemZeroBound zero), delta, true, _) and
+      node2.asInstruction() = add and
+      s1 = s2 + delta
     )
   }
 }
 
-// we don't actually check correctness yet. Right now the query just finds relevant source/sink pairs.
 from
   StringSizeConfiguration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
-  DataFlow::PathNode sink1, DataFlow2::PathNode sink2
-where conf.hasFlowPath(source1, source2, sink1, sink2)
-// TODO: pull delta out and display it
-select sink1.getNode(), source1, sink1, "Overrunning write allocated at $@ bounded by $@.", source1,
-  source1.toString(), sink2, sink2.toString()
+  DataFlow::PathNode sink1, DataFlow2::PathNode sink2, int overflow, int sinkState,
+  CallInstruction c, DataFlow::Node sourceNode, Expr buffer, string element
+where
+  conf.hasFlowPath(source1, source2, sink1, sink2) and
+  sinkState = sink2.getState().toInt() and
+  isSinkPairImpl(c, sink1.getNode(), sink2.getNode(), overflow + sinkState, buffer) and
+  overflow > 0 and
+  sourceNode = source1.getNode() and
+  if overflow = 1 then element = " element." else element = " elements."
+select c.getUnconvertedResultExpression(), source1, sink1,
+  "This write may overflow $@ by " + overflow + element, buffer, buffer.toString()
diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/OverrunWriteProductFlow.expected b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/OverrunWriteProductFlow.expected
diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/test.cpp b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-119/test.cpp
