Re: Trusting GNAT for security software

[Markus Kuhn <Markus.Kuhn@cl.cam.ac.uk>]

Richard Kenner wrote:
> In article <34F68913.2FF865DA@cl.cam.ac.uk> Markus Kuhn <Markus.Kuhn@cl.cam.ac.uk> writes:
> [gnat can only be bootstraped with gnat]
> >Paranoids will point out that this can be seen as a security problem
> >of gnat as it prevents source code review of the compiler. Read
> >Ken Thompson's legendary "Reflections on trusting trust" ACM
> >Turing award lecture if you do not understand why this is so.
> > http://www1.acm.org:81/classics/sep95/
> Only if you rewrite /bin/login in Ada and compile it with GNAT. ;-)

Actually, I am mostly interested in Ada, because I think it is a
language very suitable for security applications. Ada should
make an ITSEC E6 security evaluation significantly easier than a
language such as C and C++. I intend to use Ada to write cryptographic
access control software at least as security relevant as login or
PGP.

I know the following is paranoid, so consider it more as an
intellectual exercise than as a real concern. GNAT was financed
by the DoD, the same institution that operates NSA, an organization
well known for tampering with the production of cryptographic
systems all over the world to leave backdoors for their access.
Now if I ship my security software in Ada source code to allow
users to evaluate and trust it at a very high level, then what
real trust do I get if I compile this carefully scrutinized
backdoor free paranoid's dream softare with a compiler that I
can only bootstrap with a binary from a single DoD related source.

The practical precausion a paranoid can make is to archive now a
gnat binary version before publication of the security application
and then bootstrap all further new gnat releases with this old
release. This assumes that a Trojan Horse in gnat has to be built
into the binary distribution in with knowledge of the code that it
is supposed to affect, so if the bootstrap starts with an old
binary then Trojan's as described by Ken Tompson can be made
impractical.

Another idea would be that other compiler vendors make their
products sufficiently gcc compatible to allow GNAT bootstrapping
with their compilers.

Tampering with software by tampering with a compiler is in practice
rather easy. For instance, I only have to modify four bytes in
the Linux Netscape Navigator binary in order to build a backdoor
into its cryptographic protection facilities.

Markus

-- 
Markus G. Kuhn, Security Group, Computer Lab, Cambridge University, UK
email: mkuhn at acm.org,  home page: <http://www.cl.cam.ac.uk/~mgk25/>