diff --git a/cpp/ql/lib/change-notes/2022-03-14-flow-state-barriers.md b/cpp/ql/lib/change-notes/2022-03-14-flow-state-barriers.md new file mode 100644 index 00000000000..af6247a66fa --- /dev/null +++ b/cpp/ql/lib/change-notes/2022-03-14-flow-state-barriers.md @@ -0,0 +1,4 @@ +--- +category: feature +--- +* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states. diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll index fb806910898..07bb8ae419f 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll index fb806910898..07bb8ae419f 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll index fb806910898..07bb8ae419f 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll index fb806910898..07bb8ae419f 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll index fb806910898..07bb8ae419f 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll index fb806910898..07bb8ae419f 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll index fb806910898..07bb8ae419f 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll index fb806910898..07bb8ae419f 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll index fb806910898..07bb8ae419f 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking1/TaintTrackingImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking1/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking1/TaintTrackingImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking1/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking2/TaintTrackingImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking2/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking2/TaintTrackingImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking2/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/csharp/ql/lib/change-notes/2022-03-14-flow-state-barriers.md b/csharp/ql/lib/change-notes/2022-03-14-flow-state-barriers.md new file mode 100644 index 00000000000..af6247a66fa --- /dev/null +++ b/csharp/ql/lib/change-notes/2022-03-14-flow-state-barriers.md @@ -0,0 +1,4 @@ +--- +category: feature +--- +* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states. diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll index fb806910898..07bb8ae419f 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll index fb806910898..07bb8ae419f 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll index fb806910898..07bb8ae419f 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll index fb806910898..07bb8ae419f 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll index fb806910898..07bb8ae419f 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking3/TaintTrackingImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking3/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking3/TaintTrackingImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking3/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking4/TaintTrackingImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking4/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking4/TaintTrackingImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking4/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking5/TaintTrackingImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking5/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking5/TaintTrackingImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking5/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/java/ql/lib/change-notes/2022-03-14-flow-state-barriers.md b/java/ql/lib/change-notes/2022-03-14-flow-state-barriers.md new file mode 100644 index 00000000000..af6247a66fa --- /dev/null +++ b/java/ql/lib/change-notes/2022-03-14-flow-state-barriers.md @@ -0,0 +1,4 @@ +--- +category: feature +--- +* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states. diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll index fb806910898..07bb8ae419f 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl2.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl2.qll index fb806910898..07bb8ae419f 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl2.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl2.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl3.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl3.qll index fb806910898..07bb8ae419f 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl3.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl3.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl4.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl4.qll index fb806910898..07bb8ae419f 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl4.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl4.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl5.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl5.qll index fb806910898..07bb8ae419f 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl5.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl5.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl6.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl6.qll index fb806910898..07bb8ae419f 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl6.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl6.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForOnActivityResult.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForOnActivityResult.qll index fb806910898..07bb8ae419f 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForOnActivityResult.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForOnActivityResult.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForSerializability.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForSerializability.qll index fb806910898..07bb8ae419f 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForSerializability.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForSerializability.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/tainttracking1/TaintTrackingImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/tainttracking1/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/tainttracking1/TaintTrackingImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/tainttracking1/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/tainttracking2/TaintTrackingImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/tainttracking2/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/tainttracking2/TaintTrackingImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/tainttracking2/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/python/ql/lib/change-notes/2022-03-14-flow-state-barriers.md b/python/ql/lib/change-notes/2022-03-14-flow-state-barriers.md new file mode 100644 index 00000000000..af6247a66fa --- /dev/null +++ b/python/ql/lib/change-notes/2022-03-14-flow-state-barriers.md @@ -0,0 +1,4 @@ +--- +category: feature +--- +* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states. diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll index fb806910898..07bb8ae419f 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl2.qll b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl2.qll index fb806910898..07bb8ae419f 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl2.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl2.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl3.qll b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl3.qll index fb806910898..07bb8ae419f 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl3.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl3.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl4.qll b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl4.qll index fb806910898..07bb8ae419f 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl4.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl4.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking1/TaintTrackingImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking1/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking1/TaintTrackingImpl.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking1/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking2/TaintTrackingImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking2/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking2/TaintTrackingImpl.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking2/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking3/TaintTrackingImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking3/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking3/TaintTrackingImpl.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking3/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking4/TaintTrackingImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking4/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking4/TaintTrackingImpl.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/tainttracking4/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis. diff --git a/ruby/ql/lib/change-notes/2022-03-14-flow-state-barriers.md b/ruby/ql/lib/change-notes/2022-03-14-flow-state-barriers.md new file mode 100644 index 00000000000..af6247a66fa --- /dev/null +++ b/ruby/ql/lib/change-notes/2022-03-14-flow-state-barriers.md @@ -0,0 +1,4 @@ +--- +category: feature +--- +* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states. diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll index fb806910898..07bb8ae419f 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll index fb806910898..07bb8ae419f 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll @@ -87,12 +87,30 @@ abstract class Configuration extends string { /** Holds if data flow into `node` is prohibited. */ predicate isBarrierIn(Node node) { none() } + /** + * Holds if data flow into `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierIn(Node node, FlowState state) { none() } + /** Holds if data flow out of `node` is prohibited. */ predicate isBarrierOut(Node node) { none() } + /** + * Holds if data flow out of `node` is prohibited when the flow state is + * `state` + */ + predicate isBarrierOut(Node node, FlowState state) { none() } + /** Holds if data flow through nodes guarded by `guard` is prohibited. */ predicate isBarrierGuard(BarrierGuard guard) { none() } + /** + * Holds if data flow through nodes guarded by `guard` is prohibited when + * the flow state is `state` + */ + predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() } + /** * Holds if the additional flow step from `node1` to `node2` must be taken * into account in the analysis. @@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx { ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } } -private predicate inBarrier(NodeEx node, Configuration config) { +private predicate fullInBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierIn(n) @@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) { ) } -private predicate outBarrier(NodeEx node, Configuration config) { +private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierIn(n, state) + | + config.isSource(n, state) + ) +} + +private predicate fullOutBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n and config.isBarrierOut(n) @@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) { ) } +private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) { + exists(Node n | + node.asNode() = n and + config.isBarrierOut(n, state) + | + config.isSink(n, state) + ) +} + pragma[nomagic] private predicate fullBarrier(NodeEx node, Configuration config) { exists(Node n | node.asNode() = n | @@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) { pragma[nomagic] private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { - exists(Node n | - node.asNode() = n and + 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) + or + exists(BarrierGuard g | + config.isBarrierGuard(g, state) and + n = g.getAGuardedNode() + ) ) } @@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) { /** Provides the relevant barriers for a step from `node1` to `node2`. */ pragma[inline] private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { - not outBarrier(node1, config) and - not inBarrier(node2, config) and + not fullOutBarrier(node1, config) and + not fullInBarrier(node2, config) and not fullBarrier(node1, config) and not fullBarrier(node2, config) } @@ -430,6 +476,8 @@ private predicate additionalLocalStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) ) @@ -471,6 +519,8 @@ private predicate additionalJumpStateStep( config.isAdditionalFlowStep(n1, s1, n2, s2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and stepFilter(node1, node2, config) and + not stateOutBarrier(node1, s1, config) and + not stateInBarrier(node2, s2, config) and not stateBarrier(node1, s1, config) and not stateBarrier(node2, s2, config) and not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext @@ -870,8 +920,8 @@ private module Stage1 { private predicate throughFlowNodeCand(NodeEx node, Configuration config) { revFlow(node, true, config) and fwdFlow(node, true, config) and - not inBarrier(node, config) and - not outBarrier(node, config) + not fullInBarrier(node, config) and + not fullOutBarrier(node, config) } /** Holds if flow may return from `callable`. */ @@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1( ) { viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and Stage1::revFlow(ret, config) and - not outBarrier(ret, config) and - not inBarrier(out, config) + not fullOutBarrier(ret, config) and + not fullInBarrier(out, config) } pragma[nomagic] @@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1( ) { viableParamArgNodeCand1(call, p, arg, config) and Stage1::revFlow(p, config) and - not outBarrier(arg, config) and - not inBarrier(p, config) + not fullOutBarrier(arg, config) and + not fullInBarrier(p, config) } /** diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/tainttracking1/TaintTrackingImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/tainttracking1/TaintTrackingImpl.qll index b344ea9a864..fa756218acb 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/tainttracking1/TaintTrackingImpl.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/tainttracking1/TaintTrackingImpl.qll @@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration { /** Holds if taint propagation into `node` is prohibited. */ predicate isSanitizerIn(DataFlow::Node node) { none() } + /** + * Holds if taint propagation into `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerIn(node, state) + } + final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) } /** Holds if taint propagation out of `node` is prohibited. */ @@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration { final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) } + /** + * Holds if taint propagation out of `node` is prohibited when the flow state is + * `state`. + */ + predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() } + + final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) { + this.isSanitizerOut(node, state) + } + /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */ predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } @@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration { this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) } + /** + * Holds if taint propagation through nodes guarded by `guard` is prohibited + * when the flow state is `state`. + */ + predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() } + + final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { + this.isSanitizerGuard(guard, state) + } + /** * Holds if the additional taint propagation step from `node1` to `node2` * must be taken into account in the analysis.