Merge pull request github#13563 from jketema/clears-content

C++: Implement `clearsContent` for IR dataflow

Author: jketema

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll

@@ -651,13 +651,16 @@ predicate jumpStep(Node n1, Node n2) {
  * Holds if data can flow from `node1` to `node2` via an assignment to `f`.
  * Thus, `node2` references an object with a field `f` that contains the
  * value of `node1`.
+ *
+ * The boolean `certain` is true if the destination address does not involve
+ * any pointer arithmetic, and false otherwise.
  */
-predicate storeStep(Node node1, Content c, PostFieldUpdateNode node2) {
+predicate storeStepImpl(Node node1, Content c, PostFieldUpdateNode node2, boolean certain) {
   exists(int indirectionIndex1, int numberOfLoads, StoreInstruction store |
     nodeHasInstruction(node1, store, pragma[only_bind_into](indirectionIndex1)) and
     node2.getIndirectionIndex() = 1 and
     numberOfLoadsFromOperand(node2.getFieldAddress(), store.getDestinationAddressOperand(),
-      numberOfLoads)
+      numberOfLoads, certain)
   |
     exists(FieldContent fc | fc = c |
       fc.getField() = node2.getUpdatedField() and
@@ -671,35 +674,51 @@ predicate storeStep(Node node1, Content c, PostFieldUpdateNode node2) {
   )
 }
 
+/**
+ * Holds if data can flow from `node1` to `node2` via an assignment to `f`.
+ * Thus, `node2` references an object with a field `f` that contains the
+ * value of `node1`.
+ */
+predicate storeStep(Node node1, Content c, PostFieldUpdateNode node2) {
+  storeStepImpl(node1, c, node2, _)
+}
+
 /**
  * Holds if `operandFrom` flows to `operandTo` using a sequence of conversion-like
  * operations and exactly `n` `LoadInstruction` operations.
  */
-private predicate numberOfLoadsFromOperandRec(Operand operandFrom, Operand operandTo, int ind) {
+private predicate numberOfLoadsFromOperandRec(
+  Operand operandFrom, Operand operandTo, int ind, boolean certain
+) {
   exists(Instruction load | Ssa::isDereference(load, operandFrom) |
-    operandTo = operandFrom and ind = 0
+    operandTo = operandFrom and ind = 0 and certain = true
     or
-    numberOfLoadsFromOperand(load.getAUse(), operandTo, ind - 1)
+    numberOfLoadsFromOperand(load.getAUse(), operandTo, ind - 1, certain)
   )
   or
-  exists(Operand op, Instruction instr |
+  exists(Operand op, Instruction instr, boolean isPointerArith, boolean certain0 |
     instr = op.getDef() and
-    conversionFlow(operandFrom, instr, _, _) and
-    numberOfLoadsFromOperand(op, operandTo, ind)
+    conversionFlow(operandFrom, instr, isPointerArith, _) and
+    numberOfLoadsFromOperand(op, operandTo, ind, certain0)
+  |
+    if isPointerArith = true then certain = false else certain = certain0
   )
 }
 
 /**
  * Holds if `operandFrom` flows to `operandTo` using a sequence of conversion-like
  * operations and exactly `n` `LoadInstruction` operations.
  */
-private predicate numberOfLoadsFromOperand(Operand operandFrom, Operand operandTo, int n) {
-  numberOfLoadsFromOperandRec(operandFrom, operandTo, n)
+private predicate numberOfLoadsFromOperand(
+  Operand operandFrom, Operand operandTo, int n, boolean certain
+) {
+  numberOfLoadsFromOperandRec(operandFrom, operandTo, n, certain)
   or
   not Ssa::isDereference(_, operandFrom) and
   not conversionFlow(operandFrom, _, _, _) and
   operandFrom = operandTo and
-  n = 0
+  n = 0 and
+  certain = true
 }
 
 // Needed to join on both an operand and an index at the same time.
@@ -729,7 +748,7 @@ predicate readStep(Node node1, Content c, Node node2) {
     // The `1` here matches the `node2.getIndirectionIndex() = 1` conjunct
     // in `storeStep`.
     nodeHasOperand(node1, fa1.getObjectAddressOperand(), 1) and
-    numberOfLoadsFromOperand(fa1, operand, numberOfLoads)
+    numberOfLoadsFromOperand(fa1, operand, numberOfLoads, _)
   |
     exists(FieldContent fc | fc = c |
       fc.getField() = fa1.getField() and
@@ -747,7 +766,33 @@ predicate readStep(Node node1, Content c, Node node2) {
  * Holds if values stored inside content `c` are cleared at node `n`.
  */
 predicate clearsContent(Node n, Content c) {
-  none() // stub implementation
+  n =
+    any(PostUpdateNode pun, Content d | d.impliesClearOf(c) and storeStepImpl(_, d, pun, true) | pun)
+        .getPreUpdateNode() and
+  (
+    // The crement operations and pointer addition and subtraction self-assign. We do not
+    // want to clear the contents if it is indirectly pointed at by any of these operations,
+    // as part of the contents might still be accessible afterwards. If there is no such
+    // indirection clearing the contents is safe.
+    not exists(Operand op, Cpp::Operation p |
+      n.(IndirectOperand).hasOperandAndIndirectionIndex(op, _) and
+      (
+        p instanceof Cpp::AssignPointerAddExpr or
+        p instanceof Cpp::AssignPointerSubExpr or
+        p instanceof Cpp::CrementOperation
+      )
+    |
+      p.getAnOperand() = op.getUse().getAst()
+    )
+    or
+    forex(PostUpdateNode pun, Content d |
+      pragma[only_bind_into](d).impliesClearOf(pragma[only_bind_into](c)) and
+      storeStepImpl(_, d, pun, true) and
+      pun.getPreUpdateNode() = n
+    |
+      c.getIndirectionIndex() = d.getIndirectionIndex()
+    )
+  )
 }
 
 /**

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll

@@ -1832,6 +1832,20 @@ class Content extends TContent {
   predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
     path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
   }
+
+  /** Gets the indirection index of this `Content`. */
+  abstract int getIndirectionIndex();
+
+  /**
+   * INTERNAL: Do not use.
+   *
+   * Holds if a write to this `Content` implies that `c` is
+   * also cleared.
+   *
+   * For example, a write to a field `f` implies that any content of
+   * the form `*f` is also cleared.
+   */
+  abstract predicate impliesClearOf(Content c);
 }
 
 /** A reference through a non-union instance field. */
@@ -1849,10 +1863,21 @@ class FieldContent extends Content, TFieldContent {
 
   Field getField() { result = f }
 
+  /** Gets the indirection index of this `FieldContent`. */
   pragma[inline]
-  int getIndirectionIndex() {
+  override int getIndirectionIndex() {
     pragma[only_bind_into](result) = pragma[only_bind_out](indirectionIndex)
   }
+
+  override predicate impliesClearOf(Content c) {
+    exists(FieldContent fc |
+      fc = c and
+      fc.getField() = f and
+      // If `this` is `f` then `c` is cleared if it's of the
+      // form `*f`, `**f`, etc.
+      fc.getIndirectionIndex() >= indirectionIndex
+    )
+  }
 }
 
 /** A reference through an instance field of a union. */
@@ -1877,9 +1902,21 @@ class UnionContent extends Content, TUnionContent {
 
   /** Gets the indirection index of this `UnionContent`. */
   pragma[inline]
-  int getIndirectionIndex() {
+  override int getIndirectionIndex() {
     pragma[only_bind_into](result) = pragma[only_bind_out](indirectionIndex)
   }
+
+  override predicate impliesClearOf(Content c) {
+    exists(UnionContent uc |
+      uc = c and
+      uc.getUnion() = u and
+      // If `this` is `u` then `c` is cleared if it's of the
+      // form `*u`, `**u`, etc. (and we ignore `bytes` because
+      // we know the entire union is overwritten because it's a
+      // union).
+      uc.getIndirectionIndex() >= indirectionIndex
+    )
+  }
 }
 
 /**

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/array-access/ArrayAccessProductFlow.expected

@@ -4,8 +4,9 @@ edges
 | test.cpp:19:9:19:16 | mk_array indirection [p] | test.cpp:28:19:28:26 | call to mk_array [p] |
 | test.cpp:19:9:19:16 | mk_array indirection [p] | test.cpp:50:18:50:25 | call to mk_array [p] |
 | test.cpp:21:5:21:24 | ... = ... | test.cpp:21:9:21:9 | arr indirection [post update] [p] |
-| test.cpp:21:9:21:9 | arr indirection [post update] [p] | test.cpp:19:9:19:16 | mk_array indirection [p] |
+| test.cpp:21:9:21:9 | arr indirection [post update] [p] | test.cpp:22:5:22:7 | arr indirection [p] |
 | test.cpp:21:13:21:18 | call to malloc | test.cpp:21:5:21:24 | ... = ... |
+| test.cpp:22:5:22:7 | arr indirection [p] | test.cpp:19:9:19:16 | mk_array indirection [p] |
 | test.cpp:28:19:28:26 | call to mk_array [p] | test.cpp:31:9:31:11 | arr indirection [p] |
 | test.cpp:28:19:28:26 | call to mk_array [p] | test.cpp:35:9:35:11 | arr indirection [p] |
 | test.cpp:31:9:31:11 | arr indirection [p] | test.cpp:31:13:31:13 | p indirection |
@@ -20,18 +21,20 @@ edges
 | test.cpp:45:13:45:13 | p indirection | test.cpp:45:13:45:13 | p |
 | test.cpp:50:18:50:25 | call to mk_array [p] | test.cpp:39:27:39:29 | arr [p] |
 | test.cpp:55:5:55:24 | ... = ... | test.cpp:55:9:55:9 | arr indirection [post update] [p] |
-| test.cpp:55:9:55:9 | arr indirection [post update] [p] | test.cpp:59:9:59:11 | arr indirection [p] |
-| test.cpp:55:9:55:9 | arr indirection [post update] [p] | test.cpp:63:9:63:11 | arr indirection [p] |
+| test.cpp:55:9:55:9 | arr indirection [post update] [p] | test.cpp:56:5:56:7 | arr indirection [p] |
 | test.cpp:55:13:55:18 | call to malloc | test.cpp:55:5:55:24 | ... = ... |
+| test.cpp:56:5:56:7 | arr indirection [p] | test.cpp:59:9:59:11 | arr indirection [p] |
+| test.cpp:56:5:56:7 | arr indirection [p] | test.cpp:63:9:63:11 | arr indirection [p] |
 | test.cpp:59:9:59:11 | arr indirection [p] | test.cpp:59:13:59:13 | p indirection |
 | test.cpp:59:13:59:13 | p indirection | test.cpp:59:13:59:13 | p |
 | test.cpp:63:9:63:11 | arr indirection [p] | test.cpp:63:13:63:13 | p indirection |
 | test.cpp:63:13:63:13 | p indirection | test.cpp:63:13:63:13 | p |
 | test.cpp:67:10:67:19 | mk_array_p indirection [p] | test.cpp:76:20:76:29 | call to mk_array_p indirection [p] |
 | test.cpp:67:10:67:19 | mk_array_p indirection [p] | test.cpp:98:18:98:27 | call to mk_array_p indirection [p] |
 | test.cpp:69:5:69:25 | ... = ... | test.cpp:69:10:69:10 | arr indirection [post update] [p] |
-| test.cpp:69:10:69:10 | arr indirection [post update] [p] | test.cpp:67:10:67:19 | mk_array_p indirection [p] |
+| test.cpp:69:10:69:10 | arr indirection [post update] [p] | test.cpp:70:5:70:7 | arr indirection [p] |
 | test.cpp:69:14:69:19 | call to malloc | test.cpp:69:5:69:25 | ... = ... |
+| test.cpp:70:5:70:7 | arr indirection [p] | test.cpp:67:10:67:19 | mk_array_p indirection [p] |
 | test.cpp:76:20:76:29 | call to mk_array_p indirection [p] | test.cpp:79:9:79:11 | arr indirection [p] |
 | test.cpp:76:20:76:29 | call to mk_array_p indirection [p] | test.cpp:83:9:83:11 | arr indirection [p] |
 | test.cpp:79:9:79:11 | arr indirection [p] | test.cpp:79:14:79:14 | p indirection |
@@ -53,6 +56,7 @@ nodes
 | test.cpp:21:5:21:24 | ... = ... | semmle.label | ... = ... |
 | test.cpp:21:9:21:9 | arr indirection [post update] [p] | semmle.label | arr indirection [post update] [p] |
 | test.cpp:21:13:21:18 | call to malloc | semmle.label | call to malloc |
+| test.cpp:22:5:22:7 | arr indirection [p] | semmle.label | arr indirection [p] |
 | test.cpp:28:19:28:26 | call to mk_array [p] | semmle.label | call to mk_array [p] |
 | test.cpp:31:9:31:11 | arr indirection [p] | semmle.label | arr indirection [p] |
 | test.cpp:31:13:31:13 | p | semmle.label | p |
@@ -71,6 +75,7 @@ nodes
 | test.cpp:55:5:55:24 | ... = ... | semmle.label | ... = ... |
 | test.cpp:55:9:55:9 | arr indirection [post update] [p] | semmle.label | arr indirection [post update] [p] |
 | test.cpp:55:13:55:18 | call to malloc | semmle.label | call to malloc |
+| test.cpp:56:5:56:7 | arr indirection [p] | semmle.label | arr indirection [p] |
 | test.cpp:59:9:59:11 | arr indirection [p] | semmle.label | arr indirection [p] |
 | test.cpp:59:13:59:13 | p | semmle.label | p |
 | test.cpp:59:13:59:13 | p indirection | semmle.label | p indirection |
@@ -81,6 +86,7 @@ nodes
 | test.cpp:69:5:69:25 | ... = ... | semmle.label | ... = ... |
 | test.cpp:69:10:69:10 | arr indirection [post update] [p] | semmle.label | arr indirection [post update] [p] |
 | test.cpp:69:14:69:19 | call to malloc | semmle.label | call to malloc |
+| test.cpp:70:5:70:7 | arr indirection [p] | semmle.label | arr indirection [p] |
 | test.cpp:76:20:76:29 | call to mk_array_p indirection [p] | semmle.label | call to mk_array_p indirection [p] |
 | test.cpp:79:9:79:11 | arr indirection [p] | semmle.label | arr indirection [p] |
 | test.cpp:79:14:79:14 | p | semmle.label | p |