Skip to content

Commit b087cf9

Browse files
egregius313egregius313
committed
Add Arithmetic query libraries
1 parent b6361cd commit b087cf9

9 files changed

+183
-126
lines changed

‎java/ql/lib/change-notes/2023-03-30-add-libraries-for-query-configurations.md

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,4 +15,8 @@ category: minorAnalysis
1515
* Added the `BrokenCryptoAlgorithmQuery.qll` library to provide the `InsecureCryptoFlow` taint-tracking module to reason about broken cryptographic algorithm vulnerabilities.
1616
* Added the `NumericCastTaintedQuery.qll` library to provide the `NumericCastTaintedFlow` taint-tracking module to reason about numeric cast vulnerabilities.
1717
* Added the `ResponseSplittingLocalQuery.qll` library to provide the `ResponseSplittingLocalFlow` taint-tracking module to reason about response splitting vulnerabilities caused by local data flow.
18-
* Added the `UnsafeHostnameVerificationQuery.qll` library to provide the `TrustAllHostnameVerifierFlow` taint-tracking module to reason about insecure hostname verification vulnerabilities.
18+
* Added the `UnsafeHostnameVerificationQuery.qll` library to provide the `TrustAllHostnameVerifierFlow` taint-tracking module to reason about insecure hostname verification vulnerabilities.
19+
* Added the `ArithmeticCommon.qll` library to provide predicates for reasoning about arithmetic operations.
20+
* Added the `ArithmeticTaintedQuery.qll` library to provide the `RemoteUserInputOverflow` and `RemoteUserInputUnderflow` taint-tracking modules to reason about arithmetic with unvalidated user input.
21+
* Added the `ArithmeticUncontrolledQuery.qll` library to provide the `ArithmeticUncontrolledOverflowFlow` and `ArithmeticUncontrolledUnderflowFlow` taint-tracking modules to reason about arithmetic with uncontrolled user input.
22+
* Added the `ArithmeticWithExtremeValuesQuery.qll` library to provide the `MaxValueFlow` and `MinValueFlow` dataflow modules to reason about arithmetic with extreme values.

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

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
/** Provides taint-tracking configurations to reason about arithmetic using local-user-controlled data. */
2+
3+
import java
4+
import semmle.code.java.dataflow.FlowSources
5+
import semmle.code.java.security.ArithmeticCommon
6+
7+
/**
8+
* A taint-tracking configuration to reason about arithmetic overflow using local-user-controlled data.
9+
*/
10+
module ArithmeticTaintedLocalOverflowConfig implements DataFlow::ConfigSig {
11+
predicate isSource(DataFlow::Node source) { source instanceof LocalUserInput }
12+
13+
predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
14+
15+
predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
16+
}
17+
18+
/**
19+
* Taint-tracking flow for arithmetic overflow using local-user-controlled data.
20+
*/
21+
module ArithmeticTaintedLocalOverflowFlow =
22+
TaintTracking::Global<ArithmeticTaintedLocalOverflowConfig>;
23+
24+
/**
25+
* A taint-tracking configuration to reason about arithmetic underflow using local-user-controlled data.
26+
*/
27+
module ArithmeticTaintedLocalUnderflowConfig implements DataFlow::ConfigSig {
28+
predicate isSource(DataFlow::Node source) { source instanceof LocalUserInput }
29+
30+
predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
31+
32+
predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
33+
}
34+
35+
/**
36+
* Taint-tracking flow for arithmetic underflow using local-user-controlled data.
37+
*/
38+
module ArithmeticTaintedLocalUnderflowFlow =
39+
TaintTracking::Global<ArithmeticTaintedLocalUnderflowConfig>;

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

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
/** Provides taint-tracking configurations to reason about arithmetic with unvalidated user input. */
2+
3+
import java
4+
private import semmle.code.java.dataflow.FlowSources
5+
private import semmle.code.java.security.ArithmeticCommon
6+
7+
/** A taint-tracking configuration to reason about overflow from unvalidated user input. */
8+
module RemoteUserInputOverflowConfig implements DataFlow::ConfigSig {
9+
predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
10+
11+
predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
12+
13+
predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
14+
}
15+
16+
/** A taint-tracking configuration to reason about underflow from unvalidated user input. */
17+
module RemoteUserInputUnderflowConfig implements DataFlow::ConfigSig {
18+
predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
19+
20+
predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
21+
22+
predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
23+
}
24+
25+
/** Taint-tracking flow for overflow from unvalidated user input. */
26+
module RemoteUserInputOverflow = TaintTracking::Global<RemoteUserInputOverflowConfig>;
27+
28+
/** Taint-tracking flow for underflow from unvalidated user input. */
29+
module RemoteUserInputUnderflow = TaintTracking::Global<RemoteUserInputUnderflowConfig>;

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

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
/** Provides taint-tracking configuration to reason about arithmetic with uncontrolled values. */
2+
3+
import java
4+
import semmle.code.java.dataflow.TaintTracking
5+
private import semmle.code.java.security.RandomQuery
6+
private import semmle.code.java.security.SecurityTests
7+
private import semmle.code.java.security.ArithmeticCommon
8+
9+
private class TaintSource extends DataFlow::ExprNode {
10+
TaintSource() {
11+
exists(RandomDataSource m | not m.resultMayBeBounded() | m.getOutput() = this.getExpr())
12+
}
13+
}
14+
15+
/** A taint-tracking configuration to reason about overflow from arithmetic with uncontrolled values. */
16+
module ArithmeticUncontrolledOverflowConfig implements DataFlow::ConfigSig {
17+
predicate isSource(DataFlow::Node source) { source instanceof TaintSource }
18+
19+
predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
20+
21+
predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
22+
}
23+
24+
/** Taint-tracking flow to reason about overflow from arithmetic with uncontrolled values. */
25+
module ArithmeticUncontrolledOverflowFlow =
26+
TaintTracking::Global<ArithmeticUncontrolledOverflowConfig>;
27+
28+
/** A taint-tracking configuration to reason about underflow from arithmetic with uncontrolled values. */
29+
module ArithmeticUncontrolledUnderflowConfig implements DataFlow::ConfigSig {
30+
predicate isSource(DataFlow::Node source) { source instanceof TaintSource }
31+
32+
predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
33+
34+
predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
35+
}
36+
37+
/** Taint-tracking flow to reason about underflow from arithmetic with uncontrolled values. */
38+
module ArithmeticUncontrolledUnderflowFlow =
39+
TaintTracking::Global<ArithmeticUncontrolledUnderflowConfig>;

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

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
/** Provides predicates and classes for reasoning about arithmetic with extreme values. */
2+
3+
import java
4+
import semmle.code.java.dataflow.DataFlow
5+
import ArithmeticCommon
6+
7+
/**
8+
* A field representing an extreme value.
9+
*
10+
* For example, `Integer.MAX_VALUE` or `Long.MIN_VALUE`.
11+
*/
12+
abstract class ExtremeValueField extends Field {
13+
ExtremeValueField() { this.getType() instanceof IntegralType }
14+
}
15+
16+
/** A field representing the minimum value of a primitive type. */
17+
class MinValueField extends ExtremeValueField {
18+
MinValueField() { this.getName() = "MIN_VALUE" }
19+
}
20+
21+
/** A field representing the maximum value of a primitive type. */
22+
class MaxValueField extends ExtremeValueField {
23+
MaxValueField() { this.getName() = "MAX_VALUE" }
24+
}
25+
26+
/** A variable access that refers to an extreme value. */
27+
class ExtremeSource extends VarAccess {
28+
ExtremeSource() { this.getVariable() instanceof ExtremeValueField }
29+
}
30+
31+
/** A dataflow configuration which tracks flow from maximum values to an overflow. */
32+
module MaxValueFlowConfig implements DataFlow::ConfigSig {
33+
predicate isSource(DataFlow::Node source) {
34+
source.asExpr().(ExtremeSource).getVariable() instanceof MaxValueField
35+
}
36+
37+
predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
38+
39+
predicate isBarrierIn(DataFlow::Node n) { isSource(n) }
40+
41+
predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
42+
}
43+
44+
/** Dataflow from maximum values to an underflow. */
45+
module MaxValueFlow = DataFlow::Global<MaxValueFlowConfig>;
46+
47+
/** A dataflow configuration which tracks flow from minimum values to an underflow. */
48+
module MinValueFlowConfig implements DataFlow::ConfigSig {
49+
predicate isSource(DataFlow::Node source) {
50+
source.asExpr().(ExtremeSource).getVariable() instanceof MinValueField
51+
}
52+
53+
predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
54+
55+
predicate isBarrierIn(DataFlow::Node n) { isSource(n) }
56+
57+
predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
58+
}
59+
60+
/** Dataflow from minimum values to an underflow. */
61+
module MinValueFlow = DataFlow::Global<MinValueFlowConfig>;

