Merge pull request #21475 from owen-mc/rust/mad-barriers

Rust: Add support for defining barriers and barrier guards using models-as-data

rust/ql/lib/codeql/rust/dataflow/FlowBarrier.qll

@@ -0,0 +1,85 @@
+/**
+ * Provides classes and predicates for defining barriers and barrier guards.
+ *
+ * Flow barriers and barrier guards defined here feed into data flow configurations as follows:
+ *
+ * ```text
+ * data from *.model.yml | QL extensions of FlowBarrier::Range
+ *  v                       v
+ * FlowBarrier (associated with a models-as-data kind string)
+ *  v
+ * barrierNode predicate | other QL defined barriers, for example using concepts
+ *  v                    v
+ * various Barrier classes for specific data flow configurations
+ *
+ * data from *.model.yml | QL extensions of FlowBarrierGuard::Range
+ *  v                       v
+ * FlowBarrierGuard (associated with a models-as-data kind string)
+ *  v
+ * barrierNode predicate | other QL defined barrier guards, for example using concepts
+ *  v                          v
+ * various Barrier classes for specific data flow configurations
+ * ```
+ *
+ * New barriers and barrier guards should be defined using models-as-data, QL extensions of
+ * `FlowBarrier::Range`/`FlowBarrierGuard::Range`, or concepts. Data flow configurations should use the
+ * `barrierNode` predicate and/or concepts to define their barriers.
+ */
+
+private import rust
+private import internal.FlowSummaryImpl as Impl
+private import internal.DataFlowImpl as DataFlowImpl
+
+// import all instances below
+private module Barriers {
+  private import codeql.rust.Frameworks
+  private import codeql.rust.dataflow.internal.ModelsAsData
+}
+
+/** Provides the `Range` class used to define the extent of `FlowBarrier`. */
+module FlowBarrier {
+  /** A flow barrier. */
+  abstract class Range extends Impl::Public::BarrierElement {
+    bindingset[this]
+    Range() { any() }
+
+    override predicate isBarrier(
+      string output, string kind, Impl::Public::Provenance provenance, string model
+    ) {
+      this.isBarrier(output, kind) and provenance = "manual" and model = ""
+    }
+
+    /**
+     * Holds if this element is a flow barrier of kind `kind`, where data
+     * flows out as described by `output`.
+     */
+    predicate isBarrier(string output, string kind) { none() }
+  }
+}
+
+final class FlowBarrier = FlowBarrier::Range;
+
+/** Provides the `Range` class used to define the extent of `FlowBarrierGuard`. */
+module FlowBarrierGuard {
+  /** A flow barrier guard. */
+  abstract class Range extends Impl::Public::BarrierGuardElement {
+    bindingset[this]
+    Range() { any() }
+
+    override predicate isBarrierGuard(
+      string input, string branch, string kind, Impl::Public::Provenance provenance, string model
+    ) {
+      this.isBarrierGuard(input, branch, kind) and provenance = "manual" and model = ""
+    }
+
+    /**
+     * Holds if this element is a flow barrier guard of kind `kind`, for data
+     * flowing in as described by `input`, when `this` evaluates to `branch`.
+     */
+    predicate isBarrierGuard(string input, string branch, string kind) { none() }
+  }
+}
+
+final class FlowBarrierGuard = FlowBarrierGuard::Range;
+
+predicate barrierNode = DataFlowImpl::barrierNode/2;

rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll

