Add Arithmetic query libraries

java/ql/lib/semmle/code/java/security/ArithmeticTaintedLocalQuery.qll

@@ -0,0 +1,39 @@
+/** Provides taint-tracking configurations to reason about arithmetic using local-user-controlled data. */
+
+import java
+import semmle.code.java.dataflow.FlowSources
+import semmle.code.java.security.ArithmeticCommon
+
+/**
+ * A taint-tracking configuration to reason about arithmetic overflow using local-user-controlled data.
+ */
+module ArithmeticTaintedLocalOverflowConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { source instanceof LocalUserInput }
+
+  predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
+
+  predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
+}
+
+/**
+ * Taint-tracking flow for arithmetic overflow using local-user-controlled data.
+ */
+module ArithmeticTaintedLocalOverflowFlow =
+  TaintTracking::Global<ArithmeticTaintedLocalOverflowConfig>;
+
+/**
+ * A taint-tracking configuration to reason about arithmetic underflow using local-user-controlled data.
+ */
+module ArithmeticTaintedLocalUnderflowConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { source instanceof LocalUserInput }
+
+  predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
+
+  predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
+}
+
+/**
+ * Taint-tracking flow for arithmetic underflow using local-user-controlled data.
+ */
+module ArithmeticTaintedLocalUnderflowFlow =
+  TaintTracking::Global<ArithmeticTaintedLocalUnderflowConfig>;

java/ql/lib/semmle/code/java/security/ArithmeticTaintedQuery.qll

@@ -0,0 +1,29 @@
+/** Provides taint-tracking configurations to reason about arithmetic with unvalidated user input. */
+
+import java
+private import semmle.code.java.dataflow.FlowSources
+private import semmle.code.java.security.ArithmeticCommon
+
+/** A taint-tracking configuration to reason about overflow from unvalidated user input. */
+module RemoteUserInputOverflowConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
+
+  predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
+
+  predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
+}
+
+/** A taint-tracking configuration to reason about underflow from unvalidated user input. */
+module RemoteUserInputUnderflowConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
+
+  predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
+
+  predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
+}
+
+/** Taint-tracking flow for overflow from unvalidated user input. */
+module RemoteUserInputOverflow = TaintTracking::Global<RemoteUserInputOverflowConfig>;
+
+/** Taint-tracking flow for underflow from unvalidated user input. */
+module RemoteUserInputUnderflow = TaintTracking::Global<RemoteUserInputUnderflowConfig>;

java/ql/lib/semmle/code/java/security/ArithmeticUncontrolledQuery.qll

@@ -0,0 +1,39 @@
+/** Provides taint-tracking configuration to reason about arithmetic with uncontrolled values. */
+
+import java
+import semmle.code.java.dataflow.TaintTracking
+private import semmle.code.java.security.RandomQuery
+private import semmle.code.java.security.SecurityTests
+private import semmle.code.java.security.ArithmeticCommon
+
+private class TaintSource extends DataFlow::ExprNode {
+  TaintSource() {
+    exists(RandomDataSource m | not m.resultMayBeBounded() | m.getOutput() = this.getExpr())
+  }
+}
+
+/** A taint-tracking configuration to reason about overflow from arithmetic with uncontrolled values. */
+module ArithmeticUncontrolledOverflowConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { source instanceof TaintSource }
+
+  predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
+
+  predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
+}
+
+/** Taint-tracking flow to reason about overflow from arithmetic with uncontrolled values. */
+module ArithmeticUncontrolledOverflowFlow =
+  TaintTracking::Global<ArithmeticUncontrolledOverflowConfig>;
+
+/** A taint-tracking configuration to reason about underflow from arithmetic with uncontrolled values. */
+module ArithmeticUncontrolledUnderflowConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { source instanceof TaintSource }
+
+  predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
+
+  predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
+}
+
+/** Taint-tracking flow to reason about underflow from arithmetic with uncontrolled values. */
+module ArithmeticUncontrolledUnderflowFlow =
+  TaintTracking::Global<ArithmeticUncontrolledUnderflowConfig>;

java/ql/lib/semmle/code/java/security/ArithmeticWithExtremeValuesQuery.qll

@@ -0,0 +1,61 @@
+/** Provides predicates and classes for reasoning about arithmetic with extreme values. */
+
+import java
+import semmle.code.java.dataflow.DataFlow
+import ArithmeticCommon
+
+/**
+ * A field representing an extreme value.
+ *
+ * For example, `Integer.MAX_VALUE` or `Long.MIN_VALUE`.
+ */
+abstract class ExtremeValueField extends Field {
+  ExtremeValueField() { this.getType() instanceof IntegralType }
+}
+
+/** A field representing the minimum value of a primitive type. */
+class MinValueField extends ExtremeValueField {
+  MinValueField() { this.getName() = "MIN_VALUE" }
+}
+
+/** A field representing the maximum value of a primitive type. */
+class MaxValueField extends ExtremeValueField {
+  MaxValueField() { this.getName() = "MAX_VALUE" }
+}
+
+/** A variable access that refers to an extreme value. */
+class ExtremeSource extends VarAccess {
+  ExtremeSource() { this.getVariable() instanceof ExtremeValueField }
+}
+
+/** A dataflow configuration which tracks flow from maximum values to an overflow. */
+module MaxValueFlowConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) {
+    source.asExpr().(ExtremeSource).getVariable() instanceof MaxValueField
+  }
+
+  predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
+
+  predicate isBarrierIn(DataFlow::Node n) { isSource(n) }
+
+  predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
+}
+
+/** Dataflow from maximum values to an underflow. */
+module MaxValueFlow = DataFlow::Global<MaxValueFlowConfig>;
+
+/** A dataflow configuration which tracks flow from minimum values to an underflow. */
+module MinValueFlowConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) {
+    source.asExpr().(ExtremeSource).getVariable() instanceof MinValueField
+  }
+
+  predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
+
+  predicate isBarrierIn(DataFlow::Node n) { isSource(n) }
+
+  predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
+}
+
+/** Dataflow from minimum values to an underflow. */
+module MinValueFlow = DataFlow::Global<MinValueFlowConfig>;