Skip to main content
Information Security

Return to Answer

added 967 characters in body
Source Link
Tom Leek
Tom Leek
  • 173.8k
  • 29
  • 352
  • 483

  • The "halting problem" is about deciding whether a computer program will stop, for a given input which is known a priori. This model works only about programs which are pure calculation, and do no I/O. By definition, this does not apply to any application which is connected to the Internet or can be controlled by a human. As an illustration, consider an application which runs a video. This one will never stop as long as the human user clicks on the rewind button. But it may stop (and it should be easy to prove) if the user does not click on any button.

  • Decidability is about whether a given function can be evaluated at all, but not whether it can be evaluated efficiently. If you want an antivirus to scan for malware, you want the answer within 2 or 3 seconds -- not in ten years. This notion of decidability does not capture all the things in which we are interested.

  • We can have requirements. Consider a Java application. It is written in bytecode which is amenable to (efficient) automatic proofs. Namely, the JVM will prove, in a very formal way, that the code complies to the type rules of Java (that it never calls a method on a class which does not feature that method). It is not possible to make such a proof generically, on every possible sequence of bytecode instructions; but valid Java code is bytecode which can be proven in such a way. This means that it is possible in practice to enforce requirements of "proofability" for existing code. In a "halting problem" point of view, this would be like stating that programs for which the halting behaviour cannot be determined absolutely (and quickly) will be unceremoniously prevented from execution.

  • We are not interested in whether a program will halt, but whether a program will do evil things. I am all for a computer to alter my bank account... as long as that is what I want. The difference between me, the human/ursine user, managing my money through the bank's Web site, and a malware, siphoning my precious gold through the bank's Web site, is not something which exists in the world of computers. There is no notion of Evil in computers. If I want security, I must first define with all the needed precision what exactly I want to allow computers to do, and what I don't want. Before asking myself whether a computer program will be able to automatically decide if my core security properties will be respected by a given piece of code, I must first define these properties, and that initial part of the work is far from being done. Making computers guess what is Good is an old problem which seems hard.

For these three reasons, I claim that invoking the "halting problem" is a poor excuse. It does highlight the fact that we are dealing with issues which require a bit more thinking than writing yet another PHP Web site. But it does not imply that security is not possible, only that Science will not come up with a magical tool which will solve it effortlessly (because this Blessed +3 Hammer of Decidability would also solve the halting problem, which is not mathematically possible).

  • The "halting problem" is about deciding whether a computer program will stop, for a given input which is known a priori. This model works only about programs which are pure calculation, and do no I/O. By definition, this does not apply to any application which is connected to the Internet or can be controlled by a human. As an illustration, consider an application which runs a video. This one will never stop as long as the human user clicks on the rewind button. But it may stop (and it should be easy to prove) if the user does not click on any button.

  • Decidability is about whether a given function can be evaluated at all, but not whether it can be evaluated efficiently. If you want an antivirus to scan for malware, you want the answer within 2 or 3 seconds -- not in ten years. This notion of decidability does not capture all the things in which we are interested.

  • We can have requirements. Consider a Java application. It is written in bytecode which is amenable to (efficient) automatic proofs. Namely, the JVM will prove, in a very formal way, that the code complies to the type rules of Java (that it never calls a method on a class which does not feature that method). It is not possible to make such a proof generically, on every possible sequence of bytecode instructions; but valid Java code is bytecode which can be proven in such a way. This means that it is possible in practice to enforce requirements of "proofability" for existing code. In a "halting problem" point of view, this would be like stating that programs for which the halting behaviour cannot be determined absolutely (and quickly) will be unceremoniously prevented from execution.

