7 ms·

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

186 points by jamesmunns 7y ago

velcrovan 7y ago
sounds good
ExodusOrbitals1 7y ago
Interesting. We would love to use Rust instead of legacy aerospace programming languages for our project.
- jamesmunns 7y 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 7y 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 https://www.rust-lang.org/governance
- steveklabnik 7y 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.
- hobofan 7y 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.
- jamesmunns 7y 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.
thesuperbigfrog 7y 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.
- nickpsecurity 7y 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.
  - carlmr 7y 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.
  - carlmr 7y 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 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.
thenewwazoo 7y 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 7y 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/adaptive/17-03/AUTOSAR_RS_CPP14Guidelines.pdf https://www.autosar.org/fileadmin/user_upload/standards/adap...
  - pjmlp 7y ago
    Thanks for providing them, I wasn't aware that AUTOSAR was freely available.
- Argorak 7y 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?
- hobofan 7y 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 7y 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).
- Argorak 7y 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 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&edition=2015&gist=d15868687f79072688a0d0dd1e053721 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 7y 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.

186 points by jamesmunns 7y ago

velcrovan 7y ago

sounds good

ExodusOrbitals1 7y ago

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

jamesmunns 7y 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 7y 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 https://www.rust-lang.org/governance

steveklabnik 7y 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.
hobofan 7y 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.
jamesmunns 7y 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.

thesuperbigfrog 7y 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.

nickpsecurity 7y 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.
- carlmr 7y 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.
- carlmr 7y 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 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.

thenewwazoo 7y 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 7y 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/adaptive/17-03/AUTOSAR_RS_CPP14Guidelines.pdf https://www.autosar.org/fileadmin/user_upload/standards/adap...
- pjmlp 7y ago
  Thanks for providing them, I wasn't aware that AUTOSAR was freely available.
Argorak 7y 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?
hobofan 7y 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 7y 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).

Argorak 7y 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 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&edition=2015&gist=d15868687f79072688a0d0dd1e053721 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 7y 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.