[SystemSafety] Critical systems Linux

Matthew Squair mattsquair at gmail.com
Thu Nov 22 22:49:38 CET 2018 

I think you are accurate in your assessment of the ability of any regulator to regulate any complex evolving technology. As a regulator you’ll never be as close to the problem/technology as the industry applicant. Given we can’t regulate the technical we then fall back on regulating the social, that is your looking into the organisation to establish a degree of trust in their competence. Would I trust a proof? That depends on whether I trust the people who produced it...

John Downer wrote an interesting paper, called Watching the Watchmaker on this subject. https://core.ac.uk/display/219552

Matthew Squair

MIEAust, CPEng
Mob: +61 488770655
Email; Mattsquair at gmail.com
Web: http://criticaluncertainties.com

> On 23 Nov 2018, at 1:42 am, Olwen Morgan <olwen at phaedsys.com> wrote:
> 
> 
> 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
>> 
>> 
>> 77 Barnards Green Road
>> Malvern
>> Worcestershire
>> WR14 3LR
>> Company No. 07642673
>> VAT No:116495996
>> 
>> www.aeronautique-associates.com
>> 
>> 
>>> On Thu, 22 Nov 2018 at 13:40, Olwen Morgan <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
>>>> 
>>>> 
>>>> 77 Barnards Green Road
>>>> Malvern
>>>> Worcestershire
>>>> WR14 3LR
>>>> Company No. 07642673
>>>> VAT No:116495996
>>>> 
>>>> www.aeronautique-associates.com
>>>> 
>>>> 
>>>>> On Thu, 22 Nov 2018 at 13:11, David Crocker <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
>>>>> > Manage your subscription:
>>>>> > https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>>>>> 
>>>>> _______________________________________________
>>>>> The System Safety Mailing List
>>>>> 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
>>>> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>>> _______________________________________________
>>> The System Safety Mailing List
>>> 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
> 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/20181123/68714d78/attachment-0001.html>

More information about the systemsafety mailing list