Merge pull request github#12721 from egregius313/egregius313/java/move-configurations-to-libraries

Java: Move more dataflow configurations to `*Query.qll` files

Author: egregius313

java/ql/lib/change-notes/2023-05-04-add-libraries-for-query-configurations.md

@@ -0,0 +1,31 @@
+---
+category: minorAnalysis
+---
+* Added the `ArithmeticCommon.qll` library to provide predicates for reasoning about arithmetic operations.
+* Added the `ArithmeticTaintedLocalQuery.qll` library to provide the `ArithmeticTaintedLocalOverflowFlow` and `ArithmeticTaintedLocalUnderflowFlow` taint-tracking modules to reason about arithmetic with unvalidated user input.
+* Added the `ArithmeticTaintedQuery.qll` library to provide the `RemoteUserInputOverflow` and `RemoteUserInputUnderflow` taint-tracking modules to reason about arithmetic with unvalidated user input.
+* Added the `ArithmeticUncontrolledQuery.qll` library to provide the `ArithmeticUncontrolledOverflowFlow`  and `ArithmeticUncontrolledUnderflowFlow` taint-tracking modules to reason about arithmetic with uncontrolled user input.
+* Added the `ArithmeticWithExtremeValuesQuery.qll` library to provide the `MaxValueFlow` and `MinValueFlow` dataflow modules to reason about arithmetic with extreme values.
+* Added the `BrokenCryptoAlgorithmQuery.qll` library to provide the `InsecureCryptoFlow` taint-tracking module to reason about broken cryptographic algorithm vulnerabilities.
+* Added the `ExecTaintedLocalQuery.qll` library to provide the `LocalUserInputToArgumentToExecFlow` taint-tracking module to reason about command injection vulnerabilities caused by local data flow.
+* Added the `ExternallyControlledFormatStringLocalQuery.qll` library to provide the `ExternallyControlledFormatStringLocalFlow` taint-tracking module to reason about format string vulnerabilities caused by local data flow.
+* Added the `ImproperValidationOfArrayConstructionCodeSpecifiedQuery.qll` library to provide the `BoundedFlowSourceFlow` dataflow module to reason about improper validation of code-specified sizes used for array construction.
+* Added the `ImproperValidationOfArrayConstructionLocalQuery.qll` library to provide the `ImproperValidationOfArrayConstructionLocalFlow` taint-tracking module to reason about improper validation of local user-provided sizes used for array construction caused by local data flow.
+* Added the `ImproperValidationOfArrayConstructionQuery.qll` library to provide the `ImproperValidationOfArrayConstructionFlow` taint-tracking module to reason about improper validation of user-provided size used for array construction.
+* Added the `ImproperValidationOfArrayIndexCodeSpecifiedQuery.qll` library to provide the `BoundedFlowSourceFlow` data flow module to reason about about improper validation of code-specified array index.
+* Added the `ImproperValidationOfArrayIndexLocalQuery.qll` library to provide the `ImproperValidationOfArrayIndexLocalFlow` taint-tracking module to reason about improper validation of a local user-provided array index.
+* Added the `ImproperValidationOfArrayIndexQuery.qll` library to provide the `ImproperValidationOfArrayIndexFlow` taint-tracking module to reason about improper validation of user-provided array index.
+* Added the `InsecureCookieQuery.qll` library to provide the `SecureCookieFlow` taint-tracking module to reason about insecure cookie vulnerabilities.
+* Added the `MaybeBrokenCryptoAlgorithmQuery.qll` library to provide the `InsecureCryptoFlow` taint-tracking module to reason about broken cryptographic algorithm vulnerabilities.
+* Added the `NumericCastTaintedQuery.qll` library to provide the `NumericCastTaintedFlow` taint-tracking module to reason about numeric cast vulnerabilities.
+* Added the `ResponseSplittingLocalQuery.qll` library to provide the `ResponseSplittingLocalFlow` taint-tracking module to reason about response splitting vulnerabilities caused by local data flow.
+* Added the `SqlConcatenatedQuery.qll` library to provide the `UncontrolledStringBuilderSourceFlow` taint-tracking module to reason about SQL injection vulnerabilities caused by concatenating untrusted strings.
+* Added the `SqlTaintedLocalQuery.qll` library to provide the `LocalUserInputToArgumentToSqlFlow` taint-tracking module to reason about SQL injection vulnerabilities caused by local data flow.
+* Added the `StackTraceExposureQuery.qll` library to provide the `printsStackExternally`, `stringifiedStackFlowsExternally`, and `getMessageFlowsExternally` predicates to reason about stack trace exposure vulnerabilities.
+* Added the `TaintedPermissionQuery.qll` library to provide the `TaintedPermissionFlow` taint-tracking module to reason about tainted permission vulnerabilities.
+* Added the `TempDirLocalInformationDisclosureQuery.qll` library to provide the `TempDirSystemGetPropertyToCreate` taint-tracking module to reason about local information disclosure vulnerabilities caused by local data flow.
+* Added the `UnsafeHostnameVerificationQuery.qll` library to provide the `TrustAllHostnameVerifierFlow` taint-tracking module to reason about insecure hostname verification vulnerabilities.
+* Added the `UrlRedirectLocalQuery.qll` library to provide the `UrlRedirectLocalFlow` taint-tracking module to reason about URL redirection vulnerabilities caused by local data flow.
+* Added the `UrlRedirectQuery.qll` library to provide the `UrlRedirectFlow` taint-tracking module to reason about URL redirection vulnerabilities.
+* Added the `XPathInjectionQuery.qll` library to provide the `XPathInjectionFlow` taint-tracking module to reason about XPath injection vulnerabilities.
+* Added the `XssLocalQuery.qll` library to provide the `XssLocalFlow` taint-tracking module to reason about XSS vulnerabilities caused by local data flow.

