Re: Theoretical question about vulnerabilities

[Nash <nash () solace net>]

On Wed, Apr 13, 2005 at 11:01:11AM -0400, der Mouse wrote:
> Take the code for the checker.  Wrap it in a small amount of code that
> makes a deliberate out-of-bounds access if the checker outputs `no
> problem'.  Then write another small bit of code which ignores its input
> and runs the wrapped checker on itself.
>
> Run the original checker on the result.
>
> This is basically the same diagonalization argument Turing used to
> demonstrate that the Halting Problem was unsolvable; that's the sense
> in which I call it the Halting Theorem rephrased.

First off, I think you're more or less correct. Sortof. There is no
computable predicate that will decide for any ARBITRARY PROGRAM whether
ANY ARBITRARY CONSTRAINT is satisfied. But, this is just the statement
of the fact that there are constraints that are, themselves, not
computable.

But, this is highly naive. A useful checker would not be designed to try
to meet this objective. I think that's why he used the term "constrained
environment."

So, there are lots of cool ways to constraint the environment. You
could constrain the language in order to make certain constraints easy
to prove. You would still be unable to make proofs about all constraints,
but the sub-theory you're working in for a particular constraint might
be complete, which means that whether a program meets that constraint
would be fully computable.

This is just the assertion that if T is a deductively closed theory (in
logic) and S is a sub-theory, that T's incompleteness doesn't imply S's
incompleteness. At one level, this is just the statement that every
formal theory contains Logic itself as a sub-theory and that logic is
complete (Goedel's Completeness Theorem). Another more interesting
example is the sub-theory of Number Theory that contains only zero, the
successor function, and addition. Its a perfectly good sub-theory of
Number Theory and its been proved complete. But, its embedded** within a
much stronger Number Theory that's not complete.****

Also, one might seek to constrain the program's resource use during a
given computation. E.g., build the run-time environment with a suitably
strict watch-dog. Then, infinite loops may be made impossible and every
constraint becomes fully computable. This is basically computation
within the realm of strictly recursive functions, rather than the larger
class of partial recursive functions. So, you may be in trouble if the
program you need to write is a partial recursive function.

There's some interesting semantics of programming language being built
on top of Topological Fixed Point Theory. I read about it briefly, but
can't really comment on how well it addresses this problem. It seems to
be a promising possibility, though. See Nielson for more.


ciao,

    -nash

"Semantics with Applications", Nielson & Nielson, Wiley, 1992. Available
   as a PDF here: http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html

** By "embedded" I mean in the strict mathematical sense, but in this
   case the formal languages do not differ, so we can be a bit loose.
   It is not necessary that this happen, though. The Arithmetization
   technique used by Goedel gives us nice ways of embedding theories
   from other languages into a larger theory. Also, I think this is more
   or less what Cohen does with Forcing languages.

**** In fact, all of mathematics is considered (by logicians) to be
   embedded inside what's called Set Theory (typically given by an
   axiom system called ZFC). Set Theory is very powerful and is hence,
   incomplete. But, there are lots of theories in mathematics that are
   complete. The Theory of the Real Field, the above Number Theory, and
   others. Here are some references:

   http://en.wikipedia.org/wiki/Zermelo-Fraenkel_set_theory

   http://www.solace.net/nash/math/Set_Theory/zfc_axioms.pdf

   "The Handbook of Mathematical Logic", Jon Barwise, North Holland
   Publishing Co., 1977.  ISBN 0 444 86388 5. (No longer in print, but
   you may find a copy at your local Univ. library)


> > I really do find this line of argument rather irritating; the
> > theoretical limits of proof are quite a different thing from the
> > practical application of proof-based technology in a suitably
> > constrained environment.
>
> Entirely true.  But if you use theoretical language like "proof", you
> have to expect to be held to a theroetical standard of correctness.
>
> /~\ The ASCII                                der Mouse
> \ / Ribbon Campaign
>  X  Against HTML               [EMAIL PROTECTED]
> / \ Email!             7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B

-- 

An ideal world is left as an exercise for the reader.

        - Paul Graham