[Cryptography] formal verification +- resource exhaustion

[Nemo]

Peter Gutmann <pgut001 at cs.auckland.ac.nz> 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.

I actually did search for a newer version of the JPL spec, but all I
found was the same one referenced in this thread
(http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf). Do you have a
link to a more current version?

Or are you citing MISRA? That is a different spec. As far as I can tell,
the JPL coding guidelines were never updated beyond 1.0.

Somewhat interesting Hacker News thread on these guidelines:

https://news.ycombinator.com/item?id=4339999

It sounds like they were designed with static verification in mind by
people who actually know something about the field.

JPL treats their multi-billion-dollar one-shot toys pretty seriously

 - Nemo