java/ql/src/Security/CWE/CWE-190/ArithmeticCommon.qll renamed to java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll

@@ -1,3 +1,5 @@
+/** Provides guards and predicates to reason about arithmetic. */
+
 import semmle.code.java.arithmetic.Overflow
 import semmle.code.java.controlflow.Guards
 private import semmle.code.java.dataflow.SSA

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
+private import semmle.code.java.dataflow.FlowSources
+private 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
+private 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
+private import semmle.code.java.dataflow.DataFlow
+private import semmle.code.java.security.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. */
+private class MinValueField extends ExtremeValueField {
+  MinValueField() { this.getName() = "MIN_VALUE" }
+}
+
+/** A field representing the maximum value of a primitive type. */
+private 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>;

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

@@ -0,0 +1,38 @@
+/** Provides to taint-tracking configuration to reason about the use of broken or risky cryptographic algorithms. */
+
+import java
+private import semmle.code.java.security.Encryption
+private import semmle.code.java.dataflow.TaintTracking
+
+private class ShortStringLiteral extends StringLiteral {
+  ShortStringLiteral() { this.getValue().length() < 100 }
+}
+
+/**
+ * A string literal that may refer to a broken or risky cryptographic algorithm.
+ */
+class BrokenAlgoLiteral extends ShortStringLiteral {
+  BrokenAlgoLiteral() {
+    this.getValue().regexpMatch(getInsecureAlgorithmRegex()) and
+    // Exclude German and French sentences.
+    not this.getValue().regexpMatch(".*\\p{IsLowercase} des \\p{IsLetter}.*")
+  }
+}
+
+/**
+ * A taint-tracking configuration to reason about the use of broken or risky cryptographic algorithms.
+ */
+module InsecureCryptoConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node n) { n.asExpr() instanceof BrokenAlgoLiteral }
+
+  predicate isSink(DataFlow::Node n) { exists(CryptoAlgoSpec c | n.asExpr() = c.getAlgoSpec()) }
+
+  predicate isBarrier(DataFlow::Node node) {
+    node.getType() instanceof PrimitiveType or node.getType() instanceof BoxedType
+  }
+}
+
+/**
+ * Taint-tracking flow for use of broken or risky cryptographic algorithms.
+ */
+module InsecureCryptoFlow = TaintTracking::Global<InsecureCryptoConfig>;

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

@@ -0,0 +1,26 @@
+/** Provides a taint-tracking configuration to reason about use of externally controlled strings for command injection vulnerabilities. */
+
+import java
+private import semmle.code.java.dataflow.FlowSources
+private import semmle.code.java.security.ExternalProcess
+private import semmle.code.java.security.CommandArguments
+
+/** A taint-tracking configuration to reason about use of externally controlled strings to make command line commands. */
+module ExecTaintedLocalConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node src) { src instanceof LocalUserInput }
+
+  predicate isSink(DataFlow::Node sink) { sink.asExpr() instanceof ArgumentToExec }
+
+  predicate isBarrier(DataFlow::Node node) {
+    node.getType() instanceof PrimitiveType
+    or
+    node.getType() instanceof BoxedType
+    or
+    isSafeCommandArgument(node.asExpr())
+  }
+}
+
+/**
+ * Taint-tracking flow for use of externally controlled strings to make command line commands.
+ */
+module ExecTaintedLocalFlow = TaintTracking::Global<ExecTaintedLocalConfig>;

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

@@ -0,0 +1,20 @@
+/** Provides a taint-tracking configuration to reason about externally-controlled format strings from local sources. */
+
+import java
+private import semmle.code.java.dataflow.FlowSources
+private import semmle.code.java.StringFormat
+
+/** A taint-tracking configuration to reason about externally-controlled format strings from local sources. */
+module ExternallyControlledFormatStringLocalConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { source instanceof LocalUserInput }
+
+  predicate isSink(DataFlow::Node sink) {
+    sink.asExpr() = any(StringFormat formatCall).getFormatArgument()
+  }
+}
+
+/**
+ * Taint-tracking flow for externally-controlled format strings from local sources.
+ */
+module ExternallyControlledFormatStringLocalFlow =
+  TaintTracking::Global<ExternallyControlledFormatStringLocalConfig>;

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

@@ -0,0 +1,25 @@
+/** Provides a dataflow configuration to reason about improper validation of code-specified size used for array construction. */
+
+import java
+private import semmle.code.java.security.internal.ArraySizing
+private import semmle.code.java.dataflow.TaintTracking
+
+/**
+ * A dataflow configuration to reason about improper validation of code-specified size used for array construction.
+ */
+module BoundedFlowSourceConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) {
+    source instanceof BoundedFlowSource and
+    // There is not a fixed lower bound which is greater than zero.
+    not source.(BoundedFlowSource).lowerBound() > 0
+  }
+
+  predicate isSink(DataFlow::Node sink) {
+    any(CheckableArrayAccess caa).canThrowOutOfBoundsDueToEmptyArray(sink.asExpr(), _)
+  }
+}
+
+/**
+ * Dataflow flow for improper validation of code-specified size used for array construction.
+ */
+module BoundedFlowSourceFlow = DataFlow::Global<BoundedFlowSourceConfig>;