53
53
54
54
private import cpp
55
55
private import semmle.code.cpp.ir.dataflow.internal.ProductFlow
56
+ private import semmle.code.cpp.security.ProductFlowUtils.ProductFlowUtils
56
57
private import semmle.code.cpp.ir.ValueNumbering
57
58
private import semmle.code.cpp.controlflow.IRGuards
58
59
private import codeql.util.Unit
59
60
private import semmle.code.cpp.rangeanalysis.new.RangeAnalysisUtil
60
61
61
- private VariableAccess getAVariableAccess ( Expr e ) { e .getAChild * ( ) = result }
62
-
63
- /**
64
- * Gets a (sub)expression that may be the result of evaluating `size`.
65
- *
66
- * For example, `getASizeCandidate(a ? b : c)` gives `a ? b : c`, `b` and `c`.
67
- */
68
- bindingset [ size]
69
- pragma [ inline_late]
70
- private Expr getASizeCandidate ( Expr size ) {
71
- result = size
72
- or
73
- result = [ size .( ConditionalExpr ) .getThen ( ) , size .( ConditionalExpr ) .getElse ( ) ]
74
- }
75
-
76
- /**
77
- * Holds if the `(n, state)` pair represents the source of flow for the size
78
- * expression associated with `alloc`.
79
- */
80
- predicate hasSize ( HeuristicAllocationExpr alloc , DataFlow:: Node n , int state ) {
81
- exists ( VariableAccess va , Expr size , int delta , Expr s |
82
- size = alloc .getSizeExpr ( ) and
83
- s = getASizeCandidate ( size ) and
84
- // Get the unique variable in a size expression like `x` in `malloc(x + 1)`.
85
- va = unique( | | getAVariableAccess ( s ) ) and
86
- // Compute `delta` as the constant difference between `x` and `x + 1`.
87
- bounded1 ( any ( Instruction instr | instr .getUnconvertedResultExpression ( ) = s ) ,
88
- any ( LoadInstruction load | load .getUnconvertedResultExpression ( ) = va ) , delta ) and
89
- n .asExpr ( ) = va and
90
- state = delta
91
- )
92
- }
93
-
94
62
/**
95
63
* Gets the virtual dispatch branching limit when calculating field flow while searching
96
64
* for flow from an allocation to the construction of an out-of-bounds pointer.
@@ -100,125 +68,6 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
100
68
*/
101
69
int allocationToInvalidPointerFieldFlowBranchLimit ( ) { result = 0 }
102
70
103
- /**
104
- * A module that encapsulates a barrier guard to remove false positives from flow like:
105
- * ```cpp
106
- * char *p = new char[size];
107
- * // ...
108
- * unsigned n = size;
109
- * // ...
110
- * if(n < size) {
111
- * use(*p[n]);
112
- * }
113
- * ```
114
- * In this case, the sink pair identified by the product flow library (without any additional barriers)
115
- * would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
116
- * instruction `pai = a + b` such that:
117
- * 1. the allocation flows to `a`, and
118
- * 2. `b <= n` where `n` is the `n` in `p[n]`
119
- * but because there's a strict comparison that compares `n` against the size of the allocation this
120
- * snippet is fine.
121
- */
122
- private module SizeBarrier {
123
- private module SizeBarrierConfig implements DataFlow:: ConfigSig {
124
- predicate isSource ( DataFlow:: Node source ) {
125
- // The sources is the same as in the sources for the second
126
- // projection in the `AllocToInvalidPointerConfig` module.
127
- hasSize ( _, source , _) and
128
- InterestingPointerAddInstruction:: isInterestingSize ( source )
129
- }
130
-
131
- int fieldFlowBranchLimit ( ) { result = allocationToInvalidPointerFieldFlowBranchLimit ( ) }
132
-
133
- /**
134
- * Holds if `small <= large + k` holds if `g` evaluates to `testIsTrue`.
135
- */
136
- additional predicate isSink (
137
- DataFlow:: Node small , DataFlow:: Node large , IRGuardCondition g , int k , boolean testIsTrue
138
- ) {
139
- // The sink is any "large" side of a relational comparison. i.e., the `large` expression
140
- // in a guard such as `small <= large + k`.
141
- g .comparesLt ( small .asOperand ( ) , large .asOperand ( ) , k + 1 , true , testIsTrue )
142
- }
143
-
144
- predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
145
- }
146
-
147
- module SizeBarrierFlow = DataFlow:: Global< SizeBarrierConfig > ;
148
-
149
- private int getASizeAddend ( DataFlow:: Node node ) {
150
- exists ( DataFlow:: Node source |
151
- SizeBarrierFlow:: flow ( source , node ) and
152
- hasSize ( _, source , result )
153
- )
154
- }
155
-
156
- /**
157
- * Holds if `small <= large + k` holds if `g` evaluates to `edge`.
158
- */
159
- private predicate operandGuardChecks (
160
- IRGuardCondition g , Operand small , DataFlow:: Node large , int k , boolean edge
161
- ) {
162
- SizeBarrierFlow:: flowTo ( large ) and
163
- SizeBarrierConfig:: isSink ( DataFlow:: operandNode ( small ) , large , g , k , edge )
164
- }
165
-
166
- /**
167
- * Gets an instruction `instr` that is guarded by a check such as `instr <= small + delta` where
168
- * `small <= _ + k` and `small` is the "small side" of of a relational comparison that checks
169
- * whether `small <= size` where `size` is the size of an allocation.
170
- */
171
- Instruction getABarrierInstruction0 ( int delta , int k ) {
172
- exists (
173
- IRGuardCondition g , ValueNumber value , Operand small , boolean edge , DataFlow:: Node large
174
- |
175
- // We know:
176
- // 1. result <= value + delta (by `bounded`)
177
- // 2. value <= large + k (by `operandGuardChecks`).
178
- // So:
179
- // result <= value + delta (by 1.)
180
- // <= large + k + delta (by 2.)
181
- small = value .getAUse ( ) and
182
- operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( small ) , large ,
183
- pragma [ only_bind_into ] ( k ) , pragma [ only_bind_into ] ( edge ) ) and
184
- bounded ( result , value .getAnInstruction ( ) , delta ) and
185
- g .controls ( result .getBlock ( ) , edge ) and
186
- k < getASizeAddend ( large )
187
- )
188
- }
189
-
190
- /**
191
- * Gets an instruction that is guarded by a guard condition which ensures that
192
- * the value of the instruction is upper-bounded by size of some allocation.
193
- */
194
- bindingset [ state]
195
- pragma [ inline_late]
196
- Instruction getABarrierInstruction ( int state ) {
197
- exists ( int delta , int k |
198
- state > k + delta and
199
- // result <= "size of allocation" + delta + k
200
- // < "size of allocation" + state
201
- result = getABarrierInstruction0 ( delta , k )
202
- )
203
- }
204
-
205
- /**
206
- * Gets a `DataFlow::Node` that is guarded by a guard condition which ensures that
207
- * the value of the node is upper-bounded by size of some allocation.
208
- */
209
- DataFlow:: Node getABarrierNode ( int state ) {
210
- exists ( DataFlow:: Node source , int delta , int k |
211
- SizeBarrierFlow:: flow ( source , result ) and
212
- hasSize ( _, source , state ) and
213
- result .asInstruction ( ) = SizeBarrier:: getABarrierInstruction0 ( delta , k ) and
214
- state > k + delta
215
- // so now we have:
216
- // result <= "size of allocation" + delta + k
217
- // < "size of allocation" + state
218
- )
219
- }
220
- }
221
-
222
71
private module InterestingPointerAddInstruction {
223
72
private module PointerAddInstructionConfig implements DataFlow:: ConfigSig {
224
73
predicate isSource ( DataFlow:: Node source ) {
@@ -227,7 +76,7 @@ private module InterestingPointerAddInstruction {
227
76
hasSize ( source .asExpr ( ) , _, _)
228
77
}
229
78
230
- int fieldFlowBranchLimit ( ) { result = allocationToInvalidPointerFieldFlowBranchLimit ( ) }
79
+ predicate fieldFlowBranchLimit = allocationToInvalidPointerFieldFlowBranchLimit / 0 ;
231
80
232
81
predicate isSink ( DataFlow:: Node sink ) {
233
82
sink .asInstruction ( ) = any ( PointerAddInstruction pai ) .getLeft ( )
@@ -263,6 +112,17 @@ private module InterestingPointerAddInstruction {
263
112
}
264
113
}
265
114
115
+ private module SizeBarrierInput implements SizeBarrierInputSig {
116
+ predicate fieldFlowBranchLimit = allocationToInvalidPointerFieldFlowBranchLimit / 0 ;
117
+
118
+ predicate isSource ( DataFlow:: Node source ) {
119
+ // The sources is the same as in the sources for the second
120
+ // projection in the `AllocToInvalidPointerConfig` module.
121
+ hasSize ( _, source , _) and
122
+ InterestingPointerAddInstruction:: isInterestingSize ( source )
123
+ }
124
+ }
125
+
266
126
/**
267
127
* A product-flow configuration for flow from an `(allocation, size)` pair to a
268
128
* pointer-arithmetic operation `pai` such that `pai <= allocation + size`.
@@ -301,7 +161,7 @@ private module Config implements ProductFlow::StateConfigSig {
301
161
private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
302
162
303
163
predicate isBarrier2 ( DataFlow:: Node node , FlowState2 state ) {
304
- node = SizeBarrier:: getABarrierNode ( state )
164
+ node = SizeBarrier< SizeBarrierInput > :: getABarrierNode ( state )
305
165
}
306
166
307
167
predicate isBarrier2 ( DataFlow:: Node node ) {
@@ -357,8 +217,8 @@ private predicate pointerAddInstructionHasBounds0(
357
217
sizeInstr = sizeSink .asInstruction ( ) and
358
218
// pai.getRight() <= sizeSink + delta
359
219
bounded1 ( right , sizeInstr , delta ) and
360
- not right = SizeBarrier:: getABarrierInstruction ( delta ) and
361
- not sizeInstr = SizeBarrier:: getABarrierInstruction ( delta )
220
+ not right = SizeBarrier< SizeBarrierInput > :: getABarrierInstruction ( delta ) and
221
+ not sizeInstr = SizeBarrier< SizeBarrierInput > :: getABarrierInstruction ( delta )
362
222
)
363
223
}
364
224
0 commit comments