7 ms·

Hyperkernel – A push-button approach to building provably correct OS kernels

168 points by lainon 8y ago

jiveturkey 8y ago
uniprocessor only so i guess limited to embedded systems. does formally verified also mean bug-free?
- darkengine 8y ago
  From the project's GitHub repo: This does not mean that the kernel is guaranteed to have zero bugs. There can be bugs in unverified code (e.g., initialization and glue code), the specification (or things not modeled in the specification), or the verification toolchain including irpy/ and Z3.
- vinceguidry 8y ago
  Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth Code meeting spec doesn't magically make the spec right.
  - wiz21c 8y ago
    Is it already the case that a specification good enough to prove a program is bug free is smaller/less complex than the program itself. Because if it is not, then I'd assume the risk of failure in the specification just becomes bigger than in the program itself... So you'd need another tool to prove that the spec is correct...
    - naasking 8y ago
      Or you have the spec written twice, by two independent people and then compare.
      - vinceguidry 8y ago
        SQLite has three independently developed test codebases.
    - vinceguidry 8y ago
      The spec not being right means the human/humans that made it couldn't foresee all possible edge cases. It's not a bad thing for the spec to exceed the size of the program. SQLite does this, with over 700 times more test code than application code. The spec is the human interface to the expected behavior of the program, while the code is the human interface to the actual behavior of the program.
- sanxiyn 8y ago
  No, it doesn't, but practically speaking, it will be much more bug-free-er than those not verified.
  - amluto 8y ago
    Proof or no, seL4 has obvious bugs in its x86 asm. Citation: I read through it once.
    - im_down_w_otp 8y ago
      Did NICTA or Data61 do the work w/ x86 that they did with ARM (the Cambridge model stuff) to be able to assert equivalence between the C code and the resulting asm? If not, then it wouldn't surprise me that there's a conformance problem between the Isabelle, the Haskell, the C, and the asm.
      - ratmice 8y ago
        I don't believe that they did, at least last I read x86 was not a verification target. http://sel4.systems/pipermail/devel/2017-June/001477.html http://sel4.systems/pipermail/devel/2017-June/001477.html
        im_down_w_otp 8y ago
        Yeah I didn't think so. We only use x86_64 for convenience during active hacking on our workstations, then we simulate ARM for local testing and intermediate CI, and do release candidate CI & deployments to ARM target hardware.
      - amluto 8y ago
        I’m not sure, but I’m quite confident that they made no effort to extend the proof to include a model of the hardware and the low-level asm. Doing this would be hard — consider bugs like BadIRET or CVE-2018-8897. BadIRET would have been caught by any halfway credible model of the hardware. CVE-2018-8897, on the other hand, was the result of CPU behavior that was totally unclear in the manual and made no sense from a first-principles perspective.
andrewflnr 8y ago
Doing this kind of thing with a "mere" SMT solver seems pretty amazing to me. Haven't previous attempts to verify OS implementations and such all used heavy-duty dependent typesystems, higher-order logic and the like?
- pjmlp 8y ago
  Microsoft uses Z3 in their driver validation.
- snaky 8y ago
  It might be fruitful to combine two approaches, like for example VigNAT authors did > The beauty of symbolic execution lies in its ease of use: it enables automatic code analysis, hence can be used by developers without verification expertise. The challenge with symbolic execution is its notorious lack of scalability: applying it to real C code typically leads to path explosion. The part of real NF code that typically leads to unmanageable path explosion is the one that manipulates state. Hence, we split NF code into two parts: > A library of data structures that keep all the “difficult” state, which we then formally prove to be correct—this takes time and formal methods expertise, but can be amortized if the library is re-used across multiple NFs. > Stateless code that uses the library, which we automatically and quickly verify using symbolic execution. > The challenge lies in combining the results of these two verification techniques, and for that we developed a technique we call “lazy proofs” https://vignat.github.io/ https://vignat.github.io/
badrabbit 8y ago
Just a thought,this only proves the code is correct assuming hardware and firmware assumptions are also correct. Is it even possible to prove correctness of hardware? I've never heard of verified firmware as well.
- josh2600 8y ago
  https://www.intel.com/content/www/us/en/support/articles/000006942/boards-and-kits/desktop-boards.html https://www.intel.com/content/www/us/en/support/articles/000... << Not a total solution by any means. I have lots of thoughts about proving hardware/software/firmware correctness. Let's just say it's very hard.
  - a_t48 8y ago
    Definitely. I hit an ECC failure once. Felt like I should have bought a lotto ticket.
    - vardump 8y ago
      Just once? It's not that rare...
