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

James Goldston (jgoldstonsscs.net)
Mon, 21 Sep 1998 22:42:43 -0400

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

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