Dataflow: Sync.

This commit is contained in:
Anders Schack-Mulligen
2022-06-15 14:43:30 +02:00
parent 33deff9bae
commit 6518a01ded
47 changed files with 1292 additions and 432 deletions

View File

@@ -90,14 +90,20 @@ abstract class Configuration extends string {
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isBarrier` and `BarrierGuard` module instead.
*
* Holds if data flow through nodes guarded by `guard` is prohibited.
*/
deprecated predicate isBarrierGuard(BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isBarrier` and `BarrierGuard` module instead.
*
* Holds if data flow through nodes guarded by `guard` is prohibited when
* the flow state is `state`
*/
predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
deprecated predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
/**
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
@@ -335,6 +341,29 @@ private predicate outBarrier(NodeEx node, Configuration config) {
)
}
/** A bridge class to access the deprecated `isBarrierGuard`. */
private class BarrierGuardGuardedNodeBridge extends Unit {
abstract predicate guardedNode(Node n, Configuration config);
abstract predicate guardedNode(Node n, FlowState state, Configuration config);
}
private class BarrierGuardGuardedNode extends BarrierGuardGuardedNodeBridge {
deprecated override predicate guardedNode(Node n, Configuration config) {
exists(BarrierGuard g |
config.isBarrierGuard(g) and
n = g.getAGuardedNode()
)
}
deprecated override predicate guardedNode(Node n, FlowState state, Configuration config) {
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
)
}
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -348,10 +377,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
not config.isSink(n) and
not config.isSink(n, _)
or
exists(BarrierGuard g |
config.isBarrierGuard(g) and
n = g.getAGuardedNode()
)
any(BarrierGuardGuardedNodeBridge b).guardedNode(n, config)
)
}
@@ -360,10 +386,7 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
)
any(BarrierGuardGuardedNodeBridge b).guardedNode(n, state, config)
)
}

View File

@@ -90,14 +90,20 @@ abstract class Configuration extends string {
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isBarrier` and `BarrierGuard` module instead.
*
* Holds if data flow through nodes guarded by `guard` is prohibited.
*/
deprecated predicate isBarrierGuard(BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isBarrier` and `BarrierGuard` module instead.
*
* Holds if data flow through nodes guarded by `guard` is prohibited when
* the flow state is `state`
*/
predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
deprecated predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
/**
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
@@ -335,6 +341,29 @@ private predicate outBarrier(NodeEx node, Configuration config) {
)
}
/** A bridge class to access the deprecated `isBarrierGuard`. */
private class BarrierGuardGuardedNodeBridge extends Unit {
abstract predicate guardedNode(Node n, Configuration config);
abstract predicate guardedNode(Node n, FlowState state, Configuration config);
}
private class BarrierGuardGuardedNode extends BarrierGuardGuardedNodeBridge {
deprecated override predicate guardedNode(Node n, Configuration config) {
exists(BarrierGuard g |
config.isBarrierGuard(g) and
n = g.getAGuardedNode()
)
}
deprecated override predicate guardedNode(Node n, FlowState state, Configuration config) {
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
)
}
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -348,10 +377,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
not config.isSink(n) and
not config.isSink(n, _)
or
exists(BarrierGuard g |
config.isBarrierGuard(g) and
n = g.getAGuardedNode()
)
any(BarrierGuardGuardedNodeBridge b).guardedNode(n, config)
)
}
@@ -360,10 +386,7 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
)
any(BarrierGuardGuardedNodeBridge b).guardedNode(n, state, config)
)
}

View File

@@ -90,14 +90,20 @@ abstract class Configuration extends string {
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isBarrier` and `BarrierGuard` module instead.
*
* Holds if data flow through nodes guarded by `guard` is prohibited.
*/
deprecated predicate isBarrierGuard(BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isBarrier` and `BarrierGuard` module instead.
*
* Holds if data flow through nodes guarded by `guard` is prohibited when
* the flow state is `state`
*/
predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
deprecated predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
/**
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
@@ -335,6 +341,29 @@ private predicate outBarrier(NodeEx node, Configuration config) {
)
}
/** A bridge class to access the deprecated `isBarrierGuard`. */
private class BarrierGuardGuardedNodeBridge extends Unit {
abstract predicate guardedNode(Node n, Configuration config);
abstract predicate guardedNode(Node n, FlowState state, Configuration config);
}
private class BarrierGuardGuardedNode extends BarrierGuardGuardedNodeBridge {
deprecated override predicate guardedNode(Node n, Configuration config) {
exists(BarrierGuard g |
config.isBarrierGuard(g) and
n = g.getAGuardedNode()
)
}
deprecated override predicate guardedNode(Node n, FlowState state, Configuration config) {
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
)
}
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -348,10 +377,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
not config.isSink(n) and
not config.isSink(n, _)
or
exists(BarrierGuard g |
config.isBarrierGuard(g) and
n = g.getAGuardedNode()
)
any(BarrierGuardGuardedNodeBridge b).guardedNode(n, config)
)
}
@@ -360,10 +386,7 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
)
any(BarrierGuardGuardedNodeBridge b).guardedNode(n, state, config)
)
}

