3 ms·
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 gen
by 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 agoThough 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 agoJust 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.