4 ms·

seL4: Formal Verification of an OS Kernel (from 2009). https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf https://www.sigops.org/sosp/sosp09/papers/kle

seL4: Formal Verification of an OS Kernel (from 2009). https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf seL4 is about 9000 LOC. So this gives a good indication of what formal verification (Isabelle/HOL) is currently capable of. seL4 is also quite fast as a result of removing unnecessary checks. https://sel4.systems/ https://sel4.systems/ seL4 is smaller than L4Ka::Pistachio and it's also capability based which L4 isn't. They could have called it L5 or seL5.

godelmachine 9y ago
I want to learn formal verification on my own. Do you know of any resources? I got Rolf Dreshler's book on circuit verification, but I would like to master both hardware and software. Would you kindly provide with some pointers?
- CalChris 9y ago
  It's a broad subject and I'm only interested in software verification. It's specialized enough that you should be reading papers and reading about systems. My favorite systems+papers are: Coq: The world’s best macro assembler? https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/ https://www.microsoft.com/en-us/research/publication/coq-wor... Vale: Verifying High-Performance Cryptographic Assembly Code https://project-everest.github.io/assets/vale2017.pdf https://project-everest.github.io/assets/vale2017.pdf x86proved https://x86proved.codeplex.com/ https://x86proved.codeplex.com/
- mcguire 9y ago
  Two schools: * Coq/dependent types. Check out Software Foundations by Benjamin Pierce, et. al. Everything's online. Also see Idris, which has a good book from Manning. * SMT-solver-based verification of existing languages. See SPARK/Ada (there's a good book but I can't remember the name presently) and the GNAT website. Also, Frama-C, although the documentation is more spotty. Then there's Rustan Leino's work on Dafny and Boogie. Oh, and Why3. And some work on verifying Java code that I haven't played with yet.
  - mcguire 9y ago
    Three, three schools: * Model checking/high level formal specs. Lamport's TLA+, Alloy, possibly Z. There are some good TLA+ things online, I just couldn't get into it. (I feel bad.)
  - auggierose 9y ago
    Isabelle/HOL (the one sel4 was done in) appears in none of your two schools ... This might be because it is the best combination of interactive theorem proving with automated methods that currently exists out there.
    - mcguire 9y ago
      As far as I know, Isabelle/HOL is fairly similar to Coq, perhaps with more automation. If there is something like Software Foundations for Isabelle, I'd be slobbering all over myself in excitement to hear about it. (And I'm still a little confused about how the C code of seL4 is verified against the formal specs. Is there something like Frama-C involved?)
      - auggierose 9y ago
        Both are interactive theorem provers, so yeah. But the two school comment said Coq/dependent-types, and Isabelle/HOL is neither Coq, nor does it do dependent types :) If you are looking for developments in Isabelle/HOL, there is the AFP: https://www.isa-afp.org/ https://www.isa-afp.org/ There is also a recent book that might interest you: http://www.concrete-semantics.org/ http://www.concrete-semantics.org/
        mcguire 9y ago
        Sweet, thanks!
nickpsecurity 9y ago
Note that this is formal verification of an imperative, C-based program manipulating low-level structures done years ago. I wouldnt say that represents what we're currently capable of in general case. For starters, a functional program or imperative without pointers (eg in SPARK) is much easier to verify than a C program. Plus, the seL4 organization recently reduced effort for filesystems down by a few multiples with a functional language. Truth is the seL4 team set themselves up for a harder-than-usual job. For good reason but most folks (esp managed languages) won't see as much difficulty.

godelmachine 9y ago

I want to learn formal verification on my own. Do you know of any resources? I got Rolf Dreshler's book on circuit verification, but I would like to master both hardware and software. Would you kindly provide with some pointers?

CalChris 9y ago
It's a broad subject and I'm only interested in software verification. It's specialized enough that you should be reading papers and reading about systems. My favorite systems+papers are: Coq: The world’s best macro assembler? https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/ https://www.microsoft.com/en-us/research/publication/coq-wor... Vale: Verifying High-Performance Cryptographic Assembly Code https://project-everest.github.io/assets/vale2017.pdf https://project-everest.github.io/assets/vale2017.pdf x86proved https://x86proved.codeplex.com/ https://x86proved.codeplex.com/
mcguire 9y ago
Two schools: * Coq/dependent types. Check out Software Foundations by Benjamin Pierce, et. al. Everything's online. Also see Idris, which has a good book from Manning. * SMT-solver-based verification of existing languages. See SPARK/Ada (there's a good book but I can't remember the name presently) and the GNAT website. Also, Frama-C, although the documentation is more spotty. Then there's Rustan Leino's work on Dafny and Boogie. Oh, and Why3. And some work on verifying Java code that I haven't played with yet.
- mcguire 9y ago
  Three, three schools: * Model checking/high level formal specs. Lamport's TLA+, Alloy, possibly Z. There are some good TLA+ things online, I just couldn't get into it. (I feel bad.)
- auggierose 9y ago
  Isabelle/HOL (the one sel4 was done in) appears in none of your two schools ... This might be because it is the best combination of interactive theorem proving with automated methods that currently exists out there.
  - mcguire 9y ago
    As far as I know, Isabelle/HOL is fairly similar to Coq, perhaps with more automation. If there is something like Software Foundations for Isabelle, I'd be slobbering all over myself in excitement to hear about it. (And I'm still a little confused about how the C code of seL4 is verified against the formal specs. Is there something like Frama-C involved?)
    - auggierose 9y ago
      Both are interactive theorem provers, so yeah. But the two school comment said Coq/dependent-types, and Isabelle/HOL is neither Coq, nor does it do dependent types :) If you are looking for developments in Isabelle/HOL, there is the AFP: https://www.isa-afp.org/ https://www.isa-afp.org/ There is also a recent book that might interest you: http://www.concrete-semantics.org/ http://www.concrete-semantics.org/
      - mcguire 9y ago
        Sweet, thanks!

nickpsecurity 9y ago

Note that this is formal verification of an imperative, C-based program manipulating low-level structures done years ago. I wouldnt say that represents what we're currently capable of in general case. For starters, a functional program or imperative without pointers (eg in SPARK) is much easier to verify than a C program. Plus, the seL4 organization recently reduced effort for filesystems down by a few multiples with a functional language. Truth is the seL4 team set themselves up for a harder-than-usual job. For good reason but most folks (esp managed languages) won't see as much difficulty.