Created a new leap year check guard condition. Found that the prior definitions had gaps resulting in false positives and inconsistencies (inconsistent as to what is a guard and what is a function that does a leap year check).

Author: bdrodes

cpp/ql/src/Likely Bugs/Leap Year/UncheckedLeapYearAfterYearModification.ql

@@ -385,22 +385,11 @@ module OperationToYearAssignmentConfig implements DataFlow::ConfigSig {
 module OperationToYearAssignmentFlow = TaintTracking::Global<OperationToYearAssignmentConfig>;
 
 predicate isLeapYearCheckSink(DataFlow::Node sink) {
-  exists(ExprCheckLeapYear e | sink.asExpr() = e.getAChild*())
-  or
-  // Local leap year check
-  sink.asExpr().(LeapYearFieldAccess).isUsedInCorrectLeapYearCheck()
-  or
-  // passed to function that seems to check for leap year
-  exists(ChecksForLeapYearFunctionCall fc |
-    sink.asExpr() = fc.getAnArgument()
-    or
-    sink.asExpr() = fc.getAnArgument().(FieldAccess).getQualifier()
-    or
-    exists(AddressOfExpr aoe |
-      fc.getAnArgument() = aoe and
-      aoe.getOperand() = sink.asExpr()
-    )
+  exists(LeapYearGuardCondition lgc |
+    lgc.checkedYearAccess() = [sink.asExpr(), sink.asIndirectExpr()]
   )
+  or
+  isLeapYearCheckCall(_, [sink.asExpr(), sink.asIndirectExpr()])
 }
 
 /**
@@ -513,6 +502,147 @@ module TimeStructToCheckedTimeConversionConfig implements DataFlow::StateConfigS
 module TimeStructToCheckedTimeConversionFlow =
   DataFlow::GlobalWithState<TimeStructToCheckedTimeConversionConfig>;
 
+/**
+ * Finds flow from a parameter of a function to a leap year check.
+ * This is necessary to handle for scenarios like this:
+ *
+ *    year = DANGEROUS_OP // source
+ *    isLeap = isLeapYear(year);
+ *    // logic based on isLeap
+ *    struct.year = year; // sink
+ *
+ * In this case, we may flow a dangerous op to a year assignment, failing
+ * to barrier the flow through a leap year check, as the leap year check
+ * is nested, and dataflow does not progress down into the check and out.
+ * Instead, the point of this flow is to detect isLeapYear's argument
+ * is checked for leap year, making the isLeapYear call a barrier for
+ * the dangerous flow if we flow through the parameter identified to
+ * be checked.
+ */
+module ParameterToLeapYearCheckConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { exists(source.asParameter()) }
+
+  predicate isSink(DataFlow::Node sink) {
+    exists(LeapYearGuardCondition lgc |
+      lgc.checkedYearAccess() = [sink.asExpr(), sink.asIndirectExpr()]
+    )
+  }
+
+  predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    // flow from a YearFieldAccess to the qualifier
+    node2.asExpr() = node1.asExpr().(YearFieldAccess).getQualifier()
+    or
+    // flow from a year access qualifier to a year field
+    exists(YearFieldAccess yfa | node2.asExpr() = yfa and node1.asExpr() = yfa.getQualifier())
+  }
+
+  /**
+   * Enforcing the check must occur in the same call context as the source,
+   * i.e., do not return from the source function and check in a caller.
+   */
+  DataFlow::FlowFeature getAFeature() { result instanceof DataFlow::FeatureHasSourceCallContext }
+}
+
+// NOTE: I do not believe taint flow is necessary here as we should
+// be flowing directyly from some parameter to a leap year check.
+module ParameterToLeapYearCheckFlow = DataFlow::Global<ParameterToLeapYearCheckConfig>;
+
+predicate isLeapYearCheckCall(Call c, Expr arg) {
+  exists(ParameterToLeapYearCheckFlow::PathNode src, Function f, int i |
+    src.isSource() and
+    f.getParameter(i) = src.getNode().asParameter() and
+    c.getTarget() = f and
+    c.getArgument(i) = arg
+  )
+}
+
+class LeapYearGuardCondition extends GuardCondition {
+  Expr yearSinkDiv4;
+  Expr yearSinkDiv100;
+  Expr yearSinkDiv400;
+
+  LeapYearGuardCondition() {
+    exists(
+      LogicalAndExpr andExpr, LogicalOrExpr orExpr, GuardCondition div4Check,
+      GuardCondition div100Check, GuardCondition div400Check, GuardValue gv
+    |
+      // Cannonical case:
+      // form: `(year % 4 == 0) && (year % 100 != 0 || year % 400 == 0)`
+      // or : `!(year % 4 == 0) && (year % 100 != 0 || year % 400 == 0)`
+      this = andExpr and
+      andExpr.hasOperands(div4Check, orExpr) and
+      orExpr.hasOperands(div100Check, div400Check) and
+      exists(RemExpr e |
+        div4Check.comparesEq(e, 0, true, gv) and
+        e.getRightOperand().getValue().toInt() = 4 and
+        yearSinkDiv4 = e.getLeftOperand()
+      ) and
+      exists(RemExpr e |
+        div100Check.comparesEq(e, 0, false, gv) and
+        e.getRightOperand().getValue().toInt() = 100 and
+        yearSinkDiv100 = e.getLeftOperand()
+      ) and
+      exists(RemExpr e |
+        div400Check.comparesEq(e, 0, true, gv) and
+        e.getRightOperand().getValue().toInt() = 400 and
+        yearSinkDiv400 = e.getLeftOperand()
+      )
+      or
+      // Inverted logic case:
+      //  `year % 400 == 0 || (year % 100 != 0 && year % 4 == 0)`
+      this = orExpr and
+      orExpr.hasOperands(div4Check, andExpr) and
+      andExpr.hasOperands(div100Check, div400Check) and
+      exists(RemExpr e |
+        div4Check.comparesEq(e, 0, false, gv) and
+        e.getRightOperand().getValue().toInt() = 4 and
+        yearSinkDiv4 = e.getLeftOperand()
+      ) and
+      exists(RemExpr e |
+        div100Check.comparesEq(e, 0, true, gv) and
+        e.getRightOperand().getValue().toInt() = 100 and
+        yearSinkDiv100 = e.getLeftOperand()
+      ) and
+      exists(RemExpr e |
+        div400Check.comparesEq(e, 0, false, gv) and
+        e.getRightOperand().getValue().toInt() = 400 and
+        yearSinkDiv400 = e.getLeftOperand()
+      )
+    )
+  }
+
+  Expr getYearSinkDiv4() { result = yearSinkDiv4 }
+
+  Expr getYearSinkDiv100() { result = yearSinkDiv100 }
+
+  Expr getYearSinkDiv400() { result = yearSinkDiv400 }
+
+  /**
+   * The variable access that is used in all 3 components of the leap year check
+   * e.g., see getYearSinkDiv4/100/400..
+   * If a field access is used, the qualifier and the field access are both returned
+   * in checked condition.
+   * NOTE: if the year is not checked using the same access in all 3 components, no result is returned.
+   * The typical case observed is a consistent variable access is used. If not, this may indicate a bug.
+   * We could check more accurately with a dataflow analysis, but this is likely sufficient for now.
+   */
+  VariableAccess checkedYearAccess() {
+    exists(Variable var |
+      (
+        this.getYearSinkDiv4().getAChild*() = var.getAnAccess() and
+        this.getYearSinkDiv100().getAChild*() = var.getAnAccess() and
+        this.getYearSinkDiv400().getAChild*() = var.getAnAccess() and
+        result = var.getAnAccess() and
+        (
+          result = this.getYearSinkDiv4().getAChild*() or
+          result = this.getYearSinkDiv100().getAChild*() or
+          result = this.getYearSinkDiv400().getAChild*()
+        )
+      )
+    )
+  }
+}
+
 import OperationToYearAssignmentFlow::PathGraph
 
 from OperationToYearAssignmentFlow::PathNode src, OperationToYearAssignmentFlow::PathNode sink

