Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Data flow: Prevent quadratic blowup in Stage6Param::localStep #17739

Merged
merged 2 commits into from
Oct 31, 2024
Merged

Data flow: Prevent quadratic blowup in Stage6Param::localStep #17739

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2e7b71c
Data flow: Prevent quadratic blowup in `Stage6Param::localStep`
hvitved Oct 11, 2024
7a2105b
Go: Update expected test output
hvitved Oct 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion go/ql/test/query-tests/Security/CWE-918/RequestForgery.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,6 @@ edges
| tst.go:36:2:36:2 | implicit dereference | tst.go:36:2:36:2 | u | provenance | |
| tst.go:36:2:36:2 | implicit dereference | tst.go:37:11:37:11 | u | provenance | |
| tst.go:36:2:36:2 | u | tst.go:36:2:36:2 | implicit dereference | provenance | |
| tst.go:36:2:36:2 | u | tst.go:36:2:36:2 | u | provenance | |
| tst.go:36:2:36:2 | u | tst.go:37:11:37:11 | u | provenance | |
| tst.go:36:2:36:2 | u [pointer] | tst.go:36:2:36:2 | implicit dereference | provenance | |
| tst.go:36:11:36:17 | tainted | tst.go:36:2:36:2 | u | provenance | Config |
Expand Down
111 changes: 58 additions & 53 deletions shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2596,31 +2596,27 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
callEdgeReturn(call, c, _, _, _, _, _)
}

/** Provides the input to `LocalFlowBigStep`. */
signature module LocalFlowBigStepInputSig {
bindingset[node1, state1]
bindingset[node2, state2]
predicate localStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
);
}
/** Holds if `node1` can step to `node2` in one or more local steps. */
bindingset[node1, state1]
bindingset[node2, state2]
signature predicate localStepSig(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
);

