So is this protected from the "Ken Thompson Hack"? http://c2.com/cgi/wiki?TheKenThompsonHack
I guess it would have to be cross compiled for your system otherwise your existing compiler could corrupt it...
I guess it would have to be cross compiled for your system otherwise your existing compiler could corrupt it...
That is, CompCert is a C compiler, but it's not written in C, it's written in Coq. So when you use it, you have to trust that the Coq implementation was written correctly, and that nobody has inserted any backdoors in Coq which insert backdoors in Compcert which insert backdoors in your program.
The next level would be to also have a verified Coq compiler, which would make the whole system that much more trustworthy. And at _that_ point you could worry about self-perpetuating backdoors in that compiler, and ways to mitigate them.
If you're not doing massive amounts of implementation yourself, you have not escaped from Ken Thompson's hack. All this does is rephrase how they promise to not hack you... it doesn't change the fact that what they say they do and what they actually do have nothing in particular connecting them.
I wouldn't worry about it until strong AI comes along though. Humans are barely capable of making compilers that work, let alone shipping compromised compilers. (I know Ken demonstrated his hack, but to make something that does that under controlled conditions is one thing, to make one that could be shipped and robustly implement the hack quite another.)