(no subject)

[Martin Dalecki]

Horst von Brand wrote:
> 
> Martin Dalecki <[e-mail]> said:
> 
> [...]
> 
> > 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!)
> 
> Checking each possible combination of, say, 10 variables @ 64 bits each is
> certianly finite, but that is not very practical.

It's finite enough to make all the arguments in all those non-existence
proofs
irrelevant. Finite is finite. Unfinite is unfinite. All those
non-possibility
results of the theoretical informatcs are basically like applying 
calculus (analysis) to lets say floating point computer arithmetics ---
just an utterly wrong model. Even if you think deep enough about the
Landau symbols O(x) and therelike you should find out that they are
basically
nonsense in the real world... Just take some definition and read it.
Try then to apply it to some real computer out there with finite
input finite memmory and finite livetime...

> > 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"). [...]
> 
> Not Goedel's theorem, Turing's proof of the existence of noncomputable
> functions is relevant here. Both are essentially the same, anyway.

I have already pointed to a version of proof of Goedels theoreme which
is
using Turing machines as language instead of recursive definitions....

> 
> > [...] 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.
> 
> Can't be done, unless you _severely_ restrict the programs considered
> (where the severity depens on the resources you are able to bring to the
> task). Sure, you can restrict the programs by style guidelines, prohibiting
> use of certain functions, etc. If a smart enough program can't show it
> doesn't have problems, probably a smart human can't either, and it's time
> to rewrite/redesign. Now the problem is: How smart is "smart enough"? What
> exact types of checks should the program consider? How do we make sure no
> possibly dangerous construct slips through? The last question leads back

I have seen the *practical* causes of buffer overruns in the real world
out
there... Basically a simple grep "\[PATHMAX\]" "*.[ch]" will already
spot
90% of those errors. You just can't 
imagine how lazy the programmers are out there... 
Sometimes I think that every one writing more then let's say 1 PATHMAX
pro
10k of souce code should be punished to write down on paper 1000 times:
"alloca(), alloca(), alloca(), alloca()"...

And it would help
plenty! The fact that there are full-blown languages out there which
make
this stuff impossible shows sufficiently that the "restrictions" you are
talking about are not as severe as they appear. (Java, ksh or tcl for
one)

Applying some simlpe heuristics can really turn out to be already very
sufficient... (BTW. Please just grep for PATHMAX in the source of Proftp
to see
what I mean by lazy...)

1. Don't ever use automatic arrays for filename buffers
2. Don't apply sprintf strcpy and friend's to automtaic arrays...

All this can be quite reliable tracked... Not in a perfect way
but with very good catch quote. Such programs exist already!

And if one is trying to harden some particular program he doesn't need
to spot only the exploitable problems of the above kind.
One can arrive at a quite strong result by just for example
eliminating every use of suspicious constructs.

> to the question of how to characterize all possibly dangerous constructions
> in C. And AFAIKS there is very little that can't be abused there. Then we
> are back at the problem with lint and lclint and its ilk: No reasonable way
> to make them shut up for perfectly reasonable code. Hundreds of false
> negatives for each positive just don't make an useful tool.
> 
> > 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;
> > }
> 
> Very practical program, that one.

Sure... But it was just intendid as an counterexample for an
utterly general statement in first place.

--
	Marcin Dalecki