4 ms·

It allows academics and other informed scientists to talk confidently about their design. Everybody else like Linux admins and VM users is still working with a

It allows academics and other informed scientists to talk confidently about their design. Everybody else like Linux admins and VM users is still working with a black box software. Sure cloud vendors may get on board and start announcing how their solution is the best verified software out there. Did I mention bullshit marketing yet?

touisteur 5y ago
I don't understand. If I've proved the absence of runtime errors in some code, in addition to classical tests, are you saying that the software is not less likely to crash? Yes, there can be errors everywhere but I don't get this complete rejection of Formal verification tools as 'just a debugging tool'.
- posix_me_less 5y ago
  It is less likely to crash after you complete the proof than if you couldn't complete the proof, but this does not mean this benefit will be worth much. In general, all things being equal, software less likely to crash in production is an improvement, but: 1) all things are usually not equal, because verified software is hard to produce and typically much more restrictive and hard to modify 2) how often do standard industry solutions for hypervisor like Xen or KVM crash? Uptime/customer loss due to hypervisor crashes is a negligibly small problem. The user software should rather work with the assumption that crash can happen. That is much more robust architecture than relying on some proofs that nobody checked.
  - touisteur 5y ago
    Though I agree about being 'crash proof' we're talking security here, so DoS or RCE might happen because of a buggy parser, crash or no crash. If I can create a parser that won't produce any error whatsoever, and always return something (be it 'malformed message'), haven't I increased the security of my external interfaces, compared to, let's say, a shit parser full of UB and no check because the program is crashes happen anyway?
  - madsbuch 5y ago
    Just entering this troll thread for a small correction: > ... relying on some proofs that nobody checked It is indeed check every single time the software compiles.
  - posix_me_less 5y ago
    @madsbuch I meant classical "Dijkstra-style" proofs. I know about automated proofs, they are great accomplishment, and software that they produce may be good. I wouldn't believe those automated proofs any more than I would believe human-made proofs. Errors in intent and design can happen, I still want to test the resulting software in action and have the option to easily modify it.

touisteur 5y ago

I don't understand. If I've proved the absence of runtime errors in some code, in addition to classical tests, are you saying that the software is not less likely to crash? Yes, there can be errors everywhere but I don't get this complete rejection of Formal verification tools as 'just a debugging tool'.

posix_me_less 5y ago
It is less likely to crash after you complete the proof than if you couldn't complete the proof, but this does not mean this benefit will be worth much. In general, all things being equal, software less likely to crash in production is an improvement, but: 1) all things are usually not equal, because verified software is hard to produce and typically much more restrictive and hard to modify 2) how often do standard industry solutions for hypervisor like Xen or KVM crash? Uptime/customer loss due to hypervisor crashes is a negligibly small problem. The user software should rather work with the assumption that crash can happen. That is much more robust architecture than relying on some proofs that nobody checked.
- touisteur 5y ago
  Though I agree about being 'crash proof' we're talking security here, so DoS or RCE might happen because of a buggy parser, crash or no crash. If I can create a parser that won't produce any error whatsoever, and always return something (be it 'malformed message'), haven't I increased the security of my external interfaces, compared to, let's say, a shit parser full of UB and no check because the program is crashes happen anyway?
- madsbuch 5y ago
  Just entering this troll thread for a small correction: > ... relying on some proofs that nobody checked It is indeed check every single time the software compiles.
- posix_me_less 5y ago
  @madsbuch I meant classical "Dijkstra-style" proofs. I know about automated proofs, they are great accomplishment, and software that they produce may be good. I wouldn't believe those automated proofs any more than I would believe human-made proofs. Errors in intent and design can happen, I still want to test the resulting software in action and have the option to easily modify it.