cpp/ql/test/query-tests/Likely Bugs/Leap Year/UncheckedLeapYearAfterYearModification/UncheckedLeapYearAfterYearModification.expected

@@ -14,6 +14,9 @@
 | test.cpp:1095:16:1095:23 | increment_arg output argument | test.cpp:1083:2:1083:4 | ... ++ | test.cpp:1095:16:1095:23 | increment_arg output argument | Year field has been modified, but no appropriate check for LeapYear was found. |
 | test.cpp:1099:27:1099:35 | increment_arg_by_pointer output argument | test.cpp:1087:2:1087:7 | ... ++ | test.cpp:1099:27:1099:35 | increment_arg_by_pointer output argument | Year field has been modified, but no appropriate check for LeapYear was found. |
 | test.cpp:1153:14:1153:26 | ... - ... | test.cpp:1153:14:1153:26 | ... - ... | test.cpp:1153:14:1153:26 | ... - ... | Year field has been modified, but no appropriate check for LeapYear was found. |
+| test.cpp:1204:16:1204:19 | year | test.cpp:1202:10:1202:15 | offset | test.cpp:1204:16:1204:19 | year | Year field has been modified, but no appropriate check for LeapYear was found. |
+| test.cpp:1243:16:1243:28 | ... + ... | test.cpp:1243:16:1243:28 | ... + ... | test.cpp:1243:16:1243:28 | ... + ... | Year field has been modified, but no appropriate check for LeapYear was found. |
+| test.cpp:1257:16:1257:28 | ... + ... | test.cpp:1257:16:1257:28 | ... + ... | test.cpp:1257:16:1257:28 | ... + ... | Year field has been modified, but no appropriate check for LeapYear was found. |
 edges
 | test.cpp:854:7:854:31 | ... = ... | test.cpp:857:33:857:36 | year | provenance |  |
 | test.cpp:854:14:854:31 | ... + ... | test.cpp:854:7:854:31 | ... = ... | provenance |  |
