3 ms·

So is this protected from the "Ken Thompson Hack"? http://c2.com/cgi/wiki?TheKenThompsonHack http://c2.com/cgi/wiki?TheKenThompsonHack I guess it would have to

by khaki54 12y ago

So is this protected from the "Ken Thompson Hack"? http://c2.com/cgi/wiki?TheKenThompsonHack 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...

puetzk 12y ago
As long as it's also capable of reproducible builds (and I would think the proofs would be very hard if the output is not even predictable!), you should be able to cross-build it from a certified platform, and bootstrap it from a trusted one (or more than one), and the bootstraps should converge to an identical binary, thus giving you both claims.
jerf 12y ago
Unless you implement the proved compiler from scratch yourself, no. 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.)
vilhelm_s 12y ago
It's not self-hosted, so it is not yet at the point where the Thompson hack would apply. 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.
- more_original 12y ago
  Oh, but they're already building a verified Coq compiler: http://www.cs.princeton.edu/~appel/certicoq/ http://www.cs.princeton.edu/~appel/certicoq/

by khaki54 12y ago

puetzk 12y ago

As long as it's also capable of reproducible builds (and I would think the proofs would be very hard if the output is not even predictable!), you should be able to cross-build it from a certified platform, and bootstrap it from a trusted one (or more than one), and the bootstraps should converge to an identical binary, thus giving you both claims.

jerf 12y ago

Unless you implement the proved compiler from scratch yourself, no. 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.)

vilhelm_s 12y ago

It's not self-hosted, so it is not yet at the point where the Thompson hack would apply. 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.

more_original 12y ago
Oh, but they're already building a verified Coq compiler: http://www.cs.princeton.edu/~appel/certicoq/ http://www.cs.princeton.edu/~appel/certicoq/