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)

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.

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.

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.

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

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

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.

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

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

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

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