[Cryptography] Security proofs prove non-failproof

[James A. Donald]

On 2/23/2017 12:33 AM, Perry E. Metzger wrote:
> Not C++ yet (because producing a formal semantics for C++ is a
> nightmare), but for C, you can use techniques like those that were
> used for programs like seL4 and CertiKOS, or packages like the
> Verified Software Toolchain (VST), and prove that a chunk of code has
> no such issues.
>
> Currently this involves quite a lot of work

C++ however can substantially automate memory management through C++11 
smart pointers.  In particular it has long supported the idiom 
Resource_Acquisition_is_Initialization, also perhaps more meaningfully 
described as Scope-Bound_Resource_Management, which is the by far the 
most powerful convenient and useful idiom for avoiding leak type 
problems, and one that most other languages lack.

Further, this approach to avoiding leaks of memory, sockets, database 
handles, and such, and avoiding use of already released memory, database 
handles, and such, instead of involving quite a bit of work, saves you 
quite a bit of work.

Even if you are using a garbage collected language, memory management is 
not in itself the biggest problem, rather it is the stereotypical case 
of this entire class of problems.  C++11 Smart pointers plus 
Scope-Bound_Resource_Management provide a general solution to this 
entire class of problem, and a general solution that saves you a great 
deal of work rather than involving quite a lot of work.

Since resource management is only semi automated in C++11, you can still 
get it wrong.   Any stupid code that can be written in C can be written 
in C++. You can still make mistakes and not realize it.  But because you 
should be doing vastly less work managing resources in C++11, you have 
vastly less opportunity to get resource management wrong.

You should have defined in your classes how resources are to managed, 
and then the compiler proceeds to manage resources for you.  If you 
refrain from using obsolete C resource idioms in C++, it is quite 
difficult to leak resources or to inadvertently access already released 
resources.   You should never manually manage resources in C++11 except 
within class creators and destructors, in which case the class of C 
errors that you are using formal methods to detect cannot happen.