Variable capture: Avoid overlapping and false-positive data flow paths

This commit is contained in:
Tom Hvitved 2024-03-04 13:25:15 +01:00
Родитель e793a1e9fe
Коммит 63bb772ef9
1 изменённых файлов: 74 добавлений и 6 удалений

Просмотреть файл

@ -601,16 +601,22 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
* observed in a similarly synthesized post-update node for this read of `v`.
*/
private predicate synthRead(
CapturedVariable v, BasicBlock bb, int i, boolean topScope, Expr closure
CapturedVariable v, BasicBlock bb, int i, boolean topScope, Expr closure, boolean alias
) {
exists(ClosureExpr ce | closureCaptures(ce, v) |
ce.hasCfgNode(bb, i) and ce = closure
ce.hasCfgNode(bb, i) and ce = closure and alias = false
or
localOrNestedClosureAccess(ce, closure, bb, i)
localOrNestedClosureAccess(ce, closure, bb, i) and alias = true
) and
if v.getCallable() != bb.getEnclosingCallable() then topScope = false else topScope = true
}
private predicate synthRead(
CapturedVariable v, BasicBlock bb, int i, boolean topScope, Expr closure
) {
synthRead(v, bb, i, topScope, closure, _)
}
/**
* Holds if there is an access of a captured variable inside a closure in the
* `i`th node of `bb`, such that we need to synthesize a `this.` qualifier.
@ -919,16 +925,22 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
)
}
predicate storeStep(ClosureNode node1, CapturedVariable v, ClosureNode node2) {
// store v in the closure or in the malloc in case of a relevant constructor call
private predicate storeStepClosure(
ClosureNode node1, CapturedVariable v, ClosureNode node2, boolean alias
) {
exists(BasicBlock bb, int i, Expr closure |
synthRead(v, bb, i, _, closure) and
synthRead(v, bb, i, _, closure, alias) and
node1 = TSynthRead(v, bb, i, false)
|
node2 = TExprNode(closure, false)
or
node2 = TMallocNode(closure) and hasConstructorCapture(closure, v)
)
}
predicate storeStep(ClosureNode node1, CapturedVariable v, ClosureNode node2) {
// store v in the closure or in the malloc in case of a relevant constructor call
storeStepClosure(node1, v, node2, _)
or
// write to v inside the closure body
exists(BasicBlock bb, int i, VariableWrite vw |
@ -964,6 +976,62 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
}
predicate clearsContent(ClosureNode node, CapturedVariable v) {
/*
* Stores into closure aliases block flow from previous stores, both to
* avoid overlapping data flow paths, but also to avoid false positive
* flow.
*
* Example 1 (overlapping paths):
*
* ```rb
* def m
* x = taint
*
* fn = -> { # (1)
* sink x
* }
*
* fn.call # (2)
* ```
*
* If we don't clear `x` at `fn` (2), we will have two overlapping paths:
*
* ```
* taint -> fn (2) [captured x]
* taint -> fn (1) [captured x] -> fn (2) [captured x]
* ```
*
* where the step `fn (1) [captured x] -> fn [captured x]` arises from normal
* use-use flow for `fn`. Clearing `x` at `fn` (2) removes the second path above.
*
* Example 2 (false positive flow):
*
* ```rb
* def m
* x = taint
*
* fn = -> { # (1)
* sink x
* }
*
* x = nil # (2)
*
* fn.call # (3)
* end
* ```
*
* If we don't clear `x` at `fn` (3), we will have the following false positive
* flow path:
*
* ```
* taint -> fn (1) [captured x] -> fn (3) [captured x]
* ```
*
* since normal use-use flow for `fn` does not take the overwrite at (2) into account.
*/
storeStepClosure(_, v, node, true)
or
exists(BasicBlock bb, int i |
captureWrite(v, bb, i, false, _) and
node = TSynthThisQualifier(bb, i, false)