@@ -1157,6 +1157,64 @@ private module Cached {
   cached
   predicate sinkNode(Node n, string kind) { n.(FlowSummaryNode).isSink(kind, _) }
 
+  private newtype TKindModelPair =
+    TMkPair(string kind, string model) {
+      FlowSummaryImpl::Private::barrierGuardSpec(_, _, _, kind, model)
+    }
+
+  private boolean convertAcceptingValue(FlowSummaryImpl::Public::AcceptingValue av) {
+    av.isTrue() and result = true
+    or
+    av.isFalse() and result = false
+    // Remaining cases are not supported yet, they depend on the shared Guards library.
+    // 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(AstNode g, Expr e, boolean gv, TKindModelPair kmp) {
+    exists(
+      FlowSummaryImpl::Public::BarrierGuardElement b,
+      FlowSummaryImpl::Private::SummaryComponentStack stack,
+      FlowSummaryImpl::Public::AcceptingValue acceptingvalue, string kind, string model
+    |
+      FlowSummaryImpl::Private::barrierGuardSpec(b, stack, acceptingvalue, kind, model) and
+      e = FlowSummaryImpl::StepsInput::getSinkNode(b, stack.headOfSingleton()).asExpr() and
+      kmp = TMkPair(kind, model) and
+      gv = convertAcceptingValue(acceptingvalue) and
+      g = b.getCall()
+    )
+  }
+
+  /** Holds if `n` is a flow barrier of kind `kind` and model `model`. */
+  cached
+  predicate barrierNode(Node n, string kind, string model) {
+    exists(
+      FlowSummaryImpl::Public::BarrierElement b,
+      FlowSummaryImpl::Private::SummaryComponentStack stack
+    |
+      FlowSummaryImpl::Private::barrierSpec(b, stack, kind, model)
+    |
+      n = FlowSummaryImpl::StepsInput::getSourceNode(b, stack, false)
+      or
+      // For barriers like `Argument[0]` we want to target the pre-update node
+      n =
+        FlowSummaryImpl::StepsInput::getSourceNode(b, stack, true)
+            .(PostUpdateNode)
+            .getPreUpdateNode()
+    )
+    or
+    ParameterizedBarrierGuard<TKindModelPair, barrierGuardChecks/4>::getABarrierNode(TMkPair(kind,
+        model)) = n
+  }
+
   /**
    * A step in a flow summary defined using `OptionalStep[name]`. An `OptionalStep` is "opt-in", which means
    * that by default the step is not present in the flow summary and needs to be explicitly enabled by defining
@@ -1180,3 +1238,34 @@ private module Cached {
 }
 
 import Cached
+
+/** Holds if `n` is a flow barrier of kind `kind`. */
+predicate barrierNode(Node n, string kind) { barrierNode(n, kind, _) }
+
+bindingset[this]
+private signature class ParamSig;
+
+private 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(AstNode 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)
+  }
+}

rust/ql/lib/codeql/rust/dataflow/internal/FlowSummaryImpl.qll

