Java: Add support for boolean MaD barrier guards.

aschackmull · aschackmull · commit 1fe1703060dd · 2025-12-10T09:55:57.000+01:00
diff --git a/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll b/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll
@@ -91,6 +91,7 @@ module;
 
 import java
 private import semmle.code.java.dataflow.DataFlow::DataFlow
+private import semmle.code.java.controlflow.Guards
 private import FlowSummary as FlowSummary
 private import internal.DataFlowPrivate
 private import internal.FlowSummaryImpl
@@ -183,6 +184,15 @@ predicate barrierModel(
     madId)
 }
 
+/** Holds if a barrier guard model exists for the given parameters. */
+predicate barrierGuardModel(
+  string package, string type, boolean subtypes, string name, string signature, string ext,
+  string input, string acceptingvalue, string kind, string provenance, QlBuiltins::ExtensionId madId
+) {
+  Extensions::barrierGuardModel(package, type, subtypes, name, signature, ext, input,
+    acceptingvalue, kind, provenance, madId)
+}
+
 /** Holds if a summary model exists for the given parameters. */
 predicate summaryModel(
   string package, string type, boolean subtypes, string name, string signature, string ext,
@@ -315,7 +325,8 @@ module ModelValidation {
     summaryModel(_, _, _, _, _, _, _, path, _, _, _) or
     sinkModel(_, _, _, _, _, _, path, _, _, _) or
     sourceModel(_, _, _, _, _, _, path, _, _, _) or
-    barrierModel(_, _, _, _, _, _, path, _, _, _)
+    barrierModel(_, _, _, _, _, _, path, _, _, _) or
+    barrierGuardModel(_, _, _, _, _, _, path, _, _, _, _)
   }
 
   private module MkAccessPath = AccessPathSyntax::AccessPath<getRelevantAccessPath/1>;
@@ -328,6 +339,8 @@ module ModelValidation {
     exists(string pred, AccessPath input, AccessPathToken part |
       sinkModel(_, _, _, _, _, _, input, _, _, _) and pred = "sink"
       or
+      barrierGuardModel(_, _, _, _, _, _, input, _, _, _, _) and pred = "barrier guard"
+      or
       summaryModel(_, _, _, _, _, _, input, _, _, _, _) and pred = "summary"
     |
       (
@@ -373,6 +386,8 @@ module ModelValidation {
       sinkModel(_, _, _, _, _, _, _, kind, _, _)
       or
       barrierModel(_, _, _, _, _, _, _, kind, _, _)
+      or
+      barrierGuardModel(_, _, _, _, _, _, _, _, kind, _, _)
     }
 
     predicate sourceKind(string kind) { sourceModel(_, _, _, _, _, _, _, kind, _, _) }
@@ -393,6 +408,9 @@ module ModelValidation {
       or
       barrierModel(package, type, _, name, signature, ext, _, _, provenance, _) and pred = "barrier"
       or
+      barrierGuardModel(package, type, _, name, signature, ext, _, _, _, provenance, _) and
+      pred = "barrier guard"
+      or
       summaryModel(package, type, _, name, signature, ext, _, _, _, provenance, _) and
       pred = "summary"
       or
@@ -418,6 +436,14 @@ module ModelValidation {
       invalidProvenance(provenance) and
       result = "Unrecognized provenance description \"" + provenance + "\" in " + pred + " model."
     )
+    or
+    exists(string acceptingvalue |
+      barrierGuardModel(_, _, _, _, _, _, _, acceptingvalue, _, _, _) and
+      invalidAcceptingValue(acceptingvalue) and
+      result =
+        "Unrecognized accepting value description \"" + acceptingvalue +
+          "\" in barrier guard model."
+    )
   }
 
   /** Holds if some row in a MaD flow model appears to contain typos. */
@@ -440,6 +466,8 @@ private predicate elementSpec(
   or
   barrierModel(package, type, subtypes, name, signature, ext, _, _, _, _)
   or
+  barrierGuardModel(package, type, subtypes, name, signature, ext, _, _, _, _, _)
+  or
   summaryModel(package, type, subtypes, name, signature, ext, _, _, _, _, _)
   or
   neutralModel(package, type, name, signature, _, _) and ext = "" and subtypes = true
@@ -601,6 +629,46 @@ private module Cached {
     )
   }
 
+  private newtype TKindModelPair =
+    TMkPair(string kind, string model) { isBarrierGuardNode(_, _, kind, model) }
+
+  private boolean convertAcceptingValue(AcceptingValue av) {
+    av.isTrue() and result = true
+    or
+    av.isFalse() and result = false
+  }
+
+  // private GuardValue convertAcceptingValue(AcceptingValue av) {
+  //   av.isTrue() and result.asBooleanValue() = true
+  //   or
+  //   av.isFalse() and result.asBooleanValue() = false
+  //   or
+  //   av.isNoException() and result.getDualValue().isThrowsException()
+  //   or
+  //   av.isZero() and result.asIntValue() = 0
+  //   or
+  //   av.isNotZero() and result.getDualValue().asIntValue() = 0
+  //   or
+  //   av.isNull() and result.isNullValue()
+  //   or
+  //   av.isNotNull() and result.isNonNullValue()
+  // }
+  // private predicate barrierGuardChecks(Guard g, Expr e, GuardValue gv, TKindModelPair kmp) {
+  private predicate barrierGuardChecks(Guard g, Expr e, boolean branch, TKindModelPair kmp) {
+    exists(
+      SourceSinkInterpretationInput::InterpretNode n, AcceptingValue acceptingvalue, string kind,
+      string model
+    |
+      isBarrierGuardNode(n, acceptingvalue, kind, model) and
+      n.asNode().asExpr() = e and
+      kmp = TMkPair(kind, model) and
+      // gv = convertAcceptingValue(acceptingvalue)
+      branch = convertAcceptingValue(acceptingvalue)
+    |
+      g.(Call).getAnArgument() = e or g.(MethodCall).getQualifier() = e
+    )
+  }
+
   /**
    * Holds if `node` is specified as a barrier with the given kind in a MaD flow
    * model.
@@ -610,6 +678,9 @@ private module Cached {
     exists(SourceSinkInterpretationInput::InterpretNode n |
       isBarrierNode(n, kind, model) and n.asNode() = node
     )
+    or
+    ParameterizedBarrierGuard<TKindModelPair, barrierGuardChecks/4>::getABarrierNode(TMkPair(kind,
+        model)) = node
   }
 }
 
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowUtil.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowUtil.qll
@@ -396,3 +396,32 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
       SsaImpl::DataFlowIntegration::BarrierGuard<guardChecks/3>::getABarrierNode()
   }
 }
+
+bindingset[this]
+signature class ParamSig;
+
+module WithParam<ParamSig P> {
+  /**
+   * Holds if the guard `g` validates the expression `e` upon evaluating to `gv`.
+   *
+   * The expression `e` is expected to be a syntactic part of the guard `g`.
+   * For example, the guard `g` might be a call `isSafe(x)` and the expression `e`
+   * the argument `x`.
+   */
+  // signature predicate guardChecksSig(Guard g, Expr e, GuardValue gv, P param);
+  signature predicate guardChecksSig(Guard g, Expr e, boolean branch, P param);
+}
+
+/**
+ * Provides a set of barrier nodes for a guard that validates an expression.
+ *
+ * This is expected to be used in `isBarrier`/`isSanitizer` definitions
+ * in data flow and taint tracking.
+ */
+module ParameterizedBarrierGuard<ParamSig P, WithParam<P>::guardChecksSig/4 guardChecks> {
+  /** Gets a node that is safely guarded by the given guard check. */
+  Node getABarrierNode(P param) {
+    SsaFlow::asNode(result) =
+      SsaImpl::DataFlowIntegration::ParameterizedBarrierGuard<P, guardChecks/4>::getABarrierNode(param)
+  }
+}
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/ExternalFlowExtensions.qll b/java/ql/lib/semmle/code/java/dataflow/internal/ExternalFlowExtensions.qll
@@ -28,6 +28,14 @@ extensible predicate barrierModel(
   string output, string kind, string provenance, QlBuiltins::ExtensionId madId
 );
 
+/**
+ * Holds if a barrier guard model exists for the given parameters.
+ */
+extensible predicate barrierGuardModel(
+  string package, string type, boolean subtypes, string name, string signature, string ext,
+  string input, string acceptingvalue, string kind, string provenance, QlBuiltins::ExtensionId madId
+);
+
 /**
  * Holds if a summary model exists for the given parameters.
  */
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll
@@ -159,7 +159,8 @@ private predicate relatedArgSpec(Callable c, string spec) {
     summaryModel(namespace, type, subtypes, name, signature, ext, _, spec, _, _, _) or
     sourceModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _) or
     sinkModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _) or
-    barrierModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _)
+    barrierModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _) or
+    barrierGuardModel(namespace, type, subtypes, name, signature, ext, spec, _, _, _, _)
   |
     c = interpretElement(namespace, type, subtypes, name, signature, ext, _)
   )
