The Reliable Program

Many are tempted to say that no program is reliably resistant to corrupt input. Some do. I do not. I seek a line to draw between these categories. I do not seek a decision procedure; I am sure that is impossible. Perhaps most will agree that a program to compute and print the SHA-1 of a file will not be corrupted by any file. A proof would typically include the lemma that the sequence of executed instructions in the program depends only on the length of the file. There may be 40 conditional branches each to decide whether a hex digit of the hash is greater than 10. These cases amount to 2⁴⁰ cases that can be tested exhaustively if necessary. The point is that it is possible to write correct programs for some non trivial computing tasks. Indeed I suspect that this particular program has been correctly written many times. I suspect that the Fast Fourier Transform has been correctly programmed many times as well.

An invulnerable browser, on the other hand, is probably beyond the state of the art.

Here is an opinion that I cannot support. I think that programs should talk to programs in their native language which is binary. ASN.1 was a flawed attempt to define a language to define binary interfaces. I think that some such world of binary interfaces would mostly solve injection vulnerabilities. This is terribly vague. Fixing ASN.1 is not an easy job.