[Cryptography] formal verification +- resource exhaustion

[Nemo]

Peter Gutmann <pgut001 at cs.auckland.ac.nz> writes:

> If the spec was written before the feature existed or had any kind of
> widespread use (I doubt many, if any, embedded-systems compilers had
> VLA support in the early 00's), it's not an oversight.  They can't
> predict the future.

Well, the JPL Coding Standard is dated 2009. It names C99 (ISO/IEC
9899-1999(E)) as the target language. In C99, VLAs are a mandatory
feature. Since they name a decade-old spec, I will stick with
"oversight".

But possibly a self-correcting one: C11 makes VLAs an optional feature,
probably to cater to embedded applications. And VLAs have never been
incorporated into any C++ spec, probably because somebody thinks they
are a terrible idea.

> I'm using MISRA.  The JPL spec is... well, it may be OK for JPL use,
> but MISRA is better in general, more comprehensive, includes a
> rationale and examples, and so on.  MISRA'12 is actually something I
> can recommend, the earlier ones less so.

Could you be more specific about what you recommend MISRA for? If it's
resource-constrained environments where you cannot crash, sure. For
secure code, though, it is debatable. Resource exhaustion is not
necessarily a security hole, especially when the system is designed for
it. Controlling resources globally strikes me as both more flexible and
more reliable than trying to bound every individual use.

For example, heap-allocated self-resizing buffers are invulnerable to
buffer overruns; their failure mode is heap exhaustion. So maybe
self-resizing buffers combined with a process-wide hard memory limit is
a safer design pattern than "never call malloc()". Let the user/attacker
flood their session with data and crash it; just make sure it only
affects themselves.

Also, as mentioned elsewhere on this thread, higher-level constructs
(e.g. smart pointers) can make it easier to reason about code and prove
invariants. Unless you are talking about full formal verification of
security properties, I would trust code written for human reviewers over
code written for static analyzers any day.

I wonder whether MISRA-C code is more secure in general than ordinary
"well written" C or C++. Unfortunately I do not know how to quantify
this question.

 - Nemo