Yes, absolutely.
Static analyzers are for when your test suite is subpar.
If you're obsessive, like the SQLite guys [1], runtime checkers are better.
But you have to be obsessive about an excessive test suite.
Static analyzers are for when your test suite is subpar.
If you're obsessive, like the SQLite guys [1], runtime checkers are better.
But you have to be obsessive about an excessive test suite.
What I said is that runtime checking is better if you have a test suite that's good enough.
A way of discussing it that doesn't place them in competition with each other would instead talk about their relative characteristics, including factors that might make different options more or less effective (or even inapplicable) in certain circumstances.
For example, there are certain classes of defect that cannot be detected at runtime. But what does and does not fall into this category depends on what programming language you're using. There are other classes of defect that cannot be detected statically, and the specifics of this list also depends on what language you're using.
And then there's also a bunch of overlap, but the relative merits of one or another way of solving things cannot be boiled down to a simple "better/worse" hierarchy. The optimal strategy is often domain-specific and finding it may require weighing many tradeoffs.
Absolutely not. It says that they have tradeoffs, and one will be better in certain situations, while the other will be better in others.
If you think that means competition, you're overreading it.
You want a test suite, but it's never better or good enough.
Abstract Interpretation in a Nutshell https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html
That is a wild claim.
But how many false positives does it have?
Too bad it's not FOSS; I would pay for that is the false positive rate was not too high.
We are talking code without dynamic memory allocation, recursive function calls, no system and library calls, of course. Like some embedded aerospace, automation, healthcare and military applications. You can use it to verify some libraries if you can't do full coverage. Application domain abstractions are also available.
NASA has open source tool called IKOS based on same abstract interpretation concept, but I don't know it's features.
You can't replace testing with formal methods, but formal methods are more powerful when they work. That sqlite hasn't found them useful is just a reflection of how absurdly far out they are on the testing spectrum and how complicated the problem domain they're operating in is (very).
But you're also weakening your own point; you admit that if you test enough, they don't work as well, and you also admit that they work less well the more complicated things get.
The other problem is showing that the artifact you proved is the same artifact that you are using. The enormous amount of effort put in by the seL4 people is proof that that is non-trivial, and seL4 is tiny compared to SQLite.
So when you say, "formal methods are more powerful when they work," you are right, but "when they work" is carrying a lot of weight.
And that's one thing I disagree with the SQLite guys on; I build with all warnings enabled to get me a "stronger" type system in C. I get stronger warnings against pointer casting and things like that.
But "a lot of the benefits" is still maybe about half of the benefits of full formal methods.
It's not a good metric to claim that since seL4 did things the hard way that any formal methods project is impractical. That's simply not the case. seL4 is an OS with very specific process isolation requirements that they wanted to model using a proof assistant. SQLite wouldn't need that level of instrumentation in proofs. Most of SQLite could be formally verified using a model checker.
Model checkers, such as CBMC and others, can provide safety checks without needing to build constructive proofs. In practice, constructive proofs are only needed for things that model checking can't solve, such as data structures and algorithms requiring recursion or looping. In these cases, a proof assistant with inductive theorems can be used to extract equivalent software that can be proven to be safe in the recursive case. But, if your goal is just to check to see if your code is safe, which goes beyond the limits for most developers to test with unit testing alone, then model checking is good enough.
I use model checking in all of the C software I write, and have done so for nearly a decade now. It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. It adds, perhaps, 30% development overhead. Model checking makes my code safer because it gives me the ability to track function contracts, UB in integer and pointer math, and resource ownership. Attempting to do this with unit testing requires that I'm smart enough, every time, to create the right tests for things that simply don't show up when I look at code coverage reports. That classical trivial test of inputs using 0, -1, numbers close to or equal to integer limits, etc., don't necessarily catch the limit hole caused by wonky pointer math. The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't.
I used to think I was a great programmer. Then, I spent a couple years running my code through a model checker. Now, I know better.
Sure, if you can. And I use such checkers too.
But for a lot of people, the false positive false negative rates are still high.
That's why tests can be better: there's no false positive or false negative.
> The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't.
This is unfortunately completely naive. Of course model checkers miss things.
Perhaps you're thinking of a static analyzer which is something different.
The ENTIRE POINT of a model checker is that it translates the program into a constraint solver. Can it miss things? Yes, if there is a bug in the translation. It can't be trusted for things that it can't detect, but a model check is equivalent to a constructive proof. It just doesn't have some tools like induction that make constructive proofs necessary in cases where model checking fails.
There is no such thing as a magic tool. The scenarios under model check must be properly built, just like any formal proof. But, a constructive proof assistant and a SMT solver are both forms of proof engines. A model checker uses an SMT solver.
The seL4 team uses model checking as well, in the generated code. They trust model checking in these cases because it's thorough. If it missed things, it would be pointless to use.
So you're saying humans are bad at writing software, but good at writing translations for model checkers?
I disagree.
The reason model checkers miss things is because of humans.
> The seL4 team uses model checking as well, in the generated code.
I am aware, trust me.
Are you aware how much effort they had to expend to do that?
Nice strawman. However, that's not at all what I said. To restate in different words, even proofs can be incorrect. Even model checkers can be wrong. However, you seem to be under the impression that unless a model checker is 100% perfect, it's worthless. That's not the case. For the vast majority of situations, the model checker will either correctly generate a constraint problem based on what you provide (remember, garbage in / garbage out and proofs of bad theorems are meaningless), or will generate some kind of diagnostic error.
Everything -- EVERYTHING -- is flawed. But, if your standard of measure is "only perfect things can augment or replace unit tests" then you're doing yourself and any organization you contribute to a great disservice.
> I am aware, trust me.
Respectfully, I think you're still conflating model checkers, static analyzers, and proof systems.
> Are you aware how much effort they had to expend to do that?
Clearly, much less than you think. I've estimated both ways. Using CBMC adds 30% overhead. That's well worth the effort.
Unfortunately, unless you're careful, or have a test suite to make sure, it is the case.
You might have a good model, but if your software doesn't actually implement the model, it's giving you a false sense of security. And those bugs can persist.
> Respectfully, I think you're still conflating model checkers, static analyzers, and proof systems.
Not at all. I know the differences.
But in this context, they all have the same problem: making sure the code matches the model/proof (static analyzers have an implicit internal model).
> Clearly, much less than you think. I've estimated both ways. Using CBMC adds 30% overhead. That's well worth the effort.
Ten years of work for four people, I think. That's not 30% overhead. I think at last count, their C code was less than 10 KLoC, but their proof was beyond 200-300 KLoC.
That's a 2000% overhead.
Respectfully, you are definitely conflating these concepts. First, a test suite can't replace a model checker. These are two very different things. You can absolutely miss things in a test suite, and even get 100% branch coverage. Your tests can appear to be perfect, and can even pass code review, and still miss things. A test suite can't make sure of anything, because this would imply that your software and your test suite is perfect.
Unit testing is empirical. Not model driven or constructive. Hence, you don't actually have any indication about when you are done. Even if you get to 100% branch coverage. Even if your tests appear to be perfect. You have likely missed tests that exercise cases in your code that you don't even realize are there. Undefined behavior due to integer overflow is common, and almost every mature code base that I have seen -- including SQLite -- misses these classes of errors.
A model checker or a constructive proof system starts from a priori theory. This is used to extract software, or in the case of a source level model checker, the software is used to create the model. While it is certainly possible for gaps to exist here, it's far less likely. Furthermore, there is a direct way to translate this a priori knowledge into "done". If the model checker uses the same libraries as the code generator in the compiler, then there can be a 1:1 relationship between the constructed model and the generated code. Barring inaccuracies in hardware simulation or actual hardware errors or compiler errors, the two will be quite close. If the compiler were extracted from constructive proofs (e.g. CompCert), then the likelihood of compiler errors generating different machine code is even further removed. While nothing is perfect, we are talking about two to three orders of magnitude of added precision over hand-written unit tests.
> You might have a good model, but if your software doesn't actually implement the model...
Ah... there's part of the problem. You don't seem to understand what a model checker is. A model checker transforms source code into a constraint solver, following the same rules that the compiler uses to generate machine code. Yes, there are high-level model checkers that can work on algorithms, but as is clear from the context, I'm talking about source level model checkers. The software and the model are the same. The model is based on the same abstract machine model used for the language and for the particular machine code implementation. The software is transformed into a constraint solver on top of this model. If the two don't match, then a lot of things have gone seriously wrong. In practice, this is about as likely as your compiler generating the wrong code, or your CPU deciding that the MOV instruction really means JMP.
> Not at all. I know the differences.
Clearly not, and here's why:
> Ten years of work for four people, I think... That's a 2000% overhead.
The seL4 team used constructive proof assistant (i.e. Isabelle HOL). Not a model checker (e.g. CBMC). You're conflating the two. You don't understand the difference, and you're plunging ahead as if you do. That is where the crux of this disagreement comes from. Model checkers and constructive proof assistants are both ways to do formal methods, but they are different, with different use cases. seL4 is an atypical example, which used pure constructive proofs because they needed to prove that their operating system implemented well founded process isolation.
When I mentioned that the seL4 team used a model checker, I meant and implied, IN ADDITION TO the constructive proof assistant. This is because both systems are best used for different domains. In practice, the use of a model checker requires relatively minimal overhead. In practice -- my use case -- this is around 30%.
Respectfully, I think you should spend some time studying and using these tools. They will improve the quality of the software you write.
They can demonstrate the bugs, when found, are in the specifications
Or in the methods....
Highly recommended if you want to get more bang per line of testing code.
In fact, in my current project, I add every single path found by AFL++ to my test suite. It tests all kinds of terrible things, and then those paths are tested forever.
I even run all the paths AFL++ finds through the sanitizers and Valgrind.
No, this statement is quite wrong and expresses a failure to understand the roles and responsibilities of each class of automated tests, and the purpose of static code analysis tools.
Automated tests and static code analysis tools are complementary tools. They don't share responsibilities at all. Just because both can run in the same pipeline stage that does not mean they serve the same purpose.
But I also didn't define "subpar" for a test suite; the SQLite guys have full-coverage testing. That's probably the line for "subpar," and (almost) nobody else actually has that.
No, not really. If you read up on the basics of automated testing, you'll find out that test classes such as unit, integration, UI, performance, accessibility, and localization tests share the same goal: specify and check invariants in the code and in its interfaces.
Static code analysis tools have an entirely different set of responsibilities. They do not have the responsibility of checking the compliance with contracts, including things like SLAs or whether a button is navigatable with a keyboard as per the wishes of a Program Manager.
So what are those responsibilities?
https://en.wikipedia.org/wiki/Static_program_analysis
If you're interested in onboarding onto the topic, you can start by reading the first paragraph of the Rationale section.
> The uses of the information obtained from the analysis vary from highlighting possible coding errors (e.g., the lint tool) to formal methods that mathematically prove properties about a given program (e.g., its behaviour matches that of its specification).
Sounds like finding defects to me.
You see, I don't think you are. If you were, you certainly wouldn't make totally oblivious claims such as "static analyzers are for when your test suite is subpar."
> Sounds like finding defects to me.
If you were familiar with static analysis tools, you'd be well aware that they only cover a narrow class of defects, which other classes of automated tests do.
Again, I seriously recommend you onboard onto the basics of automated testing, specially the intro section on the classes of tests and what are their design goals, and in the meantime refrain from posting comments on testing.