Merge branch 'main' into python-remove-spurious-global-flow

This commit is contained in:
Taus Brock-Nannestad
2020-09-04 16:28:03 +02:00
9 changed files with 270 additions and 24 deletions

View File

@@ -1144,6 +1144,17 @@ private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
if guardLB > defLB then result = guardLB else result = defLB
)
or
exists(VariableAccess access, float neConstant, float lower |
isNEPhi(v, phi, access, neConstant) and
lower = getFullyConvertedLowerBounds(access) and
if lower = neConstant then result = lower + 1 else result = lower
)
or
exists(VariableAccess access |
isUnsupportedGuardPhi(v, phi, access) and
result = getFullyConvertedLowerBounds(access)
)
or
result = getDefLowerBounds(phi.getAPhiInput(v), v)
}
@@ -1161,6 +1172,17 @@ private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
if guardUB < defUB then result = guardUB else result = defUB
)
or
exists(VariableAccess access, float neConstant, float upper |
isNEPhi(v, phi, access, neConstant) and
upper = getFullyConvertedUpperBounds(access) and
if upper = neConstant then result = upper - 1 else result = upper
)
or
exists(VariableAccess access |
isUnsupportedGuardPhi(v, phi, access) and
result = getFullyConvertedUpperBounds(access)
)
or
result = getDefUpperBounds(phi.getAPhiInput(v), v)
}
@@ -1423,22 +1445,13 @@ private predicate linearBoundFromGuard(
// 1. x <= upperbound(RHS)
// 2. x >= lowerbound(RHS)
//
// For x != RHS, we create trivial bounds:
//
// 1. x <= typeUpperBound(RHS.getUnspecifiedType())
// 2. x >= typeLowerBound(RHS.getUnspecifiedType())
//
exists(Expr lhs, Expr rhs, boolean isEQ |
exists(Expr lhs, Expr rhs |
linearAccess(lhs, v, p, q) and
eqOpWithSwapAndNegate(guard, lhs, rhs, isEQ, branch) and
eqOpWithSwapAndNegate(guard, lhs, rhs, true, branch) and
getBounds(rhs, boundValue, isLowerBound) and
strictness = Nonstrict()
|
// True branch
isEQ = true and getBounds(rhs, boundValue, isLowerBound)
or
// False branch: set the bounds to the min/max for the type.
isEQ = false and exprTypeBounds(rhs, boundValue, isLowerBound)
)
// x != RHS and !x are handled elsewhere
}
/** Utility for `linearBoundFromGuard`. */
@@ -1455,6 +1468,42 @@ private predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBou
isLowerBound = false and boundValue = exprMaxVal(expr.getFullyConverted())
}
/**
* Holds if `(v, phi)` ensures that `access` is not equal to `neConstant`. For
* example, the condition `if (x + 1 != 3)` ensures that `x` is not equal to 2.
* Only integral types are supported.
*/
private predicate isNEPhi(
Variable v, RangeSsaDefinition phi, VariableAccess access, float neConstant
) {
exists(
ComparisonOperation cmp, boolean branch, Expr linearExpr, Expr rExpr, float p, float q, float r
|
access.getTarget() = v and
phi.isGuardPhi(access, cmp, branch) and
eqOpWithSwapAndNegate(cmp, linearExpr, rExpr, false, branch) and
v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!=` is too imprecise
r = getValue(rExpr).toFloat() and
linearAccess(linearExpr, access, p, q) and
neConstant = (r - q) / p
)
}
/**
* Holds if `(v, phi)` constrains the value of `access` but in a way that
* doesn't allow this library to constrain the upper or lower bounds of
* `access`. An example is `if (x != y)` if neither `x` nor `y` is a
* compile-time constant.
*/
private predicate isUnsupportedGuardPhi(Variable v, RangeSsaDefinition phi, VariableAccess access) {
exists(ComparisonOperation cmp, boolean branch |
access.getTarget() = v and
phi.isGuardPhi(access, cmp, branch) and
eqOpWithSwapAndNegate(cmp, _, _, false, branch) and
not isNEPhi(v, phi, access, _)
)
}
cached
private module SimpleRangeAnalysisCached {
/**

View File

@@ -532,6 +532,37 @@
| test.c:530:3:530:3 | i | -2147483648 |
| test.c:530:10:530:11 | sc | 1 |
| test.c:532:7:532:7 | i | -128 |
| test.c:539:7:539:7 | n | 0 |
| test.c:541:7:541:7 | n | 0 |
| test.c:542:9:542:9 | n | 1 |
| test.c:545:7:545:7 | n | 0 |
| test.c:546:9:546:9 | n | 1 |
| test.c:548:9:548:9 | n | 0 |
| test.c:551:8:551:8 | n | 0 |
| test.c:552:9:552:9 | n | 0 |
| test.c:554:9:554:9 | n | 0 |
| test.c:557:10:557:10 | n | 0 |
| test.c:558:5:558:5 | n | 1 |
| test.c:561:7:561:7 | n | 0 |
| test.c:565:7:565:7 | n | -32768 |
| test.c:568:7:568:7 | n | 0 |
| test.c:569:9:569:9 | n | 0 |
| test.c:571:9:571:9 | n | 1 |
| test.c:574:7:574:7 | n | 0 |
| test.c:575:9:575:9 | n | 0 |
| test.c:577:9:577:9 | n | 0 |
| test.c:580:10:580:10 | n | 0 |
| test.c:581:5:581:5 | n | 1 |
| test.c:584:7:584:7 | n | 0 |
| test.c:588:7:588:7 | n | -32768 |
| test.c:589:9:589:9 | n | -32768 |
| test.c:590:11:590:11 | n | 0 |
| test.c:594:7:594:7 | n | -32768 |
| test.c:595:13:595:13 | n | 5 |
| test.c:598:9:598:9 | n | 6 |
| test.c:601:7:601:7 | n | -32768 |
| test.c:601:22:601:22 | n | -32767 |
| test.c:602:9:602:9 | n | -32766 |
| test.cpp:10:7:10:7 | b | -2147483648 |
| test.cpp:11:5:11:5 | x | -2147483648 |
| test.cpp:13:10:13:10 | x | -2147483648 |

View File

@@ -533,3 +533,72 @@ int mul_by_constant(int i, int j) {
return 0;
}
int notequal_type_endpoint(unsigned n) {
out(n); // 0 ..
if (n > 0) {
out(n); // 1 ..
}
if (n != 0) {
out(n); // 1 ..
} else {
out(n); // 0 .. 0
}
if (!n) {
out(n); // 0 .. 0
} else {
out(n); // 1 .. [BUG: lower bound is deduced to be 0]
}
while (n != 0) {
n--; // 1 ..
}
out(n); // 0 .. 0
}
void notequal_refinement(short n) {
if (n < 0)
return;
if (n == 0) {
out(n); // 0 .. 0
} else {
out(n); // 1 ..
}
if (n) {
out(n); // 1 .. [BUG: lower bound is deduced to be 0]
} else {
out(n); // 0 .. 0
}
while (n != 0) {
n--; // 1 ..
}
out(n); // 0 .. 0
}
void notequal_variations(short n, float f) {
if (n != 0) {
if (n >= 0) {
out(n); // 1 .. [BUG: we can't handle `!=` coming first]
}
}
if (n >= 5) {
if (2 * n - 10 == 0) { // Same as `n == 10/2` (modulo overflow)
return;
}
out(n); // 6 ..
}
if (n != -32768 && n != -32767) {
out(n); // -32766 ..
}
}

View File

@@ -532,6 +532,37 @@
| test.c:530:3:530:3 | i | 2147483647 |
| test.c:530:10:530:11 | sc | 1 |
| test.c:532:7:532:7 | i | 127 |
| test.c:539:7:539:7 | n | 4294967295 |
| test.c:541:7:541:7 | n | 4294967295 |
| test.c:542:9:542:9 | n | 4294967295 |
| test.c:545:7:545:7 | n | 4294967295 |
| test.c:546:9:546:9 | n | 4294967295 |
| test.c:548:9:548:9 | n | 0 |
| test.c:551:8:551:8 | n | 4294967295 |
| test.c:552:9:552:9 | n | 4294967295 |
| test.c:554:9:554:9 | n | 4294967295 |
| test.c:557:10:557:10 | n | 4294967295 |
| test.c:558:5:558:5 | n | 4294967295 |
| test.c:561:7:561:7 | n | 0 |
| test.c:565:7:565:7 | n | 32767 |
| test.c:568:7:568:7 | n | 32767 |
| test.c:569:9:569:9 | n | 0 |
| test.c:571:9:571:9 | n | 32767 |
| test.c:574:7:574:7 | n | 32767 |
| test.c:575:9:575:9 | n | 32767 |
| test.c:577:9:577:9 | n | 32767 |
| test.c:580:10:580:10 | n | 32767 |
| test.c:581:5:581:5 | n | 32767 |
| test.c:584:7:584:7 | n | 0 |
| test.c:588:7:588:7 | n | 32767 |
| test.c:589:9:589:9 | n | 32767 |
| test.c:590:11:590:11 | n | 32767 |
| test.c:594:7:594:7 | n | 32767 |
| test.c:595:13:595:13 | n | 32767 |
| test.c:598:9:598:9 | n | 32767 |
| test.c:601:7:601:7 | n | 32767 |
| test.c:601:22:601:22 | n | 32767 |
| test.c:602:9:602:9 | n | 32767 |
| test.cpp:10:7:10:7 | b | 2147483647 |
| test.cpp:11:5:11:5 | x | 2147483647 |
| test.cpp:13:10:13:10 | x | 2147483647 |

View File

@@ -1,8 +1,8 @@
/** Step Summaries and Type Tracking */
import python
import internal.DataFlowPublic
import internal.DataFlowPrivate
private import python
private import internal.DataFlowPublic
private import internal.DataFlowPrivate
/** Any string that may appear as the name of an attribute or access path. */
class AttributeName extends string {
@@ -144,7 +144,7 @@ private newtype TTypeTracker = MkTypeTracker(Boolean hasCall, OptionalAttributeN
* It is recommended that all uses of this type are written in the following form,
* for tracking some type `myType`:
* ```
* Node myType(DataFlow::TypeTracker t) {
* DataFlow::Node myType(DataFlow::TypeTracker t) {
* t.start() and
* result = < source of myType >
* or
@@ -153,7 +153,7 @@ private newtype TTypeTracker = MkTypeTracker(Boolean hasCall, OptionalAttributeN
* )
* }
*
* DataFlow::SourceNode myType() { result = myType(DataFlow::TypeTracker::end()) }
* DataFlow::Node myType() { result = myType(DataFlow::TypeTracker::end()) }
* ```
*
* Instead of `result = myType(t2).track(t2, t)`, you can also use the equivalent
@@ -280,3 +280,10 @@ class TypeTracker extends TTypeTracker {
result = this
}
}
module TypeTracker {
/**
* Gets a valid end point of type tracking.
*/
TypeTracker end() { result.end() }
}

View File

@@ -0,0 +1,11 @@
import os
from flask import Flask, request
app = Flask(__name__)
@app.route("/command1")
def command_injection1():
files = request.args.get('files', '')
# Don't let files be `; rm -rf /`
os.system("ls " + files)

View File

@@ -0,0 +1,11 @@
os_import
| test.py:2:8:2:9 | GSSA Variable os |
flowstep
jumpStep
| test.py:2:8:2:9 | GSSA Variable os | test.py:5:7:5:21 | ControlFlowNode for Flask() |
| test.py:2:8:2:9 | GSSA Variable os | test.py:7:2:7:23 | ControlFlowNode for Attribute() |
| test.py:2:8:2:9 | GSSA Variable os | test.py:7:2:7:23 | ControlFlowNode for Attribute()() |
essaFlowStep
| test.py:2:8:2:9 | GSSA Variable os | test.py:5:7:5:21 | ControlFlowNode for Flask() |
| test.py:2:8:2:9 | GSSA Variable os | test.py:7:2:7:23 | ControlFlowNode for Attribute() |
| test.py:2:8:2:9 | GSSA Variable os | test.py:7:2:7:23 | ControlFlowNode for Attribute()() |

View File

@@ -0,0 +1,36 @@
import python
import experimental.dataflow.DataFlow
/** Gets the EssaNode that holds the module imported by the fully qualified module name `name` */
DataFlow::EssaNode module_import(string name) {
exists(Variable var, Import imp, Alias alias |
alias = imp.getAName() and
alias.getAsname() = var.getAStore() and
(
name = alias.getValue().(ImportMember).getImportedModuleName()
or
name = alias.getValue().(ImportExpr).getImportedModuleName()
) and
result.getVar().(AssignmentDefinition).getSourceVariable() = var
)
}
query predicate os_import(DataFlow::Node node) {
node = module_import("os") and
exists(node.getLocation().getFile().getRelativePath())
}
query predicate flowstep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
os_import(nodeFrom) and
DataFlow::localFlowStep(nodeFrom, nodeTo)
}
query predicate jumpStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
os_import(nodeFrom) and
DataFlow::jumpStep(nodeFrom, nodeTo)
}
query predicate essaFlowStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
os_import(nodeFrom) and
DataFlow::EssaFlow::essaFlowStep(nodeFrom, nodeTo)
}

View File

@@ -1,8 +1,9 @@
import python
import experimental.dataflow.DataFlow
import experimental.dataflow.TypeTracker
import TestUtilities.InlineExpectationsTest
Node tracked(TypeTracker t) {
DataFlow::Node tracked(TypeTracker t) {
t.start() and
result.asCfgNode() = any(NameNode n | n.getId() = "tracked")
or
@@ -15,7 +16,7 @@ class TrackedTest extends InlineExpectationsTest {
override string getARelevantTag() { result = "tracked" }
override predicate hasActualResult(Location location, string element, string tag, string value) {
exists(Node e, TypeTracker t |
exists(DataFlow::Node e, TypeTracker t |
e = tracked(t) and
tag = "tracked" and
location = e.getLocation() and
@@ -25,14 +26,14 @@ class TrackedTest extends InlineExpectationsTest {
}
}
Node int_type(TypeTracker t) {
DataFlow::Node int_type(TypeTracker t) {
t.start() and
result.asCfgNode() = any(CallNode c | c.getFunction().(NameNode).getId() = "int")
or
exists(TypeTracker t2 | result = int_type(t2).track(t2, t))
}
Node string_type(TypeTracker t) {
DataFlow::Node string_type(TypeTracker t) {
t.start() and
result.asCfgNode() = any(CallNode c | c.getFunction().(NameNode).getId() = "str")
or
@@ -45,7 +46,7 @@ class TrackedIntTest extends InlineExpectationsTest {
override string getARelevantTag() { result = "int" }
override predicate hasActualResult(Location location, string element, string tag, string value) {
exists(Node e, TypeTracker t |
exists(DataFlow::Node e, TypeTracker t |
e = int_type(t) and
tag = "int" and
location = e.getLocation() and
@@ -61,7 +62,7 @@ class TrackedStringTest extends InlineExpectationsTest {
override string getARelevantTag() { result = "str" }
override predicate hasActualResult(Location location, string element, string tag, string value) {
exists(Node e, TypeTracker t |
exists(DataFlow::Node e, TypeTracker t |
e = string_type(t) and
tag = "str" and
location = e.getLocation() and