Secure Coding mailing list archives
Re: Theoretical question about vulnerabilities
From: der Mouse <mouse () Rodents Montreal QC CA>
Date: Wed, 13 Apr 2005 06:31:20 +0100
Or until you find a bug in your automated prover. Or, worse, discover that a vulnerability exists despite your proof, meaning that you either missed a loophole in your spec or your prover has a bug, and you don't have the slightest idea which.On that basis, can I presume that you believe all programming should be done in machine code, in case the compiler/assembler/linker you might be tempted to use has a bug?
You can presume anything you like. But in this case you'd be wrong. I was/am not arguing that such tools should not be used (for this or any other reason). My point is merely that calling what they do "proof" is misleading to the point where I'd call it outright wrong. You have roughly the same level of assurance that code passed by such a checker is correct that you do that machine/assembly code output by a traditional compiler is correct: good enough for most purposes, but by no stretch of the imagination is it even as close to proof as most mathematics "proofs" are - and, like them, it ultimately rests on "smart people think it's OK".
Ultimately, this amounts to a VHLL, except that [...nomenclature...]. And, as with any language, whoever writes this VHLL can write bugs.Like I said, you can still fail to include important security properties in the specification. However, [...].
Basically, the same arguments usually made for any higher-level langauge versus a corresponding lower-level language: machine versus assembly, assembly versus C, C versus Lisp, etc. And I daresay that it provides at least vaguely the same advantages and disadvantages as for most of the higher/lower level comparisons, too. But it is hardly the panacea that "proving the program correct" makes it sound like. As someone (who? I forget) is said to have said, "Beware, I have only proven this program correct, not tested it". /~\ The ASCII der Mouse \ / Ribbon Campaign X Against HTML [EMAIL PROTECTED] / \ Email! 7D C8 61 52 5D E7 2D 39 4E F1 31 3E E8 B3 27 4B
Current thread:
- Theoretical question about vulnerabilities Pascal Meunier (Apr 10)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 10)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 11)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 12)
- Re: Theoretical question about vulnerabilities der Mouse (Apr 12)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 12)
- Re: Theoretical question about vulnerabilities der Mouse (Apr 12)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 13)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 13)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 14)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 15)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 17)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 12)
- <Possible follow-ups>
- RE: Theoretical question about vulnerabilities Peter Amey (Apr 12)
- Re: Theoretical question about vulnerabilities karger (Apr 12)
- RE: Theoretical question about vulnerabilities Peter Amey (Apr 13)