@@ -24,6 +27,8 @@ edges
 | test.cpp:1087:2:1087:7 | ... ++ | test.cpp:1086:37:1086:37 | *x | provenance |  |
 | test.cpp:1183:2:1183:15 | ... += ... | test.cpp:1185:16:1185:19 | year | provenance |  |
 | test.cpp:1183:10:1183:15 | offset | test.cpp:1183:2:1183:15 | ... += ... | provenance |  |
+| test.cpp:1202:2:1202:15 | ... += ... | test.cpp:1204:16:1204:19 | year | provenance |  |
+| test.cpp:1202:10:1202:15 | offset | test.cpp:1202:2:1202:15 | ... += ... | provenance |  |
 nodes
 | test.cpp:422:14:422:14 | 2 | semmle.label | 2 |
 | test.cpp:440:2:440:11 | ... ++ | semmle.label | ... ++ |
@@ -61,6 +66,15 @@ nodes
 | test.cpp:1183:2:1183:15 | ... += ... | semmle.label | ... += ... |
 | test.cpp:1183:10:1183:15 | offset | semmle.label | offset |
 | test.cpp:1185:16:1185:19 | year | semmle.label | year |
+| test.cpp:1202:2:1202:15 | ... += ... | semmle.label | ... += ... |
+| test.cpp:1202:10:1202:15 | offset | semmle.label | offset |
+| test.cpp:1204:16:1204:19 | year | semmle.label | year |
+| test.cpp:1223:16:1223:28 | ... + ... | semmle.label | ... + ... |
+| test.cpp:1229:16:1229:28 | ... + ... | semmle.label | ... + ... |
+| test.cpp:1236:16:1236:28 | ... + ... | semmle.label | ... + ... |
+| test.cpp:1243:16:1243:28 | ... + ... | semmle.label | ... + ... |
+| test.cpp:1250:16:1250:28 | ... + ... | semmle.label | ... + ... |
+| test.cpp:1257:16:1257:28 | ... + ... | semmle.label | ... + ... |
 subpaths
 testFailures
 | test.cpp:1075:2:1075:11 | ... ++ | Unexpected result: Alert |

cpp/ql/test/query-tests/Likely Bugs/Leap Year/UncheckedLeapYearAfterYearModification/test.cpp

@@ -1198,5 +1198,62 @@ void leap_year_checked_raw_false_positive2(WORD year, WORD offset, WORD day){
 	}
 
 	tmp.tm_mday = day;
-	
-}
+
+	year += offset; // $ Source
+
+	tmp.tm_year = year; // $ Alert[cpp/microsoft/public/leap-year/unchecked-after-arithmetic-year-modification]
+
+}
+
+
+bool isNotLeapYear(struct tm tm)
+{
+	return !(tm.tm_year % 4 == 0 && (tm.tm_year % 100 != 0 || tm.tm_year % 400 == 0));
+}
+
+bool isNotLeapYear2(struct tm tm)
+{
+	return (tm.tm_year % 4 != 0 || (tm.tm_year % 100 == 0 && tm.tm_year % 400 != 0));
+}
+
+
+void inverted_leap_year_check(WORD year, WORD offset, WORD day){
+	struct tm tmp;
+
+	tmp.tm_year = year + offset;
+
+	if (isNotLeapYear(tmp)){
+		day = 28;
+	}
+
+	tmp.tm_year = year + offset;
+
+	if(isNotLeapYear2(tmp)){
+		day = 28;
+	}
+
+
+	tmp.tm_year = year + offset;
+	bool isNotLeapYear = (tmp.tm_year % 4 != 0 || (tmp.tm_year % 100 == 0 && tmp.tm_year % 400 != 0));
+
+	if(isNotLeapYear){
+		day = 28;
+	}
+
+	tmp.tm_year = year + offset; // $ Alert[cpp/microsoft/public/leap-year/unchecked-after-arithmetic-year-modification]
+}
+
+
+void simplified_leap_year_check(WORD year, WORD offset){
+	struct tm tmp;
+
+	tmp.tm_year = year + offset;
+
+	bool isLeap = !(tmp.tm_year % 4) && (tmp.tm_year % 100 || !(tmp.tm_year % 400));
+	if(isLeap){
+		// do something
+	}
+
+	tmp.tm_year = year + offset; // $ Alert[cpp/microsoft/public/leap-year/unchecked-after-arithmetic-year-modification]
+}
+