RE: Theoretical question about vulnerabilities

["David Crocker" <dcrocker () eschertech com>]

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