‎java/ql/src/Security/CWE/CWE-190/ArithmeticTainted.ql

Lines changed: 3 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -13,28 +13,9 @@
1313
*/
1414

1515
import java
16-
import semmle.code.java.dataflow.FlowSources
17-
import ArithmeticCommon
18-
19-
module RemoteUserInputOverflowConfig implements DataFlow::ConfigSig {
20-
predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
21-
22-
predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
23-
24-
predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
25-
}
26-
27-
module RemoteUserInputUnderflowConfig implements DataFlow::ConfigSig {
28-
predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
29-
30-
predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
31-
32-
predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
33-
}
34-
35-
module RemoteUserInputOverflow = TaintTracking::Global<RemoteUserInputOverflowConfig>;
36-
37-
module RemoteUserInputUnderflow = TaintTracking::Global<RemoteUserInputUnderflowConfig>;
16+
import semmle.code.java.dataflow.DataFlow
17+
import semmle.code.java.security.ArithmeticCommon
18+
import semmle.code.java.security.ArithmeticTaintedQuery
3819

3920
module Flow =
4021
DataFlow::MergePathGraph<RemoteUserInputOverflow::PathNode, RemoteUserInputUnderflow::PathNode,

‎java/ql/src/Security/CWE/CWE-190/ArithmeticTaintedLocal.ql

