4 ms·

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.

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.