From d95114fb1dab9fd9dab281972c326fb89d781141 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 26 Feb 2025 14:28:28 +0100 Subject: [PATCH 1/6] SSA: Extend consistency queries. --- shared/ssa/codeql/ssa/Ssa.qll | 50 +++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 5bdc2b8a28ad..0d7a4d12ac48 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -1379,6 +1379,56 @@ module Make Input> { not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _) ) } + + /** Holds if the end of a basic block can be reached by multiple definitions. */ + query predicate nonUniqueDefReachesEndOfBlock(Definition def, SourceVariable v, BasicBlock bb) { + ssaDefReachesEndOfBlock(bb, def, v) and + not exists(unique(Definition def0 | ssaDefReachesEndOfBlock(bb, def0, v))) + } + + /** Holds if a phi node has less than two inputs. */ + query predicate uselessPhiNode(PhiNode phi, int inputs) { + inputs = count(Definition inp | phiHasInputFromBlock(phi, inp, _)) and + inputs < 2 + } + + /** Holds if a certain read does not have a prior reference. */ + query predicate readWithoutPriorRef(SourceVariable v, BasicBlock bb, int i) { + variableRead(bb, i, v, true) and + not AdjacentSsaRefs::adjacentRefRead(_, _, bb, i, v) + } + + /** + * Holds if a certain read has multiple prior references. The introduction + * of phi reads should make the prior reference unique. + */ + query predicate readWithMultiplePriorRefs( + SourceVariable v, BasicBlock bb1, int i1, BasicBlock bb2, int i2 + ) { + AdjacentSsaRefs::adjacentRefRead(bb1, i1, bb2, i2, v) and + 2 <= + strictcount(BasicBlock bb0, int i0 | AdjacentSsaRefs::adjacentRefRead(bb0, i0, bb1, i1, v)) + } + + /** Holds if `phi` has less than 2 immediately prior references. */ + query predicate phiWithoutTwoPriorRefs(PhiNode phi, int inputRefs) { + exists(BasicBlock bbPhi, SourceVariable v | + phi.definesAt(v, bbPhi, _) and + inputRefs = + count(BasicBlock bb, int i | AdjacentSsaRefs::adjacentRefPhi(bb, i, _, bbPhi, v)) and + inputRefs < 2 + ) + } + + /** + * Holds if the phi read for `v` at `bb` has less than 2 immediately prior + * references. + */ + query predicate phiReadWithoutTwoPriorRefs(BasicBlock bbPhi, SourceVariable v, int inputRefs) { + synthPhiRead(bbPhi, v) and + inputRefs = count(BasicBlock bb, int i | AdjacentSsaRefs::adjacentRefPhi(bb, i, _, bbPhi, v)) and + inputRefs < 2 + } } /** Provides the input to `DataFlowIntegration`. */ From 947a85ed282427c575811f6d9f60cb2ff345e028 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 26 Feb 2025 14:31:49 +0100 Subject: [PATCH 2/6] Java: Enable SSA consistency queries. --- java/ql/consistency-queries/SsaConsistency.ql | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 java/ql/consistency-queries/SsaConsistency.ql diff --git a/java/ql/consistency-queries/SsaConsistency.ql b/java/ql/consistency-queries/SsaConsistency.ql new file mode 100644 index 000000000000..b62db63ac5ba --- /dev/null +++ b/java/ql/consistency-queries/SsaConsistency.ql @@ -0,0 +1,3 @@ +import java +import semmle.code.java.dataflow.internal.SsaImpl +import Impl::Consistency From 9e6bdbbcbb0647235088a0009f10a8a073420a00 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 27 Feb 2025 10:46:22 +0100 Subject: [PATCH 3/6] SSA: Don't add phi-reads for frontiers of uncertain reads. --- shared/ssa/codeql/ssa/Ssa.qll | 1 + 1 file changed, 1 insertion(+) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 0d7a4d12ac48..6b0c6b0bf4d6 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -307,6 +307,7 @@ module Make Input> { private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) { exists(BasicBlock readbb | inDominanceFrontier(readbb, bb) | ssaDefReachesRead(v, _, readbb, _) and + variableRead(readbb, _, v, true) and not variableWrite(readbb, _, v, _) or synthPhiRead(readbb, v) and From 97a3411c0cc3e1ff20a71cf64e440bfbcb258630 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 6 Mar 2025 13:58:14 +0100 Subject: [PATCH 4/6] Ruby: Accept test output. --- .../dataflow/barrier-guards/barrier-guards.expected | 5 ----- 1 file changed, 5 deletions(-) diff --git a/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.expected b/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.expected index 3e838551f81d..eabbc3ad4b8c 100644 --- a/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.expected +++ b/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.expected @@ -12,7 +12,6 @@ newStyleBarrierGuards | barrier-guards.rb:28:5:28:7 | foo | | barrier-guards.rb:37:21:38:19 | [input] SSA phi read(foo) | | barrier-guards.rb:38:5:38:7 | foo | -| barrier-guards.rb:43:16:46:5 | [input] SSA phi read(foo) | | barrier-guards.rb:45:9:45:11 | foo | | barrier-guards.rb:70:22:71:19 | [input] SSA phi read(foo) | | barrier-guards.rb:71:5:71:7 | foo | @@ -51,9 +50,7 @@ newStyleBarrierGuards | barrier-guards.rb:199:4:199:15 | [input] SSA phi read(foo) | | barrier-guards.rb:199:4:199:31 | [input] SSA phi read(foo) | | barrier-guards.rb:199:20:199:31 | [input] SSA phi read(foo) | -| barrier-guards.rb:203:4:203:15 | [input] SSA phi read(foo) | | barrier-guards.rb:203:36:203:47 | [input] SSA phi read(foo) | -| barrier-guards.rb:207:21:207:21 | [input] SSA phi read(foo) | | barrier-guards.rb:207:22:208:19 | [input] SSA phi read(foo) | | barrier-guards.rb:208:5:208:7 | foo | | barrier-guards.rb:211:22:212:19 | [input] SSA phi read(foo) | @@ -64,8 +61,6 @@ newStyleBarrierGuards | barrier-guards.rb:219:21:219:32 | [input] SSA phi read(foo) | | barrier-guards.rb:219:95:220:19 | [input] SSA phi read(foo) | | barrier-guards.rb:220:5:220:7 | foo | -| barrier-guards.rb:227:21:227:21 | [input] SSA phi read(foo) | -| barrier-guards.rb:227:22:228:7 | [input] SSA phi read(foo) | | barrier-guards.rb:232:18:233:19 | [input] SSA phi read(foo) | | barrier-guards.rb:233:5:233:7 | foo | | barrier-guards.rb:237:19:237:38 | [input] SSA phi read(foo) | From b1e53f5816c1ac688e0d47b21343fe84f2998637 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 7 Mar 2025 11:11:49 +0100 Subject: [PATCH 5/6] Rust: Accept consistency failure. --- .../security/CWE-089/CONSISTENCY/SsaConsistency.expected | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 rust/ql/test/query-tests/security/CWE-089/CONSISTENCY/SsaConsistency.expected diff --git a/rust/ql/test/query-tests/security/CWE-089/CONSISTENCY/SsaConsistency.expected b/rust/ql/test/query-tests/security/CWE-089/CONSISTENCY/SsaConsistency.expected new file mode 100644 index 000000000000..d5074d0d43a3 --- /dev/null +++ b/rust/ql/test/query-tests/security/CWE-089/CONSISTENCY/SsaConsistency.expected @@ -0,0 +1,4 @@ +uselessPhiNode +| sqlx.rs:155:5:157:5 | phi | 1 | +phiWithoutTwoPriorRefs +| sqlx.rs:155:5:157:5 | phi | 1 | From 3508ca89e6c7ebea94dbbbc22f8f8b75e2feee6e Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 7 Mar 2025 11:13:53 +0100 Subject: [PATCH 6/6] Java: Restrict SSA reads to the reachable CFG. --- .../semmle/code/java/dataflow/internal/BaseSSA.qll | 13 ++++++++----- .../semmle/code/java/dataflow/internal/SsaImpl.qll | 13 ++++++++----- 2 files changed, 16 insertions(+), 10 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll index 2c37efea1a46..1b912f919756 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll @@ -168,12 +168,15 @@ private module SsaInput implements SsaImplCommon::InputSig { * Holds if the `i`th of basic block `bb` reads source variable `v`. */ predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) { - exists(VarRead use | - v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true + hasDominanceInformation(bb) and + ( + exists(VarRead use | + v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true + ) + or + variableCapture(v, _, bb, i) and + certain = false ) - or - variableCapture(v, _, bb, i) and - certain = false } } diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll index d5343834ffe2..95ba126bcf71 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll @@ -204,12 +204,15 @@ private module SsaInput implements SsaImplCommon::InputSig { * This includes implicit reads via calls. */ predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) { - exists(VarRead use | - v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true + hasDominanceInformation(bb) and + ( + exists(VarRead use | + v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true + ) + or + variableCapture(v, _, bb, i) and + certain = false ) - or - variableCapture(v, _, bb, i) and - certain = false } }