Lines changed: 1 addition & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -13,30 +13,7 @@
1313
*/
1414

1515
import java
16-
import semmle.code.java.dataflow.FlowSources
17-
import ArithmeticCommon
18-
19-
module ArithmeticTaintedLocalOverflowConfig implements DataFlow::ConfigSig {
20-
predicate isSource(DataFlow::Node source) { source instanceof LocalUserInput }
21-
22-
predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
23-
24-
predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
25-
}
26-
27-
module ArithmeticTaintedLocalOverflowFlow =
28-
TaintTracking::Global<ArithmeticTaintedLocalOverflowConfig>;
29-
30-
module ArithmeticTaintedLocalUnderflowConfig implements DataFlow::ConfigSig {
31-
predicate isSource(DataFlow::Node source) { source instanceof LocalUserInput }
32-
33-
predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
34-
35-
predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
36-
}
37-
38-
module ArithmeticTaintedLocalUnderflowFlow =
39-
TaintTracking::Global<ArithmeticTaintedLocalUnderflowConfig>;
16+
import semmle.code.java.security.ArithmeticTaintedLocalQuery
4017

4118
module Flow =
4219
DataFlow::MergePathGraph<ArithmeticTaintedLocalOverflowFlow::PathNode,

‎java/ql/src/Security/CWE/CWE-190/ArithmeticUncontrolled.ql

Lines changed: 3 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -13,38 +13,9 @@
1313
*/
1414

