C++: preserve Printf and BufferWrite API

redsun82 · web-flow · commit aa68c51797ab · 2021-12-13T11:28:02.000Z
diff --git a/cpp/ql/lib/semmle/code/cpp/commons/Printf.qll b/cpp/ql/lib/semmle/code/cpp/commons/Printf.qll
@@ -20,17 +20,22 @@ class BufferWriteEstimationReason extends TBufferWriteEstimationReason {
   }
 
   string toString() {
-    this = TTypeBoundsAnalysis() and result = "based on type bounds" or
+    this = TTypeBoundsAnalysis() and result = "based on type bounds"
+    or
     this = TValueFlowAnalysis() and result = "based on flow analysis of value bounds"
   }
 
   BufferWriteEstimationReason combineWith(BufferWriteEstimationReason other) {
-    (this = TTypeBoundsAnalysis() or other = TTypeBoundsAnalysis()) and result = TTypeBoundsAnalysis() or
-    (this = TValueFlowAnalysis() and other = TValueFlowAnalysis()) and result = TValueFlowAnalysis()
+    (this = TTypeBoundsAnalysis() or other = TTypeBoundsAnalysis()) and
+    result = TTypeBoundsAnalysis()
+    or
+    (this = TValueFlowAnalysis() and other = TValueFlowAnalysis()) and
+    result = TValueFlowAnalysis()
   }
 }
 
 BufferWriteEstimationReason typeBoundsAnalysis() { result = TTypeBoundsAnalysis() }
