Re: Penetration testing via shrinkware

[Bill_Royds () pch gc ca]

 "Stephen P. Berry" <spb () incyte com> wrote:

To:   "Joseph S. D. Yao" <jsdy () cospo osis gov>




This is another one of those moments when I think there ought
to be two separate lists:  firewalls-theory and firewalls-practice.  To
tell the truth, even if there was a schema for formally proving a
system secure (mod whatever process definition of `secure' the
schema posits), I would remain unconvinced of the real-world utility of
such a proof, excepting the possible placebo effect on The Mgmt.

Okay, _ceteris paribus_ it would be nice to know that one box was
provably `secure' whereas some other box is not.  But what does this
actually tell us?  It tells me the same thing when the provably `secure'
whatsit is a firewall as when the whatsit is a cryptosystem---the weak
spot is going to be between the ears or in the pressure-points of the
folks at either end.




  In the middle 80's, I was involved in the development of a supposed
provable programming language called Euclid.
One of the first things we learned from formal analysis was how few
features you could allow in a programming language if you wanted to prove
anything about it. One feature that was forbidden was pointer parameters to
separately compiled functions, since one had to then trust that the
separate function did not modify the data .
Another was dynamically allocated memory without assuming an infinite pool.
Buffer overflow anyone? :-)

Imagine a firewall written in a language that required static memory
assignment and only copy parameters to subroutines. Yes it could be proven
secure, but it wouldn't be useful for real world problems. THere is still a
lot of work going on to help in formally understanding programming, but it
has moved much more into the formal specification field (Z language at
Oxford for example) where one uses it to great advantage to avoid
overlooking things.

A formal specification of a security policy as a basis of a firewall
implementation would provide a framework for testing that would give one
good assurance of security (but not proof), even in a black box situation.
Until we can more formally describe what we want to prove, it is very
difficult to prove it.