In his 1984 Turing Award lecture, Reflections on Trusting Trust, Ken Thompson describes a C compiler that inserts a backdoor into Unix’s login program, even though no source file in the system contains it. To see how, it helps to start with a smaller problem.

The QUINE

Consider the task: write a program that prints its own source code exactly. One might try

read quine.c; print quine.c

but this is not allowed. The program has to produce the text itself. A naive attempt runs into infinite recursion:

main() { printf("main() { printf(\"main() { printf(\\\"...

Each time the program is written inside the print statement, the program grows, and the copy inside must grow with it.

Such a program is called a quine. The name comes from Douglas Hofstadter’s Gödel, Escher, Bach (1979), after the logician W. V. O. Quine, who wrote no programs but studied sentences that refer to themselves indirectly:

“yields falsehood when preceded by its quotation” yields falsehood when preceded by its quotation.

Thompson’s solution in C splits the file into two parts. The first is an array of numbers:

char	s[] = {
	9,
	48,
	10,
	125,
	59,
	...     (about 260 more, one per character of the second part)
	10,

The second is the rest of the program, starting from the bare 0. This text is what the array s stores:

	0
};

/*
 * The string s is a
 * representation of the body
 * of this program from '0'
 * to the end.
 */

#include <stdio.h>

int main(void)
{
	int i;

	printf("char\ts[] = {\n");
	for (i = 0; s[i]; i++)
		printf("\t%d,\n", s[i]);
	printf("%s", s);
	return 0;
}

The numbers are the second part spelled out in ASCII codes, one per character. The second part begins with a tab, the digit 0, a newline, } and ;, so the list begins 9, 48, 10, 125, 59.

The whole file is therefore three pieces of text placed end to end, and main prints each of them in turn:

piecetext in the fileprinted by
headerchar s[] = {printf("char\ts[] = {\n"), written out by hand
numbers9, 48, 10, … one line per character of sthe loop, which prints each character of s as its code
body0, };, the comment, mainprintf("%s", s), which prints s as text

Writing $\mathrm{enc}(s)$ for the list of numbers and $\|$ for joining texts end to end, the file is

$$\text{header} \,\|\, \mathrm{enc}(s) \,\|\, s.$$

The recursion is avoided because $s$ does not contain the numbers, only the code that computes them. The same data is printed twice, once as numbers and once as characters.

A note on the 0 at the end of the array. In C, a string does not store its length; by convention it ends at a character whose value is zero. The array ends with that zero, and the loop for (i = 0; s[i]; i++) stops as soon as it reaches it, without printing it. So after the loop, the output ends at 10, and the array is still unfinished. The third step finishes it: the text in s happens to begin with the characters 0, a newline and };, so printing s writes the final line of the array before going on to the rest of the program. This is why the comment says s represents the program “from ‘0’”.

Two properties matter for what follows. The program is easy to generate mechanically; the numbers above came from a three-line script. And the second part can hold any extra code, which is reproduced along with the rest.

The Trojan

Let’s consider programs written in C. Source code is written in a text file such as p.c, but what actually runs is a binary. A compiler cc, itself a binary, takes the source file p.c and produces a binary, written $\texttt{cc}(\texttt{p.c})$. The compiler has source code too, cc.c, so the next version of the compiler is $\texttt{cc}(\texttt{cc.c})$: the current binary builds its successor. Assume for now that cc is honest, so $\texttt{cc}(\texttt{p.c})$ is the correct binary of p.c.

Thompson’s tampered compiler, written $\texttt{cc}^*$ (the star marks it as tampered), behaves honestly except on two inputs:

$$ \texttt{cc}^*(\texttt{p.c}) = \begin{cases} \texttt{cc}(\texttt{login.c}) + \text{backdoor} & \texttt{p.c} = \texttt{login.c} \\ \texttt{cc}^* & \texttt{p.c} = \texttt{cc.c} \\ \texttt{cc}(\texttt{p.c}) & \text{otherwise} \end{cases} $$

The first case is the payload, a fixed password that opens any account. The second is the quine: the trojan keeps its own code as data $s$ and writes $\mathrm{enc}(s) \,\|\, s$ into every compiler it builds.

The attack, as a flow:

step 1    cc.c + trojans   ──[ honest cc ]──▶  cc*
step 2    delete the trojans from cc.c; install cc*

after     cc.c    (clean)  ──[ cc* ]──▶  cc*               (trojans restored)
          login.c (clean)  ──[ cc* ]──▶  login + backdoor
          other.c          ──[ cc* ]──▶  other             (compiled faithfully)

Every source file is now clean, and every rebuild of the compiler returns $\texttt{cc}^*$ again, so the trojan lives only in the binary lineage.

Checking the source, then, does not check the system. Lean, which is largely written in Lean, faces the same question about its own binary. This is one reason it keeps its trusted kernel small and why independent proof checkers exist.

Sources

  • Thompson, K. (1984). Reflections on Trusting Trust. Communications of the ACM 27(8), 761–763.
  • Hofstadter, D. R. (1979). Gödel, Escher, Bach: An Eternal Golden Braid. Basic Books.
  • Quine, W. V. O. (1966). The Ways of Paradox and Other Essays. Random House.