Sealed Rust: A plan to bring Rust to safety critical software domains

https://ferrous-systems.com/blog/sealed-rust-the-pitch/

by jamesmunns • 7 years ago

186 38 7 years ago

ferrous-systems.com

velcrovan• 7 years ago

sounds good

ExodusOrbitals1• 7 years ago

Interesting. We would love to use Rust instead of legacy aerospace programming languages for our project.

jamesmunns2• 7 years ago

Hey, James from Ferrous here, we'd love to chat if you're interested in this now, or a couple projects from now!

Feel free to reach out at sealed-rust at ferrous-systems.com!

wyldfire• 7 years ago

Regarding point 2, we do expect to require feedback and assistance from teams within the Rust project, particularly with regards to what parts of the language to formalize, and the most practical methods to achieve this.

It seems like some Rust developers are particular about the governance of the language and overall ecosystem [1]. This strict subsetting seems like it could be a good opportunity to engage the team. Has that already happened? If not, maybe it would be good to create an RFC and/or working group, even if the effort happens independent from the core rustlang dev. If there's some explicit endorsement, it could include guidance and an easier way to upstream changes.

Who is this effort aimed towards?

I wonder if "cryptography" is a domain that applies here? Things like enclaves/signed bootloaders are things where mistakes can be very costly.

[1] https://www.rust-lang.org/governance

steveklabnik• 7 years ago

The Ferrous folks are quite well connected; many of them are on the teams. They’ve been in touch and will be doing the right thing, for sure.

hobofan4• 7 years ago

One of the founders of Ferrous Systems is a Rust Core Team Observer and member of the Governance WG and one of the other founders is a member of the Embedded WG, so I think they are very aware of Rust governance processes.

jamesmunns2• 7 years ago

We've definitely reached out to the Core team (a few weeks ago), and are in the process of reaching out to larger parts of the project.

Cryptography is certainly an interesting target - they certainly could benefit from the specification of the language, despite not being legally required similar to the other domains listed here.

thesuperbigfrog3• 7 years ago

Funding We expect this to be a significant undertaking (likely many full time developer-years of effort), and as such, it is something that will require paid effort to make real.

It is an ambitious undertaking, but strikes me more like a way to try to make more money off of Rust.

It is definitely a moonshot since Ada has a 35-year lead here since it has been used for critical systems since the 1980s. Ada 2020 will be out soon and pulls in several of the innovative ideas that Rust pioneered.

I am not saying that it is not possible, I am just skeptical of the reasons for trying to push Rust in the critical systems direction so suddenly.

nickpsecurity3• 7 years ago

The main thing going for it is that it's not Ada. Most C and C++ developers don't want to use Ada. Some of them are adopting Rust. It also has a strong community and ecosystem. That was its key advantage. Finally, it has temporal safety that Ada doesn't with its borrow checker.

What Ada has on it are its IDE's, MDD, and testing tools that industry is currently using. With stuff like RV-Match and Astree Analyzer, MISRA-C is probably safer than Rust. Rust needs more tooling to be competitive.

carlmr4• 7 years ago

Normal rust without warnings to me is much safer than most Misra C compliant code. Misra C is an attempt to avoid 80% of C's undefined behavior and other pitfalls, but those 20% that are left are still worse than most of what can go wrong in rust.

The problem is mostly certification and having a stable spec for the language.

carlmr4• 7 years ago

The tooling that is needed is mostly productivity tooling, like better code completion (rust analyzer is now pretty promising after RLS kind of stagnated). And maybe better ways to show code coverage.

The problem for usage in safety critical areas is mostly certification and having a stable spec for the language.

irundebian• 7 years ago

How does Rust compare to Spark/Ada?

Argorak4• 7 years ago

It isn't sudden, there's a lot of verification work for Rust already going on, e.g. the Rust Belt Project.

I don't see how delaying would help in the long run.

