[Novalug] OT question about a mathematician's proof of a program

Tom Gutnick tag@sunny-banana.com
Sat Nov 16 08:28:28 EST 2013


Although one successful attack may prove an OS to be insecure, the failure
of millions of attacks to break in does NOT prove it to be secure -- it
might mean only that flaws have not yet been found. (And I can't tell you
how many times, when I was managing software development projects, that we
would find a bug and realize that it had been there for several years, but
just never triggered.)

OTOH, NSA and NIST, along with some of the major computer manufacturers,
have done significant work over the years to develop ways of writing an O/S
with ~assurance~ that the security features are correctly implemented. A big
(but certainly far from the only) part of this is to build in the security
from the beginning, rather than trying to bolt it on after the fact.) When I
worked at Data General, we developed a UNIX implementation at the B2 level
of trust. As far as I can recall, no security vulnerabilities were ever
found.

There is very extensive literature on the subjects of creating trusted
software and of writing provably-correct software.

Tom Gutnick 
Sunny Banana IT Consulting -- your personal technology assistant 
3107 North Trinidad Street, Suite 200 
Arlington, Virginia  22213 
571.449.6775 
tag@sunny-banana.com
 

> -----Original Message-----
> Date: Fri, 15 Nov 2013 15:50:22 -0500
> From: cmhowe@patriot.net
> Subject: [Novalug] OT question about a mathematician's proof of a
> 	program
> To: novalug@calypso.tux.org
> Message-ID:
> 	<3a551569a0477e71dca30cf2ba4fae5f.squirrel@www.patriot.net>
> Content-Type: text/plain;charset=iso-8859-1
> 
[snip]
> 
> I guess my question is, can any OS be secure? Proof would come in
subjecting it
> to attacks by the millions and it passing muster. It does have real world
> consequences, doesn't it?
> 
> Comments welcome.
> 
> Charlie





More information about the Novalug mailing list