[Cryptography] formal verification +- resource exhaustion

John Denker jsd at av8n.com
Tue Feb 28 12:57:31 EST 2017


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?

Related question:  What do reliability experts think of the
NASA / JPL coding standards?
  http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf

In particular, consider Rule 5, which forbids using the heap
(after the initialization phase).  I can understand where that
comes from, but it is remarkably restrictive and incurs a
terrible price in terms of efficient use of memory.

On the other edge of the same sword, one could argue that those
standards are not nearly restrictive enough.  They allow and
even require the use of local automatic variables (Rule 13),
but nowadays you can run out of room on the stack 1000 times
more easily than you can run out of room in the heap.  Typically
it's megabytes versus gigabytes, under the control of ulimit -s.

Just to rub salt into the wound, with gcc if you run out of
stack AFAICT the first and only symptom is a segfault;  g++
is no better.  The compiler's attitude seems to be:
   https://www.av8n.com/physics/not-my-job.htm

I cannot explain the inconsistency between local variables and
malloc.  The latter relatively gracefully returns a null pointer
if it runs out of resources.  C++ "new" throws a catchable
exception.

Stack exhaustion makes it appallingly easy to write seemingly
beautiful code -- with all the right loop invariants etc. --
that works fine for some parameter values yet fails for others.
The failures can involve insidious non-local interactions.

I'm a big fan of defensive programming, but it's not obvious
how to defend against this in any systematic way.

Any suggestions?



/*
 Usage:      ./ulimit-s-test nnn
 Especially: ./ulimit-s-test $(ulimit -s)
 Segfaults for not-very-large values of nnn,
 depending on ulimit -s
 */

#include <stdlib.h>     /* for atoi() */

int main(int argc, char const * const * argv){
  int nnn = (argc > 1) ? atoi(argv[1]) : 8192;
  unsigned char big[1024][nnn];
  return big[0][0];
}



More information about the cryptography mailing list