Hacker News Reader

Comment by herodotus | Hacker News Reader

In 1983, Ken Thompson gave a Turing Award talk in which he shows how to embed a backdoor into a compiler in such a way that it would not be visible, even if you had access to the compiler source. (http://delivery.acm.org/10.1145/1290000/1283940/a1983-thomps...) I wonder if the verified compiler could be altered in the same way? (A snippet from the paper so you get the idea:

>We compile the modified source with the normal C compiler to produce a bugged binary. We install this binary as the official C compiler. We can now remove the bugs from the source of the compiler and the new binary will reinsert the bugs whenever it is compiled. Of course, the login command will remain bugged with no trace in source anywhere.)

View on HN

The above assumes that the same C compiler is used everywhere. Say you suspect your gcc to be infected. If a second compiler, say clang, can compile the gcc sources and this gcc then recompiles itself bit-identical to the original, then gcc and clang would both have to be (mutually compatible) infected.

Another way is to bootstrap up to a C compiler from machine-language upwards. So that every "level upgrade" in the bootstrap chain can be verified independently.

http://bootstrappable.org/

Here is one bootstrapping effort:

https://github.com/oriansj/stage0

There is actually a neat way around this by using typed assembly language/proof carrying code. If you had a type preserving compiler down to machine code you could use a separate proof checker (which you presumably wrote by hand in machine code) to convince yourself that the resulting binary implements its spec. :)

The spec of a compiler is also relatively simple, so there isn't a lot of room for backdoors there.

As long as the compiler system is self-bootstrapping. I don't know if this is the case with CompCert C. Probably not becuse of the ML compiler tech involved, which usually doesn't bootstrap on C.

But aside from these incidental properties, yes the same thing could be done.

(This still leaves a large class of related, less recursively symmetric integrity attacks that could be made without the language fully bootstrapping itself, of course)

The ML compiler tech is OCaml which is bootstrapped on C. (It wasn't always so, but has been since Caml Light.)

There's a new extractor that can output C from Coq. There's also multiple compilers for each language you can extract to. My solution was to do diverse compilation where multiple compilers, OS's, and ISA's compiled the compiler. Then you just run it through itself on each one. Use end result that most agree on.

Are you talking about CertiCoq project? It is not ready yet and not clear when will be.

[1] https://www.cs.princeton.edu/~appel/certicoq/

Talking about this:

https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114....

They extract from Coq to C. Like in my Brute-Force Assurance concept, that would let us confirm and supplement the formal verification by hitting the C output with every V&V tool for C programs that we have on hand.

> I wonder if the verified compiler could be altered in the same way?

How do you know it hasn't already been compromised =)

i.e. Reflections on Trusting Trust.

Here's a link that worked for me: http://www.cs.cmu.edu/~dga/15-712/F14/papers/p761-thompson.p...

Reply on news.ycombinator.com