This is relevant for security, because entire operating systems have been formally proven to adhere to their specification/free of all bugs: https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
2. Even proving anything about finite state machines is NP hard so the problem is harder than just using weaker model of computation.
3. Proofs are not reuable: proving something about one program does not tell us anything about other programs.
See excellent https://pron.github.io/posts/correctness-and-complexity for more details.
> 1. Unfortunately the set of "some" programs is unknown and most probably really small.
Many useful algorithms can be proven to terminate. Compare against the situation in mathematics: many theorems are not be provable, but that does not stop us from trying to prove useful theorems, or recognizing that a given theorem has already been proven.
> 3. Proofs are not reuable: proving something about one program does not tell us anything about other programs.
This is true in the sense that a proof of arbitrary program A does not tell us anything about many other programs. But it is clear for example that if, say a program is recognized by inspection as the concatenation (splicing the final states and initial states together) of two programs that terminate, then this program terminates.
Even the link you provide gives optimism and claims that
> Now we know why writing correct programs is hard: because it has to be. But while we cannot verify all programs all the time – regardless of how they’re written – there’s nothing stopping us from verifying some programs some of the time for some properties.
I would say that one small piece of software (Sel4 is only 9,400 SLOC!) always cited as an example is actually a very small set of programs that can be formally verified. I haven't heard of a formally verified web browser...
> Many useful algorithms can be proven to terminate.
Proving that a program terminates is not that much interesting. Lack of security vulnerabilities would be much better.
> But it is clear for example that if, say a program is recognized by inspection as the concatenation (splicing the final states and initial states together) of two programs that terminate, then this program terminates
But it does not tell us anything about real programs? We don't compose software by concatenating their state machines.
> Even the link you provide gives optimism and claims that
This is a call for empiricism (aka testing) and ad-hoc heuristics exactly because the problem is not solvable in general using formal methods.
> Proving that a program terminates is not that much interesting. Lack of security vulnerabilities would be much better.
My bad, I dare make the stronger claim that most algorithms that you see in an undergrad algorithms textbook are useful and mathematically known to be correct.
> But it does not tell us anything about real programs?
I agree that most software today are extremely complicated. Most software today don't even have a proper target specification all in one place, which is kind of a prerequisite for being proven to adhere to a specification. Furthermore, most software today is so complex that attempts at a rigorous specification is likely to have bugs at the level of stating the property itself. Not to mention completely missing properties that one is unaware of that are relevant to attacks that one is unaware of.
But core parts of real software is composed of those undergrad algorithms that are proven to be correct. You can create useful libraries of useful algorithms that have guarantees, and small programs that have guarantees. For this reason I disagree that the class of useful programs is as small as you think.
> We don't compose software by concatenating their state machines.
Structured programming without loops can be modeled as concatenation of turing machines (branching composes different machines to the accept and reject states); and it is trivial that it terminates once the component machines terminate.
When you introduce a loop that is when you need to identify a nontrivial property that guarantees that the loop terminates, and this is done work for many useful algorithms.
They are reusable to some degree when the proofs are made with type systems, via Curry-Howard.
ISBN is 3423300175.
I really appreciate your comment. That book has been sitting behind me on my bookshelf for years blending into background. I just pulled it off the shelf.
I just graduated a few weeks ago after working on my BS for 10 years. The fact that you brought this book up, the piece that inspired me to go back to school in the first place… is something Hofstadter would probably refer as my minds I recursive loop of existence. Something of that sentiment at least
Good point. Also, discovering exploits is also equivalent to the halting problem. So both things are impossible in the general case.
The real world consequences of this problem are something we have become desensitized to. I didn’t quite understand the impact of the halting problem until I started working in security, specifically for a company that made a SAST product and I had to support the scanner for companies across the globe. There will always be a 0-day market because of Halting problem.
If you think down the road 20 years. Virtually everything we touch will have internet. It will all depend on a program checking a program. Since no computer can guarantee its correctness on its own. Exploits will always be able to chained, and everything will always be exploitable. Including AI systems.
A book I read had a quote that said if you want to make a product that will generate infinite profit, create a static analysis scanner.
I’m not a mathematician but the Halting problem always reminds me of the Godels incompleteness theorem in a way.
I think these are the greatest gifts humanity has ever discovered.
It means there is always hope for humanity as long as oppression depends on technology, because the technology will always be flawed.
There is always a undiscovered theorem that has to potential to change everything we know.