Re: Hey old people

[Drsolly <drsollyp () drsolly com>]

On Wed, 21 Dec 2005, Blue Boar wrote:

> David Lodge wrote:
> > I love some of the quotes:
> > "Finally, and most important, current operating systems are so large, 
> > so  complex, [sic] and so monolithic that one cannot begin to attempt a 
> > formal  proof or certification of their correct implementation."
> >
> > They'd have a field day with win 2k3 :-)
>
> Indeed.  They say that the programs are huge, as many as 100,000 
> instructions!  Much too large to audit properly. ;)
>
> I believe there's another section that talks about correctness proofs, 
> except that the biggest programs to have been proven correct have only 
> been a few hundred lines.  Real operating systems can be a couple of 
> orders of magnitude larger.

A correctness proof doesn't prove that the program is solving the correct 
problem. You could do a correctness proof for "The Prefect Antivirus"


_______________________________________________
Fun and Misc security discussion for OT posts.
https://linuxbox.org/cgi-bin/mailman/listinfo/funsec
Note: funsec is a public and open mailing list.