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

Oliver Xymoron (oxymoron@waste.org)
Tue, 4 Jan 2000 10:05:12 -0600


On Tue, 4 Jan 2000, Martin Dalecki wrote:

> Oliver Xymoron wrote:
> >
> > On Mon, 3 Jan 2000, Martin Dalecki wrote:
> >
> > [I wrote:]
> > > > 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.
> >
> > Actually, recursion is sufficient to model arithmetic. There's a nice set
> > theory representation of integers that looks something like this: {} {{}}
> > {{{}}{}} {{{{}}{}}{}}. As for needing infinite space or storage to be
> > theoretically intractible, there are far more possible machine states in
> > even the most modest computer than you can ever hope to build a state
> > transition table for.
>
> You are talking about the classical set-theory construction of natural
> numbers from Kuratowski (found in "Teoria Mnogości" from him. There is
> an english translation called "The Set Theory")... You still need
> boolean algebra of set's additinally in the
> construction <------ and this is arithmetic!

Fine. You can build a set algebra with the minimal "cons, car, cdr, and
if" in Lisp. My point still stands: the requirements are trivial. Even the
simplest of computer languages meets it.

> As it goes about infinity: In this universe any discrete machine will
> only apprioximate it, since there is only a finite number of atoms
> out there as an upper limit on memmory.... so real computers (JvN kind
> of) are really not quite Turing machines...

Which is also fine. The halting problem and related problems still can't
be solved without going outside of the formal system known as "finite
digital computer". The existence of the aforementioned uncomputable
function of the busy beaver problem is ample proof of that. To see how to
make any halting problem a security problem or vice versa, consider a
daemon designed not to halt that gives a root shell when it does (via an
exploit). s/halt/prove theorem/ to map to undecidability.

> Yeah of course they are comlex, but still Goedels theorem is just
> an utterly wrong argument for impossiblity at this place.

No, it's exactly right. You can't use more than a trivial formal system to
validate itself because there exist simple statements that are
undecidable.

--
 "Love the dolphins," she advised him. "Write by W.A.S.T.E.." 

- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.tux.org/lkml/