Java: Add pruning for local taint flow.

This commit is contained in:
Anders Schack-Mulligen
2022-10-05 12:02:05 +02:00
parent 9db65eae7f
commit 6db0db431f
2 changed files with 76 additions and 13 deletions

View File

@@ -33,6 +33,57 @@ predicate localExprTaint(Expr src, Expr sink) {
localTaint(DataFlow::exprNode(src), DataFlow::exprNode(sink))
}
/** Holds if `node` is an endpoint for local taint flow. */
signature predicate nodeSig(DataFlow::Node node);
/** Provides local taint flow restricted to a given set of sources and sinks. */
module LocalTaintFlow<nodeSig/1 source, nodeSig/1 sink> {
private predicate reachRev(DataFlow::Node n) {
sink(n)
or
exists(DataFlow::Node mid |
localTaintStep(n, mid) and
reachRev(mid)
)
}
private predicate reachFwd(DataFlow::Node n) {
reachRev(n) and
(
source(n)
or
exists(DataFlow::Node mid |
localTaintStep(mid, n) and
reachFwd(mid)
)
)
}
private predicate step(DataFlow::Node n1, DataFlow::Node n2) {
localTaintStep(n1, n2) and
reachFwd(n1) and
reachFwd(n2)
}
/**
* Holds if taint can flow from `n1` to `n2` in zero or more local
* (intra-procedural) steps that are restricted to be part of a path between
* `source` and `sink`.
*/
pragma[inline]
predicate hasFlow(DataFlow::Node n1, DataFlow::Node n2) { step*(n1, n2) }
/**
* Holds if taint can flow from `n1` to `n2` in zero or more local
* (intra-procedural) steps that are restricted to be part of a path between
* `source` and `sink`.
*/
pragma[inline]
predicate hasExprFlow(Expr n1, Expr n2) {
hasFlow(DataFlow::exprNode(n1), DataFlow::exprNode(n2))
}
}
cached
private module Cached {
private import DataFlowImplCommon as DataFlowImplCommon