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