github · aschackmull · Jul 18, 2025 · Jul 17, 2025 · Copilot · Jul 17, 2025
@@ -237,12 +237,35 @@ private predicate sink(CallPathNode sinkMethodCall) {
   )
 }
 
-
+
+/**
+ * Computes forward reachability from source nodes using transitive closure
+ * over call graph edges. Holds if `n` is reachable from a source node.
+ */
-
+
+/**
+ * Computes forward reachability from source nodes using transitive closure
+ * over call graph edges. Holds if `n` is reachable from a source node.
+ */
+private predicate fwdFlow(CallPathNode n) {
+  source(n)
+  or
+  exists(CallPathNode mid | fwdFlow(mid) and CallGraph::edges(mid, n))
+}
+
-
+
+/**
+ * Computes backward reachability from sinks within the forward-reachable nodes.
+ * This predicate implements the bidirectional pruning strategy by combining
+ * forward reachability (`fwdFlow`) with backward reachability from sinks.
+ */
-
+
+/**
+ * Computes backward reachability from sinks within the forward-reachable nodes.
+ * This predicate implements the bidirectional pruning strategy by combining
+ * forward reachability (`fwdFlow`) with backward reachability from sinks.
+ */
+private predicate revFlow(CallPathNode n) {
+  fwdFlow(n) and
+  (
+    sink(n)
+    or
+    exists(CallPathNode mid | revFlow(mid) and CallGraph::edges(n, mid))
+  )
+}
+
+/**
+ * Holds if `pred` has a successor node `succ` and this edge is in an
+ * `unprotectedStateChange` path.
+ */
- */
+ */
+/**
+ * Holds if `pred` has a successor node `succ` and this edge is in an
+ * `unprotectedStateChange` path.
+ *
+ * Performance characteristics:
+ * - This predicate relies on `revFlow`, which is a recursive flow predicate
+ *   that combines forward and reverse graph traversal.
+ * - The use of `CallGraph::edges` ensures that only valid edges in the call
+ *   graph are considered, reducing unnecessary computations.
+ *
+ * Bidirectional pruning strategy:
+ * - The predicate leverages `revFlow(pred)` and `revFlow(succ)` to prune
+ *   the search space by ensuring that both the predecessor and successor
+ *   nodes are part of valid reverse flows.
+ */
- */
+ */
+/**
+ * Holds if `pred` has a successor node `succ` and this edge is in an
+ * `unprotectedStateChange` path.
+ *
+ * Performance characteristics:
+ * - This predicate relies on `revFlow`, which is a recursive flow predicate
+ *   that combines forward and reverse graph traversal.
+ * - The use of `CallGraph::edges` ensures that only valid edges in the call
+ *   graph are considered, reducing unnecessary computations.
+ *
+ * Bidirectional pruning strategy:
+ * - The predicate leverages `revFlow(pred)` and `revFlow(succ)` to prune
+ *   the search space by ensuring that both the predecessor and successor
+ *   nodes are part of valid reverse flows.
+ */
+predicate relevantEdge(CallPathNode pred, CallPathNode succ) {
+  CallGraph::edges(pred, succ) and revFlow(pred) and revFlow(succ)
+}
+
 /**
  * Holds if `sourceMethod` is an unprotected request handler that reaches a
  * `sinkMethodCall` that updates a database.
  */
 private predicate unprotectedDatabaseUpdate(CallPathNode sourceMethod, CallPathNode sinkMethodCall) =
-  doublyBoundedFastTC(CallGraph::edges/2, source/1, sink/1)(sourceMethod, sinkMethodCall)
+  doublyBoundedFastTC(relevantEdge/2, source/1, sink/1)(sourceMethod, sinkMethodCall)
 
 /**
  * Holds if `sourceMethod` is an unprotected request handler that appears to

@@ -15,7 +15,7 @@
 import java
 import semmle.code.java.security.CsrfUnprotectedRequestTypeQuery
 
-query predicate edges(CallPathNode pred, CallPathNode succ) { CallGraph::edges(pred, succ) }
+query predicate edges(CallPathNode pred, CallPathNode succ) { relevantEdge(pred, succ) }
 
 from CallPathNode source, CallPathNode sink
 where unprotectedStateChange(source, sink)