3 ms·

Ken Thompson talked about compilers potentially injecting code in final programs in his Turing Award lecture [1]. That's why compilers need to be certified in o

Ken Thompson talked about compilers potentially injecting code in final programs in his Turing Award lecture [1]. That's why compilers need to be certified in order for the software built by these compilers also receive certification. It's a great step for Rust! [1]: https://www.cs.cmu.edu/~rdriley/487/papers/Thompson_1984_ReflectionsonTrustingTrust.pdf https://www.cs.cmu.edu/~rdriley/487/papers/Thompson_1984_Ref...

Xylakant 3y ago
Reflections on trusting trust is a great paper, but it's not the reason to have certified compilers. There are better steps to build a trust-root for your compiler, for example bootstrapping the rust compiler from source, by either starting out from the early versions or by using mrustc. Certification aims to solve a different, but maybe related, problem. Essentially "how do we verify that the compiler does what it's supposed to do." At its very basic level, it could be described as formalized qualitiy management. So certifying the rust compiler first involved deriving a sufficiently complete spec from the existing RFCs, deriving the requirements for the compiler from that and then verifying that the compiler upholds that. It also requires describing the verification process, issue managegment handling, etc. We have another blog post describing the qualification process in a little more detail https://ferrous-systems.com/blog/qualifying-rust-without-forking/ https://ferrous-systems.com/blog/qualifying-rust-without-for... Disclosure: I'm one of the founders and managing directors at Ferrous Systems
andrewl-hn 3y ago
Also, a really cool find in Ferrocene public docs is their "Traceability Matrix" [1]. For every bit in the Ferrocene language specification [2] there's a link to a set of tests that actually confirm the compiler's behavior. Just shows you how much work has been done here. [1]: https://public-docs.ferrocene.dev/main/qualification/traceability-matrix.html https://public-docs.ferrocene.dev/main/qualification/traceab... [2]: https://public-docs.ferrocene.dev/main/specification/index.html https://public-docs.ferrocene.dev/main/specification/index.h...
- Xylakant 3y ago
  Automating the generation of this beast from the test runnners output was fun. It's an essential part of the qualification documents.
miloignis 3y ago
The best defense against a trusting-trust-attack that I am aware of is Diverse Double-Compilation: https://dwheeler.com/trusting-trust/ https://dwheeler.com/trusting-trust/ It's a simple idea, but can be surprisingly tricky to get exactly the right. Basically, you bootstrap from multiple disconnected and diverse systems and then do pairwise binary comparisons of the bootstrapped program on each of those systems. (This only matters after you've checked the source code itself for Trojans, though)
- Xylakant 3y ago
  There's an issue open on the rustc issue tracker that describes what's missing https://github.com/rust-lang/rust/issues/48707 https://github.com/rust-lang/rust/issues/48707 (reproducible builds is the big one)

Xylakant 3y ago

Reflections on trusting trust is a great paper, but it's not the reason to have certified compilers. There are better steps to build a trust-root for your compiler, for example bootstrapping the rust compiler from source, by either starting out from the early versions or by using mrustc. Certification aims to solve a different, but maybe related, problem. Essentially "how do we verify that the compiler does what it's supposed to do." At its very basic level, it could be described as formalized qualitiy management. So certifying the rust compiler first involved deriving a sufficiently complete spec from the existing RFCs, deriving the requirements for the compiler from that and then verifying that the compiler upholds that. It also requires describing the verification process, issue managegment handling, etc. We have another blog post describing the qualification process in a little more detail https://ferrous-systems.com/blog/qualifying-rust-without-forking/ https://ferrous-systems.com/blog/qualifying-rust-without-for... Disclosure: I'm one of the founders and managing directors at Ferrous Systems

andrewl-hn 3y ago

Also, a really cool find in Ferrocene public docs is their "Traceability Matrix" [1]. For every bit in the Ferrocene language specification [2] there's a link to a set of tests that actually confirm the compiler's behavior. Just shows you how much work has been done here. [1]: https://public-docs.ferrocene.dev/main/qualification/traceability-matrix.html https://public-docs.ferrocene.dev/main/qualification/traceab... [2]: https://public-docs.ferrocene.dev/main/specification/index.html https://public-docs.ferrocene.dev/main/specification/index.h...

Xylakant 3y ago
Automating the generation of this beast from the test runnners output was fun. It's an essential part of the qualification documents.

miloignis 3y ago

The best defense against a trusting-trust-attack that I am aware of is Diverse Double-Compilation: https://dwheeler.com/trusting-trust/ https://dwheeler.com/trusting-trust/ It's a simple idea, but can be surprisingly tricky to get exactly the right. Basically, you bootstrap from multiple disconnected and diverse systems and then do pairwise binary comparisons of the bootstrapped program on each of those systems. (This only matters after you've checked the source code itself for Trojans, though)

Xylakant 3y ago
There's an issue open on the rustc issue tracker that describes what's missing https://github.com/rust-lang/rust/issues/48707 https://github.com/rust-lang/rust/issues/48707 (reproducible builds is the big one)