OSEC

Neohapsis is currently accepting applications for employment. For more information, please visit our website www.neohapsis.com or email hr@neohapsis.com
NFR Wizards Archive: Re: Penetration testing via shrinkware

Re: Penetration testing via shrinkware

Marcus J. Ranum (mjrnfr.net)
Sun, 20 Sep 1998 20:53:03 -0400

>Verification need not be confined to testing. You could also do
>FORMAL verfication, which involves inspecting the source code, and proving
>mathematically that there are no bugs at all. Let me be perfectly clear: I
>do NOT regard this as a practical approach, I am just observing that it is a
>theoretical possibility. Very few organizations have the resources to persue
>A1 certification for a product of any complexity. But it is theoretically
>possible to prove that a firewall is bug-free.

Bleah. That formal proof stuff is all nonsense. If you spend
a huge amount of effort and are willing to make a lot of
simplifying assumptions (like that your compiler generates
correct code and that your libraries are all correct code
and that your kernel is bug free, and that your CPU microcode
is bug free) then you can prove that "hello.c" is correct.
If things get much more complex than "hello.c" then it's
one of those life-long projects.

I agree with you that it's not practical. I'd go a step
farther and say that it's outright damaging. A lot of folks
buy that trusted system DOD snake-oil because they hear
about things like "formal verification" and "proof" and
it sounds great (if you don't know what a load of bullpuckey
it is). Formal verification, A1 systems, and all that
hooey needs to be debunked -- look how much damage M$'s
managing to market Windows NT as "C2 secure" has done!

mjr. 

--
Marcus J. Ranum, CEO, Network Flight Recorder, Inc.
work - http://www.nfr.net
home - http://www.clark.net/pub/mjr

This archive was generated by hypermail 2.0b3 on Sat Jul 17 1999 - 07:11:47 CDT