>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.
Bringing Rust to Safety-Critical Systems in Space
11–20 of 23 posts
Re: Bringing Rust to Safety-Critical Systems in Space
#12Earlier quoted context omitted.
> 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?
I agree that people mis-use the “formal” word when it comes to specifications.
But on this specific question, https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verif... is the work I am aware of.
Re: Bringing Rust to Safety-Critical Systems in Space
#13Earlier quoted context omitted.
> 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?
WebAssembly is specified in an English prose and a formal notation, as you can see from, for example, [1]. It is still true that a (mathematically) formal specification can suffer from bugs due to the lack of verification, but it is much easier to verify an already formal specification than a prose specification. It is also possible to turn a prose into a formal specification if the prose in question is already close enough to the formal notation, like ESMeta [2].
[1] https://webassembly.github.io/spec/core/valid/instructions.h...
Re: Bringing Rust to Safety-Critical Systems in Space
#14>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?
I am answering this comment from the audience at https://oxidizeconf.com/
There is a growing number of people and organizations that do see Rust as bringing advantages in this area.
That said, your parent isn’t wrong that the safety critical space has developed numerous ways of mitigating the risk of writing software, no matter what language it’s written in. But that doesn’t mean that language is irrelevant.
Re: Bringing Rust to Safety-Critical Systems in Space
#15>>>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…
>The current state of Rust is a moving target for such tools and design methods. Publish a formal language standard first.
Would it be just easier to use something like OCaml? where it offers the memory safety and a mature language.
Re: Bringing Rust to Safety-Critical Systems in Space
#16>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.
I wouldn't dismiss MISRA C so quickly as its guidelines may prove useful when deriving best practices for unsafe Rust.
Re: Bringing Rust to Safety-Critical Systems in Space
#17>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.
Not sure what you’re getting at. We take those rules and use a static analysis tool (LDRA) to prove they are met. You can write unsafe code in any language.
Re: Bringing Rust to Safety-Critical Systems in Space
#18Earlier quoted context omitted.
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.
I'm pretty sure that there are safety critical ARM CPU's and Ferrocene does support ARM.
Re: Bringing Rust to Safety-Critical Systems in Space
#19>>>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.
They tried but they were on the "nightly" branch of the standard and the compiler was on the "release" branch and then the compiler refused to compile the "nightly" standard because "nightly". /s
Re: Bringing Rust to Safety-Critical Systems in Space
#20Very cool project! I am also working on a similar topic as part of my PhD thesis.