[SystemSafety] Scalability of Formal Methods [was: Logic]

[Rod Chapman]

Patrick Wrote:
>I'll point out that neither SPARK proofs nor any other formal verification
efforts
>are deductive proof that the software will operate as specified when
deployed on real
>target hardware.

I've followed this thread with some interest.  Patrick
raises ligitimate concerns regarding the trustworthiness
of compilers, and the assumptions that underpin static
verification systems such as SPARK.

As the current technical authority of SPARK team, I feel
I can (and probably should) offer some response.

Over the years, I have worked on and with many projects
using SPARK with commerical Ada compilers for a vareity
of "real world" targets. I have observed that real
"compiler silently generates the wrong object code"
bugs are actually very rare.  Why should this be?

Well..having thought about it for a few days, I can
offer the following observations:

1) Ease and correctness of compilation really were design
goals of SPARK from the very beginning.  In 1987, reliable
compilation of Ada83 was still seen as something of a challenge,
so the language was very conservative indeed at steering clear
of hard-to-verify constructs, such as derived types, generics
and tasking.  It turns out there seems to be some
correlation between "hard to verify" and "hard to compile
correctly".  In short: if you want correct compilation,
then make your language (subset) small!

2) Over the years, SPARK has grown substantially in
expressive power, but that's been matched by the growing
maturity of commerical-grade compilers. I am personally
familiar with AdaCore's internaly quality control system,
and it's as good as anything I've ever seen for any software
product.

3) With compilers, you get what you pay for. Don't
confuse the quality of the "free" GCC builds from FSF, for example,
with the quality of compilers from commercial vendors.

4) A great many problems reported as "compiler bugs" are not
actually bugs at all, but are instance of the user
unintentionally writing code that exhibits unspecified
or undefined behaviour.  Modern compilers can do some very
surprising things with propagating undefinedness, for example.

5) SPARK's single most important design goal is the
provision of an unambiguous dynamic semantics, which basically
means getting rid of all the undefined and unspecified
behaviours. This means the verification tools can stand
a chance of being sound, but it also means SPARK seems
to be immune from many compiler-related problems - even
in the face of aggressive optimization, SPARK programs
"just work"...see our work in the SPARKSkein reference
implementation, for example.

6) This also makes SPARK program really portable, since the semantics
are independent of compiler and target machine.  We once (some time ago)
had a customer do a "mid life upgrade" on an application,
switching from Transputer (yes..that long ago) to PowerPC,
from Ada83 to Ada95, and changing compiler vendor en-passant.
It worked with apparently very little pain, and I recall
"one line of code had to change, but that was a timing constant."

7) The SPARK tools do indeed assume that memory is reliable,
so that program variables will behave as expected, although
the language draws a strict distinction between "normal"
program variables and "external" variables, which
are never trusted to be "in type" when read.  Ada95 introduced
the special 'Valid attribute to deal with this, and the SPARK
tools are smart enough to know what it means, so that proofs
can be discharged but only after an externally read value
has been properly validated.

8) Patrick is right to point that all SPARK programs
include some fragments written in Ada, C, assembler, or
something else.  I don't think I've ever seen a 100%
SPARK program deployed. At these boundaries, we are
very careful to firstly minimize the amount of
non-SPARK code, then to verify the contracts,
interface, and bodies of the non-SPARK stuff
using whatever means necessary.

I think that's all I can come up with for now.

 - Rod Chapman, Altran UK
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20140227/e18fc67e/attachment-0001.html>