Merge pull request #210 from github/hvitved/dataflow/consistency

Data flow: Add consistency queries
This commit is contained in:
Tom Hvitved
2021-06-21 14:42:55 +02:00
committed by GitHub
5 changed files with 204 additions and 4 deletions

2
codeql

Submodule codeql updated: 96d8fc78f8...0febf5a592

View File

@@ -0,0 +1 @@
import codeql_ruby.dataflow.internal.DataFlowImplConsistency::Consistency

View File

@@ -0,0 +1,181 @@
/**
* Provides consistency queries for checking invariants in the language-specific
* data-flow classes and predicates.
*/
private import DataFlowImplSpecific::Private
private import DataFlowImplSpecific::Public
private import tainttracking1.TaintTrackingParameter::Private
private import tainttracking1.TaintTrackingParameter::Public
module Consistency {
private class RelevantNode extends Node {
RelevantNode() {
this instanceof ArgumentNode or
this instanceof ParameterNode or
this instanceof ReturnNode or
this = getAnOutNode(_, _) or
simpleLocalFlowStep(this, _) or
simpleLocalFlowStep(_, this) or
jumpStep(this, _) or
jumpStep(_, this) or
storeStep(this, _, _) or
storeStep(_, _, this) or
readStep(this, _, _) or
readStep(_, _, this) or
defaultAdditionalTaintStep(this, _) or
defaultAdditionalTaintStep(_, this)
}
}
query predicate uniqueEnclosingCallable(Node n, string msg) {
exists(int c |
n instanceof RelevantNode and
c = count(n.getEnclosingCallable()) and
c != 1 and
msg = "Node should have one enclosing callable but has " + c + "."
)
}
query predicate uniqueType(Node n, string msg) {
exists(int c |
n instanceof RelevantNode and
c = count(getNodeType(n)) and
c != 1 and
msg = "Node should have one type but has " + c + "."
)
}
query predicate uniqueNodeLocation(Node n, string msg) {
exists(int c |
c =
count(string filepath, int startline, int startcolumn, int endline, int endcolumn |
n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
) and
c != 1 and
msg = "Node should have one location but has " + c + "."
)
}
query predicate missingLocation(string msg) {
exists(int c |
c =
strictcount(Node n |
not exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
)
) and
msg = "Nodes without location: " + c
)
}
query predicate uniqueNodeToString(Node n, string msg) {
exists(int c |
c = count(n.toString()) and
c != 1 and
msg = "Node should have one toString but has " + c + "."
)
}
query predicate missingToString(string msg) {
exists(int c |
c = strictcount(Node n | not exists(n.toString())) and
msg = "Nodes without toString: " + c
)
}
query predicate parameterCallable(ParameterNode p, string msg) {
exists(DataFlowCallable c | p.isParameterOf(c, _) and c != p.getEnclosingCallable()) and
msg = "Callable mismatch for parameter."
}
query predicate localFlowIsLocal(Node n1, Node n2, string msg) {
simpleLocalFlowStep(n1, n2) and
n1.getEnclosingCallable() != n2.getEnclosingCallable() and
msg = "Local flow step does not preserve enclosing callable."
}
private DataFlowType typeRepr() { result = getNodeType(_) }
query predicate compatibleTypesReflexive(DataFlowType t, string msg) {
t = typeRepr() and
not compatibleTypes(t, t) and
msg = "Type compatibility predicate is not reflexive."
}
query predicate unreachableNodeCCtx(Node n, DataFlowCall call, string msg) {
isUnreachableInCall(n, call) and
exists(DataFlowCallable c |
c = n.getEnclosingCallable() and
not viableCallable(call) = c
) and
msg = "Call context for isUnreachableInCall is inconsistent with call graph."
}
query predicate localCallNodes(DataFlowCall call, Node n, string msg) {
(
n = getAnOutNode(call, _) and
msg = "OutNode and call does not share enclosing callable."
or
n.(ArgumentNode).argumentOf(call, _) and
msg = "ArgumentNode and call does not share enclosing callable."
) and
n.getEnclosingCallable() != call.getEnclosingCallable()
}
// This predicate helps the compiler forget that in some languages
// it is impossible for a result of `getPreUpdateNode` to be an
// instance of `PostUpdateNode`.
private Node getPre(PostUpdateNode n) {
result = n.getPreUpdateNode()
or
none()
}
query predicate postIsNotPre(PostUpdateNode n, string msg) {
getPre(n) = n and
msg = "PostUpdateNode should not equal its pre-update node."
}
query predicate postHasUniquePre(PostUpdateNode n, string msg) {
exists(int c |
c = count(n.getPreUpdateNode()) and
c != 1 and
msg = "PostUpdateNode should have one pre-update node but has " + c + "."
)
}
query predicate uniquePostUpdate(Node n, string msg) {
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
msg = "Node has multiple PostUpdateNodes."
}
query predicate postIsInSameCallable(PostUpdateNode n, string msg) {
n.getEnclosingCallable() != n.getPreUpdateNode().getEnclosingCallable() and
msg = "PostUpdateNode does not share callable with its pre-update node."
}
private predicate hasPost(Node n) { exists(PostUpdateNode post | post.getPreUpdateNode() = n) }
query predicate reverseRead(Node n, string msg) {
exists(Node n2 | readStep(n, _, n2) and hasPost(n2) and not hasPost(n)) and
msg = "Origin of readStep is missing a PostUpdateNode."
}
query predicate argHasPostUpdate(ArgumentNode n, string msg) {
not hasPost(n) and
not isImmutableOrUnobservable(n) and
msg = "ArgumentNode is missing PostUpdateNode."
}
// This predicate helps the compiler forget that in some languages
// it is impossible for a `PostUpdateNode` to be the target of
// `simpleLocalFlowStep`.
private predicate isPostUpdateNode(Node n) { n instanceof PostUpdateNode or none() }
query predicate postWithInFlow(Node n, string msg) {
isPostUpdateNode(n) and
simpleLocalFlowStep(_, n) and
msg = "PostUpdateNode should not be the target of local flow."
}
}