1515
import java
16-
import semmle.code.java.dataflow.TaintTracking
17-
import semmle.code.java.security.RandomQuery
18-
import semmle.code.java.security.SecurityTests
19-
import ArithmeticCommon
20-
21-
class TaintSource extends DataFlow::ExprNode {
22-
TaintSource() {
23-
exists(RandomDataSource m | not m.resultMayBeBounded() | m.getOutput() = this.getExpr())
24-
}
25-
}
26-
27-
module ArithmeticUncontrolledOverflowConfig implements DataFlow::ConfigSig {
28-
predicate isSource(DataFlow::Node source) { source instanceof TaintSource }
29-
30-
predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
31-
32-
predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
33-
}
34-
35-
module ArithmeticUncontrolledOverflowFlow =
36-
TaintTracking::Global<ArithmeticUncontrolledOverflowConfig>;
37-
38-
module ArithmeticUncontrolledUnderflowConfig implements DataFlow::ConfigSig {
39-
predicate isSource(DataFlow::Node source) { source instanceof TaintSource }
40-
41-
predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
42-
43-
predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
44-
}
45-
46-
module ArithmeticUncontrolledUnderflowFlow =
47-
TaintTracking::Global<ArithmeticUncontrolledUnderflowConfig>;
16+
import semmle.code.java.dataflow.DataFlow
17+
import semmle.code.java.security.ArithmeticCommon
18+
import semmle.code.java.security.ArithmeticUncontrolledQuery
4819

4920
module Flow =
5021
DataFlow::MergePathGraph<ArithmeticUncontrolledOverflowFlow::PathNode,

‎java/ql/src/Security/CWE/CWE-190/ArithmeticWithExtremeValues.ql

Lines changed: 3 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -15,58 +15,14 @@
1515

1616
import java
1717
import semmle.code.java.dataflow.DataFlow
18-
import ArithmeticCommon
19-
20-
abstract class ExtremeValueField extends Field {
21-
ExtremeValueField() { this.getType() instanceof IntegralType }
22-
}
23-
24-
class MinValueField extends ExtremeValueField {
25-
MinValueField() { this.getName() = "MIN_VALUE" }
26-
}
27-
28-
class MaxValueField extends ExtremeValueField {
29-
MaxValueField() { this.getName() = "MAX_VALUE" }
30-
}
31-
32-
class ExtremeSource extends VarAccess {
33-
ExtremeSource() { this.getVariable() instanceof ExtremeValueField }
34-
}
35-
36-
module MaxValueFlowConfig implements DataFlow::ConfigSig {
37-
predicate isSource(DataFlow::Node source) {
38-
source.asExpr().(ExtremeSource).getVariable() instanceof MaxValueField
39-
}
40-
41-
predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
42-
43-
predicate isBarrierIn(DataFlow::Node n) { isSource(n) }
44-
45-
predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
46-
}
47-
48-
module MaxValueFlow = DataFlow::Global<MaxValueFlowConfig>;
49-
50-
module MinValueFlowConfig implements DataFlow::ConfigSig {
51-
predicate isSource(DataFlow::Node source) {
52-
source.asExpr().(ExtremeSource).getVariable() instanceof MinValueField
53-
}
54-
55-
predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
56-
57-
predicate isBarrierIn(DataFlow::Node n) { isSource(n) }
58-
59-
predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
60-
}
61-
62-
module MinValueFlow = DataFlow::Global<MinValueFlowConfig>;
18+
import semmle.code.java.security.ArithmeticCommon
19+
import semmle.code.java.security.ArithmeticWithExtremeValuesQuery
20+
import Flow::PathGraph
6321

6422
module Flow =
6523
DataFlow::MergePathGraph<MaxValueFlow::PathNode, MinValueFlow::PathNode, MaxValueFlow::PathGraph,
6624
MinValueFlow::PathGraph>;
6725

68-
import Flow::PathGraph
69-
7026
predicate query(
7127
Flow::PathNode source, Flow::PathNode sink, ArithExpr exp, string effect, Type srctyp
7228
) {

0 commit comments

Comments
 (0)