Skip to content

Commit

Permalink
Model generator
Browse files Browse the repository at this point in the history
  • Loading branch information
@hvitved
hvitved committed Dec 9, 2024
1 parent 28ccac4 commit 13b8249
Show file tree
Hide file tree
Showing 5 changed files with 208 additions and 22 deletions.
15 changes: 15 additions & 0 deletions shared/dataflow/codeql/dataflow/DataFlow.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -363,6 +363,11 @@ module Configs<LocationSig Location, InputSig<Location> Lang> {
*/
predicate isSink(Node sink);

/**
* Holds if `sink` is a relevant data flow sink.
*/
default predicate isSinkReverse(Node sink) { none() }

/**
* Holds if data flow through `node` is prohibited. This completely removes
* `node` from the data flow graph.
Expand Down Expand Up @@ -465,6 +470,16 @@ module Configs<LocationSig Location, InputSig<Location> Lang> {
*/
default predicate isSink(Node sink) { none() }

/**
* Holds if `sink` is a relevant data flow sink for any state.
*/
default predicate isSinkReverse(Node sink) { none() }

/**
* Holds if `sink` is a relevant data flow sink accepting `state`.
*/
default predicate isSinkReverse(Node sink, FlowState state) { none() }

/**
* Holds if data flow through `node` is prohibited. This completely removes
* `node` from the data flow graph.
Expand Down
4 changes: 4 additions & 0 deletions shared/dataflow/codeql/dataflow/TaintTracking.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,10 @@ module TaintFlowMake<
Config::isSink(sink, state.getState())
}

predicate isSinkReverse(DataFlowLang::Node sink, FlowState state) {
Config::isSinkReverse(sink, state.getState())
}

predicate isBarrier(DataFlowLang::Node node, FlowState state) {
Config::isBarrier(node, state.getState())
}
Expand Down
55 changes: 46 additions & 9 deletions shared/dataflow/codeql/dataflow/internal/ContentDataFlowImpl.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,11 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
*/
predicate isSink(Node sink);

/**
* Holds if `sink` is a relevant data flow sink.
*/
default predicate isSinkReverse(Node sink) { none() }

/**
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
*/
Expand Down Expand Up @@ -98,6 +103,15 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
)
}

predicate isSinkReverse(Node sink, FlowState state) {
ContentConfig::isSinkReverse(sink) and
(
state instanceof InitState or
state instanceof StoreState or
state instanceof ReadState
)
}

predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
storeStep(node1, state1, _, node2, state2) or
readStep(node1, state1, _, node2, state2) or
Expand All @@ -114,7 +128,35 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
predicate includeHiddenNodes() { any() }
}

private module Flow = GlobalWithState<FlowConfig>;
module Flow = GlobalWithState<FlowConfig>;

/**
* Holds if data stored inside `sourceAp` on `source` flows to `sinkAp` inside `sink`
* for this configuration. `preservesValue` indicates whether any of the additional
* flow steps defined by `isAdditionalFlowStep` are needed.
*
* For the source access path, `sourceAp`, the top of the stack represents the content
* that was last read from. That is, if `sourceAp` is `Field1.Field2` (with `Field1`
* being the top of the stack), then there is flow from `source.Field2.Field1`.
*
* For the sink access path, `sinkAp`, the top of the stack represents the content
* that was last stored into. That is, if `sinkAp` is `Field1.Field2` (with `Field1`
* being the top of the stack), then there is flow into `sink.Field1.Field2`.
*/
predicate flowPath(
Flow::PathNode source, AccessPath sourceAp, Flow::PathNode sink, AccessPath sinkAp,
boolean preservesValue
) {
Flow::flowPath(source, sink) and
nodeReaches(source, TAccessPathNil(), TAccessPathNil(), sink, sourceAp, sinkAp) and
(
sink.getState().(InitState).decode(preservesValue)
or
sink.getState().(ReadState).decode(_, preservesValue)
or
sink.getState().(StoreState).decode(_, preservesValue)
)
}