View File

@@ -117,7 +117,14 @@ private module Cached {
TNormalParameterNode(Parameter p) { not p instanceof BlockParameter } or
TSelfParameterNode(MethodBase m) or
TBlockParameterNode(MethodBase m) or
TExprPostUpdateNode(CfgNodes::ExprCfgNode n) { n.getNode() instanceof Argument }
TExprPostUpdateNode(CfgNodes::ExprCfgNode n) {
exists(AstNode node | node = n.getNode() |
node instanceof Argument and
not node instanceof BlockArgument
or
n = any(CfgNodes::ExprNodes::CallCfgNode call).getReceiver()
)
}
class TParameterNode = TNormalParameterNode or TBlockParameterNode or TSelfParameterNode;
@@ -137,7 +144,7 @@ private module Cached {
nodeTo.(ParameterNode).getParameter().(KeywordParameter).getDefaultValue() =
nodeFrom.asExpr().getExpr()
or
nodeFrom.(SelfParameterNode).getMethod() = nodeTo.asExpr().getExpr().getEnclosingMethod() and
nodeFrom.(SelfParameterNode).getMethod() = nodeTo.asExpr().getExpr().getEnclosingCallable() and
nodeTo.asExpr().getExpr() instanceof Self
or
nodeFrom.asExpr() = nodeTo.asExpr().(CfgNodes::ExprNodes::AssignExprCfgNode).getRhs()
@@ -441,6 +448,13 @@ predicate jumpStep(Node pred, Node succ) {
or
SsaImpl::captureFlowOut(pred.(SsaDefinitionNode).getDefinition(),
succ.(SsaDefinitionNode).getDefinition())
or
exists(Self s, Method m |
s = succ.asExpr().getExpr() and
pred.(SelfParameterNode).getMethod() = m and
m = s.getEnclosingMethod() and
m != s.getEnclosingCallable()
)
}
predicate storeStep(Node node1, Content c, Node node2) { none() }
@@ -532,7 +546,7 @@ class Unit extends TUnit {
*
* This predicate is only used for consistency checks.
*/
predicate isImmutableOrUnobservable(Node n) { none() }
predicate isImmutableOrUnobservable(Node n) { n instanceof BlockArgumentNode }
/**
* Holds if the node `n` is unreachable when the call context is `call`.

View File

@@ -11,6 +11,10 @@
"codeql/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll",
"ql/src/codeql_ruby/dataflow/internal/DataFlowImpl.qll"
],
"DataFlow Consistency": [
"codeql/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll",
"ql/src/codeql_ruby/dataflow/internal/DataFlowImplConsistency.qll"
],
"TaintTracking": [
"codeql/csharp/ql/src/semmle/code/csharp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
"ql/src/codeql_ruby/dataflow/internal/tainttracking1/TaintTrackingImpl.qll"