mirror of
https://github.com/github/codeql.git
synced 2026-04-30 19:26:02 +02:00
JavaScript: Introduce flow labels.
This commit is contained in:
@@ -88,15 +88,35 @@ abstract class Configuration extends string {
|
||||
/**
|
||||
* Holds if `source` is a relevant data flow source for this configuration.
|
||||
*/
|
||||
abstract predicate isSource(DataFlow::Node source);
|
||||
predicate isSource(DataFlow::Node source) {
|
||||
none()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `source` is a source of flow labelled with `lbl` that is relevant
|
||||
* for this configuration.
|
||||
*/
|
||||
predicate isSource(DataFlow::Node source, FlowLabel lbl) {
|
||||
none()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `sink` is a relevant data flow sink for this configuration.
|
||||
*/
|
||||
abstract predicate isSink(DataFlow::Node sink);
|
||||
predicate isSink(DataFlow::Node sink) {
|
||||
none()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `source -> sink` should be considered as a flow edge
|
||||
* Holds if `sink` is a sink of flow labelled with `lbl` that is relevant
|
||||
* for this configuration.
|
||||
*/
|
||||
predicate isSink(DataFlow::Node sink, FlowLabel lbl) {
|
||||
none()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `src -> trg` should be considered as a flow edge
|
||||
* in addition to standard data flow edges.
|
||||
*/
|
||||
predicate isAdditionalFlowStep(DataFlow::Node src, DataFlow::Node trg) { none() }
|
||||
@@ -105,7 +125,7 @@ abstract class Configuration extends string {
|
||||
* INTERNAL: This predicate should not normally be used outside the data flow
|
||||
* library.
|
||||
*
|
||||
* Holds if `source -> sink` should be considered as a flow edge
|
||||
* Holds if `src -> trg` should be considered as a flow edge
|
||||
* in addition to standard data flow edges, with `valuePreserving`
|
||||
* indicating whether the step preserves values or just taintedness.
|
||||
*/
|
||||
@@ -113,6 +133,14 @@ abstract class Configuration extends string {
|
||||
isAdditionalFlowStep(src, trg) and valuePreserving = true
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `src -> trg` is a flow edge converting flow with label `inlbl` to
|
||||
* flow with label `outlbl`.
|
||||
*/
|
||||
predicate isAdditionalFlowStep(DataFlow::Node src, DataFlow::Node trg, FlowLabel inlbl, FlowLabel outlbl) {
|
||||
none()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the intermediate flow node `node` is prohibited.
|
||||
*/
|
||||
@@ -128,6 +156,11 @@ abstract class Configuration extends string {
|
||||
*/
|
||||
predicate isBarrier(DataFlow::Node src, DataFlow::Node trg) { none() }
|
||||
|
||||
/**
|
||||
* Holds if flow with label `lbl` cannot flow from `src` to `trg`.
|
||||
*/
|
||||
predicate isBarrier(DataFlow::Node src, DataFlow::Node trg, FlowLabel lbl) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow node `guard` can act as a barrier when appearing
|
||||
* in a condition.
|
||||
@@ -142,7 +175,7 @@ abstract class Configuration extends string {
|
||||
* Holds if data may flow from `source` to `sink` for this configuration.
|
||||
*/
|
||||
predicate hasFlow(DataFlow::Node source, DataFlow::Node sink) {
|
||||
isSource(_, this) and isSink(_, this) and
|
||||
isSource(_, this, _) and isSink(_, this, _) and
|
||||
exists (SourcePathNode flowsource, SinkPathNode flowsink |
|
||||
hasPathFlow(flowsource, flowsink) and
|
||||
source = flowsource.getNode() and
|
||||
@@ -176,6 +209,34 @@ abstract class Configuration extends string {
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A label describing the kind of information tracked by a flow configuration.
|
||||
*
|
||||
* There are two standard labels "data" and "taint", the former describing values
|
||||
* that directly originate from a flow source, the latter values that are derived
|
||||
* from a flow source via one or more transformations (such as string operations).
|
||||
*/
|
||||
abstract class FlowLabel extends string {
|
||||
bindingset[this] FlowLabel() { any() }
|
||||
}
|
||||
|
||||
module FlowLabel {
|
||||
private class StandardFlowLabel extends FlowLabel {
|
||||
StandardFlowLabel() { this = "data" or this = "taint" }
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the standard flow label for describing values that directly originate from a flow source.
|
||||
*/
|
||||
FlowLabel data() { result = "data" }
|
||||
|
||||
/**
|
||||
* Gets the standard flow label for describing values that are influenced ("tainted") by a flow
|
||||
* source, but not necessarily directly derived from it.
|
||||
*/
|
||||
FlowLabel taint() { result = "taint" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A node that can act as a barrier when appearing in a condition.
|
||||
*
|
||||
@@ -353,9 +414,10 @@ private predicate basicFlowStep(DataFlow::Node pred, DataFlow::Node succ, PathSu
|
||||
isRelevantForward(pred, cfg) and
|
||||
(
|
||||
// Local flow
|
||||
exists (boolean valuePreserving |
|
||||
localFlowStep(pred, succ, cfg, valuePreserving) and
|
||||
summary = PathSummary::level(valuePreserving)
|
||||
exists (FlowLabel predlbl, FlowLabel succlbl |
|
||||
localFlowStep(pred, succ, cfg, predlbl, succlbl) and
|
||||
not cfg.isBarrier(pred, succ, predlbl) and
|
||||
summary = MkPathSummary(false, false, predlbl, succlbl)
|
||||
)
|
||||
or
|
||||
// Flow through properties of objects
|
||||
@@ -393,15 +455,21 @@ private predicate exploratoryFlowStep(DataFlow::Node pred, DataFlow::Node succ,
|
||||
/**
|
||||
* Holds if `nd` is a source node for configuration `cfg`.
|
||||
*/
|
||||
private predicate isSource(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
||||
cfg.isSource(nd) or nd.(AdditionalSource).isSourceFor(cfg)
|
||||
private predicate isSource(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLabel lbl) {
|
||||
(cfg.isSource(nd) or nd.(AdditionalSource).isSourceFor(cfg)) and
|
||||
lbl = FlowLabel::data()
|
||||
or
|
||||
cfg.isSource(nd, lbl)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `nd` is a sink node for configuration `cfg`.
|
||||
*/
|
||||
private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
||||
cfg.isSink(nd) or nd.(AdditionalSink).isSinkFor(cfg)
|
||||
private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLabel lbl) {
|
||||
(cfg.isSink(nd) or nd.(AdditionalSink).isSinkFor(cfg)) and
|
||||
lbl = any(FlowLabel f)
|
||||
or
|
||||
cfg.isSink(nd, lbl)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -410,7 +478,7 @@ private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
||||
* No call/return matching is done, so this is a relatively coarse over-approximation.
|
||||
*/
|
||||
private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
||||
isSource(nd, cfg)
|
||||
isSource(nd, cfg, _)
|
||||
or
|
||||
exists (DataFlow::Node mid |
|
||||
isRelevantForward(mid, cfg) and exploratoryFlowStep(mid, nd, cfg)
|
||||
@@ -424,7 +492,7 @@ private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration c
|
||||
*/
|
||||
private predicate isRelevant(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
||||
isRelevantForward(nd, cfg) and
|
||||
isSink(nd, cfg)
|
||||
isSink(nd, cfg, _)
|
||||
or
|
||||
exists (DataFlow::Node mid |
|
||||
isRelevant(mid, cfg) and
|
||||
@@ -527,7 +595,7 @@ private predicate reachableFromStoreBase(string prop, DataFlow::Node rhs, DataFl
|
||||
exists (DataFlow::Node mid, PathSummary oldSummary, PathSummary newSummary |
|
||||
reachableFromStoreBase(prop, rhs, mid, cfg, oldSummary) and
|
||||
flowStep(mid, cfg, nd, newSummary) and
|
||||
newSummary.valuePreserving() = true and
|
||||
newSummary.getEndLabel() = FlowLabel::data() and
|
||||
summary = oldSummary.append(newSummary)
|
||||
)
|
||||
}
|
||||
@@ -586,9 +654,11 @@ private predicate flowsTo(PathNode flowsource, DataFlow::Node source,
|
||||
*/
|
||||
private predicate reachableFromSource(DataFlow::Node nd, DataFlow::Configuration cfg,
|
||||
PathSummary summary) {
|
||||
isSource(nd, cfg) and
|
||||
not cfg.isBarrier(nd) and
|
||||
summary = PathSummary::empty()
|
||||
exists (FlowLabel lbl |
|
||||
isSource(nd, cfg, lbl) and
|
||||
not cfg.isBarrier(nd) and
|
||||
summary = MkPathSummary(false, false, lbl, lbl)
|
||||
)
|
||||
or
|
||||
exists (DataFlow::Node pred, PathSummary oldSummary, PathSummary newSummary |
|
||||
reachableFromSource(pred, cfg, oldSummary) and
|
||||
@@ -605,7 +675,7 @@ private predicate reachableFromSource(DataFlow::Node nd, DataFlow::Configuration
|
||||
private predicate onPath(DataFlow::Node nd, DataFlow::Configuration cfg,
|
||||
PathSummary summary1, PathSummary summary2) {
|
||||
reachableFromSource(nd, cfg, summary1) and
|
||||
isSink(nd, cfg) and
|
||||
isSink(nd, cfg, summary1.getEndLabel()) and
|
||||
not cfg.isBarrier(nd) and
|
||||
summary2 = PathSummary::empty()
|
||||
or
|
||||
@@ -691,7 +761,7 @@ class PathNode extends TPathNode {
|
||||
*/
|
||||
class SourcePathNode extends PathNode {
|
||||
SourcePathNode() {
|
||||
isSource(nd, cfg)
|
||||
isSource(nd, cfg, _)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -700,7 +770,7 @@ class SourcePathNode extends PathNode {
|
||||
*/
|
||||
class SinkPathNode extends PathNode {
|
||||
SinkPathNode() {
|
||||
isSink(nd, cfg)
|
||||
isSink(nd, cfg, _)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -38,7 +38,9 @@ module TaintTracking {
|
||||
* The smaller this predicate is, the faster `hasFlow()` will converge.
|
||||
*/
|
||||
// overridden to provide taint-tracking specific qldoc
|
||||
abstract override predicate isSource(DataFlow::Node source);
|
||||
override predicate isSource(DataFlow::Node source) {
|
||||
super.isSource(source)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `sink` is a relevant taint sink.
|
||||
@@ -46,7 +48,9 @@ module TaintTracking {
|
||||
* The smaller this predicate is, the faster `hasFlow()` will converge.
|
||||
*/
|
||||
// overridden to provide taint-tracking specific qldoc
|
||||
abstract override predicate isSink(DataFlow::Node sink);
|
||||
override predicate isSink(DataFlow::Node sink) {
|
||||
super.isSink(sink)
|
||||
}
|
||||
|
||||
/** Holds if the intermediate node `node` is a taint sanitizer. */
|
||||
predicate isSanitizer(DataFlow::Node node) {
|
||||
@@ -58,6 +62,11 @@ module TaintTracking {
|
||||
none()
|
||||
}
|
||||
|
||||
/** Holds if the edge from `source` to `sink` is a taint sanitizer for data labelled with `lbl`. */
|
||||
predicate isSanitizer(DataFlow::Node source, DataFlow::Node sink, DataFlow::FlowLabel lbl) {
|
||||
none()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data flow node `guard` can act as a sanitizer when appearing
|
||||
* in a condition.
|
||||
@@ -82,6 +91,12 @@ module TaintTracking {
|
||||
isSanitizer(source, sink)
|
||||
}
|
||||
|
||||
final
|
||||
override predicate isBarrier(DataFlow::Node source, DataFlow::Node sink, DataFlow::FlowLabel lbl) {
|
||||
super.isBarrier(source, sink, lbl) or
|
||||
isSanitizer(source, sink, lbl)
|
||||
}
|
||||
|
||||
final
|
||||
override predicate isBarrierGuard(DataFlow::BarrierGuardNode guard) {
|
||||
super.isBarrierGuard(guard) or
|
||||
|
||||
@@ -5,6 +5,7 @@
|
||||
*/
|
||||
|
||||
import javascript
|
||||
import semmle.javascript.dataflow.Configuration
|
||||
|
||||
/**
|
||||
* Holds if flow should be tracked through properties of `obj`.
|
||||
@@ -66,12 +67,20 @@ predicate returnExpr(Function f, DataFlow::Node source, DataFlow::Node sink) {
|
||||
*/
|
||||
pragma[inline]
|
||||
predicate localFlowStep(DataFlow::Node pred, DataFlow::Node succ,
|
||||
DataFlow::Configuration configuration, boolean valuePreserving) {
|
||||
pred = succ.getAPredecessor() and valuePreserving = true
|
||||
or
|
||||
any(DataFlow::AdditionalFlowStep afs).step(pred, succ) and valuePreserving = true
|
||||
or
|
||||
configuration.isAdditionalFlowStep(pred, succ, valuePreserving)
|
||||
DataFlow::Configuration configuration,
|
||||
FlowLabel predlbl, FlowLabel succlbl) {
|
||||
pred = succ.getAPredecessor() and predlbl = succlbl
|
||||
or
|
||||
any(DataFlow::AdditionalFlowStep afs).step(pred, succ) and predlbl = succlbl
|
||||
or
|
||||
exists (boolean vp | configuration.isAdditionalFlowStep(pred, succ, vp) |
|
||||
if vp = false and (predlbl = FlowLabel::data() or predlbl = FlowLabel::taint()) then
|
||||
succlbl = FlowLabel::taint()
|
||||
else
|
||||
predlbl = succlbl
|
||||
)
|
||||
or
|
||||
configuration.isAdditionalFlowStep(pred, succ, predlbl, succlbl)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -240,17 +249,15 @@ class Boolean extends boolean {
|
||||
*/
|
||||
newtype TPathSummary =
|
||||
/** A summary of an inter-procedural data flow path. */
|
||||
MkPathSummary(Boolean hasReturn, Boolean hasCall, Boolean valuePreserving)
|
||||
MkPathSummary(Boolean hasReturn, Boolean hasCall, FlowLabel start, FlowLabel end)
|
||||
|
||||
/**
|
||||
* A summary of an inter-procedural data flow path.
|
||||
*
|
||||
* The summary keeps track of whether the path contains any call steps from an argument
|
||||
* of a function call to the corresponding parameter, and/or any return steps from the
|
||||
* `return` statement of a function to a call of that function.
|
||||
*
|
||||
* Additionally, it records and whether each step on the path preserves the value of its
|
||||
* input node (and not just its taintedness).
|
||||
* The summary includes a start flow label and an end flow label, and keeps track of
|
||||
* whether the path contains any call steps from an argument of a function call to the
|
||||
* corresponding parameter, and/or any return steps from the `return` statement of a
|
||||
* function to a call of that function.
|
||||
*
|
||||
* We only want to build properly matched call/return sequences, so if a path has both
|
||||
* call steps and return steps, all return steps must precede all call steps.
|
||||
@@ -258,10 +265,11 @@ newtype TPathSummary =
|
||||
class PathSummary extends TPathSummary {
|
||||
Boolean hasReturn;
|
||||
Boolean hasCall;
|
||||
Boolean valuePreserving;
|
||||
FlowLabel start;
|
||||
FlowLabel end;
|
||||
|
||||
PathSummary() {
|
||||
this = MkPathSummary(hasReturn, hasCall, valuePreserving)
|
||||
this = MkPathSummary(hasReturn, hasCall, start, end)
|
||||
}
|
||||
|
||||
/** Indicates whether the path represented by this summary contains any return steps. */
|
||||
@@ -274,12 +282,9 @@ class PathSummary extends TPathSummary {
|
||||
result = hasCall
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the path represented by this summary preserves the value of
|
||||
* its start node or only its taintedness.
|
||||
*/
|
||||
boolean valuePreserving() {
|
||||
result = valuePreserving
|
||||
/** Gets the flow label describing data at the end of this flow path. */
|
||||
FlowLabel getEndLabel() {
|
||||
result = end
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -289,11 +294,14 @@ class PathSummary extends TPathSummary {
|
||||
* a `call` step in order to maintain well-formedness.
|
||||
*/
|
||||
PathSummary append(PathSummary that) {
|
||||
result = MkPathSummary(this.hasReturn().booleanOr(that.hasReturn()),
|
||||
this.hasCall().booleanOr(that.hasCall()),
|
||||
this.valuePreserving().booleanAnd(that.valuePreserving())) and
|
||||
// avoid constructing invalid paths
|
||||
not (this.hasCall() = true and that.hasReturn() = true)
|
||||
exists (Boolean hasReturn2, Boolean hasCall2, FlowLabel end2 |
|
||||
that = MkPathSummary(hasReturn2, hasCall2, end, end2) |
|
||||
result = MkPathSummary(hasReturn.booleanOr(hasReturn2),
|
||||
hasCall.booleanOr(hasCall2),
|
||||
start, end2) and
|
||||
// avoid constructing invalid paths
|
||||
not (hasCall = true and hasReturn2 = true)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -321,13 +329,24 @@ module PathSummary {
|
||||
result = level(true)
|
||||
}
|
||||
|
||||
private PathSummary mkPathSummary(boolean hasCall, boolean hasReturn, Boolean valuePreserving) {
|
||||
exists (FlowLabel start, FlowLabel end |
|
||||
if valuePreserving = false then
|
||||
end = FlowLabel::taint()
|
||||
else
|
||||
start = end
|
||||
|
|
||||
result = MkPathSummary(hasCall, hasReturn, start, end)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a summary describing a path without any calls or returns.
|
||||
* `valuePreserving` indicates whether the path preserves the value of its
|
||||
* start node or only its taintedness.
|
||||
*/
|
||||
PathSummary level(Boolean valuePreserving) {
|
||||
result = MkPathSummary(false, false, valuePreserving)
|
||||
result = mkPathSummary(false, false, valuePreserving)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -336,7 +355,7 @@ module PathSummary {
|
||||
* start node or only its taintedness.
|
||||
*/
|
||||
PathSummary call(Boolean valuePreserving) {
|
||||
result = MkPathSummary(false, true, valuePreserving)
|
||||
result = mkPathSummary(false, true, valuePreserving)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -345,6 +364,6 @@ module PathSummary {
|
||||
* start node or only its taintedness.
|
||||
*/
|
||||
PathSummary return(Boolean valuePreserving) {
|
||||
result = MkPathSummary(true, false, valuePreserving)
|
||||
result = mkPathSummary(true, false, valuePreserving)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -2,4 +2,4 @@ import DataFlowConfig
|
||||
|
||||
from TestDataFlowConfiguration tttc, DataFlow::Node src, DataFlow::Node snk
|
||||
where tttc.hasFlow(src, snk)
|
||||
select src, snk
|
||||
select src, snk
|
||||
|
||||
Reference in New Issue
Block a user