/**
* Holds if data stored inside `sourceAp` on `source` flows to `sinkAp` inside `sink`
Expand All @@ -133,16 +175,9 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
Node source, AccessPath sourceAp, Node sink, AccessPath sinkAp, boolean preservesValue
) {
exists(Flow::PathNode pathSource, Flow::PathNode pathSink |
Flow::flowPath(pathSource, pathSink) and
nodeReaches(pathSource, TAccessPathNil(), TAccessPathNil(), pathSink, sourceAp, sinkAp) and
flowPath(pathSource, sourceAp, pathSink, sinkAp, preservesValue) and
source = pathSource.getNode() and
sink = pathSink.getNode()
|
pathSink.getState().(InitState).decode(preservesValue)
or
pathSink.getState().(ReadState).decode(_, preservesValue)
or
pathSink.getState().(StoreState).decode(_, preservesValue)
)
}

Expand Down Expand Up @@ -359,6 +394,8 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
or
FlowConfig::isSink(node.getNode(), node.getState())
or
FlowConfig::isSinkReverse(node.getNode(), node.getState())
or
excludeStep(node, _)
or
Flow::PathGraph::subpaths(_, _, node, _)
Expand Down
115 changes: 109 additions & 6 deletions shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
*/
predicate isSink(Node sink);

/**
* Holds if `sink` is a relevant data flow sink accepting `state`.
*/
predicate isSinkReverse(Node sink, FlowState state);

/**
* Holds if `sink` is a relevant data flow sink for any state.
*/
predicate isSinkReverse(Node sink);

/**
* Holds if data flow through `node` is prohibited. This completely removes
* `node` from the data flow graph.
Expand Down Expand Up @@ -149,6 +159,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {

predicate isSink(Node sink, FlowState state) { Config::isSink(sink) and exists(state) }

predicate isSinkReverse(Node sink, FlowState state) {
Config::isSinkReverse(sink) and exists(state)
}

predicate isBarrier(Node node, FlowState state) { none() }

predicate isBarrierIn(Node node, FlowState state) { none() }
Expand Down Expand Up @@ -192,18 +206,32 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
else any()
}

pragma[nomagic]
private predicate isFilteredSinkReverse(Node sink) {
(
Config::isSinkReverse(sink, _) or
Config::isSinkReverse(sink)
) and
if Config::observeDiffInformedIncrementalMode()
then AlertFiltering::filterByLocation(sink.getLocation())
else any()
}

private predicate hasFilteredSource() { isFilteredSource(_) }

private predicate hasFilteredSink() { isFilteredSink(_) }

private predicate hasFilteredSinkReverse() { isFilteredSinkReverse(_) }

predicate isRelevantSource(Node source, FlowState state) {
// If there are filtered sinks, we need to pass through all sources to preserve all alerts
// with filtered sinks. Otherwise the only alerts of interest are those with filtered
// sources, so we can perform the source filtering right here.
Config::isSource(source, state) and
(
isFilteredSource(source) or
hasFilteredSink()
hasFilteredSink() or
hasFilteredSinkReverse()
)
}

Expand All @@ -218,6 +246,17 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
}

predicate isRelevantSinkReverse(Node sink, FlowState state) {
// If there are filtered sources, we need to pass through all sinks to preserve all alerts
// with filtered sources. Otherwise the only alerts of interest are those with filtered
// sinks, so we can perform the sink filtering right here.
Config::isSinkReverse(sink, state) and
(
isFilteredSinkReverse(sink) or
hasFilteredSource()
)
}

predicate isRelevantSink(Node sink) {
// If there are filtered sources, we need to pass through all sinks to preserve all alerts
// with filtered sources. Otherwise the only alerts of interest are those with filtered
Expand All @@ -229,12 +268,30 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
}

predicate isRelevantSinkReverse(Node sink) {
// If there are filtered sources, we need to pass through all sinks to preserve all alerts
// with filtered sources. Otherwise the only alerts of interest are those with filtered
// sinks, so we can perform the sink filtering right here.
Config::isSinkReverse(sink) and
(
isFilteredSinkReverse(sink) or
hasFilteredSource()
)
}

bindingset[source, sink]
pragma[inline_late]
predicate isRelevantSourceSinkPair(Node source, Node sink) {
isFilteredSource(source) or
isFilteredSink(sink)
}

bindingset[source, sink]
pragma[inline_late]
predicate isRelevantSourceSinkPairReverse(Node source, Node sink) {

Check warning

Code scanning / CodeQL

Dead code Warning

This code is never used, and it's not publicly exported.
isFilteredSource(source) or
isFilteredSinkReverse(sink)
}
}

private import SourceSinkFiltering
Expand All @@ -258,19 +315,28 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {

private predicate outBarrier(NodeEx node) {
exists(Node n |
[node.asNodeOrImplicitRead(), node.asNodeReverse(_)] = n and
node.asNodeOrImplicitRead() = n and
Config::isBarrierOut(n)
|
isRelevantSink(n, _)
or
isRelevantSink(n)
)
or
exists(Node n |
node.asNodeReverse(_) = n and
Config::isBarrierOut(n)
|
isRelevantSinkReverse(n, _)
or
isRelevantSinkReverse(n)
)
}

pragma[nomagic]
private predicate outBarrier(NodeEx node, FlowState state) {
exists(Node n |
[node.asNodeOrImplicitRead(), node.asNodeReverse(_)] = n and
node.asNodeOrImplicitRead() = n and
Config::isBarrierOut(n, state)
|
isRelevantSink(n, state)
Expand Down Expand Up @@ -321,6 +387,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
not stateBarrier(node, state)
}

pragma[nomagic]
private predicate sinkNodeWithStateReverse(NodeEx node, FlowState state) {
isRelevantSinkReverse(node.asNodeReverse(_), state) and
not fullBarrier(node) and
not stateBarrier(node, state)
}

/** Provides the relevant barriers for a step from `node1` to `node2`. */
bindingset[node1, node2]
private predicate stepFilter(NodeEx node1, NodeEx node2) {
Expand Down Expand Up @@ -707,6 +780,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
fwdFlow(node) and
fwdFlowState(state) and
sinkNodeWithState(node, state)
or
fwdFlow(pragma[only_bind_into](node)) and
fwdFlowState(state) and
isRelevantSinkReverse(node.asNodeReverse(_))
or
fwdFlow(node) and
fwdFlowState(state) and
sinkNodeWithState(node, state)
or
fwdFlow(node) and
fwdFlowState(state) and
sinkNodeWithStateReverse(node, state)
}

