[Cryptography] formal verification +- resource exhaustion

[Perry E. Metzger]

On Tue, 28 Feb 2017 10:57:31 -0700 John Denker <jsd at av8n.com> wrote:
> On 03/22/2016 05:31 AM, Perry E. Metzger wrote:
> 
> > It was de facto impossible back
> > then, and now it is something you can actually do.  
> 
> Question:  How do formal methods handle the possibility of
> resource exhaustion?

It's a property to be verified, like any other property you might
want to verify.

Verifying that you cannot overflow your (limited) stack or that you
will not allocate more memory than a particular limit or that if you
do allocate too much memory you still fail gracefully (by some
definition of gracefully) are all properties that you can specify and
then attempt to verify. (One of the harder bits the first time you
try it is figuring out how to express the property at all in a formal
way!)

Some things are harder to verify than others because the community
doesn't yet have deep enough experience in doing such verification,
but the state of the art is rapidly improving. The first real
verification of the safety of concurrent operating system code was
quite recent. Verifying real time properties (like that you are
guaranteed to get enough CPU time often enough for your real time
task) is still quite hard but serious progress is being made on
making it more routine.

In many ways the situation is reminiscent of the 1960s to early
1970s, when a new garbage collection algorithm might still be
noteworthy enough to publish in CACM. Right now, instead of learning
the fundamentals of algorithms and data structures needed for
building higher level constructs on top of, the community is learning
the fundamentals of proof techniques to use in various circumstances,
and how to do the proof engineering so the proofs remain robust even
in the face of code that gets updated. The speed with which
techniques are being developed is quite high.


Perry
-- 
Perry E. Metzger		perry at piermont.com