Thou shalt have no other gods before the ANSI C standard 1562

with kind report very surprising,

Correct.

AFAICT the most effective approach has been to do the following:

* Formal proofs (ie: that maths stuff that hackers don't like). * Design Review. * Code Review. * Testing. * Reconciliation between the test results and proofs.

In addition you can take the OpenBSD approach which is to audit the code written, in other words you do Code Review. I find it highly amusing that people who slag off code-review frequently praise OpenBSD's audit and the Open Source "many eyes make bugs shallow" philosophy... :)

The other aspect that those wild eyed loons tend to overlook is that security is only as good as the weakest link. That means you really do have to go through the *entire* system from top to bottom, cherry picking the bits you are interested in is NOT good enough. It's also the case that you have to consider the interaction between all the components of the system.

As with most bug squishing : the earlier you find the bug the cheaper it is to fix. That is the main reason why I advocate the use of formal methods for this kind of work, writing it and then auditing it afterwards will leave you wide open to mis- features creeping in by design (which are very expensive to fix).

Cheers, Rupert