(Full disclosure: I'm MD at Ferrous Systems)

hobofan4• 7 years ago

It is an ambitious undertaking, but strikes me more like a way to try to make more money off of Rust.

There is nothing wrong with making money off of Rust, and one of the goals of this standardization is to erase doubts that Rust is ready for commercial prime time.

The proposed specification and standardization effort is a enormous undertaking and asking for that effort to be payed for is fair (they even spell out the two funding alternatives).

If you are trying to say that this is a quick cash-grab by Ferrous Systems, you should also consider that their members have been doing a lot of upaid work for a _long_ time for Rust and its community and most of the time without direct monetary benefit.

thesuperbigfrog3• 7 years ago

There is nothing wrong with making money off of Rust, and one of the goals of this standardization is to erase doubts that Rust is ready for commercial prime time.

Agreed. After what Oracle has done with Java, I am hesitant when corporations come bearing gifts.

If you are trying to say that this is a quick cash-grab by Ferrous Systems, you should also consider that their members have been doing a lot of upaid work for a _long_ time for Rust and its community and most of the time without direct monetary benefit.

I am not making any accusations against Ferrous Systems. I have no reason to believe that they are not well-intentioned.

I am just concerned about what might happen to the Rust community when truckloads of money gets involved. Rust has an incredible community and has made rapid progress. I hope that it continues that way.

Xylakant2• 7 years ago

Disclosure: I’m one of the founders of ferrous, though I’m the one with practically no involvement in the Rust community.

To be quite honest here: Ferrous is a for-profit endeavor, but my co-founders and most of our employees both have been involved in the rust community for a long time. We’re also sponsoring conferences, speakers, open source projects in the rust space since the beginning, for example rust-analyzer (1)

So yes, we intend to find funding, people working on this need to be paid. People doing the organizational legwork (such as running the company, keeping the office tidy, making sure there’s enough coffee) need to be paid. Standards documents need to be paid. This isn’t something we as a 6-people company can self-fund. But we intend to make as much of this open source as possible. If there’s sufficient funding, all of it.

On the other side, we’ve been at embedded conferences (even before ferrous as a company was a thing), talking to people in the automobile, robotics and aerospace sector and the question of “is this certified/certifiable” has come up quite a few times. There’s definite interest in finding a replacement for C in that space, and that’s where rust could shine. It’s certainly early, but this is not a project that will come to fruition in the short run. It’s something that rust could profit from in a decade.

(1) https://github.com/rust-analyzer/rust-analyzer/blob/master/R...

thesuperbigfrog3• 7 years ago

Thank you for what your developers have done for Rust. I wish Ferrous Systems the best in the Sealed Rust project.

Despite being entrenched, Ada needs the competition in the critical systems space. Rust is showing great promise as a competitor.

thenewwazoo• 7 years ago

I've got a partially-complete blog post about what "MISRA Rust" would look like (based on MISRA C rules). A surprisingly small amount is relevant. That's a far smaller undertaking, but I found it to be encouraging. There are entire classes of considerations you can dispense with entirely due to how the Rust language works. That gives me hope that this work would be smaller in scope than trying to do many other languages.

wadim• 7 years ago

Have you thought about also looking at the guidelines for MISRA C++? The AUTOSAR ones[1] are fairly recent and might be a bit closer to Rust.

[1] https://www.autosar.org/fileadmin/user_upload/standards/adap...

pjmlp4• 7 years ago

Thanks for providing them, I wasn't aware that AUTOSAR was freely available.

Argorak4• 7 years ago

We'd be super interested in talking and giving feedback on the draft! If you are interested, feel free to get in touch somewhere, preferably on sealed-rust@ferrous-systems.com?

hobofan4• 7 years ago

There are entire classes of considerations you can dispense with entirely due to how the Rust language works.

That sounds like it would still be necessary to standardize, specify and prove a lot about Rust and its compiler, to exploit those facets of Rusts' behaviour?

jasonhansel• 7 years ago

Wow! I'm really impressed. One thing that might help is to require formal verification of code marked as "unsafe" to ensure memory safety (or simply to replace unsafe code in the standard library with safe-but-slower code, e.g. by having a version of the standard library where the get_unchecked() method actually does perform bounds checks).

Argorak4• 7 years ago

Unsafe code is a really hot subject in the Rust project already and there's tons of research work around that done by Ralf: https://www.ralfj.de/blog/categories/research.html.

He's also building Rust tooling for finding bugs in this space, see for example miri.

https://play.rust-lang.org/?version=stable&mode=debug&editio...

(click "Tools" -> "Miri")

This will figure out that you do produce an illegal borrow in that unsafe code.

Lowkeyloki• 7 years ago

This is fantastic and I think it aligns perfectly with many of the goals of the language, at least so far as I perceive them. As the blog post says, it's going to be a long, hard road to reach Sealed Rust. But I, for one, believe it's worth it. I hope Ferrous Systems sticks with it.

Also, please let the community know how we can help. Whether that involves writing code, unit tests, or financial contributions with a Patreon-like system. I really want to see this become a reality and a first class citizen of the Rust ecosystem.

Sealed Rust: A plan to bring Rust to safety critical software domains

Related Stories