Merge pull request #1807 from hvitved/csharp/dataflow/barrier-guard

Approved by calumgrant
This commit is contained in:
semmle-qlci 2019-08-30 12:40:25 +01:00 коммит произвёл GitHub
Родитель 3d3797f829 6e7ef66642
Коммит 394563de43
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: 4AEE18F83AFDEB23
11 изменённых файлов: 171 добавлений и 148 удалений

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

@ -16,6 +16,9 @@ The following changes in version 1.23 affect C# analysis in all applications.
## Changes to QL libraries
* The new class `NamespaceAccess` models accesses to namespaces, for example in `nameof` expressions.
* The data-flow library now makes it easier to specify barriers/sanitizers
arising from guards by overriding the predicate
`isBarrierGuard`/`isSanitizerGuard` on data-flow and taint-tracking
configurations respectively.
## Changes to autobuilder

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

@ -13,6 +13,23 @@ private import semmle.code.csharp.controlflow.BasicBlocks
private import semmle.code.csharp.controlflow.internal.Completion
private import semmle.code.csharp.frameworks.System
/** An expression whose value may control the execution of another element. */
class Guard extends Expr {
Guard() { isGuard(this, _) }
/**
* Holds if `cfn` is guarded by this expression having value `v`, where `sub` is
* a sub expression of this expression that is structurally equal to the expression
* belonging to `cfn`.
*
* In case `cfn` or `sub` access an SSA variable in their left-most qualifier, then
* so must the other (accessing the same SSA variable).
*/
predicate controlsNode(ControlFlow::Nodes::ElementNode cfn, AccessOrCallExpr sub, AbstractValue v) {
isGuardedByNode(cfn, this, sub, v)
}
}
/** An abstract value. */
abstract class AbstractValue extends TAbstractValue {
/** Holds if the `s` branch out of `cfe` is taken iff `e` has this value. */
@ -481,7 +498,7 @@ class GuardedExpr extends AccessOrCallExpr {
* left-most qualifier, then so must the other (accessing the same SSA
* variable).
*/
Expr getAGuard(Expr sub, AbstractValue v) {
Guard getAGuard(Expr sub, AbstractValue v) {
result = g and
sub = sub0 and
v = v0
@ -492,7 +509,7 @@ class GuardedExpr extends AccessOrCallExpr {
* expression is guarded by a structurally equal expression having abstract
* value `v`.
*/
predicate mustHaveValue(AbstractValue v) { exists(Expr e | e = this.getAGuard(e, v)) }
predicate mustHaveValue(AbstractValue v) { g = this.getAGuard(g, v) }
/**
* Holds if this expression is guarded by expression `cond`, which must
@ -533,7 +550,7 @@ class GuardedControlFlowNode extends ControlFlow::Nodes::ElementNode {
private AbstractValue v0;
GuardedControlFlowNode() { isGuardedByNode(this, g, sub0, v0) }
GuardedControlFlowNode() { g.controlsNode(this, sub0, v0) }
/**
* Gets an expression that guards this control flow node. That is, this control
@ -546,7 +563,7 @@ class GuardedControlFlowNode extends ControlFlow::Nodes::ElementNode {
* left-most qualifier, then so must the other (accessing the same SSA
* variable).
*/
Expr getAGuard(Expr sub, AbstractValue v) {
Guard getAGuard(Expr sub, AbstractValue v) {
result = g and
sub = sub0 and
v = v0
@ -557,7 +574,7 @@ class GuardedControlFlowNode extends ControlFlow::Nodes::ElementNode {
* control flow node is guarded by a structurally equal expression having
* abstract value `v`.
*/
predicate mustHaveValue(AbstractValue v) { exists(Expr e | e = this.getAGuard(e, v)) }
predicate mustHaveValue(AbstractValue v) { g = this.getAGuard(g, v) }
}
/**
@ -587,7 +604,7 @@ class GuardedDataFlowNode extends DataFlow::ExprNode {
GuardedDataFlowNode() {
exists(ControlFlow::Nodes::ElementNode cfn | exists(this.getExprAtNode(cfn)) |
isGuardedByNode(cfn, g, sub0, v0)
g.controlsNode(cfn, sub0, v0)
)
}
@ -602,7 +619,7 @@ class GuardedDataFlowNode extends DataFlow::ExprNode {
* left-most qualifier, then so must the other (accessing the same SSA
* variable).
*/
Expr getAGuard(Expr sub, AbstractValue v) {
Guard getAGuard(Expr sub, AbstractValue v) {
result = g and
sub = sub0 and
v = v0
@ -613,7 +630,7 @@ class GuardedDataFlowNode extends DataFlow::ExprNode {
* data flow node is guarded by a structurally equal expression having
* abstract value `v`.
*/
predicate mustHaveValue(AbstractValue v) { exists(Expr e | e = this.getAGuard(e, v)) }
predicate mustHaveValue(AbstractValue v) { g = this.getAGuard(g, v) }
}
/** An expression guarded by a `null` check. */
@ -761,72 +778,49 @@ module Internal {
e = any(BinaryArithmeticOperation bao | result = bao.getAnOperand())
}
/** An expression whose value may control the execution of another element. */
class Guard extends Expr {
private AbstractValue val;
/** Holds if basic block `bb` only is reached when guard `g` has abstract value `v`. */
private predicate guardControls(Guard g, BasicBlock bb, AbstractValue v) {
exists(ControlFlowElement cfe, ConditionalSuccessor s, AbstractValue v0, Guard g0 |
cfe.controlsBlock(bb, s)
|
v0.branch(cfe, s, g0) and
impliesSteps(g0, v0, g, v)
)
}
Guard() {
this.getType() instanceof BoolType and
not this instanceof BoolLiteral and
not this instanceof SwitchCaseExpr and
not this instanceof PatternExpr and
val = TBooleanValue(_)
/**
* Holds if control flow node `cfn` only is reached when guard `g` evaluates to `v`,
* because of an assertion.
*/
private predicate guardAssertionControlsNode(Guard g, ControlFlow::Node cfn, AbstractValue v) {
exists(Assertion a, Guard g0, AbstractValue v0 |
asserts(a, g0, v0) and
impliesSteps(g0, v0, g, v)
|
a.strictlyDominates(cfn.getBasicBlock())
or
this instanceof DereferenceableExpr and
val = TNullValue(_)
or
val.branch(_, _, this)
or
asserts(_, this, val)
}
/** Gets an abstract value that this guard may have. */
AbstractValue getAValue() { result = val }
/** Holds if basic block `bb` only is reached when this guard has abstract value `v`. */
predicate controls(BasicBlock bb, AbstractValue v) {
exists(ControlFlowElement cfe, ConditionalSuccessor s, AbstractValue v0, Guard g |
cfe.controlsBlock(bb, s)
|
v0.branch(cfe, s, g) and
impliesSteps(g, v0, this, v)
exists(BasicBlock bb, int i, int j | bb.getNode(i) = a.getAControlFlowNode() |
bb.getNode(j) = cfn and
j > i
)
}
)
}
/**
* Holds if control flow node `cfn` only is reached when this guard evaluates to `v`,
* because of an assertion.
*/
predicate assertionControlsNode(ControlFlow::Node cfn, AbstractValue v) {
exists(Assertion a, Guard g, AbstractValue v0 |
asserts(a, g, v0) and
impliesSteps(g, v0, this, v)
|
a.strictlyDominates(cfn.getBasicBlock())
or
exists(BasicBlock bb, int i, int j | bb.getNode(i) = a.getAControlFlowNode() |
bb.getNode(j) = cfn and
j > i
)
)
}
/**
* Holds if control flow element `cfe` only is reached when guard `g` evaluates to `v`,
* because of an assertion.
*/
private predicate guardAssertionControlsElement(Guard g, ControlFlowElement cfe, AbstractValue v) {
forex(ControlFlow::Node cfn | cfn = cfe.getAControlFlowNode() |
guardAssertionControlsNode(g, cfn, v)
)
}
/**
* Holds if control flow element `cfe` only is reached when this guard evaluates to `v`,
* because of an assertion.
*/
predicate assertionControlsElement(ControlFlowElement cfe, AbstractValue v) {
forex(ControlFlow::Node cfn | cfn = cfe.getAControlFlowNode() |
this.assertionControlsNode(cfn, v)
)
}
/** Same as `this.getAChildExpr*()`, but avoids `fastTC`. */
Expr getAChildExprStar() {
result = this
or
result = this.getAChildExprStar().getAChildExpr()
}
/** Same as `this.getAChildExpr*()`, but avoids `fastTC`. */
private Expr getAChildExprStar(Guard g) {
result = g
or
result = getAChildExprStar(g).getAChildExpr()
}
/**
@ -1273,8 +1267,24 @@ module Internal {
private import semmle.code.csharp.Caching
cached
predicate isCustomNullCheck(Call call, Expr arg, BooleanValue v, boolean isNull) {
predicate isGuard(Expr e, AbstractValue val) {
Stages::ControlFlowStage::forceCachingInSameStage() and
e.getType() instanceof BoolType and
not e instanceof BoolLiteral and
not e instanceof SwitchCaseExpr and
not e instanceof PatternExpr and
val = TBooleanValue(_)
or
e instanceof DereferenceableExpr and
val = TNullValue(_)
or
val.branch(_, _, e)
or
asserts(_, e, val)
}
cached
predicate isCustomNullCheck(Call call, Expr arg, BooleanValue v, boolean isNull) {
exists(Callable callable, Parameter p |
arg = call.getArgumentForParameter(any(Parameter p0 | p0.getSourceDeclaration() = p)) and
call.getTarget().getSourceDeclaration() = callable and
@ -1355,7 +1365,7 @@ module Internal {
)
)
or
v1 = g1.getAValue() and
isGuard(g1, v1) and
v1 = any(MatchValue mv |
mv.isMatch() and
g2 = g1 and
@ -1379,20 +1389,20 @@ module Internal {
v2 = v1
or
g2 = g1.(AssignExpr).getRValue() and
v1 = g1.getAValue() and
isGuard(g1, v1) and
v2 = v1
or
g2 = g1.(Assignment).getLValue() and
v1 = g1.getAValue() and
isGuard(g1, v1) and
v2 = v1
or
g2 = g1.(CastExpr).getExpr() and
v1 = g1.getAValue() and
isGuard(g1, v1) and
v2 = v1.(NullValue)
or
exists(PreSsa::Definition def | def.getDefinition().getSource() = g2 |
g1 = def.getARead() and
v1 = g1.getAValue() and
isGuard(g1, v1) and
v2 = v1
)
or
@ -1473,10 +1483,10 @@ module Internal {
pragma[noinline]
private predicate candidateAux(AccessOrCallExpr e, Declaration target, BasicBlock bb) {
target = e.getTarget() and
exists(Guard g | e = g.getAChildExprStar() |
g.controls(bb, _)
exists(Guard g | e = getAChildExprStar(g) |
guardControls(g, bb, _)
or
g.assertionControlsNode(bb.getANode(), _)
guardAssertionControlsNode(g, bb.getANode(), _)
)
}
}
@ -1492,7 +1502,7 @@ module Internal {
) {
Stages::GuardsStage::forceCachingInSameStage() and
cfn = guarded.getAControlFlowNode() and
g.controls(cfn.getBasicBlock(), v) and
guardControls(g, cfn.getBasicBlock(), v) and
exists(ConditionOnExprComparisonConfig c | c.same(sub, guarded))
}
@ -1504,7 +1514,7 @@ module Internal {
isGuardedByNode0(cfn, guarded, g, sub, v)
)
or
g.assertionControlsElement(guarded, v) and
guardAssertionControlsElement(g, guarded, v) and
exists(ConditionOnExprComparisonConfig c | c.same(sub, guarded))
}
@ -1513,7 +1523,7 @@ module Internal {
AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub, AbstractValue v
) {
isGuardedByExpr1(guarded, g, sub, v) and
sub = g.getAChildExprStar() and
sub = getAChildExprStar(g) and
forall(Ssa::Definition def | def = sub.getAnSsaQualifier(_) |
def = guarded.getAnSsaQualifier(_)
)
@ -1525,7 +1535,7 @@ module Internal {
) {
isGuardedByNode0(guarded, _, g, sub, v)
or
g.assertionControlsNode(guarded, v) and
guardAssertionControlsNode(g, guarded, v) and
exists(ConditionOnExprComparisonConfig c | c.same(sub, guarded.getElement()))
}
@ -1542,7 +1552,7 @@ module Internal {
ControlFlow::Nodes::ElementNode guarded, Guard g, AccessOrCallExpr sub, AbstractValue v
) {
isGuardedByNode1(guarded, g, sub, v) and
sub = g.getAChildExprStar() and
sub = getAChildExprStar(g) and
forall(Ssa::Definition def | def = sub.getAnSsaQualifier(_) | isGuardedByNode2(guarded, def))
}
@ -1560,7 +1570,7 @@ module Internal {
forex(ControlFlow::Node cfn | cfn = g1.getAControlFlowNode() |
exists(Ssa::ExplicitDefinition def | def.getADefinition().getSource() = g2 |
g1 = def.getAReadAtNode(cfn) and
v1 = g1.getAValue() and
isGuard(g1, v1) and
v2 = v1
)
)
@ -1578,7 +1588,7 @@ module Internal {
predicate preImpliesSteps(Guard g1, AbstractValue v1, Guard g2, AbstractValue v2) {
g1 = g2 and
v1 = v2 and
v1 = g1.getAValue()
isGuard(g1, v1)
or
exists(Expr mid, AbstractValue vMid | preImpliesSteps(g1, v1, mid, vMid) |
preImpliesStep(mid, vMid, g2, v2)
@ -1595,7 +1605,7 @@ module Internal {
predicate impliesSteps(Guard g1, AbstractValue v1, Guard g2, AbstractValue v2) {
g1 = g2 and
v1 = v2 and
v1 = g1.getAValue()
isGuard(g1, v1)
or
exists(Expr mid, AbstractValue vMid | impliesSteps(g1, v1, mid, vMid) |
impliesStep(mid, vMid, g2, v2)

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

@ -127,7 +127,7 @@ private predicate dereferenceAt(BasicBlock bb, int i, Ssa::Definition def, Deref
private predicate exprImpliesSsaDef(
Expr e, G::AbstractValue vExpr, Ssa::Definition def, G::AbstractValue vDef
) {
exists(G::Internal::Guard g | G::Internal::impliesSteps(e, vExpr, g, vDef) |
exists(G::Guard g | G::Internal::impliesSteps(e, vExpr, g, vDef) |
g = def.getARead()
or
g = def.(Ssa::ExplicitDefinition).getADefinition().getTargetAccess()

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

@ -182,12 +182,15 @@ abstract class NonLocalJumpNode extends Node {
*
* It is important that all extending classes in scope are disjoint.
*/
class BarrierGuard extends Internal::Guard {
/** NOT YET SUPPORTED. Holds if this guard validates `e` upon evaluating to `v`. */
abstract deprecated predicate checks(Expr e, AbstractValue v);
class BarrierGuard extends Guard {
/** Holds if this guard validates `e` upon evaluating to `v`. */
abstract predicate checks(Expr e, AbstractValue v);
/** Gets a node guarded by this guard. */
final Node getAGuardedNode() {
none() // stub
final ExprNode getAGuardedNode() {
exists(Expr e, AbstractValue v |
this.checks(e, v) and
this.controlsNode(result.getControlFlowNode(), e, v)
)
}
}

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

@ -94,28 +94,23 @@ module TaintedPath {
}
/**
* Holds if this expression is part of a check that is insufficient to prevent path tampering.
* A weak guard that is insufficient to prevent path tampering.
*/
private predicate inWeakCheck(Expr e) {
// None of these are sufficient to guarantee that a string is safe.
exists(MethodCall m, Method def | m.getTarget() = def |
m.getQualifier() = e and
(
def.getName() = "StartsWith" or
def.getName() = "EndsWith"
private class WeakGuard extends Guard {
WeakGuard() {
// None of these are sufficient to guarantee that a string is safe.
exists(MethodCall mc, Method m | this = mc and mc.getTarget() = m |
m.getName() = "StartsWith" or
m.getName() = "EndsWith" or
m.getName() = "IsNullOrEmpty" or
m.getName() = "IsNullOrWhitespace" or
m = any(SystemIOFileClass f).getAMethod("Exists") or
m = any(SystemIODirectoryClass f).getAMethod("Exists")
)
or
m.getArgument(0) = e and
(
def.getName() = "IsNullOrEmpty" or
def.getName() = "IsNullOrWhitespace" or
def = any(SystemIOFileClass f).getAMethod("Exists") or
def = any(SystemIODirectoryClass f).getAMethod("Exists")
)
)
or
// Checking against `null` has no bearing on path traversal.
exists(EqualityOperation b | b.getAnOperand() = e | b.getAnOperand() instanceof NullLiteral)
// Checking against `null` has no bearing on path traversal.
this.controlsNode(_, _, any(AbstractValues::NullValue nv))
}
}
/**
@ -126,9 +121,9 @@ module TaintedPath {
class PathCheck extends Sanitizer {
PathCheck() {
// This expression is structurally replicated in a dominating guard which is not a "weak" check
exists(Expr e, AbstractValues::BooleanValue v |
exists(this.(GuardedDataFlowNode).getAGuard(e, v)) and
not inWeakCheck(e)
exists(Guard g, AbstractValues::BooleanValue v |
g = this.(GuardedDataFlowNode).getAGuard(_, v) and
not g instanceof WeakGuard
)
}
}

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

@ -27,6 +27,11 @@ module UrlRedirect {
*/
abstract class Sanitizer extends DataFlow::ExprNode { }
/**
* A guard for unvalidated URL redirect vulnerabilities.
*/
abstract class SanitizerGuard extends DataFlow::BarrierGuard { }
/**
* A taint-tracking configuration for reasoning about unvalidated URL redirect vulnerabilities.
*/
@ -38,6 +43,10 @@ module UrlRedirect {
override predicate isSink(DataFlow::Node sink) { sink instanceof Sink }
override predicate isSanitizer(DataFlow::Node node) { node instanceof Sanitizer }
override predicate isSanitizerGuard(DataFlow::BarrierGuard guard) {
guard instanceof SanitizerGuard
}
}
/** A source of remote user input. */
@ -98,12 +107,12 @@ module UrlRedirect {
/**
* A URL argument to a call to `UrlHelper.isLocalUrl()` that is a sanitizer for URL redirects.
*/
class IsLocalUrlSanitizer extends Sanitizer {
IsLocalUrlSanitizer() {
exists(MethodCall mc, AbstractValues::BooleanValue v | mc.getTarget().hasName("IsLocalUrl") |
mc = this.(GuardedDataFlowNode).getAGuard(mc.getArgument(0), v) and
v.getValue() = true
)
class IsLocalUrlSanitizer extends SanitizerGuard, MethodCall {
IsLocalUrlSanitizer() { this.getTarget().hasName("IsLocalUrl") }
override predicate checks(Expr e, AbstractValue v) {
e = this.getArgument(0) and
v.(AbstractValues::BooleanValue).getValue() = true
}
}

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

@ -22,6 +22,11 @@ module ZipSlip {
*/
abstract class Sanitizer extends DataFlow::ExprNode { }
/**
* A guard for unsafe zip extraction.
*/
abstract class SanitizerGuard extends DataFlow::BarrierGuard { }
/** A taint tracking configuration for Zip Slip */
class TaintTrackingConfiguration extends TaintTracking::Configuration {
TaintTrackingConfiguration() { this = "ZipSlipTaintTracking" }
@ -31,6 +36,10 @@ module ZipSlip {
override predicate isSink(DataFlow::Node sink) { sink instanceof Sink }
override predicate isSanitizer(DataFlow::Node node) { node instanceof Sanitizer }
override predicate isSanitizerGuard(DataFlow::BarrierGuard guard) {
guard instanceof SanitizerGuard
}
}
/** An access to the `FullName` property of a `ZipArchiveEntry`. */
@ -120,27 +129,26 @@ module ZipSlip {
}
/**
* An expression which is guarded by a call to `String.StartsWith`.
*
* A call to the method `String.StartsWith` can indicate the the tainted path value is being
* A call to `String.StartsWith()` that indicates that the tainted path value is being
* validated to ensure that it occurs within a permitted output path.
*/
class StringCheckSanitizer extends Sanitizer {
StringCheckSanitizer() {
exists(MethodCall mc, Expr startsWithQualifier, AbstractValues::BooleanValue v |
mc = this.(GuardedDataFlowNode).getAGuard(startsWithQualifier, v)
|
v.getValue() = true and
mc.getTarget().hasQualifiedName("System.String", "StartsWith") and
mc.getQualifier() = startsWithQualifier and
// A StartsWith check against Path.Combine is not sufficient, because the ".." elements have
// not yet been resolved.
not exists(MethodCall combineCall |
combineCall.getTarget().hasQualifiedName("System.IO.Path", "Combine") and
DataFlow::localFlow(DataFlow::exprNode(combineCall),
DataFlow::exprNode(startsWithQualifier))
)
class StringCheckGuard extends SanitizerGuard, MethodCall {
private Expr q;
StringCheckGuard() {
this.getTarget().hasQualifiedName("System.String", "StartsWith") and
this.getQualifier() = q and
// A StartsWith check against Path.Combine is not sufficient, because the ".." elements have
// not yet been resolved.
not exists(MethodCall combineCall |
combineCall.getTarget().hasQualifiedName("System.IO.Path", "Combine") and
DataFlow::localFlow(DataFlow::exprNode(combineCall), DataFlow::exprNode(q))
)
}
override predicate checks(Expr e, AbstractValue v) {
e = q and
v.(AbstractValues::BooleanValue).getValue() = true
}
}
}

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

@ -1,5 +1,5 @@
import csharp
import semmle.code.csharp.controlflow.Guards
private import semmle.code.csharp.controlflow.Guards
class Configuration extends DataFlow::Configuration {
Configuration() { this = "Configuration" }
@ -9,12 +9,8 @@ class Configuration extends DataFlow::Configuration {
override predicate isSink(DataFlow::Node sink) { any() }
override predicate isBarrier(DataFlow::Node node) {
exists(EQExpr eq, Expr e, AbstractValues::BooleanValue v |
eq = node.(GuardedDataFlowNode).getAGuard(e, v)
|
v.getValue() = true and
eq.getAnOperand() = e and
eq.getAnOperand() instanceof NullLiteral
exists(AbstractValues::NullValue nv | node.(GuardedDataFlowNode).mustHaveValue(nv) |
nv.isNull()
)
}
}

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

@ -1,4 +1,5 @@
import csharp
import semmle.code.csharp.controlflow.Guards
private import semmle.code.csharp.dataflow.internal.DataFlowPrivate
class MyFlowSource extends DataFlow::Node {

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

@ -1,6 +1,5 @@
import csharp
import Common
import semmle.code.csharp.controlflow.Guards
predicate step(DataFlow::Node pred, DataFlow::Node succ) {
DataFlow::localFlowStep(pred, succ) and

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

@ -1,6 +1,5 @@
import csharp
import Common
import semmle.code.csharp.controlflow.Guards
predicate step(DataFlow::Node pred, DataFlow::Node succ) {
TaintTracking::localTaintStep(pred, succ) and