Re:Select Code_execution from * Using SQLite; (2019)
by anyfoo on Saturday June 13, 2020 @05:14PM
(#23512792)
Thanks, this is for once in this thread, a real caveat in the application formal verification (or rigorous type systems). It's hard, it's not unlimited, and one may have fail to state crucial properties that matter in the first place.
Still, there are a lot of properties that are easy to state, and a lot of properties that are feasible to prove, and the intersection of these two can be very valuable in eradicating common issues in critical software, be it out-of-bounds pointers or your garden variety type confusion. (Again, not always possible, thanks to the halting problem, but often.)
The cost may indeed be prohibitive, though.
I don't think this is obvious, even for theoretical software, much less for practical software. Even formal methods have limitations.
A very public recent example was of the formally proven logic in Intel and other processors around speculative execution (Spectre, Meltdown etc.). That logic was formally proven not to leak information, but the formal model wasn't actually sophisticated enough. Note that these weren't hardware bugs (they weren't bugs in the electrical components of the processor or in the analog logic), they were logic bugs in the processor's code (whether that was microcode or burned into the processor is less relevant).
In general, you can prove that a piece of software adheres to some specification, but you can't prove that the specification itself is complete enough.
Of course, realistic software has many more layers of uncertainty, and realistic formal verification is far to costly to apply to anything but very short programs.