Merge pull request #8435 from jketema/all-the-barriers

Add flow state versions of isBarrierIn, isBarrierOut, and isBarrierGuard
This commit is contained in:
Jeroen Ketema
2022-03-16 15:50:19 +01:00
committed by GitHub
50 changed files with 2266 additions and 336 deletions

View File

@@ -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.

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -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.

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -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.

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -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.

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.

View File

@@ -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.

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -87,12 +87,30 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */ /** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() } 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. */ /** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() } 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. */ /** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() } 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 * Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis. * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() } ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
} }
private predicate inBarrier(NodeEx node, Configuration config) { private predicate fullInBarrier(NodeEx node, Configuration config) {
exists(Node n | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierIn(n) 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 | exists(Node n |
node.asNode() = n and node.asNode() = n and
config.isBarrierOut(n) 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] pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) { private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n | exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic] pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) { private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n | exists(Node n | node.asNode() = n |
node.asNode() = n and
config.isBarrier(n, state) 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`. */ /** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline] pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) { private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not outBarrier(node1, config) and not fullOutBarrier(node1, config) and
not inBarrier(node2, config) and not fullInBarrier(node2, config) and
not fullBarrier(node1, config) and not fullBarrier(node1, config) and
not fullBarrier(node2, config) not fullBarrier(node2, config)
} }
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) not stateBarrier(node2, s2, config)
) )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) 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(node1, s1, config) and
not stateBarrier(node2, s2, config) and not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) { private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and revFlow(node, true, config) and
fwdFlow(node, true, config) and fwdFlow(node, true, config) and
not inBarrier(node, config) and not fullInBarrier(node, config) and
not outBarrier(node, config) not fullOutBarrier(node, config)
} }
/** Holds if flow may return from `callable`. */ /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
) { ) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and Stage1::revFlow(ret, config) and
not outBarrier(ret, config) and not fullOutBarrier(ret, config) and
not inBarrier(out, config) not fullInBarrier(out, config)
} }
pragma[nomagic] pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
) { ) {
viableParamArgNodeCand1(call, p, arg, config) and viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and Stage1::revFlow(p, config) and
not outBarrier(arg, config) and not fullOutBarrier(arg, config) and
not inBarrier(p, config) not fullInBarrier(p, config)
} }
/** /**

View File

@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */ /** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() } 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) } final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */ /** 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) } 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. */ /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() } predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
@@ -123,6 +143,16 @@ abstract class Configuration extends DataFlow::Configuration {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard) 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` * Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis. * must be taken into account in the analysis.