[Cryptography] formal verification +- resource exhaustion

Peter Gutmann pgut001 at cs.auckland.ac.nz
Wed Mar 1 18:59:51 EST 2017


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

>> It's not an oversight, it's in the spec, you're just using an obsolete
>> form of it.
>
>In other words, it's an oversight.

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.

>Or are you citing MISRA? 

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.

Peter.


More information about the cryptography mailing list