A sound static analyzer in theory can check the safety of that by examining all code paths and complain whenever any exist where it is possible to go out of bounds. It is called sound because the absence of a complaint means it has proven the absence of the issues it is meant to catch.
If it has a limitation that prevents it from finding a proof, it will complain about the lines that could not be proven safe.
> Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones.
You're only commenting on your personal belief of how your ideal static analyzer would magically work to meet your expectations.
This doesn't correspond to how static analyzers work in reality.
Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility.
C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible?
> You're only commenting on your personal belief of how your ideal static analyzer would magically work to meet your expectations.
This is how sound static analyzers are advertised.
> This doesn't correspond to how static analyzers work in reality.
Of course it does not, since a normal static analyzer is not sound. However, a sound static analyzer is sound.
> Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility.
I already did (and explained that while I have yet to use it, NIST did a positive review). Until you learn better reading comprehension, you will never see it. Here is a hint. Look 6 comments up.
> C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible?
You, like myself a few months ago, had never heard of it. However, when was the last time you seriously looked for something like this? I have been making a major push to resolve all static analysis reports from Coverity, Clang and others in OpenZFS. I found it when looking into additional static analyzers. If it were not for that, I would still be entirely unaware.
That being said, you have a clear reading comprehension issue, since I already provided links showing that NASA has deployed software implementing that theory and NIST did a positive review of software implementing it. It is absurd to read that and think “this is not feasible”.
> Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility.
> C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible?
Depends on how you define "feasible".
Abstract interpretation and symbolic execution are crazy complex¹. Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types.
Trying to make static guaranties about imperative code is indeed a dead end by now.
The problem is that proving any properties of imperative code needs much more effort (and therefore code) than what is expressed by the code that needs proves, so it's actually likely that you haven than bugs in the code that proves things. So this approach is not really "feasible" in the end.
---
¹ Just have a look at the documentation around the KeY tool used to prove things about Java programs.
That's the most complex stuff I've ever seen! Depended type systems are "trivially simple" in contrast, no joke. But this is just about a "simple language" like Java… The complexity of C is much much higher.
> Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types.
This is not entirely true. Patrick Cousot‘s group, which invented the theory of abstract interpretation, kept working on it and produced Astree.
I had previously been under the impression that Astree was from the same people that made Compcert C, but upon double checking for this reply, I realized that was wrong. The two groups are both in France though. It was an easy mistake to make considering that Absint sells licenses for both.
> Trying to make static guaranties about imperative code is indeed a dead end by now.
The astree static analyzer is available from Absint. One of the inventors of both it and the theory on which it is based is also still alive:
Presumably, NASA heard about Astree from the ESA and decided to make its own tool, possibly due to NIH syndrome. I am not sure if NASA counts as academia.
This is far from a dead end, even if most researchers cannot be bothered to do things in that area. You will probably find a number of the ones that can be bothered to do things in that area at farma-c:
It's justified for aerospace, because failures are quite expensive there, but for usual business it will be much easier to implement automatic bound checking, like at 1% complexity of the C compiler.
I wonder what operating systems the aerospace industry uses, since failures in the operating system could be equally expensive, yet operating system developers generally do not have access to these tools.
Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking.
> Type checking is actually a special case of abstract interpretation.
I'm not sure about that.
Maybe in regard to type level functions? But else? I'm skeptical.
Could you explain what you exactly mean? Preferably with some examples as I'm having a hard time to imagine something in that direction.
> For all we know, it may even be that dependent types can already express many complex uses of it;
That for sure! Otherwise, corresponding type systems wouldn't be considered being an alternative.
Depended types can express anything computable. (Which also makes them undecidable in general).
In theory, you can prove any property of a program using depended types. That's why they're the preferred method by now. But you can't bold on such thing after the fact usually. Your language needs to be pure to benefit form the proving powers of depended types. So no hope for C and such like.
He appears to be right in saying "Type checking is actually a special case of abstract interpretation". The paper that presented Abstract Interpretation to the world concludes:
"It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..."
That said, abstract interpretation promises that the absence of reports proves the absence of the errors that the sound static analyzer implementing it is designed to catch. Provided that you do not abuse casts/unions, the absence of warnings/errors from a compiler's type checking on a strongly typed language should prove an absence of type errors, which does sound like what abstract interpretation promises.
Lastly, I need make time to actually read that paper. I have only read a very small part of it.
You could model C in a dependently-typed language by embedding the C abstract machine and C program expressions in it. Then you could use the Poincaré principle applied to C-program fragments to perform any "abstract interpretation" of them and derive any property you might care about. So it looks like the Poincaré's principle (as it was named by Barendegt) is the actual "missing link" that would enable you to generalize from purely syntax-based analysis (as in the traditional definition of type systems/type checks) to "interpretation" of a more general sort.
> Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking.
See the paper that presented abstract interpretation to the world:
"It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..."
With "cross translation units" (CTU) analysis a static analyzer could derive a constraint on `some_function` return value and check this against the array size to detect a possible bug.
The Clang static analyzer [1], used through CodeChecker (CC) [2], do support CTU (enabled with `--ctu`). I'm very happy with the result on the code I'm working on.
Of course this is not magic, and it's important to understand the limitations. The CTU analysis is well suited for an application: there is a `main` function, and all the paths from there can (in theory) be analyzed through the code base files. But if the code to analyze is a library, then the CTU analysis will be done from one or more unit test applications and the paths constraints analysis will only be as good as the unit tests. To avoid this one can analyze without CTU, but then the above code will always trigger a report as the static analyzer has no information on `some_function` return value and must assume the worst.
The other limitation is that there's only a limited complexity budget the analyzer can handle, so it cannot track all constraints on all paths. Depending on how the approximation is done it can lead to missed detection or false alarms.
IKOS (last time I checked) does not support CTU, it's doing "a file at a time" analysis. As far as open source tools go the Clang static analyzer is the only one I know with a working support for CTU (best used through CC). I there are other ones I missed I'd be happy to learn about them and try them out.
Clang SA + CC is a really nice combo. It's not sound (the limited complexity budget above), so can miss issues. Still, with CTU and the use of Z3 to cross check alarms (very nice when using bitfield) it is a nice user experience with very few false alarms, which matters to make the tool more acceptable (people tend to ignore tools with too many false alarms after a while IME). Still some rough edges for people doing embedded cross compiled development but manageable.
> The Clang static analyzer [1], used through CodeChecker (CC) [2], do support CTU (enabled with `--ctu`). I'm very happy with the result on the code I'm working on.
I have done some preliminary testing with this on the OpenZFS codebase and I am less than happy with the result since I receive many reports of subtle variations of the same thing on top of Clang already reporting a decent number of false positives. That turned around 80 mostly false positive reports from scan-build into 300 to 400 mostly false positive reports (I forget which offhand). This is in part because I started with around 240 reports from scan-build and fixed many of the actually fixable reports, which has gotten it down to around ~80 in my local branch that has some experimental header annotations for improving Clang’s static analyzer’s analysis that I have yet to upstream.
Interestingly, the additional reports from CSA CTU analysis duplicating scan-build reports far outweigh the additional reports from CSA CTU analysis reporting new things. I have not yet tried using the differential reports, but I suspect it will make this more useful for evaluating patches.
Also, codechecker uses clang tidy by default, which has problematic bugprone-assignment-in-if-condition rule. While there are ways to miswrite that pattern, it is better in my opinion to write checks for those. This pattern makes code cleaner and easier to read. Coincidentally, it is used all over the ZFS codebase with the addition of extra parentheses to tell GCC’s diagnostics “yes, I really meant to use assignment in a conditional expression here”. Just that alone should suppress this, but it does not (and perhaps I should file a bug report), so I had to disable it in my runs of codechecker, since it turned a list with hundreds of reports into a list of ~3000 reports, with all of the additional reports that I managed to check being perfectly fine code.
Not only Clang + CC is not sound static analysis, but I know for a fact that it does miss bugs that other tools have caught. Going a step further based on bug reports filed against OpenZFS, I say with certainty that a number of bugs that static analyzers should catch were never reported to me by any static analyzer. This has me considering the sound options for a next step as a way to get the missing reports after I am finished processing reports from the conventional static analyzers that I use.
> The other limitation is that there's only a limited complexity budget the analyzer can handle, so it cannot track all constraints on all paths. Depending on how the approximation is done it can lead to missed detection or false alarms.
I really should start looking into how to find statistics on unnecessarily pruned paths and look at knobs I can turn to reduce that.
Also, Clang’s static analyzer has an issue where it cannot understand even simple cases of reference counting. It also fails to understand error checking of libc functions (off the top of my head, it involved errno). No amount of knob turning will fix that sadly. There are a other bugs in how it’s checkers work too, although I will refrain from enumerating them off the top of my head since I do not remember them well at the moment.
> IKOS (last time I checked) does not support CTU, it's doing "a file at a time" analysis. As far as open source tools go the Clang static analyzer is the only one I know with a working support for CTU (best used through CC). I there are other ones I missed I'd be happy to learn about them and try them out.
I had not known that IKOS did not do cross translation unit analysis. Thanks for telling me about that. There is always the hack of concatenating all C files via the C preprocessor and static analyzing that. I have yet to be desperate enough to use that hack with a static analyzer to bolt on CTU analysis, so it remains an untested possibility. Perhaps I will finally deploy that hack when I try IKOS.
> This has me considering the sound options for a next step [...]
I'm definitely not an expert but look into SA a bit out of curiosity. Sound analysis normally comes with significant restrictions. For example Astrée does not support dynamic memory allocation nor recursion (not too bad for embedded). There's likely more.
Let's consider the case of an iteration, with a number of loops unknown at compile/analysis time. What an unsound SA will typically do is unroll the loop a fixed number of times (5 by default for CC/ClangSA from memory). Obviously this could miss bugs if less than the actual number of loops.
To do better, a fully automatic sound analyzer would have to derive the relevant loop invariants and the associated induction proofs automatically, not to have to make any guess on the number of iterations. As far as I know this is still a research topic. Or alternatively, enforce a known, small enough bounds for any loop.
In general, either the sound SA must be able to derive quite complex proofs for the characteristics to enforce (research topic), or it must enforce simplicity to make the problem manageable automatically.
An alternative is a tool like frama-C that can kick the ball back to a human, to do the correctness proof manually using a proof assistant for automatic verification, if automation fails. And that can be a hard job.
The more constrained the application, the more realistic sound analysis should be. I don't know where a filesystem like OpenZFS sits here. Best of luck in any case!
> For example Astrée does not support dynamic memory allocation nor recursion (not too bad for embedded).
Are you sure? Around 2019, they seem to have overcome those limitations, since they removed mention of them from their website. Another OpenZFS developer found that on an old university page and pointed it out to me, but that webpage was made well before then. I wonder if you read the same page that he did.
I plan to look into that when I am using the free trial.
> To do better, a fully automatic sound analyzer would have to derive the relevant loop invariants and the associated induction proofs automatically, not to have to make any guess on the number of iterations. As far as I know this is still a research topic. Or alternatively, enforce a known, small enough bounds for any loop.
I plan to look into this when I try using sound static analyzers, since if they cannot do induction proofs on loops to prove loop correctness, it would either invalidate their claims of soundness, or at the very least limit the scope of such claims, which would mean that I would not be able to semi-formally verify ZFS using them. I know that frama-c’s Eva is specifically documented as not being able to do this.
No, I just picked it from the ENS web page (https://www.astree.ens.fr) but it may have not been updated for a while.
As I understand it there's been improvement on dynamic allocation with separation logic in general, TBC what Astrée supports (I've no first hand experience).
For recursion, it's a similar problem as for loops as I understand it: to handle it fully automatically the analyzer would have to prove recursion terminates and find and prove induction invariant. But safety critical code tend to forbid it anyway so it may not be a big limitation for most Astrée customers.
> > The Clang static analyzer [1], used through CodeChecker (CC) [2], do support CTU (enabled with `--ctu`). I'm very happy with the result on the code I'm working on.
> I have done some preliminary testing with this on the OpenZFS codebase and I am less than happy with the result [...]
A question: have you verified that the Z3 support is enabled in the LLVM toolchain you use for Clang SA? It is in Debian Bookworm, but not in Buster, and from memory I don't think it is for Ubuntu 20.04 (LTS) due to a packaging snafu.
I would expect the lack of Z3 support to lead to a lot more false alarms in a FS, as the analysis with only the Clang SA build it range analysis will be basic and won't understand anything related to bit fields and operations for example.
The `llvm` package must depend on a `libz3-4` package, recent enough (on Bookworm it's 4.8.10, but IIRC anything >= 4.7 would be used). Another way to check could be to use the CodeChecker `--z3-refutation`: this is enabled by default if LLVM has the Z3 support, but if requested explicitly should fail if not (untried, TBC).
> A question: have you verified that the Z3 support is enabled in the LLVM toolchain you use for Clang SA? It is in Debian Bookworm, but not in Buster, and from memory I don't think it is for Ubuntu 20.04 (LTS) due to a packaging snafu.
That was one of the first things I did. Recompiling with z3 support made little difference. That said, I thought --z3-refutation Was the default when it was available.
I will try rerunning tests with it explicitly specified, but I do not expect much from that, since running tests with --z3, which replaces the range checker with z3, did not really eliminate reports beyond those that were in files that caused clang’s static analyzer to crash when that was set.
Yes, if the LLVM toolchain has Z3 support then `--z3-refutation` will be the default. It's only useful if you want an error in case the LLVM toolchain may not have this support.
I've read somewhere that the "full Z3" mode with `--z3` is very experimental and not well maintained. It didn't crash when I tried it but was no better and way too slow: typically 15 times slower on average, but a few files took over 24 hours to check.
> This is essentially the status quo, and it's not helpful. Better is possible.
It is helpful, since if you address all of the complaints, then your code will be proven to be free of the issues that the sound static analyzer can detect. In theory, you can produce C code that is proven to be memory safe by doing that, which effectively makes it semi-formally verified code. Unlike other methods of doing semi-formal verification, this method is actually usable by an average programmer.
Would you explain to me how that is the status quo? How would you do better?
