Skip to content

Commit

Permalink
C++: Tweak the bounded barrier
Browse files Browse the repository at this point in the history
  • Loading branch information
paldepind committed Aug 29, 2024
1 parent 047a655 commit e7f059a
Show file tree
Hide file tree
Showing 5 changed files with 110 additions and 79 deletions.
44 changes: 21 additions & 23 deletions cpp/ql/src/Security/CWE/CWE-190/Bounded.qll
Original file line number Diff line number Diff line change
@@ -1,27 +1,25 @@
/**
* This file provides the `bounded` predicate that is used in both `cpp/uncontrolled-arithmetic`
* and `cpp/tainted-arithmetic`.
* This file provides the `bounded` predicate that is used in `cpp/uncontrolled-arithmetic`,
* `cpp/tainted-arithmetic` and `cpp/uncontrolled-allocation-size`.
*/

private import cpp
private import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils

/**
* An operand `e` of a bitwise and expression `andExpr` (i.e., `andExpr` is either an `BitwiseAndExpr`
* or an `AssignAndExpr`) with operands `operand1` and `operand2` is the operand that is not `e` is upper
* bounded by some number that is less than the maximum integer allowed by the result type of `andExpr`.
* An operand `operand` of a bitwise and expression `andExpr` (i.e., `andExpr` is either a
* `BitwiseAndExpr` or an `AssignAndExpr`) is upper bounded by some number that is less than the
* maximum integer allowed by the result type of `andExpr`.
*/
pragma[inline]
private predicate boundedBitwiseAnd(Expr e, Expr andExpr, Expr operand1, Expr operand2) {
operand1 != operand2 and
e = operand1 and
upperBound(operand2.getFullyConverted()) < exprMaxVal(andExpr.getFullyConverted())
private predicate boundedBitwiseAnd(Expr operand, Expr andExpr) {
upperBound(operand.getFullyConverted()) < exprMaxVal(andExpr.getFullyConverted())
}

/**
* Holds if `e` is an arithmetic expression that cannot overflow, or if `e` is an operand of an
* operation that may greatly reduce the range of possible values.
* Holds if `e` is an arithmetic expression that cannot overflow, or if `e` is an operation that
* may greatly reduce the range of possible values.
*/
predicate bounded(Expr e) {
// There can be two separate reasons for `convertedExprMightOverflow` not holding:
Expand All @@ -35,25 +33,25 @@ predicate bounded(Expr e) {
) and
not convertedExprMightOverflow(e)
or
// Optimistically assume that a remainder expression always yields a much smaller value.
e = any(RemExpr rem).getLeftOperand()
// Optimistically assume that the following operations always yields a much smaller value.
e instanceof RemExpr
or
e = any(AssignRemExpr rem).getLValue()
e instanceof DivExpr
or
exists(BitwiseAndExpr andExpr |
boundedBitwiseAnd(e, andExpr, andExpr.getAnOperand(), andExpr.getAnOperand())
)
e instanceof RShiftExpr
or
exists(AssignAndExpr andExpr |
boundedBitwiseAnd(e, andExpr, andExpr.getAnOperand(), andExpr.getAnOperand())
exists(BitwiseAndExpr andExpr |
e = andExpr and boundedBitwiseAnd(andExpr.getAnOperand(), andExpr)
)
or
// Optimistically assume that a division always yields a much smaller value.
e = any(DivExpr div).getLeftOperand()
// For the assignment variant of the operations we place the barrier on the assigned lvalue.
e = any(AssignRemExpr rem).getLValue()
or
e = any(AssignDivExpr div).getLValue()
or
e = any(RShiftExpr shift).getLeftOperand()
or
e = any(AssignRShiftExpr div).getLValue()
or
exists(AssignAndExpr andExpr |
e = andExpr.getLValue() and boundedBitwiseAnd(andExpr.getRValue(), andExpr)
)
}
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,8 @@ edges
| test.cpp:24:11:24:18 | call to get_rand | test.cpp:25:7:25:7 | r | provenance | |
| test.cpp:30:13:30:14 | get_rand2 output argument | test.cpp:31:7:31:7 | r | provenance | |
| test.cpp:36:13:36:13 | get_rand3 output argument | test.cpp:37:7:37:7 | r | provenance | |
| test.cpp:62:19:62:24 | call to rand | test.cpp:62:19:62:24 | call to rand | provenance | |
| test.cpp:62:19:62:24 | call to rand | test.cpp:65:9:65:9 | x | provenance | |
| test.cpp:86:10:86:13 | call to rand | test.cpp:86:10:86:13 | call to rand | provenance | |
| test.cpp:86:10:86:13 | call to rand | test.cpp:90:10:90:10 | x | provenance | |
| test.cpp:98:10:98:13 | call to rand | test.cpp:98:10:98:13 | call to rand | provenance | |
Expand Down Expand Up @@ -105,6 +107,9 @@ nodes
| test.cpp:31:7:31:7 | r | semmle.label | r |
| test.cpp:36:13:36:13 | get_rand3 output argument | semmle.label | get_rand3 output argument |
| test.cpp:37:7:37:7 | r | semmle.label | r |
| test.cpp:62:19:62:24 | call to rand | semmle.label | call to rand |
| test.cpp:62:19:62:24 | call to rand | semmle.label | call to rand |
| test.cpp:65:9:65:9 | x | semmle.label | x |
| test.cpp:86:10:86:13 | call to rand | semmle.label | call to rand |
| test.cpp:86:10:86:13 | call to rand | semmle.label | call to rand |
| test.cpp:90:10:90:10 | x | semmle.label | x |
Expand Down Expand Up @@ -156,6 +161,7 @@ subpaths
| test.cpp:25:7:25:7 | r | test.cpp:8:9:8:12 | call to rand | test.cpp:25:7:25:7 | r | This arithmetic expression depends on an $@, potentially causing an overflow. | test.cpp:8:9:8:12 | call to rand | uncontrolled value |
| test.cpp:31:7:31:7 | r | test.cpp:13:10:13:13 | call to rand | test.cpp:31:7:31:7 | r | This arithmetic expression depends on an $@, potentially causing an overflow. | test.cpp:13:10:13:13 | call to rand | uncontrolled value |
| test.cpp:37:7:37:7 | r | test.cpp:18:9:18:12 | call to rand | test.cpp:37:7:37:7 | r | This arithmetic expression depends on an $@, potentially causing an overflow. | test.cpp:18:9:18:12 | call to rand | uncontrolled value |
| test.cpp:65:9:65:9 | x | test.cpp:62:19:62:24 | call to rand | test.cpp:65:9:65:9 | x | This arithmetic expression depends on an $@, potentially causing an underflow. | test.cpp:62:19:62:22 | call to rand | uncontrolled value |
| test.cpp:90:10:90:10 | x | test.cpp:86:10:86:13 | call to rand | test.cpp:90:10:90:10 | x | This arithmetic expression depends on an $@, potentially causing an overflow. | test.cpp:86:10:86:13 | call to rand | uncontrolled value |
| test.cpp:102:10:102:10 | x | test.cpp:98:10:98:13 | call to rand | test.cpp:102:10:102:10 | x | This arithmetic expression depends on an $@, potentially causing an overflow. | test.cpp:98:10:98:13 | call to rand | uncontrolled value |
| test.cpp:146:9:146:9 | y | test.cpp:137:10:137:13 | call to rand | test.cpp:146:9:146:9 | y | This arithmetic expression depends on an $@, potentially causing an overflow. | test.cpp:137:10:137:13 | call to rand | uncontrolled value |
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ unsigned int test_remainder_subtract_unsigned()
unsigned int x = rand();
unsigned int y = x % 100; // y <= x

return x - y; // GOOD (as y <= x)
return x - y; // GOOD (as y <= x) [FALSE POSITIVE]
}

typedef unsigned long size_t;
Expand Down
Loading

0 comments on commit e7f059a

Please sign in to comment.