+
 BufferWriteEstimationReason valueFlowAnalysis() { result = TValueFlowAnalysis() }
 
 class PrintfFormatAttribute extends FormatAttribute {
@@ -1014,6 +1019,8 @@ class FormatLiteral extends Literal {
    * conversion specifier of this format string; has no result if this cannot
    * be determined.
    */
+  int getMaxConvertedLength(int n) { result = max(int l | l = getMaxConvertedLength(n, _) | l) }
+
   int getMaxConvertedLength(int n, BufferWriteEstimationReason reason) {
     exists(int len |
       (
@@ -1026,10 +1033,12 @@ class FormatLiteral extends Literal {
       ) and
       (
         this.getConversionChar(n) = "%" and
-        len = 1 and reason = TValueFlowAnalysis()
+        len = 1 and
+        reason = TValueFlowAnalysis()
         or
         this.getConversionChar(n).toLowerCase() = "c" and
-        len = 1 and reason = TValueFlowAnalysis() // e.g. 'a'
+        len = 1 and
+        reason = TValueFlowAnalysis() // e.g. 'a'
         or
         this.getConversionChar(n).toLowerCase() = "f" and
         exists(int dot, int afterdot |
@@ -1043,7 +1052,8 @@ class FormatLiteral extends Literal {
             afterdot = 6
           ) and
           len = 1 + 309 + dot + afterdot
-        ) and reason = TTypeBoundsAnalysis() // e.g. -1e308="-100000"...
+        ) and
+        reason = TTypeBoundsAnalysis() // e.g. -1e308="-100000"...
         or
         this.getConversionChar(n).toLowerCase() = "e" and
         exists(int dot, int afterdot |
@@ -1057,7 +1067,8 @@ class FormatLiteral extends Literal {
             afterdot = 6
           ) and
           len = 1 + 1 + dot + afterdot + 1 + 1 + 3
-        ) and reason = TTypeBoundsAnalysis() // -1e308="-1.000000e+308"
+        ) and
+        reason = TTypeBoundsAnalysis() // -1e308="-1.000000e+308"
         or
         this.getConversionChar(n).toLowerCase() = "g" and
         exists(int dot, int afterdot |
@@ -1080,77 +1091,79 @@ class FormatLiteral extends Literal {
           //       (e.g. 123456, 0.000123456 are just OK)
           //       so case %f can be at most P characters + 4 zeroes, sign, dot = P + 6
           len = (afterdot.maximum(1) + 6).maximum(1 + 1 + dot + afterdot + 1 + 1 + 3)
-        ) and reason = TTypeBoundsAnalysis() // (e.g. "-1.59203e-319")
+        ) and
+        reason = TTypeBoundsAnalysis() // (e.g. "-1.59203e-319")
         or
         this.getConversionChar(n).toLowerCase() = ["d", "i"] and
         // e.g. -2^31 = "-2147483648"
         exists(float typeBasedBound, float valueBasedBound |
-            // The first case handles length sub-specifiers
-            // Subtract one in the exponent because one bit is for the sign.
-            // Add 1 to account for the possible sign in the output.
-            typeBasedBound = 1 + lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8 - 1)) and
-            // The second case uses range analysis to deduce a length that's shorter than the length
-            // of the number -2^31.
-            exists(Expr arg, float lower, float upper, float typeLower, float typeUpper |
-              arg = this.getUse().getConversionArgument(n) and
-              lower = lowerBound(arg.getFullyConverted()) and
-              upper = upperBound(arg.getFullyConverted()) and
-              typeLower = exprMinVal(arg.getFullyConverted()) and
-              typeUpper = exprMaxVal(arg.getFullyConverted()) 
-            |
-              valueBasedBound =
-                max(int cand |
-                  // Include the sign bit in the length if it can be negative
-                  (
-                    if lower < 0
-                    then cand = 1 + lengthInBase10(lower.abs())
-                    else cand = lengthInBase10(lower)
-                  )
-                  or
-                  (
-                    if upper < 0
-                    then cand = 1 + lengthInBase10(upper.abs())
-                    else cand = lengthInBase10(upper)
-                  )
-                ) and
-              (
-                if lower > typeLower or upper < typeUpper
-                then reason = TValueFlowAnalysis()
-                else reason = TTypeBoundsAnalysis()
-              )
-            ) and
-            len = valueBasedBound.minimum(typeBasedBound)
+          // The first case handles length sub-specifiers
+          // Subtract one in the exponent because one bit is for the sign.
+          // Add 1 to account for the possible sign in the output.
+          typeBasedBound =
+            1 + lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8 - 1)) and
+          // The second case uses range analysis to deduce a length that's shorter than the length
+          // of the number -2^31.
+          exists(Expr arg, float lower, float upper, float typeLower, float typeUpper |
+            arg = this.getUse().getConversionArgument(n) and
+            lower = lowerBound(arg.getFullyConverted()) and
+            upper = upperBound(arg.getFullyConverted()) and
+            typeLower = exprMinVal(arg.getFullyConverted()) and
+            typeUpper = exprMaxVal(arg.getFullyConverted())
+          |
+            valueBasedBound =
+              max(int cand |
+                // Include the sign bit in the length if it can be negative
+                (
+                  if lower < 0
+                  then cand = 1 + lengthInBase10(lower.abs())
+                  else cand = lengthInBase10(lower)
+                )
+                or
+                (
+                  if upper < 0
+                  then cand = 1 + lengthInBase10(upper.abs())
+                  else cand = lengthInBase10(upper)
+                )
+              ) and
+            (
+              if lower > typeLower or upper < typeUpper
+              then reason = TValueFlowAnalysis()
+              else reason = TTypeBoundsAnalysis()
+            )
+          ) and
+          len = valueBasedBound.minimum(typeBasedBound)
         )
         or
         this.getConversionChar(n).toLowerCase() = "u" and
         // e.g. 2^32 - 1 = "4294967295"
         exists(float typeBasedBound, float valueBasedBound |
-            // The first case handles length sub-specifiers
-            typeBasedBound = lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8) - 1) and
-            // The second case uses range analysis to deduce a length that's shorter than
-            // the length of the number 2^31 - 1.
-            exists(Expr arg, float lower, float upper, float typeLower, float typeUpper |
-              arg = this.getUse().getConversionArgument(n) and
-              lower = lowerBound(arg.getFullyConverted()) and
-              upper = upperBound(arg.getFullyConverted()) and
-              typeLower = exprMinVal(arg.getFullyConverted()) and
-              typeUpper = exprMaxVal(arg.getFullyConverted()) 
-            |
-              valueBasedBound =
-                lengthInBase10(max(float cand |
+          // The first case handles length sub-specifiers
+          typeBasedBound = lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8) - 1) and
+          // The second case uses range analysis to deduce a length that's shorter than
+          // the length of the number 2^31 - 1.
+          exists(Expr arg, float lower, float upper, float typeLower, float typeUpper |
+            arg = this.getUse().getConversionArgument(n) and
+            lower = lowerBound(arg.getFullyConverted()) and
+            upper = upperBound(arg.getFullyConverted()) and
+            typeLower = exprMinVal(arg.getFullyConverted()) and
+            typeUpper = exprMaxVal(arg.getFullyConverted())
+          |
+            valueBasedBound =
+              lengthInBase10(max(float cand |
                   // If lower can be negative we use `(unsigned)-1` as the candidate value.
                   lower < 0 and
                   cand = 2.pow(any(IntType t | t.isUnsigned()).getSize() * 8)
                   or
                   cand = upper
                 )) and
-              (
-                if lower > typeLower or upper < typeUpper
-                then reason = TValueFlowAnalysis()
-                else reason = TTypeBoundsAnalysis()
-              )
-            ) and
-            len = valueBasedBound.minimum(typeBasedBound)
+            (
+              if lower > typeLower or upper < typeUpper
+              then reason = TValueFlowAnalysis()
+              else reason = TTypeBoundsAnalysis()
+            )
+          ) and
+          len = valueBasedBound.minimum(typeBasedBound)
         )
         or
         this.getConversionChar(n).toLowerCase() = "x" and