@@ -267,8 +268,28 @@ module SourceSinkInterpretationInput implements
       string namespace, string type, boolean subtypes, string name, string signature, string ext,
       SourceOrSinkElement baseBarrier, string originalOutput, QlBuiltins::ExtensionId madId
     |
-      barrierModel(namespace, type, subtypes, name, signature, ext, originalOutput, kind, provenance,
-        madId) and
+      barrierModel(namespace, type, subtypes, name, signature, ext, originalOutput, kind,
+        provenance, madId) and
+      model = "MaD:" + madId.toString() and
+      baseBarrier = interpretElement(namespace, type, subtypes, name, signature, ext, _) and
+      (
+        e = baseBarrier and output = originalOutput
+        or
+        correspondingKotlinParameterDefaultsArgSpec(baseBarrier, e, originalOutput, output)
+      )
+    )
+  }
+
+  predicate barrierGuardElement(
+    Element e, string output, Public::AcceptingValue acceptingvalue, string kind,
+    Public::Provenance provenance, string model
+  ) {
+    exists(
+      string namespace, string type, boolean subtypes, string name, string signature, string ext,
+      SourceOrSinkElement baseBarrier, string originalOutput, QlBuiltins::ExtensionId madId
+    |
+      barrierGuardModel(namespace, type, subtypes, name, signature, ext, originalOutput,
+        acceptingvalue, kind, provenance, madId) and
       model = "MaD:" + madId.toString() and
       baseBarrier = interpretElement(namespace, type, subtypes, name, signature, ext, _) and
       (
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
@@ -586,6 +586,41 @@ private module Cached {
 
       predicate getABarrierNode = getABarrierNodeImpl/0;
     }
+
+    bindingset[this]
+    signature class ParamSig;
+
+    cached // nothing is actually cached
+    module WithParam<ParamSig P> {
+      // signature predicate guardChecksSig(Guards::Guard g, Expr e, Guards::GuardValue gv, P param);
+      signature predicate guardChecksSig(Guards::Guard g, Expr e, boolean branch, P param);
+    }
+
+    cached // nothing is actually cached
+    module ParameterizedBarrierGuard<ParamSig P, WithParam<P>::guardChecksSig/4 guardChecks> {
+      // private predicate guardChecksAdjTypes(Guards::Guards_v3::Guard g, Expr e, Guards::GuardValue gv, P param) {
+      //   guardChecks(g, e, gv, param)
+      // }
+      private predicate guardChecksAdjTypes(
+        Guards::Guards_v3::Guard g, Expr e, boolean branch, P param
+      ) {
+        guardChecks(g, e, branch, param)
+      }
+
+      private predicate guardChecksWithWrappers(
+        DataFlowIntegrationInput::Guard g, Definition def, Guards::GuardValue val, P param
+      ) {
+        Guards::Guards_v3::ValidationWrapperWithState<P, guardChecksAdjTypes/4>::guardChecksDef(g,
+          def, val, param)
+      }
+
+      private Node getABarrierNodeImpl(P param) {
+        result =
+          DataFlowIntegrationImpl::BarrierGuardDefWithState<P, guardChecksWithWrappers/4>::getABarrierNode(param)
+      }
+
+      predicate getABarrierNode = getABarrierNodeImpl/1;
+    }
   }
 
   cached
diff --git a/shared/dataflow/codeql/dataflow/internal/FlowSummaryImpl.qll b/shared/dataflow/codeql/dataflow/internal/FlowSummaryImpl.qll
@@ -215,6 +215,35 @@ module Make<
         ]
     }
 
