3 ms·
You've over-egged the pudding here: neither Gödel's incompleteness theorem, nor Rice's Theorem, guarantee that an algorithm in a certain complexity class will h
by samatman 2y ago
You've over-egged the pudding here: neither Gödel's incompleteness theorem, nor Rice's Theorem, guarantee that an algorithm in a certain complexity class will have exploitable defect. Rice's Theorem in particular suggests that it's unlikely one will be able to statically prove that such an algorithm has the properties it's designed to have. That should be enough to make anyone nervous.
I hope readers will be able to look past this one sentence in your post and take a good hard look at the rest of it, which is quite important.
- nextos 2y agoRice's Theorem, as all Free Lunch Theorems, is too pessimistic. In real conditions, static analysis and theorem proving can verify lots of safety properties. See e.g. Astrée & Airbus, or F* and Project Everest. IMHO, the solution is to use static analysis in conjunction with DSLs that have restricted semantics to make static analysis and hand-written proofs easy.
- samatman 2y agoIt doesn't appear that we're disagreeing. You're referring to verifying 'lots' of safety properties, I referred to verifying that an algorithm does everything it's supposed to. These are not the same thing in the general case. My actual point was that generic incompleteness and undecidability theorems do not guarantee that any given program must be defective. The thrust of langsec is in fact to parse all inputs at the boundaries, using algorithms with known properties, that is, ones where it's feasible to prove that they'll halt, won't overrun buffers, and so on.