/**
Expand Down Expand Up @@ -1025,7 +1110,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {

private predicate sinkModel(NodeEx node, string model) {
sinkNode(node, _) and
exists(Node n | n = node.asNodeOrImplicitRead() |
exists(Node n | n = [node.asNodeOrImplicitRead(), node.asNodeReverse(_)] |
knownSinkModel(n, model)
or
not knownSinkModel(n, _) and model = ""
Expand Down Expand Up @@ -3021,6 +3106,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
(isRelevantSink(n) or isRelevantSink(n, _)) and
result.asNode() = n
)
or
exists(Node n |
node.asNodeReverse(_) = n and
(isRelevantSinkReverse(n) or isRelevantSinkReverse(n, _)) and
result = node
)
}

override PathNodeImpl getASuccessorImpl(string label) {
Expand Down Expand Up @@ -3520,6 +3611,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
/** Gets the underlying `Node`. */
final Node getNode() { super.getNodeEx().projectToNode() = result }

/** Gets the underlying `Node`, but only when it represents a reverse-flow node. */
final Node getNodeReverse() { super.getNodeEx().asNodeReverse(_) = result }

/** Gets the parameter node through which data is returned, if any. */
final ParameterNode asParameterReturnNode() {
result = super.getNodeEx().asNodeReverse(_)
Expand Down Expand Up @@ -4869,7 +4963,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate interestingCallableSink(DataFlowCallable c) {
exists(Node n | c = getNodeEnclosingCallable(n) |
isRelevantSink(n, _) or
isRelevantSink(n)
isRelevantSink(n) or
isRelevantSinkReverse(n, _) or
isRelevantSinkReverse(n)
)
or
exists(DataFlowCallable mid | interestingCallableSink(mid) and callableStep(c, mid))
Expand Down Expand Up @@ -4905,7 +5001,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
ce1 = TCallable(getNodeEnclosingCallable(n))
|
isRelevantSink(n, _) or
isRelevantSink(n)
isRelevantSink(n) or
isRelevantSinkReverse(n, _) or
isRelevantSinkReverse(n)
)
}

Expand Down Expand Up @@ -4973,6 +5071,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
relevantState(state) and
not fullBarrier(node) and
not stateBarrier(node, state)
or
isRelevantSinkReverse(node.asNodeReverse(_)) and
relevantState(state) and
not fullBarrier(node) and
not stateBarrier(node, state)
}

private newtype TSummaryCtx1 =
Expand Down
Loading

0 comments on commit 13b8249

Please sign in to comment.