der Mouse wrote: >> Then either (a) there exist programs which never access out-of-bounds but which the checker incorrectly flags as doing so, or (b) there exist programs for which the checker never terminates (quite possibly both). (This is simply the Halting Theorem rephrased.) <<
It is of course possible to construct programs which can never access out-of-bounds elements but for which the prover is unable to prove that property. In such a case, if you can construct a reasonable argument as to why the program never accesses out-of-bounds elements, you can express the main points of that argument in the form of extra assertions that guide the prover towards a proof. If you can't construct such an argument, then the code needs to be redesigned anyway. >> 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? >> Ultimately, this amounts to a VHLL, except that you're calling it a "specification" rather than "code" - and that rather than "compiling" the "code" with a program, you're using (falliable) humans, with a program (the "prover") checking that the "compiler" output is correct. 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, once you know that a particular security property matters, it is much easier to express that as a part of the specification than it is to write code and be sure that it obeys the security property for all possible inputs. You are also much more likely to make an error writing the code than writing the specification, simply because the specification is so much shorter. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
