Skip to content

Commit d1efffe

Browse files
authored
Merge branch 'main' into deref-size
2 parents b83aaf9 + e3aecd3 commit d1efffe

File tree

105 files changed

+3421
-2372
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

105 files changed

+3421
-2372
lines changed

.vscode/tasks.json

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,22 @@
2222
"command": "${config:python.pythonPath}",
2323
},
2424
"problemMatcher": []
25+
},
26+
{
27+
"label": "Accept .expected changes from CI",
28+
"type": "process",
29+
// Non-Windows OS will usually have Python 3 already installed at /usr/bin/python3.
30+
"command": "python3",
31+
"args": [
32+
"misc/scripts/accept-expected-changes-from-ci.py"
33+
],
34+
"group": "build",
35+
"windows": {
36+
// On Windows, use whatever Python interpreter is configured for this workspace. The default is
37+
// just `python`, so if Python is already on the path, this will find it.
38+
"command": "${config:python.pythonPath}",
39+
},
40+
"problemMatcher": []
2541
}
2642
]
27-
}
43+
}

CODEOWNERS

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,3 +40,6 @@ WORKSPACE.bazel @github/codeql-ci-reviewers
4040
/.github/workflows/ql-for-ql-* @github/codeql-ql-for-ql-reviewers
4141
/.github/workflows/ruby-* @github/codeql-ruby
4242
/.github/workflows/swift.yml @github/codeql-swift
43+
44+
# Misc
45+
/misc/scripts/accept-expected-changes-from-ci.py @RasmusWL

cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll

Lines changed: 87 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -290,9 +290,9 @@ module ProductFlow {
290290
predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn1(node) }
291291
}
292292

293-
module Flow1 = DataFlow::GlobalWithState<Config1>;
293+
private module Flow1 = DataFlow::GlobalWithState<Config1>;
294294

