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

[Olwen Morgan]

On 02/07/2020 16:12, Roderick Chapman wrote:
>
>> But, considering that a compiler for a functional language may 
>> convert tail recursion to iteration, I ask whether anything in the 
>> Ada standard explicitly forbids an Ada compiler from implementing 
>> iteration by recursion?
>>
> Not sure... but I have never seen a compiler do this.

Praise be to the Gods that you have not!


>
> Note again - things changed a bit with SPARK2014...
>
> SPARK83 - SPARK2005 did not directly support proof of termination of 
> loops, so all proof was "partial".
>
> SPARK2014 _does_ support proof of termination (for loops) through a 
> user-defined "Loop_Variant" expression. Not sure about what happens 
> with termination of recursive subprograms, though - I'm a bit out of 
> the loop with those details. The current SPARK user guide should have 
> more... yeah.. see


Well, in principle, this is an example of the kind of problem to which I 
alluded. If a compiler is not banned from implementing iteration 
recursively and takes advantage of latitude to do so, then the 
termination of a loop may be conditional upon the compiled code 
operating in an environment where it can run the loop to termination 
without running out of memory. So, the next question is, do the analysis 
tools take this into account when seeking to prove loop termination? If 
so, great. If not, then we have identified possible circumstances in 
which the analysis tools may not correctly predict program behaviour. 
The more such lacunae we identify, the more it tends to cast doubt on 
the idea that CbyC allows us to forgo unit-testing.


Olwen