6 ms·

This might add some clarifications: https://highassurance.rs/faq.html#7-can-i-use-rust-in-safety-critical-domains https://highassurance.rs/faq.html#7-can-i-use-

This might add some clarifications: https://highassurance.rs/faq.html#7-can-i-use-rust-in-safety-critical-domains https://highassurance.rs/faq.html#7-can-i-use-rust-in-safety... 7. Can I use Rust in safety-critical domains? Not yet. Rust isn't certified for use in a safety-critical setting.

belter 5y ago
Surely the first step should be to push the language and formalize a spec first? Example of a beginning effort: "KRust: A Formal Executable Semantics of Rust"' https://arxiv.org/abs/1804.10806 https://arxiv.org/abs/1804.10806
goodpoint 5y ago
Rust is not even designed to for safety-critical use. You need Ada or other languages for that.
- rcxdude 5y ago
  Neither's C, but it is extremely common in safety-critical software.
  - pjmlp 5y ago
    I wouldn't call MISRA C still C, it is more like playing Ada with C compilers.
    - tialaramex 5y ago
      MISRA: Of course the C language provides loads of standard library functions which look ordinary but are actually defined in a way that's hideously dangerous. You can use most of those but please take care to avoid mistakes (MISRA D4.11). Ada: It would be insane to provide a standard library full of dangerous sharp edges so we didn't do that. pjmlp: See? Practically twins.
    - rcxdude 5y ago
      It's not a very good impression: MISRA C is basically a list of guidelines, half of which say "don't invoke undefined behaviour" (duh) and the other half are questionable coding-style rules. None of it really corresponds to any Ada features (not to mention you basically ignore any MISRA rule you like if you just write down that you've done it and attempt some justification).
      - a-priori 5y ago
        The goal of MISRA C mostly isn't to prevent problems in your code. It's to make the code more amenable to static analysis, which _can_ detect problems.
        woodruffw 5y ago
        Which, notably, is what Rust does by construction: you don't have to do (much) alias or escape analysis against Rust, because it's given to you by the compiler for free. There's also been a decent amount of empirical research on MISRA C's effectiveness, most of which has shown that attempting compliance actually makes programmer-introduced faults more likely[1]. [1]: http://resolver.tudelft.nl/uuid:646de5ba-eee8-4ec8-8bbc-2c188e1847ea http://resolver.tudelft.nl/uuid:646de5ba-eee8-4ec8-8bbc-2c18...
        rcxdude 5y ago
        It's extremely common to use MISRA without static analysis (I would personally advocate for the opposite way around). Also, if the goal is to make static analysis easier, why not just have the rule be 'the static analyser must be able to say this is OK'? (which will depend greatly on what the capabilities of your static analyser are).
      - pjmlp 5y ago
        That is why there are companies that do MISRA-C certifications.
Veserv 5y ago
So they are going to teach a process to consistently make and deliver high assurance, robust systems written in Rust when they knowingly claim that they have never even heard of, let alone made, even a single high assurance, robust system in Rust. This is absolutely ridiculous. Having a process for making high assurance, robust systems is a extraordinary claim which requires the extraordinary evidence of repeated success at delivering such systems in real-life adversarial environments and succeeding at audits and verification efforts that are demonstrably passed only by robust systems. Anybody who has not reached that standard should not use the words “high assurance”, “robust”, or “secure” as they have no evidence of their claims and anything they say should be completely, 100% ignored. It is frankly outrageous that people so far from that standard that they can not even point to a single system that anybody has done have the gall to use those words.
- woodruffw 5y ago
  "Secure," "robust," "high-assurance," etc. are not standard terms with a single agreed upon definition. Like just about anything that concerns computer security, their definitions depend on threat models and maybe a domain-specific specification. I don't particularly care whether a particular flavor of Rust (or C, for that matter) brands itself as "high-assurance," as long as it is not dishonestly claiming compliance with a particular domain's assurance or robustness requirements.
- throwawaygh 5y ago
  > when they knowingly claim that they have never even heard of, let alone made, even a single high assurance, robust system in Rust. Huh?! They said you can't build safety-critical software in Rust because it's not certified. Not all high assurance software is safety-critical, not all correct software is certifiable, and FOR SURE not all certifiable software is correct. > evidence of repeated success at delivering such systems in real-life adversarial environments and succeeding at audits and verification efforts that are demonstrably passed only by robust systems. Can you name one such process? The old auto and aero software standards from the 90s/early aughts are crufty, have demonstrably failed on any number of occasions, and leave much to be desired. (BTW, "verification" in those standards means something totally different from what "verification" means to software experts today.) The Rust compiler and ecosystem would need a thorough audit before its use in safety-critical settings, but I have no doubt that this audit will happen and that when it does the evidence generated y that audit will blow way past the standards applied to MISRA C/Ada/etc.

