5353
5454private import cpp
5555private import semmle.code.cpp.ir.dataflow.internal.ProductFlow
56+ private import semmle.code.cpp.security.ProductFlowUtils.ProductFlowUtils
5657private import semmle.code.cpp.ir.ValueNumbering
5758private import semmle.code.cpp.controlflow.IRGuards
5859private import codeql.util.Unit
5960private import semmle.code.cpp.rangeanalysis.new.RangeAnalysisUtil
6061
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-
9462/**
9563 * Gets the virtual dispatch branching limit when calculating field flow while searching
9664 * 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) {
10068 */
10169int allocationToInvalidPointerFieldFlowBranchLimit ( ) { result = 0 }
10270
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-
22271private module InterestingPointerAddInstruction {
22372 private module PointerAddInstructionConfig implements DataFlow:: ConfigSig {
22473 predicate isSource ( DataFlow:: Node source ) {
@@ -227,7 +76,7 @@ private module InterestingPointerAddInstruction {
22776 hasSize ( source .asExpr ( ) , _, _)
22877 }
22978
230- int fieldFlowBranchLimit ( ) { result = allocationToInvalidPointerFieldFlowBranchLimit ( ) }
79+ predicate fieldFlowBranchLimit = allocationToInvalidPointerFieldFlowBranchLimit / 0 ;
23180
23281 predicate isSink ( DataFlow:: Node sink ) {
23382 sink .asInstruction ( ) = any ( PointerAddInstruction pai ) .getLeft ( )
@@ -263,6 +112,17 @@ private module InterestingPointerAddInstruction {
263112 }
264113}
265114
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+
266126/**
267127 * A product-flow configuration for flow from an `(allocation, size)` pair to a
268128 * pointer-arithmetic operation `pai` such that `pai <= allocation + size`.
@@ -301,7 +161,7 @@ private module Config implements ProductFlow::StateConfigSig {
301161 private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
302162
303163 predicate isBarrier2 ( DataFlow:: Node node , FlowState2 state ) {
304- node = SizeBarrier:: getABarrierNode ( state )
164+ node = SizeBarrier< SizeBarrierInput > :: getABarrierNode ( state )
305165 }
306166
307167 predicate isBarrier2 ( DataFlow:: Node node ) {
@@ -357,8 +217,8 @@ private predicate pointerAddInstructionHasBounds0(
357217 sizeInstr = sizeSink .asInstruction ( ) and
358218 // pai.getRight() <= sizeSink + delta
359219 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 )
362222 )
363223}
364224
0 commit comments