Re: Penetration testing via shrinkware

["Joseph S. D. Yao" <jsdy () cospo osis gov>]

> 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!

Right now, it's not practical.  Right now, a lot of things ARE
practical that weren't when we got into this field.  [I remember
predicting that these new "floppy" disks would be too unreliable to
ever be worth anything - so much for my life in market futures.]  So,
let's be fair about this.

Formal proofs [which, by the way, have nothing to do with C2] are still
in their infancy.  Logical tools have advanced since I got a degree in
logic "a few" years ago, and yet they can't do a fraction of what they
need to do.  That doesn't mean that they're EEEVVVIIILLLLL.  It doesn't
mean that they're debunkable "hooey".  It does mean, as everyone has
agreed, that RIGHT NOW they're not something you want to rely on.

But they DON'T require all of those assumptions.  Formal proofs start
with a formally proved "trusted code base" and an assumption that the
processor works as advertised [which, for Intel as well as others, may
be an iffy assumption].

And they MAY well be incredibly useful, especially if we get to a point
where we can reliably do not only code transformations, but also
transformations and relationships among specifications, design, and
code.  One can hope for that day.

And one MUST educate the [interested] public that a C2 rating for a
product with a similar name but totally different code base, hardware
set, and network connectivity set [NONE!] is MEANINGLESS.  Public
ignorance is the reason that M$ marketers - and many other marketers -
can work their evil ways.

--
Joe Yao                         jsdy () cospo osis gov - Joseph S. D. Yao
COSPO Computer Support                                          EMT-A/B
-----------------------------------------------------------------------
This message is not an official statement of COSPO policies.