2 ms·
Detecting 100% of buffer overflows with 0% false alarms, would require solving the Halting Problem. For applications that demand both maximum speed as well as
by xamuel 9y ago
Detecting 100% of buffer overflows with 0% false alarms, would require solving the Halting Problem.
For applications that demand both maximum speed as well as maximum security, the best solution is probably something like a C compiler that requires the code to be accompanied by formal proofs of defined behavior. Even this will necessarily sacrifice speed in a theoretical sense, because there are certain problems for which the fastest solution is safe but can't be proven safe within (PA/ZF/ZFC/insert any consistent foundation of mathematics you like).
Eventually we'll have people writing fast programs and proving their soundness using large cardinal axioms which might or might not actually be true. Then someday one of those large cardinal axioms will turn out to be inconsistent [1] and suddenly some "proven" code will be proven no more.
[1] https://en.wikipedia.org/wiki/Kunen%27s_inconsistency_theorem https://en.wikipedia.org/wiki/Kunen%27s_inconsistency_theore...
- andrewflnr 9y agoWhy would you need large cardinal axioms to prove a program correct?
- xamuel 9y agoI used large cardinal axioms as [the canonical] example of any axiom stronger than standard mathematical foundations. A contrived example: there are certain large cardinal axioms that imply the consistency of ZFC. Thus ZFC cannot prove those axioms unless ZFC is inconsistent (Godel's incompleteness theorem). Consider the following problem: "If ZFC can prove 1=0 in n steps, output 1. Else, output 0." A naive solution would brute-force search all ZFC-proofs of length n. A faster solution would be: "Ignore n and immediately output 0." This is correct, because ZFC never proves 1=0. You could formally verify the correctness by using certain large cardinal axioms, but not using raw ZFC.