Data flow: Model field clearing.

cf https://github.com/github/codeql/pull/3762
This commit is contained in:
Max Schaefer
2020-06-29 11:06:35 +01:00
parent f7ed65692f
commit 2b3e3bda8f
4 changed files with 34 additions and 8 deletions

View File

@@ -19,7 +19,7 @@ import DataFlowImplSpecific::Public
* a subclass whose characteristic predicate is a unique singleton string.
* For example, write
*
* ```
* ```ql
* class MyAnalysisConfiguration extends DataFlow::Configuration {
* MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
* // Override `isSource` and `isSink`.
@@ -37,7 +37,7 @@ import DataFlowImplSpecific::Public
* Then, to query whether there is flow between some `source` and `sink`,
* write
*
* ```
* ```ql
* exists(MyAnalysisConfiguration cfg | cfg.hasFlow(source, sink))
* ```
*
@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
}
private module LocalFlowBigStep {
/**
* A node where some checking is required, and hence the big-step relation
* is not allowed to step over.
*/
private class FlowCheckNode extends Node {
FlowCheckNode() {
this instanceof CastNode or
clearsContent(this, _)
}
}
/**
* Holds if `node` can be the first node in a maximal subsequence of local
* flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
node instanceof OutNodeExt or
store(_, _, node, _) or
read(_, _, node) or
node instanceof CastNode
node instanceof FlowCheckNode
)
}
@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
read(node, _, next)
)
or
node instanceof CastNode
node instanceof FlowCheckNode
or
config.isSink(node)
}
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
exists(Node mid |
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
localFlowStepNodeCand1(mid, node2, config) and
not mid instanceof CastNode and
not mid instanceof FlowCheckNode and
nodeCand2(node2, unbind(config))
)
or
exists(Node mid |
localFlowStepPlus(node1, mid, _, _, config, cc) and
additionalLocalFlowStepNodeCand2(mid, node2, config) and
not mid instanceof CastNode and
not mid instanceof FlowCheckNode and
preservesValue = false and
t = getErasedNodeTypeBound(node2) and
nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
Configuration config
) {
flowCandFwd0(node, fromArg, argApf, apf, config) and
not apf.isClearedAt(node) and
if node instanceof CastingNode
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
else any()

View File

@@ -754,6 +754,13 @@ abstract class AccessPathFront extends TAccessPathFront {
abstract boolean toBoolNonEmpty();
predicate headUsesContent(TypedContent tc) { this = TFrontHead(tc) }
predicate isClearedAt(Node n) {
exists(TypedContent tc |
this.headUsesContent(tc) and
clearsContent(n, tc.getContent())
)
}
}
class AccessPathFrontNil extends AccessPathFront, TFrontNil {

View File

@@ -141,6 +141,13 @@ predicate readStep(Node node1, Content f, Node node2) {
)
}
/**
* Holds if values stored inside content `c` are cleared at node `n`.
*/
predicate clearsContent(Node n, Content c) {
none() // stub implementation
}
/**
* Gets a representative (boxed) type for `t` for the purpose of pruning
* possible flow. A single type is used for all numeric types to account for

View File

@@ -26,7 +26,7 @@ private import TaintTrackingParameter::Private
* To create a configuration, extend this class with a subclass whose
* characteristic predicate is a unique singleton string. For example, write
*
* ```
* ```ql
* class MyAnalysisConfiguration extends TaintTracking::Configuration {
* MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
* // Override `isSource` and `isSink`.
@@ -41,7 +41,7 @@ private import TaintTrackingParameter::Private
* Then, to query whether there is flow between some `source` and `sink`,
* write
*
* ```
* ```ql
* exists(MyAnalysisConfiguration cfg | cfg.hasFlow(source, sink))
* ```
*