[SystemSafety] 7% of mistakes in Coq proofs go undetected

[Dewi Daniels]

Peter,

I'm not familiar with Coq. I have done a lot of proof using the SPADE Proof
Checker. That was back in the early nineties, verifying assembler code that
was used on various Rolls-Royce jet engines. The tools have improved a lot
since then.

Cases where this could happen using the thirty-year-old technology include:
1. Writing a post-condition that was weaker than intended.
2. Writing an incorrect local proof rule (this insecurity has since been
removed from the SPADE/SPARK toolchain).

Yours,

Dewi Daniels | Director | Software Safety Limited

Telephone +44 7968 837742 | Email d <ddaniels at verocel.com>
ewi.daniels at software-safety.com

Software Safety Limited is a company registered in England and Wales.
Company number: 9390590. Registered office: Fairfield, 30F Bratton Road,
West Ashton, Trowbridge, United Kingdom BA14 6AZ


On Thu, 14 Nov 2019 at 16:57, Peter Bishop <pgb at adelard.com> wrote:

> I am trying of think of cases where this could actually happen.
>
> The only things I have come up with so far are:
>
> - cosmetic changes (white space characters and comments)
>
> - changes to unreachable code
>
> Any other ideas?
> On 14/11/2019 16:40, Gergely Buday wrote:
>
> The change was in the code, not in the specification. Changes in the code
> can result in specification-conforming code.
>
> Derek M Jones <derek at knosof.co.uk> ezt írta (időpont: 2019. nov. 14., Csü
> 17:28):
>
>> Gergely,
>>
>> > This means that Coq verification scripts are 7% robust against slight
>> > changes in definitions. That's important in verification, ask any
>> developer
>>
>> Mutations are random changes, which may or may not be slight.
>>
>> You appear to be suggesting that failure to detect 7% of random changes
>> is a desirable property.  I find this surprising.  Do you think the 7%
>> figure is about right (for this 'desirable' property), or should it be
>> higher/lower?
>>
>> > who maintains large scale verification projects.
>> >
>> > Derek M Jones <derek at knosof.co.uk> ezt írta (időpont: 2019. nov. 14.,
>> Csü
>> > 16:35):
>> >
>> >> All,
>> >>
>> >> Some interesting results from the mutation analysis of Coq proofs:
>> >> http://cozy.ece.utexas.edu/mcoq/
>> >>
>> >> Mutation analysis introduces a mistake into code, by mutating existing
>> >> code at some point (there is a small cottage industry working on new
>> >> mutation operators), and the modified code is executed in some way.
>> >>
>> >> A common research use (not much used in industry) is using mutated
>> >> code to check the quality of a test suite, i.e., a thorough test
>> >> suite will detect the added mistake.
>> >>
>> >> "Mutation Analysis for Coq" does what it says on the tin.  It mutates
>> >> Coq proofs, and then checks whether the verification fails (which it
>> >> should do).
>> >>
>> >> In 7% of cases (6.82% to be exact), verification succeeded (averaged
>> >> over all mutations).
>> >>
>> >> So, those of you who have paid for Coq proofs to be written for your
>> >> software.  If the proof contains a mistake, there is something like
>> >> a 7% chance it has gone undetected.
>> >>
>> >> Do companies offering "proofs of correctness" provide fix-it for free
>> >> guarantees?  Or do the claims of correctness never make it from the
>> >> marketing department to a signed contract?
>> >>
>> >> --
>> >> Derek M. Jones           Software analysis
>> >> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
>> >> _______________________________________________
>> >> The System Safety Mailing List
>> >> systemsafety at TechFak.Uni-Bielefeld.DE
>> >> Manage your subscription:
>> >> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>> >>
>> >
>>
>> --
>> Derek M. Jones           Software analysis
>> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
>>
>
> _______________________________________________
> The System Safety Mailing Listsystemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>
> --
>
> Peter Bishop
> Chief Scientist
> Adelard LLP
> 24 Waterside, 44-48 Wharf Road, London N1 7UX
>
> Email: pgb at adelard.com
> Tel:  +44-(0)20-7832 5850
>
> Registered office: 5th Floor, Ashford Commercial Quarter, 1 Dover Place, Ashford, Kent TN23 1FB
> Registered in England & Wales no. OC 304551. VAT no. 454 489808
>
> This e-mail, and any attachments, is confidential and for the use of
> the addressee only. If you are not the intended recipient, please
> telephone 020 7832 5850. We do not accept legal responsibility for
> this e-mail or any viruses.
>
> _______________________________________________
> 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/mailman/private/systemsafety/attachments/20191114/34f067a1/attachment.html>