C++: Rewrite 'cpp/arithmetic-with-extreme-values' away from 'DefaultTaintTracking'.

Author: MathiasVP

cpp/ql/src/Security/CWE/CWE-190/ArithmeticWithExtremeValues.ql

@@ -16,45 +16,30 @@
 
 import cpp
 import semmle.code.cpp.security.Overflow
-import semmle.code.cpp.security.Security
-import semmle.code.cpp.ir.dataflow.internal.DefaultTaintTrackingImpl
+import semmle.code.cpp.dataflow.new.TaintTracking
+import semmle.code.cpp.ir.IR
+import semmle.code.cpp.controlflow.IRGuards as IRGuards
 
 predicate isMaxValue(Expr mie) {
   exists(MacroInvocation mi |
     mi.getExpr() = mie and
-    (
-      mi.getMacroName() = "CHAR_MAX" or
-      mi.getMacroName() = "LLONG_MAX" or
-      mi.getMacroName() = "INT_MAX" or
-      mi.getMacroName() = "SHRT_MAX" or
-      mi.getMacroName() = "UINT_MAX"
-    )
+    mi.getMacroName() = ["CHAR_MAX", "LLONG_MAX", "INT_MAX", "SHRT_MAX", "UINT_MAX"]
   )
 }
 
 predicate isMinValue(Expr mie) {
   exists(MacroInvocation mi |
     mi.getExpr() = mie and
-    (
-      mi.getMacroName() = "CHAR_MIN" or
-      mi.getMacroName() = "LLONG_MIN" or
-      mi.getMacroName() = "INT_MIN" or
-      mi.getMacroName() = "SHRT_MIN"
-    )
+    mi.getMacroName() = ["CHAR_MIN", "LLONG_MIN", "INT_MIN", "SHRT_MIN"]
   )
 }
 
-class SecurityOptionsArith extends SecurityOptions {
-  override predicate isUserInput(Expr expr, string cause) {
+predicate isSource(DataFlow::Node source, string cause) {
+  exists(Expr expr | expr = source.asExpr() |
     isMaxValue(expr) and cause = "max value"
     or
     isMinValue(expr) and cause = "min value"
-  }
-}
-
-predicate taintedVarAccess(Expr origin, VariableAccess va, string cause) {
-  isUserInput(origin, cause) and
-  tainted(origin, va)
+  )
 }
 
 predicate causeEffectCorrespond(string cause, string effect) {
@@ -65,16 +50,79 @@ predicate causeEffectCorrespond(string cause, string effect) {
   effect = "underflow"
 }
 
-from Expr origin, Operation op, VariableAccess va, string cause, string effect
-where
-  taintedVarAccess(origin, va, cause) and
-  op.getAnOperand() = va and
-  (
+predicate isSink(DataFlow::Node sink, VariableAccess va, string effect) {
+  exists(Operation op |
+    sink.asExpr() = va and
+    op.getAnOperand() = va
+  |
     missingGuardAgainstUnderflow(op, va) and effect = "underflow"
     or
     missingGuardAgainstOverflow(op, va) and effect = "overflow"
-  ) and
-  causeEffectCorrespond(cause, effect)
+  )
+}
+
+predicate hasUpperBoundsCheck(Variable var) {
+  exists(RelationalOperation oper, VariableAccess access |
+    oper.getAnOperand() = access and
+    access.getTarget() = var and
+    // Comparing to 0 is not an upper bound check
+    not oper.getAnOperand().getValue() = "0"
+  )
+}
+
+predicate constantInstruction(Instruction instr) {
+  instr instanceof ConstantInstruction or
+  constantInstruction(instr.(UnaryInstruction).getUnary())
+}
+
+predicate readsVariable(LoadInstruction load, Variable var) {
+  load.getSourceAddress().(VariableAddressInstruction).getAstVariable() = var
+}
+
+predicate nodeIsBarrierEqualityCandidate(DataFlow::Node node, Operand access, Variable checkedVar) {
+  exists(Instruction instr | instr = node.asInstruction() |
+    readsVariable(instr, checkedVar) and
+    any(IRGuards::IRGuardCondition guard).ensuresEq(access, _, _, instr.getBlock(), true)
+  )
+}
+
+module Config implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { isSource(source, _) }
+
+  predicate isSink(DataFlow::Node sink) { isSink(sink, _, _) }
+
+  predicate isBarrier(DataFlow::Node node) {
+    // Block flow if there's an upper bound check of the variable anywhere in the program
+    exists(Variable checkedVar, Instruction instr | instr = node.asInstruction() |
+      readsVariable(instr, checkedVar) and
+      hasUpperBoundsCheck(checkedVar)
+    )
+    or
+    // Block flow if the node is guarded by an equality check
+    exists(Variable checkedVar, Operand access |
+      nodeIsBarrierEqualityCandidate(node, access, checkedVar) and
+      readsVariable(access.getDef(), checkedVar)
+    )
+    or
+    // Block flow to any binary instruction whose operands are both non-constants.
+    exists(BinaryInstruction iTo |
+      iTo = node.asInstruction() and
+      not constantInstruction(iTo.getLeft()) and
+      not constantInstruction(iTo.getRight()) and
+      // propagate taint from either the pointer or the offset, regardless of constantness
+      not iTo instanceof PointerArithmeticInstruction
+    )
+  }
+}
+
+module Flow = TaintTracking::Global<Config>;
+
+from DataFlow::Node source, DataFlow::Node sink, VariableAccess va, string cause, string effect
+where
+  Flow::flow(source, sink) and
+  isSource(source, cause) and
+  causeEffectCorrespond(cause, effect) and
+  isSink(sink, va, effect)
 select va,
   "$@ flows to an operand of an arithmetic expression, potentially causing an " + effect + ".",
-  origin, "Extreme value"
+  source, "Extreme value"