Re: Super Lint (was: Unexecutable Stack / Buffer Overflow Exploits...)

[Martin Dalecki]

Oliver Xymoron wrote:
> 
> On Mon, 3 Jan 2000, Eric W. Biederman wrote:
> 
> > Oliver Xymoron <[e-mail]> writes:
> >
> > > On Sat, 1 Jan 2000, Kai Henningsen wrote:
> > >
> > > > [e-mail] (Magnus Danielson) wrote on 01.01.00 in
> > > <[e-mail]>:
> > >
> > > >
> > > > > Oh yes... like those that those who avoid strcpy by doing
> > > > >
> > > > >    memcpy(t, s, strlen(s)+1)
> > > > >
> > > > > I mean, memcpy is supposed to be safe, ain't it ;)
> > > >
> > > > I guess what we _really_ need is some sort of super lint. That is, a
> > > > program that can analyze C code (others are fine, but C is the most
> > > > important by far) and highlights problematic points in the code.
> > > >
> > > > This would not mean that your program actually does anything useful, only
> > > > that it's safe against some kinds of attack.
> > > >
> > > > And it would have zero runtime overhead.
> > >
> > > Unfortunately, your approach was proved impossible well before the
> > > transistor was invented. See "halting problem".
> >
> > The halting problem is only true for the set of all programs.
> > There should be well defined sets for which halting can be proved.
> 
> Yes, but most of the well defined sets aren't interesting. Godel's theorem
> tells us this. The sets are all too simple to encompass the rules of
> arithmetic or recursion. See also the busy beaver problem for examples of

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!)
This means Goedels Unvollstaendigkeitheorem is about theories, where all
the definitions can be expressed by a formalization "roughly" equivalent
to the Turing-machines (Please don't take me by word: This is just an
"explanation for
dummies"). If you like to read a proof of Goedels theorem based
on Turing-machines instead of recursive definitions then please see:
Mayer's book published by Springer. BTW. The whole theorem is compleatly
irrelevant
here, since one dosn't need to find an universal tester for overflows in
arrays
of all programms but just a prober for all the programms one will feed
it.
And in practical cases in CAN BE PROVEN THAT PROGRAMMS DON'T CONTAIN 
POSSIBLE OVERFLOWS. Like in the following example:

int main(int argc, char *argv[] )
{
	return 0;
}