3 ms·

Sadly, mathematically proving that it does what the spec says does not necessarily mean that it's not vulnerable. The spec can be wrong too. Or the compiler. Or

Sadly, mathematically proving that it does what the spec says does not necessarily mean that it's not vulnerable. The spec can be wrong too. Or the compiler. Or both. Nevertheless, it's very interesting.

pluies 16y ago
As Donald Knuth would say: "Beware of bugs in the above code; I have only proved it correct, not tried it."
- shadowfox 16y ago
  This quote shows up like canon in almost every thread that has anything to do with formally verifiable/verified software :P
limmeau 16y ago
On http://ertos.nicta.com.au/research/l4.verified/ http://ertos.nicta.com.au/research/l4.verified/ , they explicitly do not claim that they have proven security properties.