Secure Coding mailing list archives
RE: Bug-free software (was: Re rant about viruses on VMS...)
From: "David Crocker" <dcrocker () eschertech com>
Date: Thu, 05 Feb 2004 21:28:25 +0000
Andreas Saurwein wrote:
With the guarantee that both the B->ADA compiler and the ADA compiler are bugfree, right? Also of course granted that the embedded hardware and its BIOS is bugfree. I have worked myself on "embedded hardware" where the processor itself did not work as specified by the producer. How do you make a program bugfree under this conditions? Anybody remember the pentium bug? Sorry, but I do not believe that anybody can claim to have any piece of non-trivial bugfree software. << There can of course be no absolute guarantee that any kind of system is completely free from defects. Nobody can guarantee that the bridge I will drive over tomorrow won't collapse due to some unknown defect. But for practical purposes, I can assume that it won't (barring earthquakes and tidal waves). Similarly, it is possible to build software that is, for practical purposes, bug free (rather than building software that is almost certain to contain bugs as is usually the case). Perhaps you are not aware that since the Pentium bug, both Intel and AMD engineers have employed mathematical methods to prove that their floating-point units function correctly for all inputs. My information is that Intel uses model-checking, while AMD uses theorem proving. In any case, it is very rate that hardware fails to perform according the specification that software producers code to. Apart from the Pentium FDIV bug, can you name any other comparable problem with x86 processors that had similar ramifications? Personally, I would be delighted if all the software I use was as reliable as the hardware it runs on. Similar considerations apply to compilers. Instances of compilers producing object code that is not semantically consistent with the source code, while by no means unknown, are actually quite rate in mature, mainstream compilers. If the compilers themselves were built using the sorts of technology I advocate, code-generation errors would be virtually unknown. The vast majority of bugs are not caused by faulty compilers or faulty processors, they are caused by use of outdated methods of program construction. Using better methods of software construction together with mature compilers and mainstream hardware, while one can never totally guarantee that the end-product is bug-free, one can produce software that is, for practical purposes, bug-free in the sense that it can be depended on. By "bug free software" I mean software that behaves entirely in accordance with the original defined requirements. Getting the requirements right is another matter altogether. David Crocker Escher Technologies Ltd. www.eschertech.com Tel. +44(0)1252 336565 Fax +44(0)1252 320954 -----Original Message----- From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] Behalf Of Andreas Saurwein Sent: 05 February 2004 16:31 To: David Crocker; [EMAIL PROTECTED] Subject: RE: [SC-L] Bug-free software (was: Re rant about virii on VMS...) At 5/2/2004 06:43 Thursday, you wrote:
No, there are some nontrivial pieces of software in which bugs have never been found and there is no reason to believe any exist. I'm thinking here of safety-critical software developed using formal specification, verified refinement and automatic code generation, such as the METEOR system that controls driverless trains on the Paris metro. To quote from the paper by Patrick Cousot and Radhia Cousot: "The 115 000 lines specification written in B compiles into a 87 000 lines ADA program. ... Since the metro is running, no error was ever claimed to be found in the embedded software nor in its B specification.
With the guarantee that both the B->ADA compiler and the ADA compiler are bugfree, right? Also of course granted that the embedded hardware and its BIOS is bugfree. I have worked myself on "embedded hardware" where the processor itself did not work as specified by the producer. How do you make a program bugfree under this conditions? Anybody remember the pentium bug? Sorry, but I do not believe that anybody can claim to have any piece of non-trivial bugfree software. Andreas
Current thread:
- Re rant about virii on VMS... Glenn and Mary Everhart (Feb 03)
- Re: Re rant about virii on VMS... der Mouse (Feb 03)
- Re: Re rant about virii on VMS... Andreas Saurwein (Feb 04)
- RE: Bug-free software (was: Re rant about virii on VMS...) David Crocker (Feb 05)
- RE: Bug-free software (was: Re rant about virii on VMS...) Andreas Saurwein (Feb 05)
- RE: Bug-free software (was: Re rant about viruses on VMS...) David Crocker (Feb 05)
- RE: Bug-free software (was: Re rant about viruses on VMS...) Andreas Saurwein (Feb 05)
- RE: Bug-free software (was: Re rant about viruses on VMS...) David Crocker (Feb 05)
- RE: Bug-free software Andreas Saurwein (Feb 05)
- Re: Bug-free software (was: Re rant about viruses on VMS...) der Mouse (Feb 05)
- Re: (whimsy) Bug-free software Terrence Enger (Feb 06)
- RE: (whimsy) Bug-free software David Crocker (Feb 06)
- RE: (whimsy) Bug-free software Alun Jones (Feb 07)
- Re: Re rant about virii on VMS... der Mouse (Feb 03)
- Re: Bug-free software (was: Re rant about viruses on VMS...) der Mouse (Feb 05)