Java: Change in/out barriers to be explicit in the configuration.

This commit is contained in:
Anders Schack-Mulligen
2019-08-05 12:05:12 +02:00
parent 6d022aa359
commit f8804943ee
4 changed files with 45 additions and 13 deletions

View File

@@ -63,13 +63,23 @@ module TaintTracking {
node.asExpr() instanceof ValidatedVariableAccess
}
/** DEPRECATED: override `isSanitizer` instead. */
/** DEPRECATED: override `isSanitizerIn` and `isSanitizerOut` instead. */
deprecated predicate isSanitizerEdge(DataFlow::Node node1, DataFlow::Node node2) { none() }
deprecated final override predicate isBarrierEdge(DataFlow::Node node1, DataFlow::Node node2) {
isSanitizerEdge(node1, node2)
}
/** Holds if data flow into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() }
final override predicate isBarrierIn(DataFlow::Node node) { isSanitizerIn(node) }
/** Holds if data flow out of `node` is prohibited. */
predicate isSanitizerOut(DataFlow::Node node) { none() }
final override predicate isBarrierOut(DataFlow::Node node) { isSanitizerOut(node) }
/**
* Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis.
@@ -135,13 +145,23 @@ module TaintTracking {
node.asExpr() instanceof ValidatedVariableAccess
}
/** DEPRECATED: override `isSanitizer` instead. */
/** DEPRECATED: override `isSanitizerIn` and `isSanitizerOut` instead. */
deprecated predicate isSanitizerEdge(DataFlow::Node node1, DataFlow::Node node2) { none() }
deprecated final override predicate isBarrierEdge(DataFlow::Node node1, DataFlow::Node node2) {
isSanitizerEdge(node1, node2)
}
/** Holds if data flow into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() }
final override predicate isBarrierIn(DataFlow::Node node) { isSanitizerIn(node) }
/** Holds if data flow out of `node` is prohibited. */
predicate isSanitizerOut(DataFlow::Node node) { none() }
final override predicate isBarrierOut(DataFlow::Node node) { isSanitizerOut(node) }
/**
* Holds if the additional taint propagation step from `node1` to `node2`
* must be taken into account in the analysis.

View File

@@ -57,9 +57,15 @@ abstract class Configuration extends string {
/** Holds if data flow through `node` is prohibited. */
predicate isBarrier(Node node) { none() }
/** DEPRECATED: override `isBarrier` instead. */
/** DEPRECATED: override `isBarrierIn` and `isBarrierOut` instead. */
deprecated predicate isBarrierEdge(Node node1, Node node2) { none() }
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis.
@@ -104,18 +110,22 @@ abstract class Configuration extends string {
}
private predicate inBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierIn(node) and
config.isSource(node)
}
private predicate outBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierOut(node) and
config.isSink(node)
}
private predicate fullBarrier(Node node, Configuration config) {
config.isBarrier(node) and
not config.isSource(node) and
config.isBarrier(node)
or
config.isBarrierIn(node) and
not config.isSource(node)
or
config.isBarrierOut(node) and
not config.isSink(node)
}