From cfed7e9b6cfb79fce57d2e77e661d298703826cd Mon Sep 17 00:00:00 2001 From: Asger F Date: Fri, 22 Sep 2023 13:00:48 +0200 Subject: [PATCH] Shared: add in/out barriers with flow state --- shared/dataflow/codeql/dataflow/DataFlow.qll | 6 ++ .../codeql/dataflow/internal/DataFlowImpl.qll | 60 ++++++++++++++++--- 2 files changed, 59 insertions(+), 7 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/DataFlow.qll b/shared/dataflow/codeql/dataflow/DataFlow.qll index 67948db0ee8..197afc8eec4 100644 --- a/shared/dataflow/codeql/dataflow/DataFlow.qll +++ b/shared/dataflow/codeql/dataflow/DataFlow.qll @@ -357,9 +357,15 @@ module Configs { /** Holds if data flow into `node` is prohibited. */ default predicate isBarrierIn(Node node) { none() } + /** Holds if data flow into `node` is prohibited when the target flow state is `state`. */ + default predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ default predicate isBarrierOut(Node node) { none() } + /** Holds if data flow out of `node` is prohibited when the originating flow state is `state`. */ + default predicate isBarrierOut(Node node, FlowState state) { none() } + /** * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps. */ diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index e4182a32a4b..fa5cb9744ea 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -53,9 +53,15 @@ module MakeImpl { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node); + /** Holds if data flow into `node` is prohibited when the target flow state is `state`. */ + predicate isBarrierIn(Node node, FlowState state); + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node); + /** Holds if data flow out of `node` is prohibited when the originating flow state is `state`. */ + predicate isBarrierOut(Node node, FlowState state); + /** * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps. */ @@ -133,6 +139,10 @@ module MakeImpl { predicate isBarrier(Node node, FlowState state) { none() } + predicate isBarrierIn(Node node, FlowState state) { none() } + + predicate isBarrierOut(Node node, FlowState state) { none() } + predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) { none() } @@ -220,6 +230,14 @@ module MakeImpl { ) } + private predicate inBarrier(NodeEx node, FlowState state) { + exists(Node n | + node.asNode() = n and + Config::isBarrierIn(n, state) and + Config::isSource(n, state) + ) + } + private predicate outBarrier(NodeEx node) { exists(Node n | node.asNode() = n and @@ -231,6 +249,17 @@ module MakeImpl { ) } + private predicate outBarrier(NodeEx node, FlowState state) { + exists(Node n | + node.asNode() = n and + Config::isBarrierOut(n, state) + | + Config::isSink(n, state) + or + Config::isSink(n) + ) + } + pragma[nomagic] private predicate fullBarrier(NodeEx node) { exists(Node n | node.asNode() = n | @@ -247,7 +276,16 @@ module MakeImpl { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state) { - exists(Node n | node.asNode() = n | Config::isBarrier(n, state)) + exists(Node n | node.asNode() = n | + Config::isBarrier(n, state) + or + Config::isBarrierIn(n, state) and + not Config::isSource(n, state) + or + Config::isBarrierOut(n, state) and + not Config::isSink(n, state) and + not Config::isSink(n) + ) } pragma[nomagic] @@ -265,6 +303,7 @@ module MakeImpl { } /** Provides the relevant barriers for a step from `node1` to `node2`. */ + bindingset[node1, node2] pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2) { not outBarrier(node1) and @@ -273,6 +312,17 @@ module MakeImpl { not fullBarrier(node2) } + /** Provides the relevant barriers for a step from `node1,state1` to `node2,state2`, including stateless barriers for `node1` to `node2`. */ + bindingset[node1, state1, node2, state2] + pragma[inline] + private predicate stateStepFilter(NodeEx node1, FlowState state1, NodeEx node2, FlowState state2) { + stepFilter(node1, node2) and + not outBarrier(node1, state1) and + not inBarrier(node2, state2) and + not stateBarrier(node1, state1) and + not stateBarrier(node2, state2) + } + pragma[nomagic] private predicate isUnreachableInCall1(NodeEx n, LocalCallContextSpecificCall cc) { isUnreachableInCallCached(n.asNode(), cc.getCall()) @@ -325,9 +375,7 @@ module MakeImpl { node2.asNode() = n2 and Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and - stepFilter(node1, node2) and - not stateBarrier(node1, s1) and - not stateBarrier(node2, s2) + stateStepFilter(node1, s1, node2, s2) ) } @@ -364,9 +412,7 @@ module MakeImpl { node2.asNode() = n2 and Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and - stepFilter(node1, node2) and - not stateBarrier(node1, s1) and - not stateBarrier(node2, s2) and + stateStepFilter(node1, s1, node2, s2) and not Config::getAFeature() instanceof FeatureEqualSourceSinkCallContext ) }