Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 8, 2015 5:02 UTC (Tue) by xophos (subscriber, #75267)
In reply to: Mozilla: Improving Security for Bugzilla is the wrong angle by Wol
Parent article: Mozilla: Improving Security for Bugzilla

I am a software developer, i know that there is no non-trivial program without bugs.
But it seems that the whole industry has their priorities backwards.
I know it makes economic sense: Users see new features, but they don't notice, when their computers are not owned by some stealthy malware.
Firefox crashes. It does this at least twice a week for me without using flash or other horrible plugins.
It does it even on android, where there are none of those.
I know that not all crashes are exploitable bugs, but they are more often than not.
Firefox doesn't need any more features. It doesen't need a new look. Heck it doesn't even need to go any faster.
The only thing that could make it better would be less bugs.
And when there are as few bugs in firefox as possible, as many unittests as possible, as much static checking of invariants as possible.
Then maybe html 6 or the next generation of ecmascript is out, and Feature development is needed for a short while.

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 8, 2015 8:06 UTC (Tue) by ovitters (guest, #27950) [Link]

Are you a sole software developer? In a big team, you don't focus on one thing at a time. Mozilla has loads of people working for them. Like any big company, all those people focus on different things. Simplistic example, try having every single person in a company solely focus on sales. It doesn't work!

PS: No need to press enter all the time. Paragraphs are cool! :-P

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 8, 2015 17:05 UTC (Tue) by zlynx (guest, #2285) [Link]

Removing a bunch of bugs from code is the entire idea with Rust. So Mozilla IS doing something about it. Hopefully Rust will be able to help reason about the code and prove things are right. As well as being fast and memory efficient.

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 14, 2015 19:52 UTC (Mon) by ballombe (subscriber, #9523) [Link] (11 responses)

> I am a software developer, i know that there is no non-trivial program without bugs.

There are complex software with almost no bugs: TeX, IJG libjpeg, qmail
but there is little interest in bug-free software.

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 14, 2015 23:20 UTC (Mon) by anselm (subscriber, #2796) [Link] (10 responses)

The problem is that these programs weren't cleverly developed to be bug-free from the start – they started out just as buggy as all other programs, but were beaten on long enough for virtually all their bugs to be fixed (in the case of TeX, over 30 years by now). This approach is not very helpful if, like most people, you want to write your software and use (or sell) it right away.

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 15, 2015 10:39 UTC (Tue) by jezuch (subscriber, #52988) [Link] (9 responses)

> they started out just as buggy as all other programs, but were beaten on long enough for virtually all their bugs to be fixed (in the case of TeX, over 30 years by now).

...and no new features added. That's the only way to bug-free software: 30 years of bug fixing + no new functionality, ever :)

Mozilla: Improving Security for Bugzilla is the wrong angle

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

> That's the only way to bug-free software: 30 years of bug fixing

No, you can also use theorem provers. For example, there is already a bug free C compiler and a microkernel, http://compcert.inria.fr/compcert-C.html . The real problem is that perceived cost of using formal verification is considered way too high even for mission critical software. I wonder what kind of hacking attack it would take to change the balance cost.

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 15, 2015 11:16 UTC (Tue) by anselm (subscriber, #2796) [Link] (3 responses)

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".

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 15, 2015 15:49 UTC (Tue) by NAR (subscriber, #1313) [Link] (3 responses)

From the linked article:

"(transformation of C source text to CompCert C abstract syntax trees) is not formally verified"

So I think this is not a formally verified program that converts C source code into executable. Not surprisingly the hard part (handling user input) is missing. That's where most bugs are.

I remember CS class when I furiously tried to verify a practically "Hello World" level concurrent program and it took better part of the 90 minutes exam to achieve grade 2 (5 is best, 1 is failing). If I remember correctly, the avarage grade for the class on this particalar exam was below 2 - not because we were such lazy bastards who didn't study, but because it was hard and complicated. I knew the theory to pass the oral exam with grade 5, but computing the verification was really complicated even for a trivial task.

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 16, 2015 8:16 UTC (Wed) by cebewee (guest, #94775) [Link] (2 responses)

I would disagree that converting source code to ASTs is "the hard part". There isn't much interesting happening there in most languages.

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 18, 2015 22:36 UTC (Fri) by Wol (subscriber, #4433) [Link] (1 responses)

You've clearly never tried to write a lexer/parser.

Try and parse the following (legal!!!) statement in databasic

REM: REM = REM(10, 4); REM this calculates the remainder from dividing 10 by 4

That's a label, a variable, a function and a statement, all different, and all using the same identifier. (Incidentally, I don't know of a single compiler that correctly identifies all four - different implementations permit different syntaxes, but they are ALL valid.)

Now try providing a formal proof for a system that can cope with that ... :-)

Cheers,
Wol

Mozilla: Improving Security for Bugzilla is the wrong angle

Posted Sep 19, 2015 13:01 UTC (Sat) by cebewee (guest, #94775) [Link]

Why is this any harder to parse than "A: B = C(100); D foo"? I mean, it's somewhat unusual for modern languages to have variables, functions and statements in separate namespaces, but otherwise?