C++: Add path-sensitivity to `StackVariableReachability` #6004

MathiasVP · 2021-06-03T16:06:52Z

This PR adds path-sensitivity to StackVariableReachability. There is a slight performance regression since we now do the whole forwards-backward path-finding algorithm, followed by a second stage that checks path feasibility. It seems to remove quite a lot of false positives on LGTM for the cpp/use-after-free query: https://lgtm.com/query/4215884668081020126/.

It does require some join-order gymnastics, but I think I fixed all the bad joins. But let's see what Jenkins says. 🤞

CPP-Differences: ~~https://jenkins.internal.semmle.com/job/Changes/job/CPP-Differences/2110/~~ <-- Bad join. https://jenkins.internal.semmle.com/job/Changes/job/CPP-Differences/2114/

geoffw0 · 2021-06-07T11:41:28Z

Most of the LGTM false positives we lose seem to be cases of realloc in a loop, and the changes look good to me. There are a couple I came across and couldn't see what was going on, namely the text_file results in scummvm/scummvm and Node_Main in MediaArea/MediaInfoLib. These probably deserve a second look.

There are no new results.

The CPP-Differences results show a lot of changes for a different query, cpp/uninitialized-local, which I believe are not wobble. A very quick look suggests that they are good fixes. This looks really good.

Is there an explanation of the code changes anywhere?

MathiasVP · 2021-06-07T11:49:26Z

Most of the LGTM false positives we lose seem to be cases of realloc in a loop, and the changes look good to me. There are a couple I came across and couldn't see what was going on, namely the text_file results in scummvm/scummvm and Node_Main in MediaArea/MediaInfoLib. These probably deserve a second look.

There are no new results.

The CPP-Differences results show a lot of changes for a different query, cpp/uninitialized-local, which I believe are not wobble. A very quick look suggests that they are good fixes. This looks really good.

Is there an explanation of the code changes anywhere?

Thanks for taking a look at the results! I'll go over the ones you mention. I did find a bug that caused some false negatives, and I have a fix for that locally that I'm testing now. That might be why we lose some results that you couldn't make sense of.

I will add explanatory comments once I know that I can get a handle on performance. The main problem is the recursive getACondition predicate that picks up basically all conditions in a O(n^2) fashion without much filtering, and this causes some slowdown. Once I have a solution to that I'll update the code with comments.

CPP-Differences only shows results for cpp/uninitialized-local as that's the only query that's in the extended security suite. I expect this PR will have a similar effect on all other queries that use StackVariableReachability.

…tyWithReassignment' by using the old StackVariableReachability predicates that don't care about paths.

…nalysis

…ively pull in 'semmle.code.cpp.Print' when including 'cpp'.

geoffw0 · 2021-06-15T14:23:42Z

I gather you're happy with results and performance now?

The results I've seen from this PR are great, but I've still little idea how to approach reviewing the QL changes. What kind of path sensitivity do we now support, and what are the limitations?

C++: Accept more test changes. These all arise because we now transitively pull in 'semmle.code.cpp.Print' when including 'cpp'.

Is that necessary? It doesn't seem like a desirable change.

MathiasVP · 2021-06-15T15:27:32Z

I gather you're happy with results and performance now?

I'm running a last CPP-Difference to make sure that I didn't mess up anything: https://jenkins.internal.semmle.com/job/Changes/job/CPP-Differences/2080/. It's been running for quite a while now, so maybe I did mess up something 🤔. It should still be fine to start reviewing it at this point, however. As the changes at some point in the past had good performance, I don't expect any performance fixes to involve a major rewrite.

[...] What kind of path sensitivity do we now support, [...]?

On main we do a single pass from a source to a sink. This PR adds a second pass that's run before we report a path from a source to a sink. This pass:

Collects a set of Conditions that hold for each node in the path.
Checks that none of the conditions at a given node in the path contract each other.

For instance, let's say we're analyzing this piece of code:

1. source();
2. if(b)
3.   foo();
4. if(!b)
5.   sink();

and the first pass reports a path 1 -> 2 -> 3 -> 4 -> 5. The second stage then follows this path and deduces that b is true on line 3 since b controls the execution of that statement. We then follow the path to edge 4 and deduce that b is still a valid path condition (since it was a valid path condition on the previous node). Since the true edge 4 -> 5 would imply that b is both true and false, this edge is discarded.

[...] and what are the limitations?

