Skip to content

Commit 9a0e94f

Browse files
jketemajketema
committed
Add flow state versions of isBarrierIn, isBarrierOut, and isBarrierGuard
1 parent 9642e59 commit 9a0e94f

File tree

50 files changed

+2238
-280
lines changed

Some content is hidden

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

50 files changed

+2238
-280
lines changed

‎cpp/ql/lib/change-notes/2022-03-14-flow-state-barriers.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
---
2+
category: feature
3+
---
4+
* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states.

‎cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll

Lines changed: 61 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -87,12 +87,30 @@ abstract class Configuration extends string {
8787
/** Holds if data flow into `node` is prohibited. */
8888
predicate isBarrierIn(Node node) { none() }
8989

90+
/**
91+
* Holds if data flow into `node` is prohibited when the flow state is
92+
* `state`
93+
*/
94+
predicate isBarrierIn(Node node, FlowState state) { none() }
95+
9096
/** Holds if data flow out of `node` is prohibited. */
9197
predicate isBarrierOut(Node node) { none() }
9298

99+
/**
100+
* Holds if data flow out of `node` is prohibited when the flow state is
101+
* `state`
102+
*/
103+
predicate isBarrierOut(Node node, FlowState state) { none() }
104+
93105
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
94106
predicate isBarrierGuard(BarrierGuard guard) { none() }
95107

108+
/**
109+
* Holds if data flow through nodes guarded by `guard` is prohibited when
110+
* the flow state is `state`
111+
*/
112+
predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
113+
96114
/**
97115
* Holds if the additional flow step from `node1` to `node2` must be taken
98116
* into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
305323
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
306324
}
307325

308-
private predicate inBarrier(NodeEx node, Configuration config) {
326+
private predicate fullInBarrier(NodeEx node, Configuration config) {
309327
exists(Node n |
310328
node.asNode() = n and
311329
config.isBarrierIn(n)
@@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
314332
)
315333
}
316334

317-
private predicate outBarrier(NodeEx node, Configuration config) {
335+
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
336+
exists(Node n |
337+
node.asNode() = n and
338+
config.isBarrierIn(n, state)
339+
|
340+
config.isSource(n, state)
341+
)
342+
}
343+
344+
private predicate fullOutBarrier(NodeEx node, Configuration config) {
318345
exists(Node n |
319346
node.asNode() = n and
320347
config.isBarrierOut(n)
@@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
323350
)
324351
}
325352

353+
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
354+
exists(Node n |
355+
node.asNode() = n and
356+
config.isBarrierOut(n, state)
357+
|
358+
config.isSink(n, state)
359+
)
360+
}
361+
326362
pragma[nomagic]
327363
private predicate fullBarrier(NodeEx node, Configuration config) {
328364
exists(Node n | node.asNode() = n |
@@ -348,6 +384,17 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
348384
exists(Node n |
349385
node.asNode() = n and
350386
config.isBarrier(n, state)
387+
or
388+
config.isBarrierIn(n, state) and
389+
not config.isSource(n, state)
390+
or
391+
config.isBarrierOut(n, state) and
392+
not config.isSink(n, state)
393+
or
394+
exists(BarrierGuard g |
395+
config.isBarrierGuard(g, state) and
396+
n = g.getAGuardedNode()
397+
)
351398
)
352399
}
353400

@@ -376,8 +423,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
376423
/** Provides the relevant barriers for a step from `node1` to `node2`. */
377424
pragma[inline]
378425
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
379-
not outBarrier(node1, config) and
380-
not inBarrier(node2, config) and
426+
not fullOutBarrier(node1, config) and
427+
not fullInBarrier(node2, config) and
381428
not fullBarrier(node1, config) and
382429
not fullBarrier(node2, config)
383430
}
@@ -430,6 +477,8 @@ private predicate additionalLocalStateStep(
430477
config.isAdditionalFlowStep(n1, s1, n2, s2) and
431478
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
432479
stepFilter(node1, node2, config) and
480+
not stateOutBarrier(node1, s1, config) and
481+
not stateInBarrier(node2, s2, config) and
433482
not stateBarrier(node1, s1, config) and
434483
not stateBarrier(node2, s2, config)
435484
)
@@ -471,6 +520,8 @@ private predicate additionalJumpStateStep(
471520
config.isAdditionalFlowStep(n1, s1, n2, s2) and
472521
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
473522
stepFilter(node1, node2, config) and
523+
not stateOutBarrier(node1, s1, config) and
524+
not stateInBarrier(node2, s2, config) and
474525
not stateBarrier(node1, s1, config) and
475526
not stateBarrier(node2, s2, config) and
476527
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +921,8 @@ private module Stage1 {
870921
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
871922
revFlow(node, true, config) and
872923
fwdFlow(node, true, config) and
873-
not inBarrier(node, config) and
874-
not outBarrier(node, config)
924+
not fullInBarrier(node, config) and
925+
not fullOutBarrier(node, config)
875926
}
876927

877928
/** Holds if flow may return from `callable`. */
@@ -966,8 +1017,8 @@ private predicate flowOutOfCallNodeCand1(
9661017
) {
9671018
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
9681019
Stage1::revFlow(ret, config) and
969-
not outBarrier(ret, config) and
970-
not inBarrier(out, config)
1020+
not fullOutBarrier(ret, config) and
1021+
not fullInBarrier(out, config)
9711022
}
9721023

9731024
pragma[nomagic]
@@ -988,8 +1039,8 @@ private predicate flowIntoCallNodeCand1(
9881039
) {
9891040
viableParamArgNodeCand1(call, p, arg, config) and
9901041
Stage1::revFlow(p, config) and
991-
not outBarrier(arg, config) and
992-
not inBarrier(p, config)
1042+
not fullOutBarrier(arg, config) and
1043+
not fullInBarrier(p, config)
9931044
}
9941045

9951046
/**

‎cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll

Lines changed: 61 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -87,12 +87,30 @@ abstract class Configuration extends string {
8787
/** Holds if data flow into `node` is prohibited. */
8888
predicate isBarrierIn(Node node) { none() }
8989

90+
/**
91+
* Holds if data flow into `node` is prohibited when the flow state is
92+
* `state`
93+
*/
94+
predicate isBarrierIn(Node node, FlowState state) { none() }
95+
9096
/** Holds if data flow out of `node` is prohibited. */
9197
predicate isBarrierOut(Node node) { none() }
9298

99+
/**
100+
* Holds if data flow out of `node` is prohibited when the flow state is
101+
* `state`
102+
*/
103+
predicate isBarrierOut(Node node, FlowState state) { none() }
104+
93105
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
94106
predicate isBarrierGuard(BarrierGuard guard) { none() }
95107

108+
/**
109+
* Holds if data flow through nodes guarded by `guard` is prohibited when
110+
* the flow state is `state`
111+
*/
112+
predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
113+
96114
/**
97115
* Holds if the additional flow step from `node1` to `node2` must be taken
98116
* into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
305323
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
306324
}
307325

308-
private predicate inBarrier(NodeEx node, Configuration config) {
326+
private predicate fullInBarrier(NodeEx node, Configuration config) {
309327
exists(Node n |
310328
node.asNode() = n and
311329
config.isBarrierIn(n)
@@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
314332
)
315333
}
316334

317-
private predicate outBarrier(NodeEx node, Configuration config) {
335+
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
336+
exists(Node n |
337+
node.asNode() = n and
338+
config.isBarrierIn(n, state)
339+
|
340+
config.isSource(n, state)
341+
)
342+
}
343+
344+
private predicate fullOutBarrier(NodeEx node, Configuration config) {
318345
exists(Node n |
319346
node.asNode() = n and
320347
config.isBarrierOut(n)
@@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
323350
)
324351
}
325352

353+
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
354+
exists(Node n |
355+
node.asNode() = n and
356+
config.isBarrierOut(n, state)
357+
|
358+
config.isSink(n, state)
359+
)
360+
}
361+
326362
pragma[nomagic]
327363
private predicate fullBarrier(NodeEx node, Configuration config) {
328364
exists(Node n | node.asNode() = n |
@@ -348,6 +384,17 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
348384
exists(Node n |
349385
node.asNode() = n and
350386
config.isBarrier(n, state)
387+
or
388+
config.isBarrierIn(n, state) and
389+
not config.isSource(n, state)
390+
or
391+
config.isBarrierOut(n, state) and
392+
not config.isSink(n, state)
393+
or
394+
exists(BarrierGuard g |
395+
config.isBarrierGuard(g, state) and
396+
n = g.getAGuardedNode()
397+
)
351398
)
352399
}
353400

@@ -376,8 +423,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
376423
/** Provides the relevant barriers for a step from `node1` to `node2`. */
377424
pragma[inline]
378425
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
379-
not outBarrier(node1, config) and
380-
not inBarrier(node2, config) and
426+
not fullOutBarrier(node1, config) and
427+
not fullInBarrier(node2, config) and
381428
not fullBarrier(node1, config) and
382429
not fullBarrier(node2, config)
383430
}
@@ -430,6 +477,8 @@ private predicate additionalLocalStateStep(
430477
config.isAdditionalFlowStep(n1, s1, n2, s2) and
431478
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
432479
stepFilter(node1, node2, config) and
480+
not stateOutBarrier(node1, s1, config) and
481+
not stateInBarrier(node2, s2, config) and
433482
not stateBarrier(node1, s1, config) and
434483
not stateBarrier(node2, s2, config)
435484
)
@@ -471,6 +520,8 @@ private predicate additionalJumpStateStep(
471520
config.isAdditionalFlowStep(n1, s1, n2, s2) and
472521
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
473522
stepFilter(node1, node2, config) and
523+
not stateOutBarrier(node1, s1, config) and
524+
not stateInBarrier(node2, s2, config) and
474525
not stateBarrier(node1, s1, config) and
475526
not stateBarrier(node2, s2, config) and
476527
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +921,8 @@ private module Stage1 {
870921
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
871922
revFlow(node, true, config) and
872923
fwdFlow(node, true, config) and
873-
not inBarrier(node, config) and
874-
not outBarrier(node, config)
924+
not fullInBarrier(node, config) and
925+
not fullOutBarrier(node, config)
875926
}
876927

877928
/** Holds if flow may return from `callable`. */
@@ -966,8 +1017,8 @@ private predicate flowOutOfCallNodeCand1(
9661017
) {
9671018
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
9681019
Stage1::revFlow(ret, config) and
969-
not outBarrier(ret, config) and
970-
not inBarrier(out, config)
1020+
not fullOutBarrier(ret, config) and
1021+
not fullInBarrier(out, config)
9711022
}
9721023

9731024
pragma[nomagic]
@@ -988,8 +1039,8 @@ private predicate flowIntoCallNodeCand1(
9881039
) {
9891040
viableParamArgNodeCand1(call, p, arg, config) and
9901041
Stage1::revFlow(p, config) and
991-
not outBarrier(arg, config) and
992-
not inBarrier(p, config)
1042+
not fullOutBarrier(arg, config) and
1043+
not fullInBarrier(p, config)
9931044
}
9941045

9951046
/**

0 commit comments

Comments
 (0)