3 ms·

seL4 primarily uses a proof assistant, which is a MUCH harder way to go about formal methods. It's thorough, sure, but for 80% to 95% of the average code base,

seL4 primarily uses a proof assistant, which is a MUCH harder way to go about formal methods. It's thorough, sure, but for 80% to 95% of the average code base, model checking would work just fine. 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.

gavinhoward 3y ago
> 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. 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.
- nanolith 3y ago
  > 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.
  - gavinhoward 3y ago
    > Can it miss things? Yes, if there is a bug in the translation. 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?
    - nanolith 3y ago
      > So you're saying humans are bad at writing software, but good at writing translations for model checkers? 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.

gavinhoward 3y ago

> 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. 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.

nanolith 3y ago
> 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.
- gavinhoward 3y ago
  > Can it miss things? Yes, if there is a bug in the translation. 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?
  - nanolith 3y ago
    > So you're saying humans are bad at writing software, but good at writing translations for model checkers? 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.