[Cryptography] Security proofs prove non-failproof

[Jerry Leichter]

>> C++ however can substantially automate memory management through
>> C++11 smart pointers.
> 
> Sure, but formal verification is much more extensive than that.
> 
> For example, say that you want to show not only that the scheduler in
> your operating system will not access past the end of an array,
> but also that it will faithfully schedule things....
I think you're missing the point here.  We started with the assertion the C++'s semantics was, at the moment, too complex/messy for formal analysis.  The response was "yes, but certain C++ features would make verification easier".  And that latter is true:  If you have a verified smart pointer implementation, then proving assertions about the lifetime of resources managed through smart pointers becomes very easy.  All kinds of intractable issues about pointer equivalence go away with smart pointers.  So C++ code written using that style should be more easily verifiable than traditional C code.

This is low-level stuff on which the operating system and everything else has to be built.  And ... since C++, despite the new features, still has all the old complicated stuff that makes verifiers choke, the fact that *some* C++ programs are now easier to verify doesn't help you write a verifier for *all* C++ programs.

Also, off on the side, even if you don't get to full verification, partial verification - human, machine, combined, formal or informal - of C++ code which uses the smart pointer style is also much easier.  It's necessarily "partial" - the fact that correct C++ semantics for such a pointer ensures that no code outside of this scope can access the value can't help if there's other code that casts pointers to long's and back and walks through all of memory.  (Or simply exceeds an array bound.) But we should take what we can get.
                                                        -- Jerry