Sealed Rust: A plan to bring Rust to safety critical software domains(ferrous-systems.com)
ferrous-systems.com
Sealed Rust: A plan to bring Rust to safety critical software domains
https://ferrous-systems.com/blog/sealed-rust-the-pitch/
7 comments
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.
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...
[1] https://www.autosar.org/fileadmin/user_upload/standards/adap...
Thanks for providing them, I wasn't aware that AUTOSAR was freely available.
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 [email protected]?
> 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?
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?
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.
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.
Interesting. We would love to use Rust instead of legacy aerospace programming languages for our project.
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!
Feel free to reach out at sealed-rust at ferrous-systems.com!
> 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
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
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.
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.
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.
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.
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).
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.
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.
> 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.
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.
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...
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...
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.
Despite being entrenched, Ada needs the competition in the critical systems space. Rust is showing great promise as a competitor.
I have talked to a couple of AdaCore folks personally and the competition is friendly, because Rust brings movement into the space.
We also respect Ada a ton and fundamentally believe that clients having actual choice improves all products.
We also respect Ada a ton and fundamentally believe that clients having actual choice improves all products.
> 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.
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.
> 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.
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.
> Agreed. After what Oracle has done with Java, I am hesitant when corporations come bearing gifts.
I honestly don’t know what to make of that comparison. On one hand, as a sailing fan, I’d love to own a boat competing in the America’s Cup (1), on the other hand I can’t really see why you insult us that way.
On a more serious note: Companies with money will enter (and already have entered) the rust space, but unlike Java which was designed as a proprietary language and never free as open source, the rust language cannot be owned the way oracle owns java. So in that regard I wouldn’t worry. That doesn’t mean that all players will be well intentioned, but the leverage a hostile player can gain is substantially more limited.
(1) The Wannsee certainly would make a great training ground for Team Ferrous!
I honestly don’t know what to make of that comparison. On one hand, as a sailing fan, I’d love to own a boat competing in the America’s Cup (1), on the other hand I can’t really see why you insult us that way.
On a more serious note: Companies with money will enter (and already have entered) the rust space, but unlike Java which was designed as a proprietary language and never free as open source, the rust language cannot be owned the way oracle owns java. So in that regard I wouldn’t worry. That doesn’t mean that all players will be well intentioned, but the leverage a hostile player can gain is substantially more limited.
(1) The Wannsee certainly would make a great training ground for Team Ferrous!
You mean rescuing Java from dying at version 6 and having beers with a market share going into the same size as Delphi or similar?
After Google screwed a deal that could eventually save Sun, and letting it sink afterwards.
Or keeping MaximeVM alive and spending truckloads of money to make it into GraalVM, which also supports the fastest implementation of Ruby?
Maybe it was merging the JIT/AOT compiler from JRockit into GraalVM project and eventually into OpenJDK.
Or even, a infrastructure monitoring system, capable to plug into production systems with very little impact probs.
Yeah Oracle has done a lot of bad stuff to Java.
After Google screwed a deal that could eventually save Sun, and letting it sink afterwards.
Or keeping MaximeVM alive and spending truckloads of money to make it into GraalVM, which also supports the fastest implementation of Ruby?
Maybe it was merging the JIT/AOT compiler from JRockit into GraalVM project and eventually into OpenJDK.
Or even, a infrastructure monitoring system, capable to plug into production systems with very little impact probs.
Yeah Oracle has done a lot of bad stuff to Java.
> I am just concerned about what might happen to the Rust community when truckloads of money gets involved.
Well, either truckloads of money get involved, or the community will fail to grow. I'm sure some people would love to keep the Rust community exactly as they currently enjoy it (for a multitude of different reasons, but I think most of them somewhat selfish), but for Rust to grow, there has to be money involved by the nature of how our economy works.
Either Rust is useful and provides benefit over alternatives, in which case it's also useful and provides benefit for commercial interests, or it isn't.
That isn't to say your concern is entirely unwarranted. It makes sense to be leery about what the money is applied to and how it influences the outcomes, as that isn't in the best interest of the community either.
Well, either truckloads of money get involved, or the community will fail to grow. I'm sure some people would love to keep the Rust community exactly as they currently enjoy it (for a multitude of different reasons, but I think most of them somewhat selfish), but for Rust to grow, there has to be money involved by the nature of how our economy works.
Either Rust is useful and provides benefit over alternatives, in which case it's also useful and provides benefit for commercial interests, or it isn't.
That isn't to say your concern is entirely unwarranted. It makes sense to be leery about what the money is applied to and how it influences the outcomes, as that isn't in the best interest of the community either.
> I am just concerned about what might happen to the Rust community when truckloads of money gets involved.
Ah okay, I can very well understand that concern.
I'm personally not too worried about it, as I feel like Rust already had a bit of a "truckloads of money" moment with the cryptocurrency hype the last 2 years. During that time that sector probably became the biggest one in terms of number of employees working with Rust full-time. I can't say I noticed any significant effects from that in the Rust community. That might in part be due to the fact that your stereotypical Rust developer is very critical of blockchain technology, but I think the Rust community has fared pretty well in that money influx exercise.
Ah okay, I can very well understand that concern.
I'm personally not too worried about it, as I feel like Rust already had a bit of a "truckloads of money" moment with the cryptocurrency hype the last 2 years. During that time that sector probably became the biggest one in terms of number of employees working with Rust full-time. I can't say I noticed any significant effects from that in the Rust community. That might in part be due to the fact that your stereotypical Rust developer is very critical of blockchain technology, but I think the Rust community has fared pretty well in that money influx exercise.
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.
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.
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.
The problem is mostly certification and having a stable spec for the language.
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.
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.
Remember there's tools that can prove absence of or detect many classes of error in C with no runtime checks. RV-Match and Astree Analyzer come to mind. Plus all kinds of test generators and a verified compiler. Plus lots of open tooling to do same thing. Safety-critical vendors buy that kind of stuff more than most C shops. C subset with such tooling is safer and more correct than Rust.
The advantage of Ada and Rust is they're cheaper and faster to get safe code out of. Businesses will like that. I don't know how compiler qualification plays out these days.
The advantage of Ada and Rust is they're cheaper and faster to get safe code out of. Businesses will like that. I don't know how compiler qualification plays out these days.
I'll repeat this from another comment. There are a few things a coding standard like Misra can't do for you.
Lacking a strict type system, discriminated unions, if-expressions (they exist in C but are often discouraged because of readability concerns), match expressions, macros that are AST members, procedural macros, guaranteed mutability restrictions with the borrow checker, etc. are things that a coding rule and analyzer can't bring into a language like C. Most importantly no module system to keep yourself somewhat isolated from third party code that you have no control over.
Add to that that you have humans checking each violation whether they think it will cause problems. Humans fixing these. And in a lot of cases humans not fixing these. Then you're actually still left with a lot of code that a stricter compiler like Rust or Ada would have rejected in the first place.
Lacking a strict type system, discriminated unions, if-expressions (they exist in C but are often discouraged because of readability concerns), match expressions, macros that are AST members, procedural macros, guaranteed mutability restrictions with the borrow checker, etc. are things that a coding rule and analyzer can't bring into a language like C. Most importantly no module system to keep yourself somewhat isolated from third party code that you have no control over.
Add to that that you have humans checking each violation whether they think it will cause problems. Humans fixing these. And in a lot of cases humans not fixing these. Then you're actually still left with a lot of code that a stricter compiler like Rust or Ada would have rejected in the first place.
True, but many companies still try the shortcut of MISRA plus cheaper C devs, than paying for Ada compilers plus more skilled developers.
Your other comment is irrelevant in this subthread, because neither RV-Match nor Astree are coding standards.
Furthermore, there's zero proof that e.g. macros, match or variant types have any impact on code quality. Bringing the module system into this is really grasping at straws.
Furthermore, there's zero proof that e.g. macros, match or variant types have any impact on code quality. Bringing the module system into this is really grasping at straws.
Where did you get this 80%/20% figures from?
Rough numbers from experience of what these analyzers discover and what actually turns out to be a bug, vs. What rust keeps you from doing out of the box. I could have said a lot or a little, but I wanted to convey an idea of how much and how little.
Lacking a strict type system, discriminated unions, if-expressions (they exist in C but are often discouraged because of readability concerns), match expressions, macros that are AST members, procedural macros, guaranteed mutability restrictions with the borrow checker, etc. are things that a coding rule and analyzer can't bring into a language like C. Most importantly no module system to keep yourself somewhat isolated from third party code that you have no control over.
Add to that that you have humans checking each violation whether they think it will cause problems. Humans fixing these. And in a lot of cases humans not fixing these. Then you're actually still left with a lot of code that à stricter compiler like Rust or Ada would have rejected in the first place.
Lacking a strict type system, discriminated unions, if-expressions (they exist in C but are often discouraged because of readability concerns), match expressions, macros that are AST members, procedural macros, guaranteed mutability restrictions with the borrow checker, etc. are things that a coding rule and analyzer can't bring into a language like C. Most importantly no module system to keep yourself somewhat isolated from third party code that you have no control over.
Add to that that you have humans checking each violation whether they think it will cause problems. Humans fixing these. And in a lot of cases humans not fixing these. Then you're actually still left with a lot of code that à stricter compiler like Rust or Ada would have rejected in the first place.
How does Rust compare to Spark/Ada?
I don't know them well enough to compare. Haven't been coding in a while. Best resource on Ada to do that comparison is Barnes:
https://www.adacore.com/books/safe-and-secure-software
SPARK is a subset without pointers that feeds information about the program into solvers that prove absence of common classes of errors like overflows and divide by zero. Inspired by Rust, recent work is adding pointers. Praxis' Correct-by-Construction defaulted on Ada with SPARK saved for most critical stuff, esp safety- or security-enforcing.
Right now, Rust is mainly ahead of Ada on dealing with the pointer safety and better safe concurrency. Ada's Ravenscar aimed for safety but was restrictive. That's my take.
https://www.adacore.com/books/safe-and-secure-software
SPARK is a subset without pointers that feeds information about the program into solvers that prove absence of common classes of errors like overflows and divide by zero. Inspired by Rust, recent work is adding pointers. Praxis' Correct-by-Construction defaulted on Ada with SPARK saved for most critical stuff, esp safety- or security-enforcing.
Right now, Rust is mainly ahead of Ada on dealing with the pointer safety and better safe concurrency. Ada's Ravenscar aimed for safety but was restrictive. That's my take.
Like nichsecurity states, Rust is ahead in pointer safety, but that is being taken care for Ada 2020, even if just a subset.
Ada/SPARK wins in almost everything else, it has multiple implementations, proven industrial use since early 80's (first standard was in 1983), IDE tooling, it is a common theme in high security computing conferences, libraries for safety critical domains, and people that know the language.
Naturally it has a price disadvantage for FOSS devs that are allergic to GNAT, given that the remaining Ada compilers are well into the enterprise price range.
Ada/SPARK wins in almost everything else, it has multiple implementations, proven industrial use since early 80's (first standard was in 1983), IDE tooling, it is a common theme in high security computing conferences, libraries for safety critical domains, and people that know the language.
Naturally it has a price disadvantage for FOSS devs that are allergic to GNAT, given that the remaining Ada compilers are well into the enterprise price range.
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)
I don't see how delaying would help in the long run.
(Full disclosure: I'm MD at Ferrous Systems)
sounds good