View File

@@ -90,14 +90,20 @@ abstract class Configuration extends string {
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isBarrier` and `BarrierGuard` module instead.
*
* Holds if data flow through nodes guarded by `guard` is prohibited.
*/
deprecated predicate isBarrierGuard(BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isBarrier` and `BarrierGuard` module instead.
*
* Holds if data flow through nodes guarded by `guard` is prohibited when
* the flow state is `state`
*/
predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
deprecated predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
/**
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
@@ -335,6 +341,29 @@ private predicate outBarrier(NodeEx node, Configuration config) {
)
}
/** A bridge class to access the deprecated `isBarrierGuard`. */
private class BarrierGuardGuardedNodeBridge extends Unit {
abstract predicate guardedNode(Node n, Configuration config);
abstract predicate guardedNode(Node n, FlowState state, Configuration config);
}
private class BarrierGuardGuardedNode extends BarrierGuardGuardedNodeBridge {
deprecated override predicate guardedNode(Node n, Configuration config) {
exists(BarrierGuard g |
config.isBarrierGuard(g) and
n = g.getAGuardedNode()
)
}
deprecated override predicate guardedNode(Node n, FlowState state, Configuration config) {
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
)
}
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -348,10 +377,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
not config.isSink(n) and
not config.isSink(n, _)
or
exists(BarrierGuard g |
config.isBarrierGuard(g) and
n = g.getAGuardedNode()
)
any(BarrierGuardGuardedNodeBridge b).guardedNode(n, config)
)
}
@@ -360,10 +386,7 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
)
any(BarrierGuardGuardedNodeBridge b).guardedNode(n, state, config)
)
}

View File

@@ -116,20 +116,30 @@ abstract class Configuration extends DataFlow::Configuration {
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
*
* Holds if taint propagation through nodes guarded by `guard` is prohibited.
*/
deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard)
deprecated final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
this.isSanitizerGuard(guard)
}
/**
* DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
*
* 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() }
deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
none()
}
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
deprecated final override predicate isBarrierGuard(
DataFlow::BarrierGuard guard, DataFlow::FlowState state
) {
this.isSanitizerGuard(guard, state)
}

View File

@@ -116,20 +116,30 @@ abstract class Configuration extends DataFlow::Configuration {
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
*
* Holds if taint propagation through nodes guarded by `guard` is prohibited.
*/
deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard)
deprecated final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
this.isSanitizerGuard(guard)
}
/**
* DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
*
* 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() }
deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
none()
}
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
deprecated final override predicate isBarrierGuard(
DataFlow::BarrierGuard guard, DataFlow::FlowState state
) {
this.isSanitizerGuard(guard, state)
}

View File

@@ -116,20 +116,30 @@ abstract class Configuration extends DataFlow::Configuration {
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
*
* Holds if taint propagation through nodes guarded by `guard` is prohibited.
*/
deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard)
deprecated final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
this.isSanitizerGuard(guard)
}
/**
* DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
*
* 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() }
deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
none()
}
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
deprecated final override predicate isBarrierGuard(
DataFlow::BarrierGuard guard, DataFlow::FlowState state
) {
this.isSanitizerGuard(guard, state)
}

View File

@@ -116,20 +116,30 @@ abstract class Configuration extends DataFlow::Configuration {
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
/**
* DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
*
* Holds if taint propagation through nodes guarded by `guard` is prohibited.
*/
deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard)
deprecated final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
this.isSanitizerGuard(guard)
}
/**
* DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
*
* 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() }
deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
none()
}
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
deprecated final override predicate isBarrierGuard(
DataFlow::BarrierGuard guard, DataFlow::FlowState state
) {
this.isSanitizerGuard(guard, state)
}