[Cryptography] Security proofs prove non-failproof

[James A. Donald]

On 2/22/2017 1:03 AM, Perry E. Metzger wrote:
> We can prove that code has no buffer
> overflows, integer overflows, stack overflows, etc., and those proofs
> mean something.

That would be handy.  Are you telling me that there is a system that can 
digest a suitably prepared C++ program and tell me it cannot have a 
buffer overflow, memory leak, signed integer overflow etc, and complain 
to me if there is potential for these things?

Obviously there is no mechanical or automated method that can tell 
whether or not an arbitrary program can develop such errors.

Visual Studio comes with a bunch of built in analysis tools that I have 
so far not found terribly useful or informative.  They tend to tell me 
the glaringly obvious or nothing at all.

What I have found useful is making sure a program does not in fact 
develop memory leaks when actually run.  Profiling is also handy when 
one wants to optimize a program.  But these are ancient tools.