Merge pull request #7063 from MathiasVP/use-range-analysis-in-buffer-write

C++: Use `SimpleRangeAnalysis` in `Printf.qll`

Author: geoffw0

cpp/ql/lib/semmle/code/cpp/commons/Printf.qll

@@ -6,6 +6,8 @@ import semmle.code.cpp.Type
 import semmle.code.cpp.commons.CommonType
 import semmle.code.cpp.commons.StringAnalysis
 import semmle.code.cpp.models.interfaces.FormattingFunction
+private import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 
 class PrintfFormatAttribute extends FormatAttribute {
   PrintfFormatAttribute() { this.getArchetype() = ["printf", "__printf__"] }
@@ -268,6 +270,18 @@ class FormattingFunctionCall extends Expr {
   }
 }
 
+/**
+ * Gets the number of digits required to represent the integer represented by `f`.
+ *
+ * `f` is assumed to be nonnegative.
+ */
+bindingset[f]
+private int lengthInBase10(float f) {
+  f = 0 and result = 1
+  or
+  result = f.log10().floor() + 1
+}
+
 /**
  * A class to represent format strings that occur as arguments to invocations of formatting functions.
  */
@@ -1046,39 +1060,63 @@ class FormatLiteral extends Literal {
         or
         this.getConversionChar(n).toLowerCase() = ["d", "i"] and
         // e.g. -2^31 = "-2147483648"
-        exists(int sizeBits |
-          sizeBits =
-            min(int bits |
-              bits = this.getIntegralDisplayType(n).getSize() * 8
-              or
-              exists(IntegralType t |
-                t = this.getUse().getConversionArgument(n).getType().getUnderlyingType()
-              |
-                t.isSigned() and bits = t.getSize() * 8
-              )
-            ) and
-          len = 1 + ((sizeBits - 1) / 10.0.log2()).ceil()
-          // this calculation is as %u (below) only we take out the sign bit (- 1) and allow a whole
-          // character for it to be expressed as '-'.
-        )
+        len =
+          min(float cand |
+            // 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.
+            cand = 1 + lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8 - 1))
+            or
+            // 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 |
+              arg = this.getUse().getConversionArgument(n) and
+              lower = lowerBound(arg.getFullyConverted()) and
+              upper = upperBound(arg.getFullyConverted())
+            |
+              cand =
+                max(int cand0 |
+                  // Include the sign bit in the length if it can be negative
+                  (
+                    if lower < 0
+                    then cand0 = 1 + lengthInBase10(lower.abs())
+                    else cand0 = lengthInBase10(lower)
+                  )
+                  or
+                  (
+                    if upper < 0
+                    then cand0 = 1 + lengthInBase10(upper.abs())
+                    else cand0 = lengthInBase10(upper)
+                  )
+                )
+            )
+          )
         or
         this.getConversionChar(n).toLowerCase() = "u" and
         // e.g. 2^32 - 1 = "4294967295"
-        exists(int sizeBits |
-          sizeBits =
-            min(int bits |
-              bits = this.getIntegralDisplayType(n).getSize() * 8
-              or
-              exists(IntegralType t |
-                t = this.getUse().getConversionArgument(n).getType().getUnderlyingType()
-              |
-                t.isUnsigned() and bits = t.getSize() * 8
-              )
-            ) and
-          len = (sizeBits / 10.0.log2()).ceil()
-          // convert the size from bits to decimal characters, and round up as you can't have
-          // fractional characters (10.0.log2() is the number of bits expressed per decimal character)
-        )
+        len =
+          min(float cand |
+            // The first case handles length sub-specifiers
+            cand = 2.pow(this.getIntegralDisplayType(n).getSize() * 8)
+            or
+            // 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 |
+              arg = this.getUse().getConversionArgument(n) and
+              lower = lowerBound(arg.getFullyConverted())
+            |
+              cand =
+                max(float cand0 |
+                  // If lower can be negative we use `(unsigned)-1` as the candidate value.
+                  lower < 0 and
+                  cand0 = 2.pow(any(IntType t | t.isUnsigned()).getSize() * 8)
+                  or
+                  cand0 = upperBound(arg.getFullyConverted())
+                )
+            )
+          |
+            lengthInBase10(cand)
+          )
         or
         this.getConversionChar(n).toLowerCase() = "x" and
         // e.g. "12345678"

