[SystemSafety] Bursting the formal methods bubble

[Martyn Thomas]

Randolf Johnson of the NSA presented the work at a SPARK user group
meeting. I have his slides somewhere ...

Tokeneer was an NSA experiment, not intended to be put into operation
but a realistic testbed that was the way that NSA compared software
engineering approaches.

All the project documentation, all the deliverables, the code, the
tools, the proofs and the final report are available on the AdaCore
website for free download so that anyone can run the tools, modify the
code and break the proofs, try their own proof tools etc. Several
academics have used Tokeneer as the example for testing their own tools.
It may be the most analysed code ever ...

Anyone who is developing or selling safety-critical software in the UK
should look at sections 2 and 3 (in particular) of the 1974 Health and
Safety at Work Act, and at the Operational Guidance on cybersecurity
that HSE has published this year. Anyone selling software in Europe
should perhaps also read the NIS directive and the GDPR. And then think
about whether they can comply with the laws.

The phrase "reasonably practicable" in the HSWA means that a risk to
healt or safety must be reduced further unless the cost of doing so
would be grossly disproportionate to the benefit. Not all regulators are
currently applying the law fully, as will be obvious from the VW Diesel
scandal for example. But I wouldn't be a business on them continuing to
be lax, and the new sentencing guidlines have led to some much larger
fines (not yet for software) and NIS and GDPR have fines up to 4% of
global turnover.

We can't go on for ever building software with a test-and-fix approach
to assurance. NIS and GDPR (and the HSE OG) may be the comets that
finally kill the dinosaurs.

Martyn


On 25/10/2017 16:10, Derek M Jones wrote:
> Martyn,
>
>> The NSA concluded that Z/SPARK CorrectbyConstruction beat every other
>> software development approach they had experienced. Search for Tokeneer
>> on line.
>
> My searches only located congratulatory statements by the usual
> suspects.
>
> Is their an internal report that you know about (it was your company
> that did the work, after all)?
>
> Those involved seem to make a big thing about only two bugs being found.
> One possible reason for such a small number of bugs is that very few
> people used the software in anger.
>
> This work found new 20 problems, of which half could lead to
> system failure:
> www.open-do.org/wp-content/uploads/2010/04/ERTS2010_final.pdf
>
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20171025/3978abc8/attachment.html>