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

Re:Hyperkernel – A push-button approach to building provably... by zaarn on Wednesday September 12, 2018 @02:40AM (#17966066)

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

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by natmaka on Wednesday September 12, 2018 @03:47AM (#17966324)

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)

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by zaarn on Wednesday September 12, 2018 @04:45AM (#17966601)

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.

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by adrianN on Wednesday September 12, 2018 @05:45AM (#17966906)

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.

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by Piskvorrr on Wednesday September 12, 2018 @03:59AM (#17966377)

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

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by naasking on Wednesday September 12, 2018 @07:55AM (#17967565)

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

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by baybal2 on Wednesday September 12, 2018 @06:13AM (#17967024)

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

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by zaarn on Wednesday September 12, 2018 @07:01AM (#17967246)

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

There is also a number of other hardware failure scenarios.

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by analognoise on Wednesday September 12, 2018 @11:22AM (#17969662)

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.

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by zaarn on Thursday September 13, 2018 @12:10AM (#17975944)

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

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by baybal2 on Thursday September 13, 2018 @07:30AM (#17977757)

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.

[ Parent | on HN ]