We're certainly limited by the inferences we can make from conditions. We can, for instance, infer that c1 && c2 == true implies that c1 == true or c2 == true, but we cannot infer that c1 == true and c2 == true implies c1 && c2 == true.
We're also limited by GVN's ability to compare guards.

C++: Accept more test changes. These all arise because we now transitively pull in 'semmle.code.cpp.Print' when including 'cpp'.
Is that necessary? It doesn't seem like a desirable change.

I totally agree. I haven't been able to figure out how to avoid this, though. If you have any ideas on how to fix this I'd very much like to hear them.

With that said, no code should really depend on the output of getAQlClass anyway. It already includes a bunch of weird classes that no one really cares about.

The results I've seen from this PR are great, but I've still little idea how to approach reviewing the QL changes.

I would happily jump on a Zoom call at some point so we can discuss the changes. Would that help?

criemen · 2021-06-18T10:03:09Z

Not a review, just curiosity from my side:
Assuming StackVariableReachability is sound, but not complete: Does it report a path from source to sink in this code?

int array[] = {0, 1, 0, 1};
char* data = nullptr;
for (int i = 0; i < 4; ++i) {
  int b = array[i];
  if (b) sink(data);
  if (!b) data = source();
}

If yes, how does it work?

I tried coming up with a meaningful example that could be plugged into the use-after-free query, but I'm not so sure that works great:

int array[] = {0, 1, 0, 1};
char* data = malloc(10 * sizeof(char));
for (int i = 0; i < 4; ++i) {
  int b = array[i];
  if (b) use(data);
  if (!b) free(data);
}

However, as there is special loop handling, a test showcasing some of that could be nice?

MathiasVP · 2021-06-18T10:29:28Z

Assuming StackVariableReachability is sound, but not complete: Does it report a path from source to sink in this code?
int array[] = {0, 1, 0, 1};
char* data = nullptr;
for (int i = 0; i < 4; ++i) {
  int b = array[i];
  if (b) sink(data);
  if (!b) data = source();
}
If yes, how does it work?

My idea was that this would work because we used GVN to compare conditions and so the b in if(!b) { ... } in the first iteration would have a different GVN than the b in if(b) { ... } (and so the conditions would have no relation between each other). I see now that I didn't actually think too hard about that case, because they will obviously have the same GVN. I'll think more about this and add a testcase that covers this. 🤔

(This goes back to an old discussion regarding GVN in loops I happened to come across on Slack.)

geoffw0 · 2021-06-21T14:28:19Z

C++: Accept more test changes. These all arise because we now transitively pull in 'semmle.code.cpp.Print' when including 'cpp'.
...
I haven't been able to figure out how to avoid this, though. If you have any ideas on how to fix this I'd very much like to hear them.

The code seems to be pulled in by private imports (thankfully), so it's 'invisible' outside of the files it's imported into except it seems by the getAQlClass mechanism. We might want to change the design of getAQlClass to respect the privacy of privately imported classes, but I've no idea how difficult this change would be or whether it's likely to cause more problems than it would solve.

With that said, no code should really depend on the output of getAQlClass anyway. It already includes a bunch of weird classes that no one really cares about.

Which leads me to the likely practical fix - remove getAQlClass from as many of those tests as possible, or only use it in a restricted way. I'm surprised there are so many uses of getAQlClass in the tests as a few years ago I made an effort to remove them (perhaps it's time for me to repeat that effort?)

geoffw0

Lots of questions and a few trivial corrections. Not a finished review.

cpp/ql/src/semmle/code/cpp/controlflow/StackVariableReachability.qll

geoffw0 · 2021-06-22T15:20:05Z

cpp/ql/src/semmle/code/cpp/controlflow/StackVariableReachability.qll

