Merge pull request #186 from sauyon/taint-split

Split taintStep into many predicates
This commit is contained in:
Max Schaefer
2019-11-20 20:39:27 +00:00
committed by GitHub Enterprise

View File

@@ -87,29 +87,40 @@ module TaintTracking {
}
}
/**
* Holds if taint flows from `pred` to `succ` in one step.
*/
private predicate taintStep(DataFlow::Node pred, DataFlow::Node succ) {
// if x is tainted, then so is &x
/** Holds if taint flows from `pred` to `succ` via a reference or dereference. */
predicate referenceStep(DataFlow::Node pred, DataFlow::Node succ) {
succ.asExpr().(AddressExpr).getOperand() = pred.asExpr()
or
// if x is tainted, then so is *x
succ.asExpr().(StarExpr).getBase() = pred.asExpr()
or
// if an array is tainted, then so are all its elements
}
/** Holds if taint flows from `pred` to `succ` via a field read. */
predicate fieldReadStep(DataFlow::Node pred, DataFlow::Node succ) {
succ.(DataFlow::FieldReadNode).getBase() = pred
}
/** Holds if taint flows from `pred` to `succ` via an array index operation. */
predicate arrayStep(DataFlow::Node pred, DataFlow::Node succ) {
succ.asExpr().(IndexExpr).getBase() = pred.asExpr()
or
// if a tuple is tainted, then so are all its components
}
/** Holds if taint flows from `pred` to `succ` via an extract tuple operation. */
predicate tupleStep(DataFlow::Node pred, DataFlow::Node succ) {
succ = DataFlow::extractTupleElement(pred, _)
or
// taint propagates through string concatenation
}
/** Holds if taint flows from `pred` to `succ` via string concatenation. */
predicate stringConcatStep(DataFlow::Node pred, DataFlow::Node succ) {
succ.asExpr().(AddExpr).getAnOperand() = pred.asExpr()
or
// taint propagates through slicing
}
/** Holds if taint flows from `pred` to `succ` via a slice operation. */
predicate sliceStep(DataFlow::Node pred, DataFlow::Node succ) {
succ.asExpr().(SliceExpr).getBase() = pred.asExpr()
or
// step through function model
}
/** Holds if taint flows from `pred` to `succ` via a function model. */
predicate functionModelStep(DataFlow::Node pred, DataFlow::Node succ) {
exists(FunctionModel m, DataFlow::CallNode c, FunctionInput inp, FunctionOutput outp |
c = m.getACall() and
m.hasTaintFlow(inp, outp) and
@@ -118,6 +129,19 @@ module TaintTracking {
)
}
/**
* Holds if taint flows from `pred` to `succ` in one step.
*/
private predicate taintStep(DataFlow::Node pred, DataFlow::Node succ) {
referenceStep(pred, succ) or
fieldReadStep(pred, succ) or
arrayStep(pred, succ) or
tupleStep(pred, succ) or
stringConcatStep(pred, succ) or
sliceStep(pred, succ) or
functionModelStep(pred, succ)
}
/**
* A model of a function specifying that the function propagates taint from
* a parameter or qualifier to a result.