6 ms·

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 har

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.

josh2600 8y ago
https://www.intel.com/content/www/us/en/support/articles/000006942/boards-and-kits/desktop-boards.html 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.
- a_t48 8y ago
  Definitely. I hit an ECC failure once. Felt like I should have bought a lotto ticket.
  - vardump 8y ago
    Just once? It's not that rare...
sidereal 8y ago
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 http://plv.csail.mit.edu/kami/papers/icfp17.pdf
zaarn 8y ago
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).
- natmaka 8y ago
  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/ECC_memory https://en.wikipedia.org/wiki/Redundancy_(engineering) https://en.wikipedia.org/wiki/Redundancy_(engineering)
  - Piskvorrr 8y ago
    They're capable of pushing down the odds, at a price.
  - zaarn 8y ago
    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.
    - adrianN 8y ago
      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.
- baybal2 8y ago
  8T Sram + advanced error correction codes push that into realms of astronomically improbable
  - zaarn 8y ago
    SRAM is fun until you need more than 100MB of it. There is also a number of other hardware failure scenarios.
    - 8y ago
sterlind 8y ago
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)
- baybal2 8y ago
  >Famously, a Microsoft intern modeled the XBox's cache coherence protocol and caught a bug there before they went to prod. xdcbt bug?
  - sterlind 8y ago
    Different bug! Good guess, though. http://channel9.msdn.com/Events/Build/2014/3-642#time=21m46s 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-leslie-lamport-turing-award/ https://www.asianscientist.com/2016/01/features/gyss-2016-le...
ajb 8y ago
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.
- Filligree 8y ago
  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. >_>
snaky 8y ago
> 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 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
- tonyg 8y ago
  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-through-45-years.pdf https://www.inf.ed.ac.uk/teaching/courses/ar/j_moore_sprint-...
longtermsec 8y ago
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).

josh2600 8y ago

https://www.intel.com/content/www/us/en/support/articles/000006942/boards-and-kits/desktop-boards.html 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.

a_t48 8y ago
Definitely. I hit an ECC failure once. Felt like I should have bought a lotto ticket.
- vardump 8y ago
  Just once? It's not that rare...

sidereal 8y ago

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 http://plv.csail.mit.edu/kami/papers/icfp17.pdf

zaarn 8y ago

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

natmaka 8y ago
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/ECC_memory https://en.wikipedia.org/wiki/Redundancy_(engineering) https://en.wikipedia.org/wiki/Redundancy_(engineering)
- Piskvorrr 8y ago
  They're capable of pushing down the odds, at a price.
- zaarn 8y ago
  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.
  - adrianN 8y ago
    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.
baybal2 8y ago
8T Sram + advanced error correction codes push that into realms of astronomically improbable
- zaarn 8y ago
  SRAM is fun until you need more than 100MB of it. There is also a number of other hardware failure scenarios.
  - 8y ago

sterlind 8y ago

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)

baybal2 8y ago
>Famously, a Microsoft intern modeled the XBox's cache coherence protocol and caught a bug there before they went to prod. xdcbt bug?
- sterlind 8y ago
  Different bug! Good guess, though. http://channel9.msdn.com/Events/Build/2014/3-642#time=21m46s 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-leslie-lamport-turing-award/ https://www.asianscientist.com/2016/01/features/gyss-2016-le...

ajb 8y ago

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.

Filligree 8y ago
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. >_>

snaky 8y ago

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

tonyg 8y ago
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-through-45-years.pdf https://www.inf.ed.ac.uk/teaching/courses/ar/j_moore_sprint-...

longtermsec 8y ago

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