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

[Olwen Morgan]

Thanks to Rod for this. Now two questions:

AFAI recall, recursion is banned in the SPARK subset. 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 that I'd 
expect any sensible compiler to do it, but failure to prohibit it would 
be an example of the possible lacunae to which I have previously 
alluded. An analysis tool assuming an iterative implementation might 
well fail to predict correctly the behaviour of a program in which 
iteration is implemented recursively.

Also when did the Ada standard start using the 
implementation-defined/unspecified/erroneous classification that blights 
the C standard? Did it not start out with the same classification as 
Pascal, namely implementation-defined/implementation-dependent/error?


Olwen




On 02/07/2020 12:29, Roderick Chapman wrote:
> On 01/07/2020 17:10, Olwen Morgan wrote:
>> I'll defer to those more familiar with the Ada RM but I'd be very 
>> surprised if the language specification were entirely free from 
>> lacunae related to implementation-defined features that could, at 
>> least in principle, lead to similar problems. Does the RM tie down 
>> the compiler strictly enough to preclude different instances of 
>> implementation-defined constructs behaving differently in different 
>> places?
>
> The Ada RM defines three levels-of-evil when it comes to ambiguous 
> features. These set different challenges to verification tools. The 
> levels are:
>
> 1. "Implementation-defined". This is something that is left to an 
> implementation to choose, but it must be documented and a compiler 
> must make a single choice that never changes - essentially it's always 
> the same for all versions of the same compiler, and will not change 
> with optimization and so on. Obvious example: the range of values of 
> the predefined type "Integer".  Things like this are unlikely to 
> change for the lifetime of a project, unless you change (say) the 
> target machine ISA and the compiler.  Static analysis tools can be 
> "configured" (hopefully just once) to "know" these values.
>
> 2. "Unspecified" - Compiler has a choice from a set of behaviors but 
> the set might be very large, and the compiler is under no obligation 
> to document its behaviour. Compilers are expected to produce binary 
> equivalence for the same program, but behaviour might change given an 
> arbitrarily small change in a program. These things can also be 
> context-dependent, so changing line N of a program can change the 
> behaviour of line N+1. Obvious examples in Ada: expression evaluation 
> order, and parameter passing mechanism for "in out" mode record types.
>
> 3. "Erroneous" (This is equivalent to "undefined behaviour" in C). 
> Anything goes, and all bets are off! Unrecoverable, in that once your 
> program becomes erroneous then you can't recover to a well-defined 
> state. Example in Ada: accessing an array outside its bounds if you 
> have chosen to compile with runtime checks disabled.
>
> The approach taken by SPARK is essentially:
>
> 1. Implementation-defined behaviours are known to the toolset by 
> default, or can be overridden through a simple configuration file.
>
> Some care is needed here to get these things right, but once you've 
> got it right, they are very unlikely to change for the lifetime of a 
> project.
>
> 2. Unspecified features are either eliminated by simple subsetting, or 
> are rendered harmless by some combination of subsetting and analysis. 
> For example - any expression evaluation order is allowed and valid in 
> SPARK (so a compiler can do anything it likes), but several other 
> rules in the language work together to ensure that the expression 
> always evaluates to the same value, so it doesn't matter.
>
> 3. Erroneous behaviour. Eliminated by subsetting and/or various 
> analyses. For example: unchecked buffer overflow is eliminated by 
> data-flow analysis (to ensure variables are initialized) then 
> theorem-proving (to show that index expressions are in range) and so on.
>
>  - Rod
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200702/3eb46e4a/attachment-0001.html>