Re: Penetration testing via shrinkware

[James Goldston <jgoldston () sscs net>]

Couple of observations.  First, it is all too easy to toss out words like
code walk-throughs and proving this or that.  As far as I know the NCSC has
never done code walk-throughs, except on possibly the smallest code
segments and certainly not an entire system.  I don't think we can expect
the ICSA or anyone else to do this anytime soon.  For a very old reference
(1984) on why you should not trust code walk-throughs, I would direct
interested readers to Ken thompson's paper, "Reflections on Trusting Trust"
at http://www.acm.org/classics/sep95/.


=-=-=-=-= At 08:53 PM 9/20/98 -0400, Marcus wrote: =-=-=-=-=
> > 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.

Formal vertification is not "inspecting the source code, and proving
mathematically that there are no bugs at all."  For the lack of a better
reference, from the NCSC Purple Book 'design verification is mapping specs
to the security model.  Implementation verification is mapping code to
specs.'  Last time I checked, the latter has been beyond the
state-of-the-art since it was first written for all but play systems.

Also, I'm not sure which is harder, proving the statement that "it is
theoretically possible to prove that a firewall is bug-free" or the
converse.  I would bet on the latter.

James