[SystemSafety] "Ripple20 vulnerabilities will haunt the IoT landscape for years to come"

[Roderick Chapman]

On 02/07/2020 16:41, Olwen Morgan wrote:
> So, the next question is, do the analysis tools take this into account 
> when seeking to prove loop termination?

There is a separate tool (called, unsurprisingly, "GNATStack") that does 
static worst-case stack usage analysis.

For any hard real-time system running on bare-metal or a small RTOS, I 
would never allow recursion anyway, so analysis of stack usage is 
reasonably easy.  See 
http://docs.adacore.com/live/wave/gnatstack/html/gnatstack_ug/ for the 
details of what it can do.

As for a compiler maliciously turning iteration into recursion... I have 
never seen this in 30-odd years of compiling and running SPARK programs, 
so it's not something that I'm ever gonna lose sleep over.

  - Rod


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200702/65aa769b/attachment.html>