On Mon, Sep 7, 2015 at 12:30 PM, Georgi Guninski <guninski@guninski.com> wrote: ...
btw, doesn't your post contradict another post of yours here: https://cpunks.org/pipermail/cypherpunks/2015-September/009032.html
It doesn't, as long as we don't confuse what is desirable -- and indeed it is so -- with the practically and systematically attainable. Or, to paraphrase Danny Strong, idealism loses to pragmatism when it comes to engineering security. I'm not even persuaded that writing a formal specifications gives us always the ability to check the equivalence of implementations. As a negative case in point, take languages/protocols and their parsers. A grammar can be understood as a specification. Still, "arithmetically checking the computational equivalence of parsers [...] is decidable up to a level of computational power required to parse the language, and becomes undecidable thereafter". [1] All of which is to say that checking the computational equivalence of parsers is still possible. But, as designers, in order to reconcile the desirable with the practically attainable, we need to stick to the simplest possible input languages (i.e., regular and context-free). This is the kind of security trade-offs I was alluding to. And this also links us to the other thread on browser security, exploits, and Firefox. -- Alfonso [1] http://langsec.org/papers/Bratus.pdf