@@ -143,7 +143,7 @@ module Input implements InputSig<Location, RustDataFlow> {
 
 private import Make<Location, RustDataFlow, Input> as Impl
 
-private module StepsInput implements Impl::Private::StepsInputSig {
+module StepsInput implements Impl::Private::StepsInputSig {
   DataFlowCall getACall(Public::SummarizedCallable sc) { result.asCall().getStaticTarget() = sc }
 
   /** Gets the argument of `source` described by `sc`, if any. */
@@ -171,18 +171,27 @@ private module StepsInput implements Impl::Private::StepsInputSig {
     result.asCfgScope() = source.getEnclosingCfgScope()
   }
 
-  RustDataFlow::Node getSourceNode(Input::SourceBase source, Impl::Private::SummaryComponentStack s) {
+  additional RustDataFlow::Node getSourceNode(
+    Input::SourceBase source, Impl::Private::SummaryComponentStack s, boolean isArgPostUpdate
+  ) {
     s.head() = Impl::Private::SummaryComponent::return(_) and
-    result.asExpr() = source.getCall()
+    result.asExpr() = source.getCall() and
+    isArgPostUpdate = false
     or
     exists(RustDataFlow::ArgumentPosition pos, Expr arg |
       s.head() = Impl::Private::SummaryComponent::parameter(pos) and
       arg = getSourceNodeArgument(source, s.tail().headOfSingleton()) and
-      result.asParameter() = getCallable(arg).getParam(pos.getPosition())
+      result.asParameter() = getCallable(arg).getParam(pos.getPosition()) and
+      isArgPostUpdate = false
     )
     or
     result.(RustDataFlow::PostUpdateNode).getPreUpdateNode().asExpr() =
-      getSourceNodeArgument(source, s.headOfSingleton())
+      getSourceNodeArgument(source, s.headOfSingleton()) and
+    isArgPostUpdate = true
+  }
+
+  RustDataFlow::Node getSourceNode(Input::SourceBase source, Impl::Private::SummaryComponentStack s) {
+    result = getSourceNode(source, s, _)
   }
 
   RustDataFlow::Node getSinkNode(Input::SinkBase sink, Impl::Private::SummaryComponent sc) {

rust/ql/lib/codeql/rust/dataflow/internal/ModelsAsData.qll

@@ -44,6 +44,7 @@
  */
 
 private import rust
+private import codeql.rust.dataflow.FlowBarrier
 private import codeql.rust.dataflow.FlowSummary
 private import codeql.rust.dataflow.FlowSource
 private import codeql.rust.dataflow.FlowSink
@@ -98,6 +99,29 @@ extensible predicate neutralModel(
   string path, string kind, string provenance, QlBuiltins::ExtensionId madId
 );
 
+/**
+ * Holds if in a call to the function with canonical path `path`, the value referred
+ * to by `output` is a barrier of the given `kind` and `madId` is the data
+ * extension row number.
+ */
+extensible predicate barrierModel(
+  string path, string output, string kind, string provenance, QlBuiltins::ExtensionId madId
+);
+
+/**
+ * Holds if in a call to the function with canonical path `path`, the value referred
+ * to by `input` is a barrier guard of the given `kind` and `madId` is the data
+ * extension row number.
+ *
+ * The value referred to by `input` is assumed to lead to an argument of a call
+ * (possibly `self`), and the call is guarding the argument. `branch` is either `true`
+ * or `false`, indicating which branch of the guard is protecting the argument.
+ */
+extensible predicate barrierGuardModel(
+  string path, string input, string branch, string kind, string provenance,
+  QlBuiltins::ExtensionId madId
+);
+
 /**
  * Holds if the given extension tuple `madId` should pretty-print as `model`.
  *
@@ -123,6 +147,16 @@ predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) {
     neutralModel(path, kind, _, madId) and
     model = "Neutral: " + path + "; " + kind
   )
+  or
+  exists(string path, string output, string kind |
+    barrierModel(path, output, kind, _, madId) and
+    model = "Barrier: " + path + "; " + output + "; " + kind
+  )
+  or
+  exists(string path, string input, string branch, string kind |
+    barrierGuardModel(path, input, branch, kind, _, madId) and
+    model = "Barrier guard: " + path + "; " + input + "; " + branch + "; " + kind
+  )
 }
 
 private class SummarizedCallableFromModel extends SummarizedCallable::Range {
@@ -206,6 +240,40 @@ private class FlowSinkFromModel extends FlowSink::Range {
   }
 }
 
+private class FlowBarrierFromModel extends FlowBarrier::Range {
+  private string path;
+
+  FlowBarrierFromModel() {
+    barrierModel(path, _, _, _, _) and
+    this.callResolvesTo(path)
+  }
+
+  override predicate isBarrier(string output, string kind, Provenance provenance, string model) {
+    exists(QlBuiltins::ExtensionId madId |
+      barrierModel(path, output, kind, provenance, madId) and
+      model = "MaD:" + madId.toString()
+    )
+  }
+}
+
+private class FlowBarrierGuardFromModel extends FlowBarrierGuard::Range {
+  private string path;
+
+  FlowBarrierGuardFromModel() {
+    barrierGuardModel(path, _, _, _, _, _) and
+    this.callResolvesTo(path)
+  }
+
+  override predicate isBarrierGuard(
+    string input, string branch, string kind, Provenance provenance, string model
+  ) {
+    exists(QlBuiltins::ExtensionId madId |
+      barrierGuardModel(path, input, branch, kind, provenance, madId) and
+      model = "MaD:" + madId.toString()
+    )
+  }
+}
+
 private module Debug {
   private import FlowSummaryImpl
   private import Private

rust/ql/lib/codeql/rust/dataflow/internal/Node.qll

@@ -82,12 +82,12 @@ class FlowSummaryNode extends Node, TFlowSummaryNode {
     result = this.getSummaryNode().getSinkElement()
   }
 
-  /** Holds is this node is a source node of kind `kind`. */
+  /** Holds if this node is a source node of kind `kind`. */
   predicate isSource(string kind, string model) {
     this.getSummaryNode().(FlowSummaryImpl::Private::SourceOutputNode).isEntry(kind, model)
   }
 
-  /** Holds is this node is a sink node of kind `kind`. */
+  /** Holds if this node is a sink node of kind `kind`. */
   predicate isSink(string kind, string model) {
     this.getSummaryNode().(FlowSummaryImpl::Private::SinkInputNode).isExit(kind, model)
   }

rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll

@@ -305,6 +305,31 @@ private module Cached {
 
       predicate getABarrierNode = getABarrierNodeImpl/0;
     }
+
+    bindingset[this]
+    private signature class ParamSig;
+
+    private module WithParam<ParamSig P> {
+      signature predicate guardChecksSig(AstNode g, Expr e, boolean branch, P param);
+    }
+
+    overlay[global]
+    cached // nothing is actually cached
+    module ParameterizedBarrierGuard<ParamSig P, WithParam<P>::guardChecksSig/4 guardChecks> {
+      private predicate guardChecksAdjTypes(
+        DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e,
+        DataFlowIntegrationInput::GuardValue branch, P param
+      ) {
+        guardChecks(g, e, branch, param)
+      }
+
+      private Node getABarrierNodeImpl(P param) {
+        result =
+          DataFlowIntegrationImpl::BarrierGuardWithState<P, guardChecksAdjTypes/4>::getABarrierNode(param)
+      }
+
+      predicate getABarrierNode = getABarrierNodeImpl/1;
+    }
   }
 }
 

rust/ql/lib/codeql/rust/dataflow/internal/empty.model.yml

@@ -15,3 +15,13 @@ extensions:
       pack: codeql/rust-all
       extensible: summaryModel
     data: []
+
+  - addsTo:
+      pack: codeql/rust-all
+      extensible: barrierModel
+    data: []
+
+  - addsTo:
+      pack: codeql/rust-all
+      extensible: barrierGuardModel
+    data: []

rust/ql/test/library-tests/dataflow/barrier/inline-flow.expected

@@ -1,41 +1,20 @@
 models
 edges
-| main.rs:9:13:9:19 | ...: ... | main.rs:10:11:10:11 | s | provenance |  |
-| main.rs:10:11:10:11 | s | main.rs:12:9:12:9 | s | provenance |  |
-| main.rs:12:9:12:9 | s | main.rs:9:30:14:1 | { ... } | provenance |  |
 | main.rs:21:9:21:9 | s | main.rs:22:10:22:10 | s | provenance |  |
 | main.rs:21:13:21:21 | source(...) | main.rs:21:9:21:9 | s | provenance |  |
-| main.rs:26:9:26:9 | s | main.rs:27:22:27:22 | s | provenance |  |
-| main.rs:26:13:26:21 | source(...) | main.rs:26:9:26:9 | s | provenance |  |
-| main.rs:27:9:27:9 | s | main.rs:28:10:28:10 | s | provenance |  |
-| main.rs:27:13:27:23 | sanitize(...) | main.rs:27:9:27:9 | s | provenance |  |
-| main.rs:27:22:27:22 | s | main.rs:9:13:9:19 | ...: ... | provenance |  |
-| main.rs:27:22:27:22 | s | main.rs:27:13:27:23 | sanitize(...) | provenance |  |
 | main.rs:32:9:32:9 | s | main.rs:33:10:33:10 | s | provenance |  |
 | main.rs:32:13:32:21 | source(...) | main.rs:32:9:32:9 | s | provenance |  |
 nodes
-| main.rs:9:13:9:19 | ...: ... | semmle.label | ...: ... |
-| main.rs:9:30:14:1 | { ... } | semmle.label | { ... } |
-| main.rs:10:11:10:11 | s | semmle.label | s |
-| main.rs:12:9:12:9 | s | semmle.label | s |
 | main.rs:17:10:17:18 | source(...) | semmle.label | source(...) |
 | main.rs:21:9:21:9 | s | semmle.label | s |
 | main.rs:21:13:21:21 | source(...) | semmle.label | source(...) |
 | main.rs:22:10:22:10 | s | semmle.label | s |
-| main.rs:26:9:26:9 | s | semmle.label | s |
-| main.rs:26:13:26:21 | source(...) | semmle.label | source(...) |
-| main.rs:27:9:27:9 | s | semmle.label | s |
-| main.rs:27:13:27:23 | sanitize(...) | semmle.label | sanitize(...) |
-| main.rs:27:22:27:22 | s | semmle.label | s |
-| main.rs:28:10:28:10 | s | semmle.label | s |
 | main.rs:32:9:32:9 | s | semmle.label | s |
 | main.rs:32:13:32:21 | source(...) | semmle.label | source(...) |
 | main.rs:33:10:33:10 | s | semmle.label | s |
 subpaths
-| main.rs:27:22:27:22 | s | main.rs:9:13:9:19 | ...: ... | main.rs:9:30:14:1 | { ... } | main.rs:27:13:27:23 | sanitize(...) |
 testFailures
 #select
 | main.rs:17:10:17:18 | source(...) | main.rs:17:10:17:18 | source(...) | main.rs:17:10:17:18 | source(...) | $@ | main.rs:17:10:17:18 | source(...) | source(...) |
 | main.rs:22:10:22:10 | s | main.rs:21:13:21:21 | source(...) | main.rs:22:10:22:10 | s | $@ | main.rs:21:13:21:21 | source(...) | source(...) |
-| main.rs:28:10:28:10 | s | main.rs:26:13:26:21 | source(...) | main.rs:28:10:28:10 | s | $@ | main.rs:26:13:26:21 | source(...) | source(...) |
 | main.rs:33:10:33:10 | s | main.rs:32:13:32:21 | source(...) | main.rs:33:10:33:10 | s | $@ | main.rs:32:13:32:21 | source(...) | source(...) |

rust/ql/test/library-tests/dataflow/barrier/inline-flow.ext.yml

@@ -0,0 +1,11 @@
+extensions:
+  - addsTo:
+      pack: codeql/rust-all
+      extensible: barrierModel
+    data:
+      - ["main::sanitize", "ReturnValue", "test-barrier", "manual"]
+  - addsTo:
+      pack: codeql/rust-all
+      extensible: barrierGuardModel
+    data:
+      - ["main::verify_safe", "Argument[0]", "true", "test-barrier", "manual"]

rust/ql/test/library-tests/dataflow/barrier/inline-flow.ql

@@ -3,8 +3,19 @@
  */
 
 import rust
+import codeql.rust.dataflow.DataFlow
+import codeql.rust.dataflow.FlowBarrier
 import utils.test.InlineFlowTest
-import DefaultFlowTest
+
+module CustomConfig implements DataFlow::ConfigSig {
+  predicate isSource = DefaultFlowConfig::isSource/1;
+
+  predicate isSink = DefaultFlowConfig::isSink/1;
+
+  predicate isBarrier(DataFlow::Node n) { barrierNode(n, "test-barrier") }
+}
+
+import FlowTest<CustomConfig, CustomConfig>
 import TaintFlow::PathGraph
 
 from TaintFlow::PathNode source, TaintFlow::PathNode sink

rust/ql/test/library-tests/dataflow/barrier/main.rs

@@ -25,10 +25,24 @@ fn through_variable() {
 fn with_barrier() {
     let s = source(1);
     let s = sanitize(s);
-    sink(s); // $ SPURIOUS: hasValueFlow=1
+    sink(s);
 }
 
 fn main() {
     let s = source(1);
     sink(s); // $ hasValueFlow=1
 }
+
+fn verify_safe(s: &str) -> bool {
+    match s {
+        "dangerous" => false,
+        _ => true,
+    }
+}
+
+fn with_barrier_guard() {
+    let s = source(1);
+    if verify_safe(s) {
+        sink(s);
+    }
+}

shared/dataflow/codeql/dataflow/internal/FlowSummaryImpl.qll

@@ -368,6 +368,34 @@ module Make<
       abstract predicate isSink(string input, string kind, Provenance provenance, string model);
     }
 
+    /** A barrier element. */
+    abstract class BarrierElement extends SourceBaseFinal {
+      bindingset[this]
+      BarrierElement() { any() }
+
+      /**
+       * Holds if this element is a flow barrier of kind `kind`, where data
+       * flows out as described by `output`.
+       */
+      pragma[nomagic]
+      abstract predicate isBarrier(string output, string kind, Provenance provenance, string model);
+    }
+
+    /** A barrier guard element. */
+    abstract class BarrierGuardElement extends SinkBaseFinal {
+      bindingset[this]
+      BarrierGuardElement() { any() }
+
+      /**
+       * Holds if this element is a flow barrier guard of kind `kind`, for data
+       * flowing in as described by `input`, when `this` evaluates to `branch`.
+       */
+      pragma[nomagic]
+      abstract predicate isBarrierGuard(
+        string input, string branch, string kind, Provenance provenance, string model
+      );
+    }
+
     private signature predicate hasKindSig(string kind);
 
     signature class NeutralCallableSig extends SummarizedCallableBaseFinal {
@@ -723,7 +751,32 @@ module Make<
       )
     }
 
-    private predicate summarySpec(string spec) {
+    private predicate isRelevantBarrier(
+      BarrierElement e, string output, string kind, Provenance provenance, string model
+    ) {
+      e.isBarrier(output, kind, provenance, model) and
+      (
+        provenance.isManual()
+        or
+        provenance.isGenerated() and
+        not exists(Provenance p | p.isManual() and e.isBarrier(_, kind, p, _))
+      )
+    }
+
+    private predicate isRelevantBarrierGuard(
+      BarrierGuardElement e, string input, string branch, string kind, Provenance provenance,
+      string model
+    ) {
+      e.isBarrierGuard(input, branch, kind, provenance, model) and
+      (
+        provenance.isManual()
+        or
+        provenance.isGenerated() and
+        not exists(Provenance p | p.isManual() and e.isBarrierGuard(_, _, kind, p, _))
+      )
+    }
+
+    private predicate flowSpec(string spec) {
       exists(SummarizedCallable c |
         c.propagatesFlow(spec, _, _, _, _, _)
         or
@@ -732,10 +785,14 @@ module Make<
       or
       isRelevantSource(_, spec, _, _, _)
       or
+      isRelevantBarrier(_, spec, _, _, _)
+      or
+      isRelevantBarrierGuard(_, spec, _, _, _, _)
+      or
       isRelevantSink(_, spec, _, _, _)
     }
 
-    import AccessPathSyntax::AccessPath<summarySpec/1>
+    import AccessPathSyntax::AccessPath<flowSpec/1>
 
     /** Holds if specification component `token` parses as parameter `pos`. */
     predicate parseParam(AccessPathToken token, ArgumentPosition pos) {
@@ -1515,6 +1572,31 @@ module Make<
       )
     }
 
+    /**
+     * Holds if `barrier` is a relevant barrier element with output specification `outSpec`.
+     */
+    predicate barrierSpec(
+      BarrierElement barrier, SummaryComponentStack outSpec, string kind, string model
+    ) {
+      exists(string output |
+        isRelevantBarrier(barrier, output, kind, _, model) and
+        External::interpretSpec(output, outSpec)
+      )
+    }
+
+    /**
+     * Holds if `barrierGuard` is a relevant barrier guard element with input specification `inSpec`.
+     */
+    predicate barrierGuardSpec(
+      BarrierGuardElement barrierGuard, SummaryComponentStack inSpec, string branch, string kind,
+      string model
+    ) {
+      exists(string input |
+        isRelevantBarrierGuard(barrierGuard, input, branch, kind, _, model) and
+        External::interpretSpec(input, inSpec)
+      )
+    }
+
     signature module TypesInputSig {
       /** Gets the type of content `c`. */
       DataFlowType getContentType(ContentSet c);