[Cryptography] formal verification +- resource exhaustion

[Peter Gutmann]

Nemo <nemo at self-evident.org> writes:

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

MISRA isn't for resource-exhaustion prevention, it's for safe programming in
general.  It's for creating highly reliable systems with the lowest possible
chances of unexpected behaviour.  Even without the additional security
guidelines (2012 Amendment 1), MISRA produces pretty solid code.

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

As far as I know they make it much harder to analyse, not easier.  That's why
things like DO-178C don't do C++ (just the basic C++ language, not things like
smart pointers) despite a decade or more of effort in trying to deal with it,
you can't analyse what's going on under the covers.

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

Almost certainly, since it bans a whole range of risky C behaviour, and also
forces you to think a lot more about how you structure your code.

Peter.