Hyperkernel – A push-button approach to building provably correct OS kernels(unsat.cs.washington.edu)
unsat.cs.washington.edu
Hyperkernel – A push-button approach to building provably correct OS kernels
https://unsat.cs.washington.edu/projects/hyperkernel/
45 comments
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?
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/
> 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/
Microsoft uses Z3 in their driver validation.
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.
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).
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)
https://en.wikipedia.org/wiki/ECC_memory https://en.wikipedia.org/wiki/Redundancy_(engineering)
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.
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.
They're capable of pushing down the odds, at a price.
> 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.
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.
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.
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.
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.
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?
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...
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...
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
> 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
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-...
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.
I have lots of thoughts about proving hardware/software/firmware correctness. Let's just say it's very hard.
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. >_>
The flip side is, your CPU may need a firmware update. >_>
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).
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.
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?
does formally verified also mean bug-free?
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.
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...
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.
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.
Or you have the spec written twice, by two independent people and then compare.
SQLite has three independently developed test codebases.
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.
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.
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’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.
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.
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.
This little verified OS should be useful for routers, IoT devices, and such.