Skip to content

Commit 37df9a6

Browse files
lcarteylcartey
committed
IntegerOverflow: Implement INT32-C
Adds a query to detect signed integer operation overflow/underflow. Initially this only supports add and subtract operations, and detects CERT recommended patterns of avoiding overflow/underflow.
1 parent 3f2db7a commit 37df9a6

File tree

6 files changed

+320
-0
lines changed

6 files changed

+320
-0
lines changed

‎c/cert/src/rules/INT32-C/SignedIntegerOverflow.md‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
# INT32-C: Ensure that operations on signed integers do not result in overflow
2+
3+
This query implements the CERT-C rule INT32-C:
4+
5+
> Ensure that operations on signed integers do not result in overflow
6+
7+
8+
## CERT
9+
10+
** REPLACE THIS BY RUNNING THE SCRIPT `scripts/help/cert-help-extraction.py` **
11+
12+
## Implementation notes
13+
14+
None
15+
16+
## References
17+
18+
* CERT-C: [INT32-C: Ensure that operations on signed integers do not result in overflow](https://wiki.sei.cmu.edu/confluence/display/c)

‎c/cert/src/rules/INT32-C/SignedIntegerOverflow.ql‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
/**
2+
* @id c/cert/signed-integer-overflow
3+
* @name INT32-C: Ensure that operations on signed integers do not result in overflow
4+
* @description
5+
* @kind problem
6+
* @precision high
7+
* @problem.severity error
8+
* @tags external/cert/id/int32-c
9+
* correctness
10+
* security
11+
* external/cert/obligation/rule
12+
*/
13+
14+
import cpp
15+
import codingstandards.c.cert
16+
import codingstandards.cpp.Overflow
17+
import semmle.code.cpp.controlflow.Guards
18+
import semmle.code.cpp.valuenumbering.GlobalValueNumbering
19+
20+
/* TODO: review the table to restrict to only those operations that actually overflow */
21+
from InterestingBinaryOverflowingExpr bop
22+
where
23+
not isExcluded(bop, IntegerOverflowPackage::signedIntegerOverflowQuery()) and
24+
bop.getType().getUnderlyingType().(IntegralType).isSigned() and
25+
// Not within a guard condition
26+
not exists(GuardCondition gc | gc.getAChild*() = bop) and
27+
// Not checked before the operation
28+
not bop.hasValidPreCheck() and
29+
// Not guarded by a check, where the check is not an invalid overflow check
30+
not bop.getAGuardingGVN() = globalValueNumber(bop.getAChild*())
31+
select bop,
32+
"Binary expression ..." + bop.getOperator() + "... of type " + bop.getType().getUnderlyingType() +
33+
" may overflow or underflow."

‎c/cert/test/rules/INT32-C/SignedIntegerOverflow.expected‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
| test.c:6:3:6:9 | ... + ... | Binary expression ...+... of type int may overflow or underflow. |
2+
| test.c:23:5:23:11 | ... + ... | Binary expression ...+... of type int may overflow or underflow. |
3+
| test.c:28:19:28:25 | ... + ... | Binary expression ...+... of type int may overflow or underflow. |
4+
| test.c:36:3:36:9 | ... - ... | Binary expression ...-... of type int may overflow or underflow. |
5+
| test.c:49:19:49:25 | ... - ... | Binary expression ...-... of type int may overflow or underflow. |

‎c/cert/test/rules/INT32-C/SignedIntegerOverflow.qlref‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
rules/INT32-C/SignedIntegerOverflow.ql

‎c/cert/test/rules/INT32-C/test.c‎

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
#include <limits.h>
2+
#include <stddef.h>
3+
#include <stdint.h>
4+
5+
void test_add_simple(signed int i1, signed int i2) {
6+
i1 + i2; // NON_COMPLIANT - not bounds checked
7+
}
8+
9+
void test_add_precheck(signed int i1, signed int i2) {
10+
// Style recommended by CERT
11+
if (((i2 > 0) && (i1 > (INT_MAX - i2))) ||
12+
((i2 < 0) && (i1 < (INT_MIN - i2)))) {
13+
// handle error
14+
} else {
15+
i1 + i2; // COMPLIANT - bounds appropriately checked
16+
}
17+
}
18+
19+
void test_add_precheck_2(signed int i1, signed int i2) {
20+
if (i1 + i2 < i1) { // Bad overflow check - undefined behavior
21+
// handle error
22+
} else {
23+
i1 + i2; // NON_COMPLIANT
24+
}
25+
}
26+
27+
void test_add_postcheck(signed int i1, signed int i2) {
28+
signed int i3 = i1 + i2; // NON_COMPLIANT - signed overflow is undefined
29+
// behavior, so checking afterwards is not sufficient
30+
if (i3 < i1) {
31+
// handle error
32+
}
33+
}
34+
35+
void test_sub_simple(signed int i1, signed int i2) {
36+
i1 - i2; // NON_COMPLIANT - not bounds checked
37+
}
38+
39+
void test_sub_precheck(signed int i1, signed int i2) {
40+
// Style recomended by CERT
41+
if ((i2 > 0 && i1 < INT_MIN + i2) || (i2 < 0 && i1 > INT_MAX + i2)) {
42+
// handle error
43+
} else {
44+
i1 - i2; // COMPLIANT - bounds checked
45+
}
46+
}
47+
48+
void test_sub_postcheck(signed int i1, signed int i2) {
49+
signed int i3 = i1 - i2; // NON_COMPLIANT - underflow is undefined behavior.
50+
if (i3 > i1) {
51+
// handle error
52+
}
53+
}
54+
55+
void test_mul_simple(signed int i1, signed int i2) {
56+
i1 *i2; // NON_COMPLIANT
57+
}
58+
59+
void test_mul_precheck(signed int i1, signed int i2) {
60+
signed long long tmp =
61+
(signed long long)i1 * (signed long long)i2; // COMPLIANT
62+
signed int result;
63+
64+
if (tmp > INT_MAX || tmp < INT_MIN) {
65+
// handle error
66+
} else {
67+
i1 *i2; // COMPLIANT - checked
68+
result = (signed int)tmp;
69+
}
70+
}
71+
72+
void test_mul_precheck_2(signed int i1, signed int i2) {
73+
if (i1 > 0) {
74+
if (i2 > 0) {
75+
if (i1 > (INT_MAX / i2)) {
76+
return; // handle error
77+
}
78+
} else {
79+
if (i2 < (INT_MIN / i1)) {
80+
// handle error
81+
return; // handle error
82+
}
83+
}
84+
} else {
85+
if (i2 > 0) {
86+
if (i1 < (INT_MIN / i2)) {
87+
// handle error
88+
return; // handle error
89+
}
90+
} else {
91+
if ((i1 != 0) && (i2 < (INT_MAX / i1))) {
92+
// handle error
93+
return; // handle error
94+
}
95+
}
96+
}
97+
i1 *i2; // COMPLIANT
98+
}
99+
100+
void test_simple_div(signed int i1, signed int i2) {
101+
if (i2 == 0) {
102+
// handle error
103+
} else {
104+
i1 / i2; // NON_COMPLIANT
105+
}
106+
}
107+
108+
void test_div_precheck(signed int i1, signed int i2) {
109+
if ((i2 == 0) || ((i1 == LONG_MIN) && (i2 == -1))) {
110+
/* Handle error */
111+
} else {
112+
i1 / i2; // COMPLIANT
113+
}
114+
}
115+
116+
void test_simple_rem(signed int i1, signed int i2) {
117+
if (i2 == 0) {
118+
// handle error
119+
} else {
120+
i1 % i2; // NON_COMPLIANT
121+
}
122+
}
123+
124+
void test_rem_precheck(signed int i1, signed int i2) {
125+
if ((i2 == 0) || ((i1 == LONG_MIN) && (i2 == -1))) {
126+
/* Handle error */
127+
} else {
128+
i1 % i2; // COMPLIANT
129+
}
130+
}
131+
132+
void test_simple_left_shift(signed int i1, signed int i2) {
133+
i1 << i2; // NON_COMPLIANT
134+
}
135+
136+
/* Returns the number of set bits */
137+
size_t popcount(uintmax_t num);
138+
139+
#define PRECISION(umax_value) popcount(umax_value)
140+
141+
void test_left_shift_precheck(signed int i1, signed int i2) {
142+
if ((i1 < 0) || (i2 < 0) || (i2 >= PRECISION(UINT_MAX)) ||
143+
(i1 > (INT_MAX >> i2))) {
144+
// handle error
145+
} else {
146+
i1 << i2; // COMPLIANT
147+
}
148+
}
149+
150+
void test_simple_negate(signed int i1) {
151+
-i1; // NON_COMPLIANT
152+
}
153+
154+
void test_negate_precheck(signed int i1) {
155+
if (i1 == INT_MIN) {
156+
// handle error
157+
} else {
158+
-i1; // COMPLIANT
159+
}
160+
}

‎cpp/common/src/codingstandards/cpp/Overflow.qll‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,105 @@ class InterestingBinaryOverflowingExpr extends BinaryArithmeticOperation {
4242
)
4343
}
4444