For these three reasons, I claim that invoking the "halting problem" is a poor excuse. It does highlight the fact that we are dealing with issues which require a bit more thinking than writing yet another PHP Web site. But it does not imply that security is not possible, only that Science will not come up with a magical tool which will solve it effortlessly (because this Blessed +3 Hammer of Decidability would also solve the halting problem, which is not mathematically possible).

  • The "halting problem" is about deciding whether a computer program will stop, for a given input which is known a priori. This model works only about programs which are pure calculation, and do no I/O. By definition, this does not apply to any application which is connected to the Internet or can be controlled by a human. As an illustration, consider an application which runs a video. This one will never stop as long as the human user clicks on the rewind button. But it may stop (and it should be easy to prove) if the user does not click on any button.

  • Decidability is about whether a given function can be evaluated at all, but not whether it can be evaluated efficiently. If you want an antivirus to scan for malware, you want the answer within 2 or 3 seconds -- not in ten years. This notion of decidability does not capture all the things in which we are interested.

  • We can have requirements. Consider a Java application. It is written in bytecode which is amenable to (efficient) automatic proofs. Namely, the JVM will prove, in a very formal way, that the code complies to the type rules of Java (that it never calls a method on a class which does not feature that method). It is not possible to make such a proof generically, on every possible sequence of bytecode instructions; but valid Java code is bytecode which can be proven in such a way. This means that it is possible in practice to enforce requirements of "proofability" for existing code. In a "halting problem" point of view, this would be like stating that programs for which the halting behaviour cannot be determined absolutely (and quickly) will be unceremoniously prevented from execution.

  • We are not interested in whether a program will halt, but whether a program will do evil things. I am all for a computer to alter my bank account... as long as that is what I want. The difference between me, the human/ursine user, managing my money through the bank's Web site, and a malware, siphoning my precious gold through the bank's Web site, is not something which exists in the world of computers. There is no notion of Evil in computers. If I want security, I must first define with all the needed precision what exactly I want to allow computers to do, and what I don't want. Before asking myself whether a computer program will be able to automatically decide if my core security properties will be respected by a given piece of code, I must first define these properties, and that initial part of the work is far from being done. Making computers guess what is Good is an old problem which seems hard.

For these reasons, I claim that invoking the "halting problem" is a poor excuse. It does highlight the fact that we are dealing with issues which require a bit more thinking than writing yet another PHP Web site. But it does not imply that security is not possible, only that Science will not come up with a magical tool which will solve it effortlessly (because this Blessed +3 Hammer of Decidability would also solve the halting problem, which is not mathematically possible).

Source Link
Tom Leek
Tom Leek
  • 173.8k
  • 29
  • 352
  • 483

Established expert... that would be me (although not under this name -- I use a pseudonym because I am tremendously humble). Allow me to answer, then.

The "halting problem" is indeed an illustration of the impossibility to decide (for a computer) whether a given program will halt or not. Of course, a lot of programs are decidable, but not all of them. People tend to think that if we could accurately "predict the behaviour" of computer programs, then malware would not be possible. This is oversimplistic, for the following reasons:

  • The "halting problem" is about deciding whether a computer program will stop, for a given input which is known a priori. This model works only about programs which are pure calculation, and do no I/O. By definition, this does not apply to any application which is connected to the Internet or can be controlled by a human. As an illustration, consider an application which runs a video. This one will never stop as long as the human user clicks on the rewind button. But it may stop (and it should be easy to prove) if the user does not click on any button.

  • Decidability is about whether a given function can be evaluated at all, but not whether it can be evaluated efficiently. If you want an antivirus to scan for malware, you want the answer within 2 or 3 seconds -- not in ten years. This notion of decidability does not capture all the things in which we are interested.

  • We can have requirements. Consider a Java application. It is written in bytecode which is amenable to (efficient) automatic proofs. Namely, the JVM will prove, in a very formal way, that the code complies to the type rules of Java (that it never calls a method on a class which does not feature that method). It is not possible to make such a proof generically, on every possible sequence of bytecode instructions; but valid Java code is bytecode which can be proven in such a way. This means that it is possible in practice to enforce requirements of "proofability" for existing code. In a "halting problem" point of view, this would be like stating that programs for which the halting behaviour cannot be determined absolutely (and quickly) will be unceremoniously prevented from execution.

For these three reasons, I claim that invoking the "halting problem" is a poor excuse. It does highlight the fact that we are dealing with issues which require a bit more thinking than writing yet another PHP Web site. But it does not imply that security is not possible, only that Science will not come up with a magical tool which will solve it effortlessly (because this Blessed +3 Hammer of Decidability would also solve the halting problem, which is not mathematically possible).