Hyperkernel – A push-button approach to building provably correct OS kernels | Hacker News Reader

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

unsat.cs.washington.edu

168 pointslainon45 comments

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.

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?

Microsoft uses Z3 in their driver validation.

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/

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.

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.

Definitely. I hit an ECC failure once. Felt like I should have bought a lotto ticket.

Just once? It's not that rare...

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

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

Aren't ECC RAM and redundancy able to keep both the dead and the chocolate where they belong?

https://en.wikipedia.org/wiki/ECC_memory https://en.wikipedia.org/wiki/Redundancy_(engineering)

They're capable of pushing down the odds, at a price.

With some probability, yes, but it's still non-zero. There are other failures where ECC doesn't help (ie, bitrot on your SSD or Harddrive, cosmic ray hitting the CPU itself, anything that does DMA).

The best we can do is deploy ECC, hope the cosmic rays don't hit our Datacenter too hard and design software to fail fast if it fails, even if math says it can't fail. Because it will fail.

It's not impossible to add enough error correction and redundancy to your stuff that it's more likely that we're wiped out by an asteroid than for your software to crash because of cosmic rays.

8T Sram + advanced error correction codes push that into realms of astronomically improbable

SRAM is fun until you need more than 100MB of it.

There is also a number of other hardware failure scenarios.

God I wish we had denser, regular SRAM. The lack of overhead makes working with old-school async rams a lot of fun - I've only ever talked to DDR via the Xilinx MIG (or the Zynq's Synopsys DDR memory controller IP), and theres just so much more going on than in an old school SRAM.

There are some options, I think MRAM and FRAM do have higher capacities but they're still expensive due to be fairly new...

MRAM is actually very good for rad hardness, but it has a showstopper for bizarre feature of "probabilistic read." Speciality 3T MRAM completely negates that flaw.

> There is no solution to such things as "bitflip in memory" because once that happens, all bets are off.

Static typing for a faulty lambda calculus: http://lambda-the-ultimate.org/node/2108

You can build as much fault tolerance as you like to the point where you'd have to wait for a proton to decay before you see an error.

Intel uses TLA+ extensively for formal verification of its subsystems, in a kind of piecemeal approach.

Famously, a Microsoft intern modeled the XBox's cache coherence protocol and caught a bug there before they went to prod.

Certainly bit flips can happen, but you can still prove that circuits obey your invariants!

(Note: TLA+ doesn't always fully prove correctness. Z3 is a more sophisticated approach but harder to apply to temporal logic)

>Famously, a Microsoft intern modeled the XBox's cache coherence protocol and caught a bug there before they went to prod.

xdcbt bug?

Different bug! Good guess, though.

http://channel9.msdn.com/Events/Build/2014/3-642#time=21m46s

> A little closer to home, Lamport shared an anecdote of how his programming language even helped Microsoft avert a near-certain disaster. While writing a TLA+ specification for an IBM-developed memory system chip in the Xbox 360, a Microsoft intern discovered a bug that would cripple the game console. The IBM engineers’ first reactions were of disbelief, saying it could not possibly happen, Lamport said. However, they changed their tune a few weeks later. “Their tests would not have discovered it, and had this intern not discovered this bug, it would have gone into production; every Xbox would have crashed after four hours of use. [That’s] a nice success story.”

Source: https://www.asianscientist.com/2016/01/features/gyss-2016-le...

Formal verification arrived at hardware first, really. Because although sofware and hardware can in principal be equally complex, the economic cost of a bug in hardware causes as much as possible of the complexity to be punted into software. That leaves the problem of verifying hardware more tractable. I don't think it's yet done comprehensively but a greater fraction of forma verification is used on hardware than software.

That's also a large part of the push towards microcode. Once you get to the level of micro-ops, even modern CPUs are... reasonably simple.

The flip side is, your CPU may need a firmware update. >_>

> ACL2 has had numerous industrial applications. In 1995, J Strother Moore, Matt Kaufmann and Tom Lynch used ACL2 to prove the correctness of the floating point division operation of the AMD K5 microprocessor in the wake of the Pentium FDIV bug. The interesting applications page of the ACL2 documentation has a summary of some uses of the system. Industrial users of ACL2 include AMD, Centaur Technology, IBM, Intel, Oracle, and Rockwell Collins. ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover, NQTHM.

https://en.wikipedia.org/wiki/ACL2

NQTHM was used to check e.g. FM9001 CPU

ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-bibliography.html

B. Brock, W. A. Hunt, and M. Kaufmann. The FM9001 Microprocessor Proof. Tech. Rept. 86, Computational Logic, Inc., 1994. ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/086.pdf

J Strother Moore has some good slides on industrial applications of ACL2 here: https://www.inf.ed.ac.uk/teaching/courses/ar/j_moore_sprint-...

Yeah it's a tough space for sure.

Given that this is a research project i'd hold off on making assumptions that the software has been adequately verified as well. Forgive the loose usage of Rumsfeld-like terminology here, verification implementation errors (Unknown Unknowns) and omissions (Unknown Unknowns) in the verification translate to exploitable software security holes. If the model is sound, it would address all Known Unknowns and to get a verified, working codebase the developers would have to address Known Knows. And there may be some security tech-debt as well which isn't mentioned publicly (Unknown Knowns).

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.

There is a license section in the readme

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

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.

uniprocessor only so i guess limited to embedded systems.

does formally verified also mean bug-free?

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.

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.

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