45+
/**
46+
* Holds if there is a correct validity check after this expression which may overflow.
47+
*/
48+
predicate hasValidPreCheck() {
49+
exists(GVN i1, GVN i2 |
50+
i1 = globalValueNumber(this.getLeftOperand()) and
51+
i2 = globalValueNumber(this.getRightOperand())
52+
or
53+
i2 = globalValueNumber(this.getLeftOperand()) and
54+
i1 = globalValueNumber(this.getRightOperand())
55+
|
56+
// The CERT rule for signed integer overflow has a very specific pattern it recommends
57+
// for checking for overflow. We try to match the pattern here.
58+
// ((i2 > 0 && i1 > (INT_MAX - i2)) || (i2 < 0 && i1 < (INT_MIN - i2)))
59+
this instanceof AddExpr and
60+
exists(LogicalOrExpr orExpr |
61+
// GuardCondition doesn't work in this case, so just confirm that this check dominates the overflow
62+
bbDominates(orExpr.getBasicBlock(), this.getBasicBlock()) and
63+
exists(LogicalAndExpr andExpr |
64+
andExpr = orExpr.getAnOperand() and
65+
exists(StrictRelationalOperation gt |
66+
gt = andExpr.getAnOperand() and
67+
gt.getLesserOperand().getValue() = "0" and
68+
globalValueNumber(gt.getGreaterOperand()) = i2
69+
) and
70+
exists(StrictRelationalOperation gt |
71+
gt = andExpr.getAnOperand() and
72+
gt.getLesserOperand() =
73+
any(SubExpr se |
74+
se.getLeftOperand().getValue().toFloat() = typeUpperBound(getType()) and
75+
globalValueNumber(se.getRightOperand()) = i2
76+
) and
77+
globalValueNumber(gt.getGreaterOperand()) = i1
78+
)
79+
) and
80+
exists(LogicalAndExpr andExpr |
81+
andExpr = orExpr.getAnOperand() and
82+
exists(StrictRelationalOperation gt |
83+
gt = andExpr.getAnOperand() and
84+
gt.getGreaterOperand().getValue() = "0" and
85+
globalValueNumber(gt.getLesserOperand()) = i2
86+
) and
87+
exists(StrictRelationalOperation gt |
88+
gt = andExpr.getAnOperand() and
89+
gt.getGreaterOperand() =
90+
any(SubExpr se |
91+
se.getLeftOperand().getValue().toFloat() = typeLowerBound(getType()) and
92+
globalValueNumber(se.getRightOperand()) = i2
93+
) and
94+
globalValueNumber(gt.getLesserOperand()) = i1
95+
)
96+
)
97+
)
98+
or
99+
// The CERT rule for signed integer overflow has a very specific pattern it recommends
100+
// for checking for underflow. We try to match the pattern here.
101+
// ((i2 > 0 && i1 > (INT_MIN + i2)) || (i2 < 0 && i1 < (INT_MAX + i2)))
102+
this instanceof SubExpr and
103+
exists(LogicalOrExpr orExpr |
104+
// GuardCondition doesn't work in this case, so just confirm that this check dominates the overflow
105+
bbDominates(orExpr.getBasicBlock(), this.getBasicBlock()) and
106+
exists(LogicalAndExpr andExpr |
107+
andExpr = orExpr.getAnOperand() and
108+
exists(StrictRelationalOperation gt |
109+
gt = andExpr.getAnOperand() and
110+
gt.getLesserOperand().getValue() = "0" and
111+
globalValueNumber(gt.getGreaterOperand()) = i2
112+
) and
113+
exists(StrictRelationalOperation gt |
114+
gt = andExpr.getAnOperand() and
115+
gt.getGreaterOperand() =
116+
any(AddExpr se |
117+
se.getLeftOperand().getValue().toFloat() = typeLowerBound(getType()) and
118+
globalValueNumber(se.getRightOperand()) = i2
119+
) and
120+
globalValueNumber(gt.getLesserOperand()) = i1
121+
)
122+
) and
123+
exists(LogicalAndExpr andExpr |
124+
andExpr = orExpr.getAnOperand() and
125+
exists(StrictRelationalOperation gt |
126+
gt = andExpr.getAnOperand() and
127+
gt.getGreaterOperand().getValue() = "0" and
128+
globalValueNumber(gt.getLesserOperand()) = i2
129+
) and
130+
exists(StrictRelationalOperation gt |
131+
gt = andExpr.getAnOperand() and
132+
gt.getLesserOperand() =
133+
any(AddExpr se |
134+
se.getLeftOperand().getValue().toFloat() = typeUpperBound(getType()) and
135+
globalValueNumber(se.getRightOperand()) = i2
136+
) and
137+
globalValueNumber(gt.getGreaterOperand()) = i1
138+
)
139+
)
140+
)
141+
)
142+
}
143+
45144
/**
46145
* Holds if there is a correct validity check after this expression which may overflow.
47146
*
@@ -90,3 +189,7 @@ class InterestingBinaryOverflowingExpr extends BinaryArithmeticOperation {
90189
)
91190
}
92191
}
192+
193+
private class StrictRelationalOperation extends RelationalOperation {
194+
StrictRelationalOperation() { this.getOperator() = [">", "<"] }
195+
}

0 commit comments

Comments
 (0)