- sidereal 8y ago
  It’s certainly possible, though it comes with a different set of challenges to software verification. Here’s a recent paper in this direction, proving the correctness of a RISC-V CPU: http://plv.csail.mit.edu/kami/papers/icfp17.pdf http://plv.csail.mit.edu/kami/papers/icfp17.pdf
- zaarn 8y ago
  You can prove correctness of software, firmware and hardware and still have it all come crashing down the moment a bit flips. There is no solution to such things as "bitflip in memory" because once that happens, all bets are off. Instructions could be entirely wrong, page tables could have been corrupted, pointers in kernel memory pointing anywhere but where they belong, fire and brimstone raining from the sky, the dead walking among the living and the local supermarket running out of chocolate. You can however reduce the risk that such a bitflip results in a full system-, security- or application failure via various means (the Apollo 11 computer for example was capable of simply restarting a program at various checkpoints if they crashed and had multiple software and hardware safeguards against bitflips and random crashes).
Animats 8y ago
That's impressive. The approach works well given simple data structures. Their OS is a reimplementation of the UNIX V6 kernel, where most data structures were arrays, searched linearly. That's within the reach of the automated provers which use Scaling this up to huge servers might be a problem. This little verified OS should be useful for routers, IoT devices, and such.
dwheeler 8y ago
Very interesting! Sadly, their code does not seem to have a license. Hopefully they will correct that soon. No one gets to opt out of laws, and the default laws don't really let you do anything.
- dooglius 8y ago
  There is a license section in the readme
  - dwheeler 8y ago
    Thanks! That helps, but doesn't answer the question. This part is very helpful: > Files we created are licensed under the Apache License, Version 2.0, viewable at http://www.apache.org/licenses/LICENSE-2.0 http://www.apache.org/licenses/LICENSE-2.0, and are marked as such. This part makes it useless: > Code borrowed from other sources keeps the original copyright and license. What are those licenses? If they used a package manager I could just see that (a nice easy list). As it is, I can't tell what rights and requirements I have.
    - frankmcsherry 8y ago
      In case you are sincerely interested, the literal very next section enumerates which other projects they borrow from and their corresponding directories in the repo. I'm sure you can come back with "the xv6 dependence is underspecified" or whatever, but maybe let's wait until it turns out you actually want to use any of this before getting excited about your troubles with the licensing.

168 points by lainon 8y ago

jiveturkey 8y ago

uniprocessor only so i guess limited to embedded systems. does formally verified also mean bug-free?

darkengine 8y ago
From the project's GitHub repo: This does not mean that the kernel is guaranteed to have zero bugs. There can be bugs in unverified code (e.g., initialization and glue code), the specification (or things not modeled in the specification), or the verification toolchain including irpy/ and Z3.
vinceguidry 8y ago
Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth Code meeting spec doesn't magically make the spec right.
- wiz21c 8y ago
  Is it already the case that a specification good enough to prove a program is bug free is smaller/less complex than the program itself. Because if it is not, then I'd assume the risk of failure in the specification just becomes bigger than in the program itself... So you'd need another tool to prove that the spec is correct...
  - naasking 8y ago
    Or you have the spec written twice, by two independent people and then compare.
    - vinceguidry 8y ago
      SQLite has three independently developed test codebases.
  - vinceguidry 8y ago
    The spec not being right means the human/humans that made it couldn't foresee all possible edge cases. It's not a bad thing for the spec to exceed the size of the program. SQLite does this, with over 700 times more test code than application code. The spec is the human interface to the expected behavior of the program, while the code is the human interface to the actual behavior of the program.
sanxiyn 8y ago
No, it doesn't, but practically speaking, it will be much more bug-free-er than those not verified.
- amluto 8y ago
  Proof or no, seL4 has obvious bugs in its x86 asm. Citation: I read through it once.
  - im_down_w_otp 8y ago
    Did NICTA or Data61 do the work w/ x86 that they did with ARM (the Cambridge model stuff) to be able to assert equivalence between the C code and the resulting asm? If not, then it wouldn't surprise me that there's a conformance problem between the Isabelle, the Haskell, the C, and the asm.
    - ratmice 8y ago
      I don't believe that they did, at least last I read x86 was not a verification target. http://sel4.systems/pipermail/devel/2017-June/001477.html http://sel4.systems/pipermail/devel/2017-June/001477.html
      - im_down_w_otp 8y ago
        Yeah I didn't think so. We only use x86_64 for convenience during active hacking on our workstations, then we simulate ARM for local testing and intermediate CI, and do release candidate CI & deployments to ARM target hardware.
    - amluto 8y ago
      I’m not sure, but I’m quite confident that they made no effort to extend the proof to include a model of the hardware and the low-level asm. Doing this would be hard — consider bugs like BadIRET or CVE-2018-8897. BadIRET would have been caught by any halfway credible model of the hardware. CVE-2018-8897, on the other hand, was the result of CPU behavior that was totally unclear in the manual and made no sense from a first-principles perspective.