/**
* Provides a big-step relation for local flow steps.
*
* The big-step releation is based on the `localStep` relation from the
* input module, restricted to nodes that are forwards and backwards
* reachable in this stage.
* The big-step releation is based on the `localStepInput` relation,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
* The big-step releation is based on the `localStepInput` relation,
* The big-step relation is based on the `localStepInput` relation,

* restricted to nodes that are forwards and backwards reachable in
* this stage.
*/
additional module LocalFlowBigStep<LocalFlowBigStepInputSig Input> {
final private class NodeExFinal = NodeEx;

additional module LocalFlowBigStep<localStepSig/8 localStepInput> {
/**
* A node where some checking is required, and hence the big-step relation
* is not allowed to step over.
*/
private class FlowCheckNode extends NodeExFinal {
private class FlowCheckNode extends NodeEx {
FlowCheckNode() {
revFlow(this, _, _) and
(
Expand All @@ -2640,7 +2636,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(ApNil nil |
revFlow(node1, state1, pragma[only_bind_into](nil)) and
revFlow(node2, state2, pragma[only_bind_into](nil)) and
Input::localStep(node1, state1, node2, state2, false, t, lcc, label) and
localStepInput(node1, state1, node2, state2, false, t, lcc, label) and
state1 != state2
)
}
Expand Down Expand Up @@ -2734,7 +2730,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
not inBarrier(node2, state) and
not outBarrier(node1, state) and
exists(NodeEx mid, boolean preservesValue2, DataFlowType t2, string label2, Ap ap |
Input::localStep(mid, state, node2, state, preservesValue2, t2, cc, label2) and
localStepInput(mid, state, node2, state, preservesValue2, t2, cc, label2) and
revFlow(node2, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and
not outBarrier(mid, state) and
(preservesValue = true or ap instanceof ApNil)
Expand Down Expand Up @@ -2769,6 +2765,33 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(Ap ap |
localFlowStepPlus(node1, state1, node2, preservesValue, t, callContext, label) and
localFlowExit(node2, state1, ap) and
state1 = state2 and
node1 != node2
geoffw0 marked this conversation as resolved.
Show resolved Hide resolved
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While the addition here might well preserve semantics relative to main, then I don't think it matches what we want and the semantics prior to the introduction of the big-step recomputation. It's an obscure corner-case, but there might be a sequence of steps around a loop that returns to the origin including a taint step that affects the tracked type. In the first application of big-step TC then such a loop is preserved as a step, but a second application removes it, which seems wrong. So I think we should drop this constraint here.

Suggested change
node1 != node2

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't the node1 != node2 constraint then also be removed from localFlowStepPlus? Even if a node steps to itself as a taint step, the old type should be compatible with the new type, so I wouldn't expect us to gain much from updating the type.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Quite possibly. It's certainly corner-case, though.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#17877 shows the effect of allowing reflexive big steps; I'm not convinced that we want to add it, DCA on this PR also showed no alert changes (the ones for C# are wobble).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, let's go with the PR as-is, then.

|
preservesValue = true or ap instanceof ApNil
)
or
additionalLocalStateStep(node1, state1, node2, state2, t, callContext, label) and
preservesValue = false
}

/**
* Holds if `node1` can step to `node2` in one or more local steps and this
* path can occur as a maximal subsequence of local steps in a dataflow path.
*
* This predicate should be used when `localStepInput` is already a big-step
* relation, which will do the same as `localFlowBigStep`, but avoids potential
* worst-case quadratic complexity.
*/
pragma[nomagic]
predicate localFlowBigStepTc(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext callContext, string label
) {
exists(Ap ap |
localFlowEntry(node1, pragma[only_bind_into](state1), pragma[only_bind_into](ap)) and
localStepInput(node1, state1, node2, state2, preservesValue, t, callContext, label) and
localFlowExit(node2, pragma[only_bind_into](state2), pragma[only_bind_into](ap)) and
geoffw0 marked this conversation as resolved.
Show resolved Hide resolved
state1 = state2
|
preservesValue = true or ap instanceof ApNil
Expand Down Expand Up @@ -3790,27 +3813,25 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
import CallContextSensitivity<CallContextSensitivityInput>
import NoLocalCallContext

private module BigStepInput implements PrevStage::LocalFlowBigStepInputSig {
bindingset[node1, state1]
bindingset[node2, state2]
predicate localStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
) {
localStepNodeCand1(node1, node2, preservesValue, t, lcc, label) and
state1 = state2
or
localStateStepNodeCand1(node1, state1, node2, state2, t, lcc, label) and
preservesValue = false
}
bindingset[node1, state1]
bindingset[node2, state2]
private predicate localStepInput(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
) {
localStepNodeCand1(node1, node2, preservesValue, t, lcc, label) and
state1 = state2
or
localStateStepNodeCand1(node1, state1, node2, state2, t, lcc, label) and
preservesValue = false
}

additional predicate localFlowBigStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
) {
PrevStage::LocalFlowBigStep<BigStepInput>::localFlowBigStep(node1, state1, node2, state2,
preservesValue, t, lcc, label)
PrevStage::LocalFlowBigStep<localStepInput/8>::localFlowBigStep(node1, state1, node2,
state2, preservesValue, t, lcc, label)
}

bindingset[node1, state1]
Expand Down Expand Up @@ -4205,14 +4226,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
import CallContextSensitivity<CallContextSensitivityInput>
import LocalCallContext

predicate localStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
Typ t, LocalCc lcc, string label
) {
Stage3Param::localFlowBigStep(node1, state1, node2, state2, preservesValue, t, lcc, label) and
PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
PrevStage::revFlow(node2, pragma[only_bind_into](state2), _)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the revFlow check that was here lost, or do we preserve it somewhere?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not lost, since it's part of localFlowBigStepTc.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll take your word for it!

}
predicate localStep =
PrevStage::LocalFlowBigStep<Stage3Param::localFlowBigStep/8>::localFlowBigStepTc/8;

bindingset[node, state, t0, ap]
predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
Expand Down Expand Up @@ -4410,18 +4425,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
import CallContextSensitivity<CallContextSensitivityInput>
import LocalCallContext

private module BigStepInput implements PrevStage::LocalFlowBigStepInputSig {
predicate localStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
) {
Stage3Param::localFlowBigStep(node1, state1, node2, state2, preservesValue, t, lcc, label) and
PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
PrevStage::revFlow(node2, pragma[only_bind_into](state2), _)
}
}

predicate localStep = PrevStage::LocalFlowBigStep<BigStepInput>::localFlowBigStep/8;
predicate localStep =
PrevStage::LocalFlowBigStep<Stage5Param::localStep/8>::localFlowBigStepTc/8;

bindingset[node, state, t0, ap]
predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
Expand Down
Loading