Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 15, 2015 11:16 UTC (Tue) by anselm (subscriber, #2796)
In reply to: Mozilla: Improving Security for Bugzilla is the wrong angle by ibukanov
Parent article: Mozilla: Improving Security for Bugzilla

Of course the presumption there is that your formal specifications are bug-free. A verified implementation of a buggy specification isn't much better than a buggy implementation as far as the end result is concerned.

C, for example, is probably still simple enough to lend itself to that sort of thing (although notably the authors of this compiler had to make do with a subset of the language). With something like TeX, things might look a bit different. Interactive programs, which are less easily described in terms of translating a well-specified language X into another well-specified language Y, are probably even more difficult.

Or, as Donald E. Knuth said, “Beware of bugs in the above code – I didn't try it, I only proved it correct” (as the author of TeX, he probably knows what he's talking about).

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 15, 2015 11:52 UTC (Tue) by ibukanov (subscriber, #3942) [Link] (2 responses)

> Of course the presumption there is that your formal specifications are bug-free.

One does not need a detailed and inevitably complex formal specification to have a useful statement about the program. For example, proving that a C program does not have undefined behavior or that a user input is always properly escaped would be immediately useful even if that does not prevent bugs that could lead to denial-of-service. That is, the goal should not be to specify the detailed behavior, but rather the bounds of acceptable errors and then prove those bounds.

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 16, 2015 6:10 UTC (Wed) by jezuch (subscriber, #52988) [Link] (1 responses)

On the other hand, sufficiently detailed specification is indistinguishable from a program. So if writing programs is hard, why should writing sufficiently detailed specifications be any easier?

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 16, 2015 6:14 UTC (Wed) by Cyberax (✭ supporter ✭, #52523) [Link]

It's fairly easy to come up with useful invariants in a spec, that might be difficult to uphold.

For example, for a train controller system, it's easy to come with an invariant "no trains on the same railway section" and even more elaborate like "a train must not approach a busy section with a speed more than 15 km/h".