belter 5y ago

Surely the first step should be to push the language and formalize a spec first? Example of a beginning effort: "KRust: A Formal Executable Semantics of Rust"' https://arxiv.org/abs/1804.10806 https://arxiv.org/abs/1804.10806

goodpoint 5y ago

Rust is not even designed to for safety-critical use. You need Ada or other languages for that.

rcxdude 5y ago
Neither's C, but it is extremely common in safety-critical software.
- pjmlp 5y ago
  I wouldn't call MISRA C still C, it is more like playing Ada with C compilers.
  - tialaramex 5y ago
    MISRA: Of course the C language provides loads of standard library functions which look ordinary but are actually defined in a way that's hideously dangerous. You can use most of those but please take care to avoid mistakes (MISRA D4.11). Ada: It would be insane to provide a standard library full of dangerous sharp edges so we didn't do that. pjmlp: See? Practically twins.
  - rcxdude 5y ago
    It's not a very good impression: MISRA C is basically a list of guidelines, half of which say "don't invoke undefined behaviour" (duh) and the other half are questionable coding-style rules. None of it really corresponds to any Ada features (not to mention you basically ignore any MISRA rule you like if you just write down that you've done it and attempt some justification).
    - a-priori 5y ago
      The goal of MISRA C mostly isn't to prevent problems in your code. It's to make the code more amenable to static analysis, which _can_ detect problems.
      - woodruffw 5y ago
        Which, notably, is what Rust does by construction: you don't have to do (much) alias or escape analysis against Rust, because it's given to you by the compiler for free. There's also been a decent amount of empirical research on MISRA C's effectiveness, most of which has shown that attempting compliance actually makes programmer-introduced faults more likely[1]. [1]: http://resolver.tudelft.nl/uuid:646de5ba-eee8-4ec8-8bbc-2c188e1847ea http://resolver.tudelft.nl/uuid:646de5ba-eee8-4ec8-8bbc-2c18...
      - rcxdude 5y ago
        It's extremely common to use MISRA without static analysis (I would personally advocate for the opposite way around). Also, if the goal is to make static analysis easier, why not just have the rule be 'the static analyser must be able to say this is OK'? (which will depend greatly on what the capabilities of your static analyser are).
    - pjmlp 5y ago
      That is why there are companies that do MISRA-C certifications.

Veserv 5y ago

So they are going to teach a process to consistently make and deliver high assurance, robust systems written in Rust when they knowingly claim that they have never even heard of, let alone made, even a single high assurance, robust system in Rust. This is absolutely ridiculous. Having a process for making high assurance, robust systems is a extraordinary claim which requires the extraordinary evidence of repeated success at delivering such systems in real-life adversarial environments and succeeding at audits and verification efforts that are demonstrably passed only by robust systems. Anybody who has not reached that standard should not use the words “high assurance”, “robust”, or “secure” as they have no evidence of their claims and anything they say should be completely, 100% ignored. It is frankly outrageous that people so far from that standard that they can not even point to a single system that anybody has done have the gall to use those words.

woodruffw 5y ago
"Secure," "robust," "high-assurance," etc. are not standard terms with a single agreed upon definition. Like just about anything that concerns computer security, their definitions depend on threat models and maybe a domain-specific specification. I don't particularly care whether a particular flavor of Rust (or C, for that matter) brands itself as "high-assurance," as long as it is not dishonestly claiming compliance with a particular domain's assurance or robustness requirements.
throwawaygh 5y ago
> when they knowingly claim that they have never even heard of, let alone made, even a single high assurance, robust system in Rust. Huh?! They said you can't build safety-critical software in Rust because it's not certified. Not all high assurance software is safety-critical, not all correct software is certifiable, and FOR SURE not all certifiable software is correct. > evidence of repeated success at delivering such systems in real-life adversarial environments and succeeding at audits and verification efforts that are demonstrably passed only by robust systems. Can you name one such process? The old auto and aero software standards from the 90s/early aughts are crufty, have demonstrably failed on any number of occasions, and leave much to be desired. (BTW, "verification" in those standards means something totally different from what "verification" means to software experts today.) The Rust compiler and ecosystem would need a thorough audit before its use in safety-critical settings, but I have no doubt that this audit will happen and that when it does the evidence generated y that audit will blow way past the standards applied to MISRA C/Ada/etc.