+/**
+ * Gets a `Condition` that controls `b`.
+ *
+ * Note: The trivial `True` condition always controls `b`.


To check my understanding, this is a Condition that must hold to enter b?

Correct. I've spelled this out in the QLDoc in 656ff4a.

cpp/ql/src/semmle/code/cpp/controlflow/StackVariableReachability.qll

…ty.qll Co-authored-by: Geoffrey White <40627776+geoffw0@users.noreply.github.com>

…loop variant condition refutes itself across loop iterations.

dbartol · 2021-06-23T18:17:29Z

How does the path sensitivity scale with a large number of paths, or with particularly long paths?

MathiasVP · 2021-06-23T21:08:37Z

How does the path sensitivity scale with a large number of paths, or with particularly long paths?

I'm guessing getACondition is O(number of paths * max length of paths). Hopefully, there shouldn't be that many paths since the set of blocks considered have been pruned down to only the relevant ones (i.e., the ones StackVariableReachability currently finds on main).

…ty.qll Co-authored-by: Geoffrey White <40627776+geoffw0@users.noreply.github.com>

github-actions · 2021-06-24T07:28:48Z

⚠️ The head of this PR and the base branch were compared for differences in the framework coverage reports. A recent commit removed the previously reported differences.

…ally needed.

MathiasVP · 2021-06-24T08:32:28Z

⚠️ The head of this PR and the base branch were compared for differences in the framework coverage reports. A recent commit removed the previously reported differences.

This is safe to ignore. See the conversation here: #6149 (comment)

geoffw0 · 2021-07-12T12:41:49Z

There's a lot of code in this PR and some areas have received more attention than others - but I'm starting to feel overall happy with it and looking forward to getting the benefits. The test changes due to semmle.code.cpp.print are annoying, but I think we agree the right approach is to accept them, but try to remove some uses of getAQlClass from tests in future.

I'd like to check:

that @MathiasVP is satisfied that he's sufficiently fixed the performance issues he found? ✔️
that @criemen ✔️ and @dbartol have no outstanding / further concerns?
~~I'm also going to try and do a new run of the query on LGTM with all the changes.~~

…nalysis

MathiasVP · 2021-07-12T12:52:24Z

Thanks for moving this forward, @geoffw0.

that @MathiasVP is satisfied that he's sufficiently fixed the performance issues he found?

I think the performance problems found in https://jenkins.internal.semmle.com/job/Changes/job/CPP-Differences/2110/ has been fixed by 43bbd4f. But I see that my most recent CPP-Differences to verify this (from before I went on vacation) failed. I've started a fresh one to remove any doubt: https://jenkins.internal.semmle.com/job/Changes/job/CPP-Differences/2146/.

criemen

Only two minor notes from my side that stood out when scrolling over the PR. I've not reviewed the code, it is more than I can grok 😺
My concern seems to have been addressed 👍

criemen · 2021-07-12T13:57:10Z

cpp/ql/src/semmle/code/cpp/controlflow/StackVariableReachability.qll

+
+  private predicate reaches0(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
+    /*
+     * Implementation detail: the predicates in this class are a generalization of


This comment talks about a class - should it be somewhere else?

It's present in the original file here: https://github.com/github/codeql/blob/main/cpp/ql/src/semmle/code/cpp/controlflow/StackVariableReachability.qll#L65. It's really a reminder to whoever is changing the implementation of the predicates. So I think it's in the right place.

cpp/ql/src/semmle/code/cpp/controlflow/StackVariableReachability.qll

criemen · 2021-07-12T14:33:01Z

One test failure

--- expected
+++ actual
@@ -7,4 +7,6 @@
 | test.cpp:170:6:170:9 | data | Memory pointed to by 'data' may have been previously freed $@ | test.cpp:165:2:165:5 | call to free | here |
 | test.cpp:193:6:193:9 | data | Memory pointed to by 'data' may have been previously freed $@ | test.cpp:191:3:191:6 | call to free | here |
 | test.cpp:201:6:201:6 | x | Memory pointed to by 'x' may have been previously freed $@ | test.cpp:200:2:200:9 | delete | here |
+| test.cpp:222:9:222:12 | data | Memory pointed to by 'data' may have been previously freed $@ | test.cpp:223:5:223:8 | call to free | here |
+| test.cpp:223:10:223:13 | data | Memory pointed to by 'data' may have been previously freed $@ | test.cpp:223:5:223:8 | call to free | here |
 | test.cpp:242:14:242:17 | data | Memory pointed to by 'data' may have been previously freed $@ | test.cpp:243:11:243:14 | call to free | here |
Error: [2814/5249 comp 11.1s eval 999ms] FAILED(RESULT) /home/runner/work/semmle-code/semmle-code/ql/cpp/ql/test/query-tests/Security/CWE/CWE-416/semmle/tests/UseAfterFree.qlref

MathiasVP · 2021-07-12T15:15:13Z

One test failure

Ouch! Thanks for catching this. Fixed in 768b3c8.

MathiasVP · 2021-07-13T09:05:25Z

I've started a fresh one to remove any doubt: https://jenkins.internal.semmle.com/job/Changes/job/CPP-Differences/2146/.

CPP-Differences failed again, but only on abseil/abseil-cpp this time:

[2021-07-12T18:22:15.443Z] ssh: connect to host github.com port 22: Connection timed out
[2021-07-12T18:22:15.443Z] fatal: Could not read from remote repository.

I'll spin up another one and hope for the best 🤞.

Edit: https://jenkins.internal.semmle.com/job/Changes/job/CPP-Differences/2149/

geoffw0 · 2021-07-13T12:55:40Z

I'm also going to try and do a new run of the query on LGTM with all the changes.

Unfortunately I can't realistically do the DefinitionsAndUses.qll change on LGTM, so I got nowhere with this. I've done a little bit more local testing instead. It seems much slower to evaluate StackVariableReachability queries (e.g. on kamailio_kamailio) even with my best efforts to warm the cache up beforehand (but maybe I'm not doing it properly?). Definitely looking forward to seeing the CPP-Differences performance numbers.

MathiasVP · 2021-07-14T06:38:58Z

Unfortunately I can't realistically do the DefinitionsAndUses.qll change on LGTM, so I got nowhere with this. I've done a little bit more local testing instead.

Thanks for trying out the LGTM changes. I can see that it's problematic to test it there.

It seems much slower to evaluate StackVariableReachability queries (e.g. on kamailio_kamailio) even with my best efforts to warm the cache up beforehand (but maybe I'm not doing it properly?). Definitely looking forward to seeing the CPP-Differences performance numbers.

I do notice the performance impact as well when I test things locally. It doesn't seem to be a big deal on CPP-Differences, though:

I think we can conclude that performance is fine (at least on the projects we include in CPP-Differences - who knows what the next dist upgrade will show).

geoffw0 · 2021-07-14T08:04:41Z

Yeah, most likely it's just that we aren't warming up the cache properly despite our efforts. It's probably fine. But we should keep an eye after this is merged.

geoffw0 · 2021-07-14T15:54:19Z

I want to get this merged. I'm still a bit nervous about the volume of code, for both review quality (I've done my best) and maintaining it (we've discussed possibly moving the Condition stuff into a distinct file at some point, which should help).

I plan to merge this tomorrow morning if there's no further discussion.

geoffw0

👍

…stack-variable-reachability-analysis" This reverts commit e3e7b00, reversing changes made to 8ccdd4f.

…riablereachability C++: Revert #6004

C++: Add some testcases that require path sensitivity.

d450aa2

MathiasVP added C++ WIP This is a work-in-progress, do not merge yet! labels Jun 3, 2021

MathiasVP force-pushed the path-sensitive-stack-variable-reachability-analysis branch from 07cbec3 to 4510083 Compare June 4, 2021 12:06

MathiasVP force-pushed the path-sensitive-stack-variable-reachability-analysis branch 2 times, most recently from b984d8f to 866e5b2 Compare June 14, 2021 07:00

MathiasVP added 5 commits June 14, 2021 21:59

C++: Add path sensitivity to StackVariableReachability.

c32f720

C++: Fix non-monotonic recursion problems in 'StackVariableReachabili…

7992678

…tyWithReassignment' by using the old StackVariableReachability predicates that don't care about paths.

C++: Accept test changes.

714ad10

Merge branch 'main' into path-sensitive-stack-variable-reachability-a…

cc6ae7f

…nalysis

C++: Accept more test changes. These all arise because we now transit…

14a04ee

…ively pull in 'semmle.code.cpp.Print' when including 'cpp'.

MathiasVP force-pushed the path-sensitive-stack-variable-reachability-analysis branch from 866e5b2 to 14a04ee Compare June 14, 2021 20:03

MathiasVP marked this pull request as ready for review June 14, 2021 20:24

MathiasVP requested a review from a team as a code owner June 14, 2021 20:24

MathiasVP removed the WIP This is a work-in-progress, do not merge yet! label Jun 14, 2021

C++: Add change-note.

b2e9fe7

github-actions bot added the documentation label Jun 15, 2021

MathiasVP mentioned this pull request Jun 16, 2021

C++: Add another barrier to cpp/use-after-free #5984

Closed

geoffw0 reviewed Jun 22, 2021

View reviewed changes

MathiasVP and others added 3 commits June 23, 2021 11:54

Update cpp/ql/src/semmle/code/cpp/controlflow/StackVariableReachabili…

d308dd2

…ty.qll Co-authored-by: Geoffrey White <40627776+geoffw0@users.noreply.github.com>

C++: Prevent false negatives caused by incorrectly concluding that a …

a8c57ec

…loop variant condition refutes itself across loop iterations.

C++: Fix join order with 'pragma[noopt]'.

43bbd4f

C++: Add testcase demonstrating the fix from a8c57ec.

2938ad5

Update cpp/ql/src/semmle/code/cpp/controlflow/StackVariableReachabili…

d70ea5f

…ty.qll Co-authored-by: Geoffrey White <40627776+geoffw0@users.noreply.github.com>

MathiasVP added 2 commits June 24, 2021 09:57

C++: Add more QLDoc.

656ff4a

C++: Get rid of the trivial 'True' condition. Turns out it's not actu…

c8c7739

…ally needed.

C++: Fix join order in 'bbSuccessorEntryReachesLoopInvariant'.

fd47738

Merge branch 'main' into path-sensitive-stack-variable-reachability-a…

be06230

…nalysis

criemen reviewed Jul 12, 2021

View reviewed changes

C++: Fix a bug that slipped into fd47738.

768b3c8

geoffw0 approved these changes Jul 15, 2021

View reviewed changes

geoffw0 merged commit e3e7b00 into github:main Jul 15, 2021

MathiasVP added a commit to MathiasVP/ql that referenced this pull request Jul 20, 2021

Revert "Merge pull request github#6004 from MathiasVP/path-sensitive-…

a006a7f

…stack-variable-reachability-analysis" This reverts commit e3e7b00, reversing changes made to 8ccdd4f.

MathiasVP mentioned this pull request Jul 20, 2021

C++: Revert #6004 #6340

Merged

p0 added a commit that referenced this pull request Jul 21, 2021

Merge pull request #6340 from MathiasVP/revert-path-sensitive-stackva…

2d9600d

…riablereachability C++: Revert #6004

C++: Add path-sensitivity to StackVariableReachability #6004

C++: Add path-sensitivity to StackVariableReachability #6004

Uh oh!

Conversation

MathiasVP commented Jun 3, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

geoffw0 commented Jun 7, 2021

Uh oh!

MathiasVP commented Jun 7, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

geoffw0 commented Jun 15, 2021

Uh oh!

MathiasVP commented Jun 15, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

criemen commented Jun 18, 2021

Uh oh!

MathiasVP commented Jun 18, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

geoffw0 commented Jun 21, 2021

Uh oh!

geoffw0 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

geoffw0 Jun 22, 2021

Choose a reason for hiding this comment

Uh oh!

MathiasVP Jun 24, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

dbartol commented Jun 23, 2021

Uh oh!

MathiasVP commented Jun 23, 2021

Uh oh!

github-actions bot commented Jun 24, 2021

Uh oh!

MathiasVP commented Jun 24, 2021

Uh oh!

geoffw0 commented Jul 12, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MathiasVP commented Jul 12, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

criemen left a comment

Choose a reason for hiding this comment

Uh oh!

criemen Jul 12, 2021

Choose a reason for hiding this comment

Uh oh!

MathiasVP Jul 12, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

criemen commented Jul 12, 2021

Uh oh!

MathiasVP commented Jul 12, 2021

Uh oh!

MathiasVP commented Jul 13, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

geoffw0 commented Jul 13, 2021

Uh oh!

MathiasVP commented Jul 14, 2021

Uh oh!

geoffw0 commented Jul 14, 2021

Uh oh!

geoffw0 commented Jul 14, 2021

Uh oh!

geoffw0 left a comment

C++: Add path-sensitivity to `StackVariableReachability` #6004

C++: Add path-sensitivity to `StackVariableReachability` #6004

MathiasVP commented Jun 3, 2021 •

edited

Loading

MathiasVP commented Jun 7, 2021 •

edited

Loading

MathiasVP commented Jun 15, 2021 •

edited

Loading

MathiasVP commented Jun 18, 2021 •

edited

Loading

MathiasVP Jun 24, 2021 •

edited

Loading

geoffw0 commented Jul 12, 2021 •

edited

Loading

MathiasVP commented Jul 12, 2021 •

edited

Loading

MathiasVP commented Jul 13, 2021 •

edited

Loading