<story><title>CompCert – A formally verified C compiler</title><url>http://compcert.inria.fr/</url></story><parent_chain><item><author>herodotus</author><text>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. (&lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;delivery.acm.org&amp;#x2F;10.1145&amp;#x2F;1290000&amp;#x2F;1283940&amp;#x2F;a1983-thompson.pdf&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;delivery.acm.org&amp;#x2F;10.1145&amp;#x2F;1290000&amp;#x2F;1283940&amp;#x2F;a1983-thomps...&lt;/a&gt;)
I wonder if the verified compiler could be altered in the same way?
(A snippet from the paper so you get the idea:&lt;p&gt;&amp;gt;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.)</text></item></parent_chain><comment><author>jpfr</author><text>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.&lt;p&gt;Another way is to bootstrap up to a C compiler from machine-language upwards. So that every &amp;quot;level upgrade&amp;quot; in the bootstrap chain can be verified independently.&lt;p&gt;&lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;bootstrappable.org&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;bootstrappable.org&amp;#x2F;&lt;/a&gt;&lt;p&gt;Here is one bootstrapping effort:&lt;p&gt;&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;oriansj&amp;#x2F;stage0&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;oriansj&amp;#x2F;stage0&lt;/a&gt;</text></comment>
<story><title>CompCert – A formally verified C compiler</title><url>http://compcert.inria.fr/</url></story><parent_chain><item><author>herodotus</author><text>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. (&lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;delivery.acm.org&amp;#x2F;10.1145&amp;#x2F;1290000&amp;#x2F;1283940&amp;#x2F;a1983-thompson.pdf&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;delivery.acm.org&amp;#x2F;10.1145&amp;#x2F;1290000&amp;#x2F;1283940&amp;#x2F;a1983-thomps...&lt;/a&gt;)
I wonder if the verified compiler could be altered in the same way?
(A snippet from the paper so you get the idea:&lt;p&gt;&amp;gt;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.)</text></item></parent_chain><comment><author>fmap</author><text>There is actually a neat way around this by using typed assembly language&amp;#x2F;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. :)&lt;p&gt;The spec of a compiler is also relatively simple, so there isn&amp;#x27;t a lot of room for backdoors there.</text></comment>