[Cryptography] formal verification +- resource exhaustion

[Peter Gutmann]

John Denker <jsd at av8n.com> writes:

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

It's a bit underwhelming.  I much prefer MISRA-C (which the JPL stuff
incorporates by reference, but only the not-so-good 2004 version).  The 2012
version has finally reached a stage where it's pretty decent (although it's
been improving with every new release, the 1998 version was awful), and
they've finally made it affordable as well.

>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.

It's essential for hard realtime systems, you can't (a) wait for a memory
allocation to occur or (b) risk having one fail.  This is standard in many
industries.

If you can't deal with it easily you can always work around it by grabbing a
fixed-size block, say 64k, at startup and then using a high-water-mark
allocator within it.  I'm not sure if that's strictly compliant with the
intent of the no-dynamic-allocation rule, so you'll probably need to provide
some proof that you'll never run past the end of the block.

Peter.