8 ms·

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

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-thompson.pdf 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.)

fulafel 8y ago
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)
- iaabtpbtpnn 8y ago
  The ML compiler tech is OCaml which is bootstrapped on C. (It wasn't always so, but has been since Caml Light.)
- nickpsecurity 8y ago
  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.
  - unboxed_type 8y ago
    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/ https://www.cs.princeton.edu/~appel/certicoq/
    - nickpsecurity 8y ago
      Talking about this: https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.pdf 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.
fmap 8y ago
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.
jpfr 8y ago
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/ http://bootstrappable.org/ Here is one bootstrapping effort: https://github.com/oriansj/stage0 https://github.com/oriansj/stage0
fao_ 8y ago
> I wonder if the verified compiler could be altered in the same way? How do you know it hasn't already been compromised =)
yesenadam 8y ago
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.pdf http://www.cs.cmu.edu/~dga/15-712/F14/papers/p761-thompson.p...

fulafel 8y ago

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)

iaabtpbtpnn 8y ago
The ML compiler tech is OCaml which is bootstrapped on C. (It wasn't always so, but has been since Caml Light.)
nickpsecurity 8y ago
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.
- unboxed_type 8y ago
  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/ https://www.cs.princeton.edu/~appel/certicoq/
  - nickpsecurity 8y ago
    Talking about this: https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.pdf 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.

fmap 8y ago

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.

jpfr 8y ago

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/ http://bootstrappable.org/ Here is one bootstrapping effort: https://github.com/oriansj/stage0 https://github.com/oriansj/stage0

fao_ 8y ago

> I wonder if the verified compiler could be altered in the same way? How do you know it hasn't already been compromised =)

yesenadam 8y ago

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.pdf http://www.cs.cmu.edu/~dga/15-712/F14/papers/p761-thompson.p...