Date: Mon, 02 Oct 2006 10:04:15 -0500
From: Sol Swords

Hi again,

The ACL2 meeting will again be in ACES 3.116 at 4:00 Wednesday.  Robert 
Krug will be talking about the paper introduced below.  Hope to see you 
there.

 - Sol


INTRODUCTION

This talk is modeled after one by Ken Thompson on the occasion of his
receiving the ACM Turing Award:

Reflections on Trusting Trust

Communication of the ACM, Vol. 27, No. 8, August 1984, pp. 761-763

SUMMARY

We will insert a Trojan Horse into OpenMCL's compiler such that
it will miscompile the function:

(defun bar (x) (+ x 5))

to be:

(defun bar (x) (+ x 10)).

This bug will not be visible when inspecting the compiler's source.
It will be hidden inside the binary.  This Trojan Horse will propagate
itself even if you rebuild the compiler yourself from the ``good''
sources.

In this talk I will discuss the techniques used, show how we put
these to work to produce the Trojan Horse, and demonstrate that
it actually works.