Hacker News Reader

Hacker News

Comment by jiveturkey | Hacker News Reader

Full thread

jiveturkey

uniprocessor only so i guess limited to embedded systems.

does formally verified also mean bug-free?

View on HN

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.

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

Or you have the spec written twice, by two independent people and then compare.

SQLite has three independently developed test codebases.

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.

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.

No, it doesn't, but practically speaking, it will be much more bug-free-er than those not verified.

Proof or no, seL4 has obvious bugs in its x86 asm. Citation: I read through it once.

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.

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

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.

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.

Reply on news.ycombinator.com