+    class AcceptingValue extends string {
+      AcceptingValue() {
+        this =
+          [
+            "true",
+            "false",
+            "no-exception",
+            "zero",
+            "not-zero",
+            "null",
+            "not-null",
+          ]
+      }
+
+      predicate isTrue() { this = "true" }
+
+      predicate isFalse() { this = "false" }
+
+      predicate isNoException() { this = "no-exception" }
+
+      predicate isZero() { this = "zero" }
+
+      predicate isNotZero() { this = "not-zero" }
+
+      predicate isNull() { this = "null" }
+
+      predicate isNotNull() { this = "not-null" }
+    }
+
     /**
      * A class used to represent provenance values for MaD models.
      *
@@ -2015,6 +2044,12 @@ module Make<
         not exists(interpretComponent(c))
       }
 
+      /** Holds if `acceptingvalue` is not a valid barrier guard accepting-value. */
+      bindingset[acceptingvalue]
+      predicate invalidAcceptingValue(string acceptingvalue) {
+        not acceptingvalue instanceof AcceptingValue
+      }
+
       /** Holds if `provenance` is not a valid provenance value. */
       bindingset[provenance]
       predicate invalidProvenance(string provenance) { not provenance instanceof Provenance }
@@ -2060,6 +2095,15 @@ module Make<
           Element n, string output, string kind, Provenance provenance, string model
         );
 
