[SystemSafety] Fwd: Re: Critical systems Linux

Olwen Morgan olwen at phaedsys.com
Thu Nov 22 15:48:19 CET 2018


Actually, after having sent this, it occurred to me that blockchain 
technology might allow arbitrary proof-checkers to check putative proofs 
on a double-blind anonymity basis. Perhaps this could address 
IPR/confidentiality issues for the proof developer?

Just a thought.

O



-------- Forwarded Message --------
Subject: 	Re: [SystemSafety] Critical systems Linux
Date: 	Thu, 22 Nov 2018 14:42:24 +0000
From: 	Olwen Morgan <olwen at phaedsys.com>
To: 	The System Safety List <systemsafety at lists.techfak.uni-bielefeld.de>




We'll have to differ on that one :-)

A very interesting paper was published on the topic of program proofs 
nearly 40 years ago:

de Millo, R. A., Lipton. R. J, and Perlis, A., J., "Social Processes and 
Proofs of Theorems and Programs", CACM, V22, No.5 May 1979 (.pdf 
available on the net - just google for it).

It argues that program proofs will never have the status of proofs in 
mathematics because acceptance of a proof in mathematics depends on 
publication and acceptance by a relevant community of mathematicians. 
The authors did not see that this would necessarily be the case for 
program proofs.

To be honest, I wouldn't trust current regulators to muster enough 
expertise to do their job properly when examining a claimed proof of a 
program. At the moment, they do a rickety enough job of much simpler 
things.  That may be unduly pessimistic. Either way, I think that we 
shall have to develop some kind of institutional arrangement that allows 
greater scrutiny than regulators currently provide - although I wouldn't 
like to see this view end up by promoting the better at the expense of 
the good.

Olwen


