Mozilla: Improving Security for Bugzilla is the wrong angle

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

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?