RE: Strategies for teaching secure coding practices

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

Crispin Cowan wrote:

> >
Agreed, you can do that too. The limitation of the "proof" method is
that it leads to brittle code: if a developer changes something over
here, it may invalidate a lemma that some code over there was counting
on. As David says, the cost of the "check everything" method is, well,
the cost :)
<<

If you change something, then of course you need to ensure that the system can
still be fully proven. In practice, most changes only impact on a small part of
the system, which can be determined by change impact analysis. However, our
approach is to re-run the verifier. This is practical because a very high degree
of automatic proof is possible these days (we and our customers are getting
better than 98-99% automatic proof for small and medium projects, 96% for a
large one).

> >
You can use a hybrid method, where you use proof for parameters that are
"internal" to a "module" and error checking for "inter-module"
parameters. By scaling up or down what you consider to be a "module" you
can trade trade cost against safety to your taste.
<<

Provided that every entry point to a module is properly specified, the proof
task also becomes modular. This is because when one module calls another, the
proofs for the client module need only take account of the other module's
specifications, not its internal detail. So cost does not necessarily increase
with "module" size, provided that each "module" is itself broken into smaller
pieces (e.g. classes).

But I can see the benefits of your hybrid approach if, say, some modules were
proven 100% by the automatic prover, but others were not and it was deemed not
cost-effective to help the prover with the last few proofs.

David Crocker
Escher Technologies Ltd.
www.eschertech.com
Tel. +44(0)1252 336565  Fax +44(0)1252 320954