andrewflnr 8y ago

Doing this kind of thing with a "mere" SMT solver seems pretty amazing to me. Haven't previous attempts to verify OS implementations and such all used heavy-duty dependent typesystems, higher-order logic and the like?

pjmlp 8y ago
Microsoft uses Z3 in their driver validation.
snaky 8y ago
It might be fruitful to combine two approaches, like for example VigNAT authors did > The beauty of symbolic execution lies in its ease of use: it enables automatic code analysis, hence can be used by developers without verification expertise. The challenge with symbolic execution is its notorious lack of scalability: applying it to real C code typically leads to path explosion. The part of real NF code that typically leads to unmanageable path explosion is the one that manipulates state. Hence, we split NF code into two parts: > A library of data structures that keep all the “difficult” state, which we then formally prove to be correct—this takes time and formal methods expertise, but can be amortized if the library is re-used across multiple NFs. > Stateless code that uses the library, which we automatically and quickly verify using symbolic execution. > The challenge lies in combining the results of these two verification techniques, and for that we developed a technique we call “lazy proofs” https://vignat.github.io/ https://vignat.github.io/

badrabbit 8y ago

Just a thought,this only proves the code is correct assuming hardware and firmware assumptions are also correct. Is it even possible to prove correctness of hardware? I've never heard of verified firmware as well.

josh2600 8y ago
https://www.intel.com/content/www/us/en/support/articles/000006942/boards-and-kits/desktop-boards.html https://www.intel.com/content/www/us/en/support/articles/000... << Not a total solution by any means. I have lots of thoughts about proving hardware/software/firmware correctness. Let's just say it's very hard.
- a_t48 8y ago
  Definitely. I hit an ECC failure once. Felt like I should have bought a lotto ticket.
  - vardump 8y ago
    Just once? It's not that rare...
sidereal 8y ago
It’s certainly possible, though it comes with a different set of challenges to software verification. Here’s a recent paper in this direction, proving the correctness of a RISC-V CPU: http://plv.csail.mit.edu/kami/papers/icfp17.pdf http://plv.csail.mit.edu/kami/papers/icfp17.pdf
zaarn 8y ago
You can prove correctness of software, firmware and hardware and still have it all come crashing down the moment a bit flips. There is no solution to such things as "bitflip in memory" because once that happens, all bets are off. Instructions could be entirely wrong, page tables could have been corrupted, pointers in kernel memory pointing anywhere but where they belong, fire and brimstone raining from the sky, the dead walking among the living and the local supermarket running out of chocolate. You can however reduce the risk that such a bitflip results in a full system-, security- or application failure via various means (the Apollo 11 computer for example was capable of simply restarting a program at various checkpoints if they crashed and had multiple software and hardware safeguards against bitflips and random crashes).

Animats 8y ago

That's impressive. The approach works well given simple data structures. Their OS is a reimplementation of the UNIX V6 kernel, where most data structures were arrays, searched linearly. That's within the reach of the automated provers which use Scaling this up to huge servers might be a problem. This little verified OS should be useful for routers, IoT devices, and such.

dwheeler 8y ago

Very interesting! Sadly, their code does not seem to have a license. Hopefully they will correct that soon. No one gets to opt out of laws, and the default laws don't really let you do anything.

dooglius 8y ago
There is a license section in the readme
- dwheeler 8y ago
  Thanks! That helps, but doesn't answer the question. This part is very helpful: > Files we created are licensed under the Apache License, Version 2.0, viewable at http://www.apache.org/licenses/LICENSE-2.0 http://www.apache.org/licenses/LICENSE-2.0, and are marked as such. This part makes it useless: > Code borrowed from other sources keeps the original copyright and license. What are those licenses? If they used a package manager I could just see that (a nice easy list). As it is, I can't tell what rights and requirements I have.
  - frankmcsherry 8y ago
    In case you are sincerely interested, the literal very next section enumerates which other projects they borrow from and their corresponding directories in the repo. I'm sure you can come back with "the xv6 dependence is underspecified" or whatever, but maybe let's wait until it turns out you actually want to use any of this before getting excited about your troubles with the licensing.