@@ -1170,7 +1183,8 @@ class FormatLiteral extends Literal {
           (
             if this.hasAlternateFlag(n) then len = 2 + baseLen else len = baseLen // "0x"
           )
-        ) and reason = TTypeBoundsAnalysis()
+        ) and
+        reason = TTypeBoundsAnalysis()
         or
         this.getConversionChar(n).toLowerCase() = "p" and
         exists(PointerType ptrType, int baseLen |
@@ -1179,7 +1193,8 @@ class FormatLiteral extends Literal {
           (
             if this.hasAlternateFlag(n) then len = 2 + baseLen else len = baseLen // "0x"
           )
-        ) and reason = TValueFlowAnalysis()
+        ) and
+        reason = TValueFlowAnalysis()
         or
         this.getConversionChar(n).toLowerCase() = "o" and
         // e.g. 2^32 - 1 = "37777777777"
@@ -1198,7 +1213,8 @@ class FormatLiteral extends Literal {
           (
             if this.hasAlternateFlag(n) then len = 1 + baseLen else len = baseLen // "0"
           )
-        ) and reason = TTypeBoundsAnalysis()
+        ) and
+        reason = TTypeBoundsAnalysis()
         or
         this.getConversionChar(n).toLowerCase() = "s" and
         len =
@@ -1218,6 +1234,10 @@ class FormatLiteral extends Literal {
    * determining whether a buffer overflow is caused by long float to string
    * conversions.
    */
+  int getMaxConvertedLengthLimited(int n) {
+    result = max(int l | l = getMaxConvertedLengthLimited(n, _) | l)
+  }
+
   int getMaxConvertedLengthLimited(int n, BufferWriteEstimationReason reason) {
     if this.getConversionChar(n).toLowerCase() = "f"
     then result = this.getMaxConvertedLength(n, reason).minimum(8)
@@ -1269,20 +1289,20 @@ class FormatLiteral extends Literal {
         result =
           this.getConstantPart(n).length() + this.getMaxConvertedLength(n, headReason) +
             this.getMaxConvertedLengthAfter(n + 1, tailReason) and
-            reason = headReason.combineWith(tailReason)
+        reason = headReason.combineWith(tailReason)
       )
   }
 
   private int getMaxConvertedLengthAfterLimited(int n, BufferWriteEstimationReason reason) {
     if n = this.getNumConvSpec()
     then result = this.getConstantSuffix().length() + 1 and reason = TValueFlowAnalysis()
     else
-    exists(BufferWriteEstimationReason headReason, BufferWriteEstimationReason tailReason |
-      result =
-        this.getConstantPart(n).length() + this.getMaxConvertedLengthLimited(n, headReason) +
-          this.getMaxConvertedLengthAfterLimited(n + 1, tailReason) and
-          reason = headReason.combineWith(tailReason)
-    )
+      exists(BufferWriteEstimationReason headReason, BufferWriteEstimationReason tailReason |
+        result =
+          this.getConstantPart(n).length() + this.getMaxConvertedLengthLimited(n, headReason) +
+            this.getMaxConvertedLengthAfterLimited(n + 1, tailReason) and
+        reason = headReason.combineWith(tailReason)
+      )
   }
 
   /**
diff --git a/cpp/ql/lib/semmle/code/cpp/security/BufferWrite.qll b/cpp/ql/lib/semmle/code/cpp/security/BufferWrite.qll
@@ -69,20 +69,19 @@ abstract class BufferWrite extends Expr {
    * Gets an upper bound to the amount of data that's being written (if one
    * can be found).
    */
-  int getMaxData() { result = max(int d | d = getMaxDataWithReason(_) | d) }
+  int getMaxData() { result = max(int d | d = getMaxData(_) | d) }
 
   /**
    * Gets an upper bound to the amount of data that's being written (if one
    * can be found), except that float to string conversions are assumed to be
    * much smaller (8 bytes) than their true maximum length.  This can be
    * helpful in determining the cause of a buffer overflow issue.
    */
-  int getMaxDataLimited() { result = max(int d | d = getMaxDataLimitedWithReason(_) | d) }
+  int getMaxDataLimited() { result = max(int d | d = getMaxDataLimited(_) | d) }
 
+  int getMaxData(BufferWriteEstimationReason reason) { none() }
 
-  int getMaxDataWithReason(BufferWriteEstimationReason reason) { none() }
-
-  int getMaxDataLimitedWithReason(BufferWriteEstimationReason reason) { result = getMaxDataWithReason(reason) }
+  int getMaxDataLimited(BufferWriteEstimationReason reason) { result = getMaxData(reason) }
 
   /**
    * Gets the size of a single character of the type this
@@ -140,7 +139,7 @@ class StrCopyBW extends BufferWriteCall {
     result = this.getArgument(this.getParamSize()).getValue().toInt() * this.getCharSize()
   }
 
-  override int getMaxDataWithReason(BufferWriteEstimationReason reason) {
+  override int getMaxData(BufferWriteEstimationReason reason) {
     // when result exists, it is an exact flow analysis
     reason = valueFlowAnalysis() and
     result =
@@ -180,7 +179,7 @@ class StrCatBW extends BufferWriteCall {
     result = this.getArgument(this.getParamSize()).getValue().toInt() * this.getCharSize()
   }
 
-  override int getMaxDataWithReason(BufferWriteEstimationReason reason) {
+  override int getMaxData(BufferWriteEstimationReason reason) {
     // when result exists, it is an exact flow analysis
     reason = valueFlowAnalysis() and
     result =
@@ -242,14 +241,14 @@ class SprintfBW extends BufferWriteCall {
 
   override Expr getDest() { result = this.getArgument(f.getOutputParameterIndex(false)) }
 
-  override int getMaxDataWithReason(BufferWriteEstimationReason reason) {
+  override int getMaxData(BufferWriteEstimationReason reason) {
     exists(FormatLiteral fl |
       fl = this.(FormattingFunctionCall).getFormat() and
       result = fl.getMaxConvertedLengthWithReason(reason) * this.getCharSize()
     )
   }
 
-  override int getMaxDataLimitedWithReason(BufferWriteEstimationReason reason) {
+  override int getMaxDataLimited(BufferWriteEstimationReason reason) {
     exists(FormatLiteral fl |
       fl = this.(FormattingFunctionCall).getFormat() and
       result = fl.getMaxConvertedLengthLimitedWithReason(reason) * this.getCharSize()
@@ -345,14 +344,14 @@ class SnprintfBW extends BufferWriteCall {
     result = this.getArgument(this.getParamSize()).getValue().toInt() * this.getCharSize()
   }
 
-  override int getMaxDataWithReason(BufferWriteEstimationReason reason) {
+  override int getMaxData(BufferWriteEstimationReason reason) {
     exists(FormatLiteral fl |
       fl = this.(FormattingFunctionCall).getFormat() and
       result = fl.getMaxConvertedLengthWithReason(reason) * this.getCharSize()
     )
   }
 
-  override int getMaxDataLimitedWithReason(BufferWriteEstimationReason reason) {
+  override int getMaxDataLimited(BufferWriteEstimationReason reason) {
     exists(FormatLiteral fl |
       fl = this.(FormattingFunctionCall).getFormat() and
       result = fl.getMaxConvertedLengthLimitedWithReason(reason) * this.getCharSize()
@@ -445,7 +444,7 @@ class ScanfBW extends BufferWrite {
 
   override Expr getDest() { result = this }
 
-  override int getMaxDataWithReason(BufferWriteEstimationReason reason) {
+  override int getMaxData(BufferWriteEstimationReason reason) {
     // when this returns, it is based on exact flow analysis
     reason = valueFlowAnalysis() and
     exists(ScanfFunctionCall fc, ScanfFormatLiteral fl, int arg |
@@ -485,7 +484,7 @@ class RealpathBW extends BufferWriteCall {
 
   override Expr getASource() { result = this.getArgument(0) }
 
-  override int getMaxDataWithReason(BufferWriteEstimationReason reason) {
+  override int getMaxData(BufferWriteEstimationReason reason) {
     // although there may be some unknown invariants guaranteeing that a real path is shorter than PATH_MAX, we can consider providing less than PATH_MAX a problem with high precision
     reason = valueFlowAnalysis() and
     result = path_max() and
diff --git a/cpp/ql/src/Security/CWE/CWE-120/OverrunWrite.ql b/cpp/ql/src/Security/CWE/CWE-120/OverrunWrite.ql
@@ -28,7 +28,7 @@ where
   destSize = getBufferSize(dest, _) and
   // we can deduce that too much data may be copied (even without
   // long '%f' conversions)
-  bw.getMaxDataLimitedWithReason(reason) > destSize
+  bw.getMaxDataLimited(reason) > destSize
 select bw,
   "This '" + bw.getBWDesc() + "' operation requires " + bw.getMaxData() +
     " bytes but the destination is only " + destSize + " bytes (" + reason.toString() + ")."
