That is completely not what Godel’s incompleteness theorem says. It may say that there are programs which are secure but not provably secure, but I don’t care at all about that, because programs humans use are designed in a principled way and are not in fact designed to have their security be undecidable.
The difficulty of engineering more complex software which is provably secure increases quite rapidly, but no fundamentally new difficulties arise. In fact, the filters I describe in this article are quite simple for some problems; the one necessary for the proof of the Riemann hypothesis in fact already exists in a provably secure implementation.
There is no such thing as provably secure software, and you should know that if you know anything about software security. The best you can actually do is prove that some particular exploit won’t work on your code, but there are always new classes of exploits out there waiting to be discovered. The space of possible inputs for any interesting program is far too large to explore, or even catalogue.
I think it is safe to say without further justification that you are wrong.
The same argument shows that I can never rule out the possibility that x^5 + y^5 = z^5 for naturals x,y,z, because the space of numbers is just too large. At best you can prove that some particular approach for finding solutions won’t work.
If by interesting program you mean, programs whose behavior shows no simple behavior which can be exploited by a human-understandable proof, then maybe your statement is tautologically true. But in that case, we definitely don’t need an interesting filter. We need a simple filter, whose behavior can be verified by a human proof.
If you are referring to the fact that we can never prove that our proof system is secure, then I guess I agree. However, I strongly, strongly believe that PA is consistent, and I am OK risking the universe on that assertion.
That is completely not what Godel’s incompleteness theorem says. It may say that there are programs which are secure but not provably secure, but I don’t care at all about that, because programs humans use are designed in a principled way and are not in fact designed to have their security be undecidable.
The difficulty of engineering more complex software which is provably secure increases quite rapidly, but no fundamentally new difficulties arise. In fact, the filters I describe in this article are quite simple for some problems; the one necessary for the proof of the Riemann hypothesis in fact already exists in a provably secure implementation.
There is no such thing as provably secure software, and you should know that if you know anything about software security. The best you can actually do is prove that some particular exploit won’t work on your code, but there are always new classes of exploits out there waiting to be discovered. The space of possible inputs for any interesting program is far too large to explore, or even catalogue.
I think it is safe to say without further justification that you are wrong.
The same argument shows that I can never rule out the possibility that x^5 + y^5 = z^5 for naturals x,y,z, because the space of numbers is just too large. At best you can prove that some particular approach for finding solutions won’t work.
If by interesting program you mean, programs whose behavior shows no simple behavior which can be exploited by a human-understandable proof, then maybe your statement is tautologically true. But in that case, we definitely don’t need an interesting filter. We need a simple filter, whose behavior can be verified by a human proof.
If you are referring to the fact that we can never prove that our proof system is secure, then I guess I agree. However, I strongly, strongly believe that PA is consistent, and I am OK risking the universe on that assertion.