On 22/11/2018 14:12, Nick Tudor wrote:
> Don't agree.  Just because some would like to see the proofs, doesn't 
> mean they should and doesn't make it any less safe if they don't.  
> Airbus don't make their proofs public....but the certifier gets to see 
> them if they wish. And it's not all about the proofs per se, it about 
> what you are trying to prove.
>
>
> Nick Tudor
> Tudor Associates Ltd
> Mobile: +44(0)7412 074654
> www.tudorassoc.com <http://www.tudorassoc.com>
> *
> *
> *77 Barnards Green Road*
> *Malvern*
> *Worcestershire*
> *WR14 3LR**
> Company No. 07642673*
> *VAT No:116495996*
> *
> *
> *www.aeronautique-associates.com 
> <http://www.aeronautique-associates.com>*
>
>
> On Thu, 22 Nov 2018 at 13:40, Olwen Morgan <olwen at phaedsys.com 
> <mailto:olwen at phaedsys.com>> wrote:
>
>
>     Agreed about sub-sets. AFAI can see, tool-enforced language
>     sub-setting is still the most cost-effective way to avoid the
>     majority of problems due to poor language definitions.
>
>     I'm not so sure about proofs that are not open to public scrutiny.
>     If the FOSS camp can produce decent software - regardless of
>     whether it's up to snuff for certification purposes - then one
>     hopes that it might one day produce the kind of open proofs that
>     would be helpful. ... But I'm not holding my breath.
>
>     Olwen
>
>
>     On 22/11/2018 13:21, Nick Tudor wrote:
>>     I agree with David: just because not every individual sees all
>>     the work done on semantics (it doesn't have to be 'open' just
>>     because some might say it should be), it doesn't mean that it is
>>     not good work and can support the claims for formal proof of C
>>     code....or indeed, any other language for that matter. 
>>     Furthermore, not all C constructs are necessarily useful in
>>     practical systems and hence it strengthens the argument for use
>>     of subsets, which are [obviously] easier to formalise and then to
>>     automate the proof.
>>
>>     Nick Tudor
>>     Tudor Associates Ltd
>>     Mobile: +44(0)7412 074654
>>     www.tudorassoc.com <http://www.tudorassoc.com>
>>     *
>>     *
>>     *77 Barnards Green Road*
>>     *Malvern*
>>     *Worcestershire*
>>     *WR14 3LR**
>>     Company No. 07642673*
>>     *VAT No:116495996*
>>     *
>>     *
>>     *www.aeronautique-associates.com
>>     <http://www.aeronautique-associates.com>*
>>
>>
>>     On Thu, 22 Nov 2018 at 13:11, David Crocker
>>     <dcrocker at eschertech.com <mailto:dcrocker at eschertech.com>> wrote:
>>
>>         Olwyn,
>>
>>         While it's true that C doesn't have a formal semantics, in
>>         practice the
>>         semantics of C is well-understood by experts, who write
>>         static analysis
>>         tools to help ordinary users avoid the undefined and
>>         unspecified bits
>>         and most of the implementation-defined bits (including of
>>         course order
>>         of evaluation). So formal proof that the software
>>         specification has been
>>         mapped accurately to the semantics of C as understood by tool
>>         vendors
>>         and compiler writers is still very valuable.
>>
>>         A much bigger problem IMO is ensuring that the formal (or other)
>>         specification of the software is fit for purpose.
>>
>>         David Crocker, Escher Technologies Ltd.
>>         http://www.eschertech.com
>>         Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486
>>
>>         On 22/11/2018 12:45, Olwen Morgan wrote:
>>         >
>>         > On 22/11/2018 12:05, Peter Bernard Ladkin wrote:
>>         >> On 2018-11-22 11:47 , Olwen Morgan wrote:
>>         >>> <snip>
>>         >>> There is, of course, a massive problem with the proof,
>>         namely that
>>         >>> the target language C does not have formal semantics.
>>         >> I wouldn't categorise this as a "massive problem". It is
>>         an issue
>>         >> that is and was well-recognised.
>>         >
>>         > I think we'll have to agree to differ civilly on that one.
>>         Without
>>         > codification of semantics in a formal system, there can, by
>>         > definition, be no formal proof. The mathematician in me
>>         regards that
>>         > as a massive problem.
>>         >
>>         >
>>         >> The question is rather more direct than whether any given
>>         PL has a
>>         >> "formal semantics". Put bluntly: for any code X which your
>>         >> code-generator generates; does X have an unambiguous
>>         behavioural
>>         >> semantics?
>>         > C *does not* have unambiguous semantics. In the following
>>         program
>>         > (which I have posted before) the order of evaluation of the
>>         operands
>>         > of the assignment = operator is RL in the first instance
>>         and LR in the
>>         > other for both clang and gcc. Here both compilers are
>>         taking advantage
>>         > of C's latitude in leaving things implementation-defined or
>>         > unspecified and choose different orders according to context:
>>         >
>>         > #include <stdio.h>
>>         >
>>         > int incr(int n) { return n+1; }
>>         >
>>         > int main(void)
>>         > {
>>         >     char a[2] = {'R', 'R'};
>>         >     int  i    = 0;
>>         >
>>         >     char b[2] = {'R', 'R'};
>>         >     int j     = 0;
>>         >
>>         >     a[i] = (++i, 'L');
>>         >     b[j] = (incr(j), 'L');
>>         >
>>         >     printf("\nEvaluation of = in \"a[i] = (++i, 'L');\"     is
>>         > %c%c\n", a[0], a[1]);
>>         >     printf("\nEvaluation of = in \"b[j] = (incr(j), 'L');\" is
>>         > %c%c\n", b[0], b[1]);
>>         >
>>         >     return 0;
>>         > }
>>         >
>>         > Moreover, the compiler is free to do this differently in
>>         different
>>         > compilation runs since not even that would contradict the
>>         standard. In
>>         > fact, AFAI can see, a JIT C compiler would be free to
>>         change the order
>>         > of evaluation dynamically within the same program, again
>>         without
>>         > contradicting the standard. Worse still, the standard allows an
>>         > implementation to omit the evaluation of any operator if the
>>         > implementation can determine that no "needed side effect"
>>         is thereby
>>         > lost. Unfortunately, the standard does not defined what is
>>         meant by
>>         > the phrase "needed side effect". Unless you have absolute
>>         contol over
>>         > how optimisers work, this completely screws any attempt to
>>         avoid
>>         > ambiguity.
>>         >
>>         > The developers of the SCADE C code generator are indeed
>>         aware of these
>>         > problems but the last time I spoke to one of them about the
>>         order of
>>         > evaluation issue shown above, he didn't seem to be sure how
>>         the tool
>>         > dealt with it. If their subset avoids these problems, then
>>         strictly
>>         > speaking, they need to give a proof of it - whereat again
>>         they will
>>         > collide with the lack of formal mathematical semantics for C.
>>         >
>>         > The galling thing is that all this uncertainty is wholly
>>         unnecessary.
>>         > One could devise a language that looked exactly like C but had
>>         > unambiguous formal semantics. Though this would be a large
>>         task, it
>>         > would pose neither new nor insuperable problems, given the
>>         current
>>         > state of the art in formal methods.
>>         >
>>         > Olwen
>>         >
>>         >
>>         > _______________________________________________
>>         > The System Safety Mailing List
>>         > systemsafety at TechFak.Uni-Bielefeld.DE
>>         <mailto:systemsafety at TechFak.Uni-Bielefeld.DE>
>>         > Manage your subscription:
>>         >
>>         https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>>
>>         _______________________________________________
>>         The System Safety Mailing List
>>         systemsafety at TechFak.Uni-Bielefeld.DE
>>         <mailto:systemsafety at TechFak.Uni-Bielefeld.DE>
>>         Manage your subscription:
>>         https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>>
>>
>>     _______________________________________________
>>     The System Safety Mailing List
>>     systemsafety at TechFak.Uni-Bielefeld.DE  <mailto:systemsafety at TechFak.Uni-Bielefeld.DE>
>>     Manage your subscription:https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>     _______________________________________________
>     The System Safety Mailing List
>     systemsafety at TechFak.Uni-Bielefeld.DE
>     <mailto: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/20181122/083baf22/attachment-0001.html>


More information about the systemsafety mailing list