Re: Super Lint (was: Unexecutable Stack / Buffer Overflow

Magnus Danielson (cfmd@swipnet.se)
Tue, 04 Jan 2000 09:04:13 +0100


From: Joern Rennecke <amylaar@cygnus.co.uk>
Subject: Re: Super Lint (was: Unexecutable Stack / Buffer Overflow Exploits...)
Date: Tue, 4 Jan 2000 06:06:02 +0000 (GMT)

> > Goedel tells you about axiomatic systems which encompass both ARITHMETIC
> > and RECURSION.
> > And dman there is still the inifity requirement it needs... (int is
> > usually at best 64
> > bit!)
>
> But you might have access to a virtually infinite virtual paper tape.
> Virtually infite being defined as whenever you'd run out of space, the
> system stalls till you have added sufficient extra space.
>
> Besides, if you want to argue about finite resources, there is this little
> problem about NP-completeness of deciding if an if-statement containing ands
> and ors of some variables can yield true for some set of values of these
> variables.
>
> > int main(int argc, char *argv[] )
> > {
> > return 0;
> > }
>
> But from rice's theorem follows that for any given super-lint, there is a
> variant of this program (or any other program, for that matter) with the
> same behaviour, but which cannot be analyzed correctly.

I think that many of the test (read the bulk of tests) would for some decent
written program (let's just assume that for a moment) be terminated quickly
since the necessary limits is there by one way or another. For some you would
need to expand your scope of environment and for some you would find that you
are truly data-dependent (which is actually something we don't want in
over-run cases). One has also to recognice that as we change method (Super-Lint
instead of kernel/libc traps) we can also attack diffrent troubles easilly.
As soon as we ask the question secure(foo) for some arbitrary program foo we
have also opened the door for Kurt Gdel's incompletness theorem. In protocol
validation schemes you must learn to ask the right questions and cutting down
the problem to a sizeable one just because of this trouble. As you run into
NP-hardness it hurts but sometimes you can avoid this by trying to ask diffrent
questions, maybe a less stronger proof or a less stringent set of requirements.
Also, some very specific questions migth be asked with good success where as
more generic onces will fail, simply since you are then also exposing yourself
to the hard answers. So, varying the questionings we migth actually learn that
there was some hard problems but we migth in a feasable time get more specific
knowledge that althougth we failed to generically prove something, we at least
know it has these properties and these specific things we did prove.

So, 42 everyone!

Cheers,
Magnus
:.˛mkabzwmb˛mbz_^nrzh&zvy杶ii