+        /**
+         * Holds if an external barrier guard specification exists for `n` with input
+         * specification `input`, accepting value `acceptingvalue`, and kind `kind`.
+         */
+        predicate barrierGuardElement(
+          Element n, string input, AcceptingValue acceptingvalue, string kind,
+          Provenance provenance, string model
+        );
+
         class SourceOrSinkElement extends Element;
 
         /** An entity used to interpret a source/sink specification. */
@@ -2114,7 +2158,8 @@ module Make<
         private predicate sourceSinkSpec(string spec) {
           sourceElement(_, spec, _, _, _) or
           sinkElement(_, spec, _, _, _) or
-          barrierElement(_, spec, _, _, _)
+          barrierElement(_, spec, _, _, _) or
+          barrierGuardElement(_, spec, _, _, _, _)
         }
 
         private module AccessPath = AccessPathSyntax::AccessPath<sourceSinkSpec/1>;
@@ -2180,6 +2225,18 @@ module Make<
           )
         }
 
+        private predicate barrierGuardElementRef(
+          InterpretNode ref, SourceSinkAccessPath input, AcceptingValue acceptingvalue, string kind,
+          string model
+        ) {
+          exists(SourceOrSinkElement e |
+            barrierGuardElement(e, input, acceptingvalue, kind, _, model) and
+            if inputNeedsReferenceExt(input.getToken(0))
+            then e = ref.getCallTarget()
+            else e = ref.asElement()
+          )
+        }
+
         /** Holds if the first `n` tokens of `output` resolve to the given interpretation. */
         private predicate interpretOutput(
           SourceSinkAccessPath output, int n, InterpretNode ref, InterpretNode node
@@ -2240,7 +2297,7 @@ module Make<
         private predicate interpretInput(
           SourceSinkAccessPath input, int n, InterpretNode ref, InterpretNode node
         ) {
-          sinkElementRef(ref, input, _, _) and
+          (sinkElementRef(ref, input, _, _) or barrierGuardElementRef(ref, input, _, _, _)) and
           n = 0 and
           (
             if input = ""
@@ -2311,6 +2368,19 @@ module Make<
           )
         }
 
+        /**
+         * Holds if `node` is specified as a barrier guard argument with the
+         * given kind in a MaD flow model.
+         */
+        predicate isBarrierGuardNode(
+          InterpretNode node, AcceptingValue acceptingvalue, string kind, string model
+        ) {
+          exists(InterpretNode ref, SourceSinkAccessPath input |
+            barrierGuardElementRef(ref, input, acceptingvalue, kind, model) and
+            interpretInput(input, input.getNumToken(), ref, node)
+          )
+        }
+
         final private class SourceOrSinkElementFinal = SourceOrSinkElement;
 
         signature predicate sourceOrSinkElementSig(
