3 ms·

I love this. I’m in appsec and bring up the halting problem all the time to developers to get them to think about the security landscape. The halting problem is

I love this. I’m in appsec and bring up the halting problem all the time to developers to get them to think about the security landscape. The halting problem is why security is a unsolvable problem at its core. 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.

MikeBattaglia 3y ago
> Exploits will always be able to chained, and everything will always be exploitable. Including AI systems. Good point. Also, discovering exploits is also equivalent to the halting problem. So both things are impossible in the general case.
poorlyknit 3y ago
If you haven't already, read "Gödel, Escher, Bach". It sounds like you would enjoy it. For me its more of a "pick it up somewhere in the middle and get inspired" than "front-to-back" title but iirc it considers the halting problem and the incompleteness theorem to be two sides of the same coin. ISBN is 3423300175.
- s4mw1se 3y ago
  Funny you recommended this book. It what inspired me to go back to school and enroll in compsci. I forgot that’s where this seed was planted. I think it’s safe to say it really resonated with me lol. 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
like_any_other 3y ago
I think you misunderstand the halting problem. An algorithm that can prove any program halts or doesn't is impossible. But it's possible to prove it for some programs. 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_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
- s4mw1se 3y ago
  I hope to see the day when this makes up the majority of kernels.
- mkleczek 3y ago
  1. Unfortunately the set of "some" programs is unknown and most probably really small. 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 https://pron.github.io/posts/correctness-and-complexity for more details.
  - jhanschoo 3y ago
    I don't think your reply is particularly effective when you are replying to a comment that exhibits a formally verified microkernel. > 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.

MikeBattaglia 3y ago

> Exploits will always be able to chained, and everything will always be exploitable. Including AI systems. Good point. Also, discovering exploits is also equivalent to the halting problem. So both things are impossible in the general case.

poorlyknit 3y ago

If you haven't already, read "Gödel, Escher, Bach". It sounds like you would enjoy it. For me its more of a "pick it up somewhere in the middle and get inspired" than "front-to-back" title but iirc it considers the halting problem and the incompleteness theorem to be two sides of the same coin. ISBN is 3423300175.

s4mw1se 3y ago
Funny you recommended this book. It what inspired me to go back to school and enroll in compsci. I forgot that’s where this seed was planted. I think it’s safe to say it really resonated with me lol. 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

like_any_other 3y ago

I think you misunderstand the halting problem. An algorithm that can prove any program halts or doesn't is impossible. But it's possible to prove it for some programs. 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_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...

s4mw1se 3y ago
I hope to see the day when this makes up the majority of kernels.
mkleczek 3y ago
1. Unfortunately the set of "some" programs is unknown and most probably really small. 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 https://pron.github.io/posts/correctness-and-complexity for more details.
- jhanschoo 3y ago
  I don't think your reply is particularly effective when you are replying to a comment that exhibits a formally verified microkernel. > 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.