Bringing Rust to Safety-Critical Systems in Space
1–10 of 23 posts
Re: Bringing Rust to Safety-Critical Systems in Space
#2>>>However, due to its relatively short lifespan, industry adaption in safety-critical environments is still lacking. This work provides a set of recommendations for the development of safety-critical space systems in Rust.
Why wouldn't they use Ada/SPARK2014? They have a published language standard, verification tools, and 25 years of applied use for mission-critical, high-integrity software.
The current state of Rust is a moving target for such tools and design methods. Publish a formal language standard first.
Re: Bringing Rust to Safety-Critical Systems in Space
#3>>>However, due to its relatively short lifespan, industry adaption in safety-critical environments is still lacking. This work provides a set of recommendations for the development of safety-critical space systems in Rust. Why wouldn't they use Ada/SPARK2014? They have a published language standard, verification tools, and 25 years of applied use for mission-critical, high-integrity software. The current state of Ru…
There is a qualified and formally verified compiler called ferrocene [1].
Re: Bringing Rust to Safety-Critical Systems in Space
#4>>>However, due to its relatively short lifespan, industry adaption in safety-critical environments is still lacking. This work provides a set of recommendations for the development of safety-critical space systems in Rust. Why wouldn't they use Ada/SPARK2014? They have a published language standard, verification tools, and 25 years of applied use for mission-critical, high-integrity software. The current state of Ru…
There is a qualified and formally verified compiler called ferrocene [1]. [1]: https://ferrocene.dev/en/
Ferrocene notably doesn't support any safety critical CPUs in its current qualification, and those that are experimental only support bare metal. It's exciting, but not at quite the same level of maturity yet.
Re: Bringing Rust to Safety-Critical Systems in Space
#5>>>However, due to its relatively short lifespan, industry adaption in safety-critical environments is still lacking. This work provides a set of recommendations for the development of safety-critical space systems in Rust. Why wouldn't they use Ada/SPARK2014? They have a published language standard, verification tools, and 25 years of applied use for mission-critical, high-integrity software. The current state of Ru…
There is a qualified and formally verified compiler called ferrocene [1]. [1]: https://ferrocene.dev/en/
Nit: it's formally specified, not formally verified (which is a really rare and difficult feat in comparison).
Re: Bringing Rust to Safety-Critical Systems in Space
#6>>>However, due to its relatively short lifespan, industry adaption in safety-critical environments is still lacking. This work provides a set of recommendations for the development of safety-critical space systems in Rust. Why wouldn't they use Ada/SPARK2014? They have a published language standard, verification tools, and 25 years of applied use for mission-critical, high-integrity software. The current state of Ru…
> Publish a formal language standard first.
You don't need a formal language standard to make Rust usable for safety-critical areas. You do need a formally specified language for the certification, but it doesn't have to be official because heck, you need much more than a mere formally specified language anyway as you've just said. An expanded version of Ferrocene would just fit the bill for example.
I think some people are obsessed about the "formal" specification or the language "standard" because they are misunderstanding their effects. They are absolutely nothing without additional supports. A "formal" specification in this context is not really mathematically formal (like, say, WebAssembly [1]); it merely means that a specification is written in clearly defined terms and logically decomposable statements. A language "standard" is useless if it isn't or can't be enforced, and it doesn't even require the (non-mathematical) formality (though most standard organizations would demand that). As for now, the Rust language specification is "formal" and "standard" enough to be useful for language users, while it remains useful for third-party implementors but they can still find some gaps here and there.
Re: Bringing Rust to Safety-Critical Systems in Space
#7>Its language characteristics make it trivial to accidentally introduce memory safety issues resulting in undefined behavior or security vulnerabilities.
I worked for a space-related defense contractor. They are using MISRA C, and everything is very thoroughly designed, documented, and tested. I haven’t seen any research into bugs in safety critical systems caused by memory safety issues, but I think that in practice it is very possible to write memory safe C code if you follow industry standards.
Re: Bringing Rust to Safety-Critical Systems in Space
#8>Its language characteristics make it trivial to accidentally introduce memory safety issues resulting in undefined behavior or security vulnerabilities. I worked for a space-related defense contractor. They are using MISRA C, and everything is very thoroughly designed, documented, and tested. I haven’t seen any research into bugs in safety critical systems caused by memory safety issues, but I think that in practice…
Just curious: do you see any issues with concurrency or anything else rust would help with, or is it domain knowledge related issues?
Re: Bringing Rust to Safety-Critical Systems in Space
#9>Its language characteristics make it trivial to accidentally introduce memory safety issues resulting in undefined behavior or security vulnerabilities. I worked for a space-related defense contractor. They are using MISRA C, and everything is very thoroughly designed, documented, and tested. I haven’t seen any research into bugs in safety critical systems caused by memory safety issues, but I think that in practice…
Skimming MISRA C, it seems to be a collection of either extremely limiting or ineffectual directives. An example of each:
> Dir 4.12 Dynamic memory allocation shall not be used
> Rule 2.2 There shall be no dead code
https://github.com/sakura1083841400/MISRA-C/blob/main/MISRA%...
This provides nothing approaching the guarantees of safe Rust, as far as I can tell.
Re: Bringing Rust to Safety-Critical Systems in Space
#10>>>However, due to its relatively short lifespan, industry adaption in safety-critical environments is still lacking. This work provides a set of recommendations for the development of safety-critical space systems in Rust. Why wouldn't they use Ada/SPARK2014? They have a published language standard, verification tools, and 25 years of applied use for mission-critical, high-integrity software. The current state of Ru…
> Publish a formal language standard first. You don't need a formal language standard to make Rust usable for safety-critical areas. You do need a formally specified language for the certification, but it doesn't have to be official because heck, you need much more than a mere formally specified language anyway as you've just said. An expanded version of Ferrocene would just fit the bill for example. I think some peo…
The linked spec of wasm is written in English. Can we even say it's "formal"?
Did anyone specify wasm using something like Coq, Lean or Isabelle/HOL?