5 ms·

Am I wrong to conclude that the statement by Google's VP of Security Engineering that "we simply must eliminate every software vulnerability on Earth" (before A

by dloss 2mo ago

Am I wrong to conclude that the statement by Google's VP of Security Engineering that "we simply must eliminate every software vulnerability on Earth" (before AI Agents find them) is not only stunningly ambitious, but doomed from the start? https://youtu.be/B_7RpP90rUk https://youtu.be/B_7RpP90rUk (at 3:00)

wduquette 2mo ago
Kurt Godel says that you are correct.
- drdeca 2mo ago
  Eh? I don’t see how Gödel’s results imply that.
  - wduquette 2mo ago
    At least not automatically. From an algorithmic standpoint it seems likely to be undecidable. But let us not look too closely at what was really a throwaway remark.
    - drdeca 2mo ago
      It is true of course that there is no automatic procedure which takes in an arbitrary program and decides if it has a desired input/output behavior. (Whether an input program has a given “semantic property” is undecidable.) But that doesn’t mean that it is impossible to have all our programs be formally verified. For that, if we have a formal specification for what each should do… Well, I suppose it’s possible that some program we would want is possible to implement with the desired properties, but not possible to prove that it has those properties? It is possible to enumerate (program, proof) pairs though.
- taneq 2mo ago
  As in, there is no programming language complex enough to describe any program, that is not inherently complex enough to describe bugs? Sounds legit, how would one prove it? :)
kridsdale1 2mo ago
Shhhhh! It may be the only way to keep us all employed.
WorldMaker 2mo ago
It's my view of the Halting Problem that we've known for a surprisingly long time that eliminating all software bugs is mathematically impossible and should stop letting perfect get in the way of the good. Especially with the more recent relative of the Halting Problem combined with the Church-Turing Theorem that found mathematical proof of a "0-day" sandbox escape in the Universal Turing Machine itself. We have always lived in a house of glass. LLM agents automating trebuchets for rock throwing certainly seems like a bad idea to me and "let's simply eliminate all software vulnerabilities" an interesting bit of ostrich work (stick your head in the sand and hope it all gets better).
- layer8 2mo ago
  This has little to do with the halting problem, because we can choose to not deploy programs (or subroutines) that we want to be terminating but can’t prove that they are terminating. And that goes for any undecidable problem. There is no application where we want the program to have a certain property where we would be forced to deploy a program where we can’t prove the property due to computational theory reasons. No, the real issue is that for the most we don’t want to put the necessary effort into proving the relevant properties, because it’s costly and time-consuming, and we think we can live with the risk. The issue is not some theoretical inability to do so.
  - WorldMaker 2mo ago
    We absolutely have pragmatic compromises and shortcuts for dealing with termination problems, but that doesn't mean we've solved the Halting Problem, it means we've adapted to coexistence with it. (And maybe we've coexisted with the Problem for long enough it feels like most of those adaptations are sufficient day to day, which makes it all the harder to appreciate the bugs that are always there we just mitigate enough to worry about them less.) Potentially Infinite Loops are a great power. We've learned in most programming languages the "Uncle Ben lesson" that with such great power, comes great responsibility. In most programming languages we don't want to remove the ability to infinitely loop, because we might need that power, we work on ways to limit that responsibility (loop guards and timeouts and cancellations and teardowns). But it will likely always be possible to see some code spin in a loop we can't tell is accidentally infinite or just a loop with a lot more work than we expected. The infinite spin wait will always be a risk in our code. I think it has a lot to do with the Halting Problem.

by dloss 2mo ago

wduquette 2mo ago

Kurt Godel says that you are correct.

drdeca 2mo ago
Eh? I don’t see how Gödel’s results imply that.
- wduquette 2mo ago
  At least not automatically. From an algorithmic standpoint it seems likely to be undecidable. But let us not look too closely at what was really a throwaway remark.
  - drdeca 2mo ago
    It is true of course that there is no automatic procedure which takes in an arbitrary program and decides if it has a desired input/output behavior. (Whether an input program has a given “semantic property” is undecidable.) But that doesn’t mean that it is impossible to have all our programs be formally verified. For that, if we have a formal specification for what each should do… Well, I suppose it’s possible that some program we would want is possible to implement with the desired properties, but not possible to prove that it has those properties? It is possible to enumerate (program, proof) pairs though.
taneq 2mo ago
As in, there is no programming language complex enough to describe any program, that is not inherently complex enough to describe bugs? Sounds legit, how would one prove it? :)

kridsdale1 2mo ago

Shhhhh! It may be the only way to keep us all employed.

WorldMaker 2mo ago

It's my view of the Halting Problem that we've known for a surprisingly long time that eliminating all software bugs is mathematically impossible and should stop letting perfect get in the way of the good. Especially with the more recent relative of the Halting Problem combined with the Church-Turing Theorem that found mathematical proof of a "0-day" sandbox escape in the Universal Turing Machine itself. We have always lived in a house of glass. LLM agents automating trebuchets for rock throwing certainly seems like a bad idea to me and "let's simply eliminate all software vulnerabilities" an interesting bit of ostrich work (stick your head in the sand and hope it all gets better).

layer8 2mo ago
This has little to do with the halting problem, because we can choose to not deploy programs (or subroutines) that we want to be terminating but can’t prove that they are terminating. And that goes for any undecidable problem. There is no application where we want the program to have a certain property where we would be forced to deploy a program where we can’t prove the property due to computational theory reasons. No, the real issue is that for the most we don’t want to put the necessary effort into proving the relevant properties, because it’s costly and time-consuming, and we think we can live with the risk. The issue is not some theoretical inability to do so.
- WorldMaker 2mo ago
  We absolutely have pragmatic compromises and shortcuts for dealing with termination problems, but that doesn't mean we've solved the Halting Problem, it means we've adapted to coexistence with it. (And maybe we've coexisted with the Problem for long enough it feels like most of those adaptations are sufficient day to day, which makes it all the harder to appreciate the bugs that are always there we just mitigate enough to worry about them less.) Potentially Infinite Loops are a great power. We've learned in most programming languages the "Uncle Ben lesson" that with such great power, comes great responsibility. In most programming languages we don't want to remove the ability to infinitely loop, because we might need that power, we work on ways to limit that responsibility (loop guards and timeouts and cancellations and teardowns). But it will likely always be possible to see some code spin in a loop we can't tell is accidentally infinite or just a loop with a lot more work than we expected. The infinite spin wait will always be a risk in our code. I think it has a lot to do with the Halting Problem.