Re:Bootstrapping trust in compilers
by OR13 on Tuesday December 08, 2015 @11:18AM
(#10697274)
Obligatory reference to previous HN discussion of Reflections on Trusting Trust by Ken Thompson [1].
I'd be interested in any war stories or links to compilers verified with things like: Cryptol [2], Coq [3] or Idris [4].
I've seen Cryptol prove equivalence for cryptographic algorithms written in C and Java. Would love to learn more about how this approach can or can't be applied to compilers.
I'd be interested in any war stories or links to compilers verified with things like: Cryptol [2], Coq [3] or Idris [4].
I've seen Cryptol prove equivalence for cryptographic algorithms written in C and Java. Would love to learn more about how this approach can or can't be applied to compilers.
1. https://news.ycombinator.com/item?id=2642486
2. http://www.cryptol.net/
3. https://coq.inria.fr/
4. http://www.idris-lang.org/