Re: Penetration testing via shrinkware

["Marcus J. Ranum" <mjr () nfr net>]

> 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