cpp/ql/test/query-tests/Security/CWE/CWE-242/semmle/tests/OverrunWrite.expected

@@ -3,3 +3,13 @@
 | tests.cpp:272:2:272:8 | call to sprintf | This 'call to sprintf' operation requires 9 bytes but the destination is only 8 bytes. |
 | tests.cpp:273:2:273:8 | call to sprintf | This 'call to sprintf' operation requires 9 bytes but the destination is only 8 bytes. |
 | tests.cpp:308:3:308:9 | call to sprintf | This 'call to sprintf' operation requires 9 bytes but the destination is only 8 bytes. |
+| tests.cpp:315:2:315:8 | call to sprintf | This 'call to sprintf' operation requires 11 bytes but the destination is only 2 bytes. |
+| tests.cpp:316:2:316:8 | call to sprintf | This 'call to sprintf' operation requires 11 bytes but the destination is only 2 bytes. |
+| tests.cpp:321:2:321:8 | call to sprintf | This 'call to sprintf' operation requires 11 bytes but the destination is only 2 bytes. |
+| tests.cpp:324:3:324:9 | call to sprintf | This 'call to sprintf' operation requires 11 bytes but the destination is only 2 bytes. |
+| tests.cpp:327:2:327:8 | call to sprintf | This 'call to sprintf' operation requires 12 bytes but the destination is only 2 bytes. |
+| tests.cpp:329:3:329:9 | call to sprintf | This 'call to sprintf' operation requires 12 bytes but the destination is only 2 bytes. |
+| tests.cpp:341:2:341:8 | call to sprintf | This 'call to sprintf' operation requires 3 bytes but the destination is only 2 bytes. |
+| tests.cpp:343:2:343:8 | call to sprintf | This 'call to sprintf' operation requires 3 bytes but the destination is only 2 bytes. |
+| tests.cpp:345:2:345:8 | call to sprintf | This 'call to sprintf' operation requires 11 bytes but the destination is only 2 bytes. |
+| tests.cpp:347:2:347:8 | call to sprintf | This 'call to sprintf' operation requires 3 bytes but the destination is only 2 bytes. |

cpp/ql/test/query-tests/Security/CWE/CWE-242/semmle/tests/tests.cpp

@@ -307,4 +307,42 @@ namespace custom_sprintf_impl {
 		char buffer8[8];
 		sprintf(buffer8, "12345678"); // BAD: potential buffer overflow
 	}
+}
+
+void test6(unsigned unsigned_value, int value) {
+	char buffer[2];
+	
+	sprintf(buffer, "%u", unsigned_value); // BAD: buffer overflow
+	sprintf(buffer, "%d", unsigned_value); // BAD: buffer overflow
+	if (unsigned_value < 10) {
+		sprintf(buffer, "%u", unsigned_value); // GOOD
+	}
+
+	sprintf(buffer, "%u", -10); // BAD: buffer overflow
+
+	if(unsigned_value == (unsigned)-10) {
+		sprintf(buffer, "%u", unsigned_value); // BAD: buffer overflow
+	}
+
+	sprintf(buffer, "%d", value); // BAD: buffer overflow
+	if (value < 10) {
+		sprintf(buffer, "%d", value); // BAD: buffer overflow
+
+		if(value > 0) {
+			sprintf(buffer, "%d", value); // GOOD
+		}
+	}
+
+	sprintf(buffer, "%u", 0); // GOOD
+	sprintf(buffer, "%d", 0); // GOOD
+	sprintf(buffer, "%u", 5); // GOOD
+	sprintf(buffer, "%d", 5); // GOOD
+
+	sprintf(buffer, "%d", -1); // BAD
+	sprintf(buffer, "%d", 9); // GOOD
+	sprintf(buffer, "%d", 10); // BAD
+
+	sprintf(buffer, "%u", -1); // BAD
+	sprintf(buffer, "%u", 9); // GOOD
+	sprintf(buffer, "%u", 10); // BAD
 }