At 6:38 PM -0400 9/23/99, Eli Brandt wrote:
>Arnold Reinhold wrote:
> > Perry, if you really believe that the question of whether a given
> > lump of object code contains a Thompson Trap is formally undecidable
> > I'd be interested in seeing a proof. Otherwise Herr Goedel has
> > nothing to do with this.
>
>That sure smells undecidable to me. Any non-trivial predicate P on
>Turing machines (non-trivial meaning that both P and not-P are
>non-empty) is undecidable by Rice's Theorem. There are technical
>issues in encoding onto the tape all possible interactions with the
>world -- the theorem doesn't apply if some inputs are deemed illegal
>-- but, hey, it's all countably infinite; re-encode with the naturals.
I am not asking about the class of all Turing machines, just one
particular lump of object code OC that happens to be a compiler--say
the C++ compiler on the Red Hat 6.0 distribution. And the question is
whether OC, which was compiled from a particular source file SF, only
contains code attributable to SF or contains some additional
self-propagating code inserted by the compiler OCprev that produced
OC. SF is trusted by assumption. Only OCprev is suspect. You can
even modify SF to some extent, say to turn off optimization or to
produce an auxiliary file that matches object code to source
statements.
If you can answer this question just one time then Thompson's attack
can be defeated. This problem is not remotely undecidable. One way to
solve it is to write a new compiler from scratch OCalt. Then see if
(OCalt(SF))(SF) = OC. As others have pointed out, you can also
attempt to ascribe each byte of object code to the source that
generated it.
>
>The practical impact of this is not immediately apparent. All
>non-trivial theorem-proving about programs is futile in this same
>sense, but people do it, or try. They have a lot of difficulties less
>arcane than running into the pathological cases constructed to prove
>these undecidability theorems.
>
> > Your argument reminds me of claims I always
> > hear that nothing can be measured because of the Heisenberg
> > Uncertainty principle.
>
>I do feel your pain.
More like disgust, actually. Too many computer scientists engage in
this sort of name dropping, citing theorems that generally apply only
in some infinite limit and specifically do not apply to the case at
hand. Most people in the industry, who think an uncountable cardinal
has something to do with electing the Pope, take their pronouncements
on faith and just give up.
The fact is almost nothing in crypto is on a rigorous mathematical
foundation. No one has proved that factoring or discrete logs are
hard problems (at least not publicly). Yet almost all the
difficulties in building trustable systems do not lie in
undecidablility results but in human failings.
The Open Source model, in my opinion, is the best hope of creating
trusted systems we have. Designing a process that can demonstrate
that a given system is totally derived from a body of published code
is an important goal. The Thompson paper is a often cited as proof
that this cannot be done. It deserves to be debunked.
Arnold Reinhold
