Hacker News Reader

Comment by sodality2 | Hacker News Reader

This might add some clarifications: 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.

View on HN

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.

"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.

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

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

Rust is not even designed to for safety-critical use.

You need Ada or other languages for that.

Neither's C, but it is extremely common in safety-critical software.

I wouldn't call MISRA C still C, it is more like playing Ada with C compilers.

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).

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.

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-2c18...

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).

That is why there are companies that do MISRA-C certifications.

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.

Reply on news.ycombinator.com