Open Sourcing Ferrocene
ferrous-systems.com
Open Sourcing Ferrocene
1–10 of 20 posts
Re: Open Sourcing Ferrocene
#2Big congrats to all the team at Ferrous Systems :D
Disclosure:
My colleagues rock :)
Re: Open Sourcing Ferrocene
#3This is really cool. A really big step forward for the Rust ecosystem. Being able to use Rust in safety critical systems is a big win.
Congrats to everyone involved!
Re: Open Sourcing Ferrocene
#4Ken 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_Ref...
Re: Open Sourcing Ferrocene
#5Ken 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_Ref...
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-for...
Disclosure: I'm one of the founders and managing directors at Ferrous Systems
Re: Open Sourcing Ferrocene
#6Ken 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_Ref...
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/traceab... [2]: https://public-docs.ferrocene.dev/main/specification/index.h...
Re: Open Sourcing Ferrocene
#7Ken 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_Ref...
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/traceab... [2]: https://public-docs.ferrocene.dev/main/specification/index.h...
Automating the generation of this beast from the test runnners output was fun. It's an essential part of the qualification documents.
Re: Open Sourcing Ferrocene
#8Hopefully the work on Ferrocene can contribute to the standardization of the Rust language.
Tracking issue: https://github.com/rust-lang/rust/issues/113527
Re: Open Sourcing Ferrocene
#9Ken 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_Ref...
The best defense against a trusting-trust-attack that I am aware of is Diverse Double-Compilation: 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)
Re: Open Sourcing Ferrocene
#10Hopefully the work on Ferrocene can contribute to the standardization of the Rust language. Tracking issue: https://github.com/rust-lang/rust/issues/113527
This is explicitly a non-goal. Ferrocene considers itself a certified downstream of the rust project and as such we certified the rust compiler as it was at 1.68. There's no effort or push to standardize the language from our side.
As part of the certification efforts, we had to write a spec since some description of the language is required. But this spec is a descriptive spec, describing the intended behavior of the language at that point in time - it's mostly distilled from other forms of documenting rustcs behavior, such as the RFCs etc. If there's a divergence between the spec and the compiler, we'll need to investigate whether we uncovered a bug in the spec or in the compiler.
It's not a complete spec, nor does it intend to be. The format it's written is is useful for the certification and documentation effort, but it doesn't cover large chunks that you'd for example need to write second rust compiler implementation. The spec is likely usefor for others, but its Raison d'Être is to serve as a basis for the certification and as such, it will remain limited in scope.