295-
module Config2 implements DataFlow::StateConfigSig {
295+
private module Config2 implements DataFlow::StateConfigSig {
296296
class FlowState = FlowState2;
297297

298298
predicate isSource(DataFlow::Node source, FlowState state) {
@@ -322,27 +322,90 @@ module ProductFlow {
322322
predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn2(node) }
323323
}
324324

325-
module Flow2 = DataFlow::GlobalWithState<Config2>;
325+
private module Flow2 = DataFlow::GlobalWithState<Config2>;
326326

327+
private predicate isSourcePair(Flow1::PathNode node1, Flow2::PathNode node2) {
328+
Config::isSourcePair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState())
329+
}
330+
331+
private predicate isSinkPair(Flow1::PathNode node1, Flow2::PathNode node2) {
332+
Config::isSinkPair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState())
333+
}
334+
335+
pragma[assume_small_delta]
327336
pragma[nomagic]
328-
private predicate reachableInterprocEntry(
329-
Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode node1, Flow2::PathNode node2
337+
private predicate fwdReachableInterprocEntry(Flow1::PathNode node1, Flow2::PathNode node2) {
338+
isSourcePair(node1, node2)
339+
or
340+
fwdIsSuccessor(_, _, node1, node2)
341+
}
342+
343+
pragma[nomagic]
344+
private predicate fwdIsSuccessorExit(
345+
Flow1::PathNode mid1, Flow2::PathNode mid2, Flow1::PathNode succ1, Flow2::PathNode succ2
330346
) {
331-
Config::isSourcePair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState()) and
332-
node1 = source1 and
333-
node2 = source2
347+
isSinkPair(mid1, mid2) and
348+
succ1 = mid1 and
349+
succ2 = mid2
334350
or
335-
exists(
336-
Flow1::PathNode midEntry1, Flow2::PathNode midEntry2, Flow1::PathNode midExit1,
337-
Flow2::PathNode midExit2
338-
|
339-
reachableInterprocEntry(source1, source2, midEntry1, midEntry2) and
340-
interprocEdgePair(midExit1, midExit2, node1, node2) and
341-
localPathStep1*(midEntry1, midExit1) and
342-
localPathStep2*(midEntry2, midExit2)
351+
interprocEdgePair(mid1, mid2, succ1, succ2)
352+
}
353+
354+
private predicate fwdIsSuccessor1(
355+
Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode mid1, Flow2::PathNode mid2,
356+
Flow1::PathNode succ1, Flow2::PathNode succ2
357+
) {
358+
fwdReachableInterprocEntry(pred1, pred2) and
359+
localPathStep1*(pred1, mid1) and
360+
fwdIsSuccessorExit(pragma[only_bind_into](mid1), pragma[only_bind_into](mid2), succ1, succ2)
361+
}
362+
363+
private predicate fwdIsSuccessor2(
364+
Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode mid1, Flow2::PathNode mid2,
365+
Flow1::PathNode succ1, Flow2::PathNode succ2
366+
) {
367+
fwdReachableInterprocEntry(pred1, pred2) and
368+
localPathStep2*(pred2, mid2) and
369+
fwdIsSuccessorExit(pragma[only_bind_into](mid1), pragma[only_bind_into](mid2), succ1, succ2)
370+
}
371+
372+
pragma[assume_small_delta]
373+
private predicate fwdIsSuccessor(
374+
Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode succ1, Flow2::PathNode succ2
375+
) {
376+
exists(Flow1::PathNode mid1, Flow2::PathNode mid2 |
377+
fwdIsSuccessor1(pred1, pred2, mid1, mid2, succ1, succ2) and
378+
fwdIsSuccessor2(pred1, pred2, mid1, mid2, succ1, succ2)
379+
)
380+
}
381+
382+
pragma[assume_small_delta]
383+
pragma[nomagic]
384+
private predicate revReachableInterprocEntry(Flow1::PathNode node1, Flow2::PathNode node2) {
385+
fwdReachableInterprocEntry(node1, node2) and
386+
isSinkPair(node1, node2)
387+
or
388+
exists(Flow1::PathNode succ1, Flow2::PathNode succ2 |
389+
revReachableInterprocEntry(succ1, succ2) and
390+
fwdIsSuccessor(node1, node2, succ1, succ2)
343391
)
344392
}
345393

394+
private newtype TNodePair =
395+
TMkNodePair(Flow1::PathNode node1, Flow2::PathNode node2) {
396+
revReachableInterprocEntry(node1, node2)
397+
}
398+
399+
private predicate pathSucc(TNodePair n1, TNodePair n2) {
400+
exists(Flow1::PathNode n11, Flow2::PathNode n12, Flow1::PathNode n21, Flow2::PathNode n22 |
401+
n1 = TMkNodePair(n11, n12) and
402+
n2 = TMkNodePair(n21, n22) and
403+
fwdIsSuccessor(n11, n12, n21, n22)
404+
)
405+
}
406+
407+
private predicate pathSuccPlus(TNodePair n1, TNodePair n2) = fastTC(pathSucc/2)(n1, n2)
408+
346409
private predicate localPathStep1(Flow1::PathNode pred, Flow1::PathNode succ) {
347410
Flow1::PathGraph::edges(pred, succ) and
348411
pragma[only_bind_out](pred.getNode().getEnclosingCallable()) =
@@ -474,11 +537,14 @@ module ProductFlow {
474537
private predicate reachable(
475538
Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode sink1, Flow2::PathNode sink2
476539
) {
477-
exists(Flow1::PathNode mid1, Flow2::PathNode mid2 |
478-
reachableInterprocEntry(source1, source2, mid1, mid2) and
479-
Config::isSinkPair(sink1.getNode(), sink1.getState(), sink2.getNode(), sink2.getState()) and
480-
localPathStep1*(mid1, sink1) and
481-
localPathStep2*(mid2, sink2)
540+
isSourcePair(source1, source2) and
541+
isSinkPair(sink1, sink2) and
542+
exists(TNodePair n1, TNodePair n2 |
543+
n1 = TMkNodePair(source1, source2) and
544+
n2 = TMkNodePair(sink1, sink2)
545+
|
546+
pathSuccPlus(n1, n2) or
547+
n1 = n2
482548
)
483549
}
484550
}

cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql

Lines changed: 152 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,149 @@ predicate isSinkPairImpl(
7878
)
7979
}
8080

81+
module ValidState {
82+
/**
83+
* In the `StringSizeConfig` configuration we use an integer as the flow state for the second
84+
* projection of the dataflow graph. The integer represents an offset that is added to the
85+
* size of the allocation. For example, given:
86+
* ```cpp
87+
* char* p = new char[size + 1];
88+
* size += 1;
89+
* memset(p, 0, size);
90+
* ```
91+
* the initial flow state is `1`. This represents the fact that `size + 1` is a valid bound
92+
* for the size of the allocation pointed to by `p`. After updating the size using `+=`, the
93+
* flow state changes to `0`, which represents the fact that `size + 0` is a valid bound for
94+
* the allocation.
95+
*
96+
* So we need to compute a set of valid integers that represent the offset applied to the
97+
* size. We do this in two steps:
98+
* 1. We first perform the dataflow traversal that the second projection of the product-flow
99+
* library will perform, and visit all the places where the size argument is modified.
100+
* 2. Once that dataflow traversal is done, we accumulate the offsets added at each places
101+
* where the offset is modified (see `validStateImpl`).
102+
*
103+
* Because we want to guarantee that each place where we modify the offset has a `PathNode`
104+
* we "flip" a boolean flow state in each `isAdditionalFlowStep`. This ensures that the node
105+
* has a corresponding `PathNode`.
106+
*/
107+
private module ValidStateConfig implements DataFlow::StateConfigSig {
108+
class FlowState = boolean;
109+
110+
predicate isSource(DataFlow::Node source, FlowState state) {
111+
hasSize(_, source, _) and
112+
state = false
113+
}
114+
115+
predicate isSink(DataFlow::Node sink, FlowState state) {
116+
isSinkPairImpl(_, _, sink, _, _) and
117+
state = [false, true]
118+
}
119+
120+
predicate isBarrier(DataFlow::Node node, FlowState state) { none() }
121+
122+
predicate isAdditionalFlowStep(
123+
DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2
124+
) {
125+
exists(AddInstruction add, Operand op, int delta |
126+
add.hasOperands(node1.asOperand(), op) and
127+
semBounded(getSemanticExpr(op.getDef()), any(SemZeroBound zero), delta, true, _) and
128+
node2.asInstruction() = add and
129+
state1 = [false, true] and
130+
state2 = state1.booleanNot()
131+
)
132+
}
133+
134+
predicate includeHiddenNodes() { any() }
135+
}
136+
137+
private import DataFlow::GlobalWithState<ValidStateConfig>
138+
139+
private predicate inLoop(PathNode n) { n.getASuccessor+() = n }
140+
141+
/**
142+
* Holds if `value` is a possible offset for `n`.
143+
*
144+
* To ensure termination, we limit `value` to be in the
145+
* range `[-2, 2]` if the node is part of a loop. Without
146+
* this restriction we wouldn't terminate on an example like:
147+
* ```cpp
148+
* while(unknown()) { size++; }
149+
* ```
150+
*/
151+
private predicate validStateImpl(PathNode n, int value) {
152+
// If the dataflow node depends recursively on itself we restrict the range.
153+
(inLoop(n) implies value = [-2 .. 2]) and
154+
(
155+
// For the dataflow source we have an allocation such as `malloc(size + k)`,
156+
// and the value of the flow-state is then `k`.
157+
hasSize(_, n.getNode(), value)
158+
or
159+
// For a dataflow sink any `value` that is strictly smaller than the delta
160+
// needs to be a valid flow-state. That is, for a snippet like:
161+
// ```
162+
// p = b ? new char[size] : new char[size + 1];
163+
// memset(p, 0, size + 2);
164+
// ```
165+
// the valid flow-states at the `memset` must include the set `{0, 1}` since the
166+
// flow-state at `new char[size]` is `0`, and the flow-state at `new char[size + 1]`
167+
// is `1`.
168+
//
169+
// So we find a valid flow-state at the sink's predecessor, and use the definition
170+
// of our sink predicate to compute the valid flow-states at the sink.
171+
exists(int delta, PathNode n0 |
172+
n0.getASuccessor() = n and
173+
validStateImpl(n0, value) and
174+
isSinkPairImpl(_, _, n.getNode(), delta, _) and
175+
delta > value
176+
)
177+
or
178+
// For a non-source and non-sink node there is two cases to consider.
179+
// 1. A node where we have to update the flow-state, or
180+
// 2. A node that doesn't update the flow-state.
181+
//
182+
// For case 1, we compute the new flow-state by adding the constant operand of the
183+
// `AddInstruction` to the flow-state of any predecessor node.
184+
// For case 2 we simply propagate the valid flow-states from the predecessor node to
185+
// the next one.
186+
exists(PathNode n0, DataFlow::Node node0, DataFlow::Node node, int value0 |
187+
n0.getASuccessor() = n and
188+
validStateImpl(n0, value0) and
189+
node = n.getNode() and
190+
node0 = n0.getNode()
191+
|
192+
exists(int delta |
193+
isAdditionalFlowStep2(node0, node, delta) and
194+
value0 = value + delta
195+
)
196+
or
197+
not isAdditionalFlowStep2(node0, node, _) and
198+
value = value0
199+
)
200+
)
201+
}
202+
203+
predicate validState(DataFlow::Node n, int value) {
204+
validStateImpl(any(PathNode pn | pn.getNode() = n), value)
205+
}
206+
}
207+
208+
import ValidState
209+
210+
/**
211+
* Holds if `node2` is a dataflow node that represents an addition of two operands `op1`
212+
* and `op2` such that:
213+
* 1. `node1` is the dataflow node that represents `op1`, and
214+
* 2. the value of `op2` can be upper bounded by `delta.`
215+
*/
216+
predicate isAdditionalFlowStep2(DataFlow::Node node1, DataFlow::Node node2, int delta) {
217+
exists(AddInstruction add, Operand op |
218+
add.hasOperands(node1.asOperand(), op) and
219+
semBounded(getSemanticExpr(op.getDef()), any(SemZeroBound zero), delta, true, _) and
220+
node2.asInstruction() = add
221+
)
222+
}
223+
81224
module StringSizeConfig implements ProductFlow::StateConfigSig {
82225
class FlowState1 = Unit;
83226

@@ -100,7 +243,7 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
100243
DataFlow::Node bufSink, FlowState1 state1, DataFlow::Node sizeSink, FlowState2 state2
101244
) {
102245
exists(state1) and
103-
state2 = [-32 .. 32] and // An arbitrary bound because we need to bound `state2`
246+
validState(sizeSink, state2) and
104247
exists(int delta |
105248
isSinkPairImpl(_, bufSink, sizeSink, delta, _) and
106249
delta > state2
@@ -111,6 +254,10 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
111254

112255
predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() }
113256

257+
predicate isBarrierOut2(DataFlow::Node node) {
258+
node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
259+
}
260+
114261
predicate isAdditionalFlowStep1(
115262
DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2
116263
) {
@@ -120,14 +267,10 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
120267
predicate isAdditionalFlowStep2(
121268
DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
122269
) {
123-
exists(AddInstruction add, Operand op, int delta, int s1, int s2 |
124-
s1 = [-32 .. 32] and // An arbitrary bound because we need to bound `state`
125-
state1 = s1 and
126-
state2 = s2 and
127-
add.hasOperands(node1.asOperand(), op) and
128-
semBounded(getSemanticExpr(op.getDef()), any(SemZeroBound zero), delta, true, _) and
129-
node2.asInstruction() = add and
130-
s1 = s2 + delta
270+
validState(node2, state2) and
271+
exists(int delta |
272+
isAdditionalFlowStep2(node1, node2, delta) and
273+
state1 = state2 + delta
131274
)
132275
}
133276
}

cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -324,6 +324,16 @@ query predicate edges(MergedPathNode node1, MergedPathNode node2) {
324324
joinOn2(node1.asPathNode3(), node2.asSinkNode(), _)
325325
}
326326

327+
query predicate subpaths(
328+
MergedPathNode arg, MergedPathNode par, MergedPathNode ret, MergedPathNode out
329+
) {
330+
AllocToInvalidPointerFlow::PathGraph1::subpaths(arg.asPathNode1(), par.asPathNode1(),
331+
ret.asPathNode1(), out.asPathNode1())
332+
or
333+
InvalidPointerToDerefFlow::PathGraph::subpaths(arg.asPathNode3(), par.asPathNode3(),
334+
ret.asPathNode3(), out.asPathNode3())
335+
}
336+
327337
/**
328338
* Holds if `p1` is a sink of `AllocToInvalidPointerConf` and `p2` is a source
329339
* of `InvalidPointerToDerefConf`, and they are connected through `pai`.

0 commit comments

Comments
 (0)