[HN Gopher] High Assurance Rust: Developing Secure and Robust So...
___________________________________________________________________
High Assurance Rust: Developing Secure and Robust Software
Author : sodality2
Score : 110 points
Date : 2022-03-28 10:49 UTC (12 hours ago)
(HTM) web link (highassurance.rs)
(TXT) w3m dump (highassurance.rs)
| beepbooptheory wrote:
| What is the value of Rust's idiosyncrasies, if it takes a book to
| explain how to actually benefit from them? You need to write a
| book to teach one how to do the same in C... is it just that that
| book will be longer?
| pjmlp wrote:
| You can see that for yourself by getting a copy of MISRA C
| standard.
| mprovost wrote:
| It seems strange to me that the author's names aren't on the
| website anywhere except in a BibTeX citation and the open source
| license.
| eminence32 wrote:
| This appears to be an online book (with a physical version
| forthcoming) that will teach you rust with a focus on "building
| performant software we can justifiably trust".
|
| I think this is a learning resource (and not, for example, a more
| formal set of tools to write "high assurance rust").
| maxbond wrote:
| This sort of book is common in the Rust community, eg
| https://doc.rust-lang.org/book/ and https://serde.rs/ are two
| more examples many Rust programmers will come across.
| eminence32 wrote:
| Indeed. But in this case, it took me a while to figure out
| what exactly "high assurance rust" actually is :)
| 13415 wrote:
| Ada/Spark is the standard for high integrity systems. There are
| many things about Rust that make it unsuitable for safety
| critical software at the moment, e.g. lack of formal
| verification, lack of a standard, the fast moving of the compiler
| (it is under constant change), widespread use of dynamic memory
| allocation, etc.
| titzer wrote:
| > The State-of-the-Art in Practical Software Assurance
|
| Unfortunately I cannot take this very seriously, if it is
| completely ignorant of the Spark/Ada ecosystem and presents Rust
| as the "state of the art".
|
| Rust has some nice properties, but there is an _entire field_ of
| programming languages and compilers designed for building safety-
| critical software for aerospace and defense. Unfortunately, it
| looks like that is going to be forgotten, or rather,
| intentionally overwritten by ignorance.
| sodality2 wrote:
| 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.
| Veserv wrote:
| 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 wrote:
| "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.
| goodpoint wrote:
| Rust is not even designed to for safety-critical use.
|
| You need Ada or other languages for that.
| rcxdude wrote:
| Neither's C, but it is extremely common in safety-critical
| software.
| pjmlp wrote:
| I wouldn't call MISRA C still C, it is more like playing
| Ada with C compilers.
| rcxdude wrote:
| 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).
| pjmlp wrote:
| That is why there are companies that do MISRA-C
| certifications.
| a-priori wrote:
| 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 wrote:
| 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...
| rcxdude wrote:
| 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).
| belter wrote:
| 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
| zppln wrote:
| They seem rather ignorant of the safety aspect of high
| assurance software and appear more focused on security. Neither
| of which are ever fully solved at the software level anyway.
| okl wrote:
| > Neither of which are ever fully solved at the software
| level anyway.
|
| And not fully solvable at only the software level.
| exdsq wrote:
| Especially when you see hidden opcodes at the CPU level -
| if you can't trust the hardware how can you trust the
| software?
| jerknextdoor wrote:
| While this submission may be unaware, Ada did make an
| announcement[1] a few weeks back that they are exploring Rust
| for critical applications.
|
| [1] https://blog.adacore.com/adacore-and-ferrous-systems-
| joining...
| okl wrote:
| AdaCore != Ada
| jksmith wrote:
| This. The tyranny of popularity continues with "c" sugared
| languages, among other factors.
| tbonesteaks wrote:
| What languages and compiles are certified for satefy-critical
| software? And how is it decided? That is super interesting, and
| I didn't know it was a thing.
| pjmlp wrote:
| Search for high integrity computing, MISRA, CERT, AUTOSAR.
| estebank wrote:
| When it comes to MISRA C, it is interesting to note how
| many (a majority) of its rules do not apply or have native
| enforcement[1].
|
| You might have also seen the AUTOSTAR Rust in Automotive
| Working Group announcement recently[2].
|
| [1]: https://github.com/PolySync/misra-
| rust/blob/master/MISRA-Rul...
|
| [2]: for some reason the announcement was removed from the
| "News and events" site, https://webcache.googleusercontent.
| com/search?q=cache%3Ahttp... but it is still available as a
| PDF https://www.autosar.org/fileadmin/user_upload/20220308_
| RustW...
| pjmlp wrote:
| Yeah, it is always a matter how serious a MISRA
| certification happens to be made.
|
| It would be great if AUTOSAR would encompass Rust as
| well, currently I think they are only evaluating it.
| exdsq wrote:
| I was really interested in this sort of stuff for a year or two,
| but ended up coming to the conclusion the best thing is to use
| tried-and-tested tools with rigorous standards/practices such as
| C/C++ than theoretically interesting tools like formally verified
| Haskell/Rust. It's just far more practical and there's something
| to be said about those boring tools used in the wild > academic
| creations.
| Ar-Curunir wrote:
| ah yes, tried and tested C/C++ which has tons of memory-safety
| bugs leading to RCEs and more.
| exdsq wrote:
| But you can avoid these by following best practices and using
| tools to find them. These are known knowns and there are
| solutions. The issue with Rust and others is that there are
| so many unknown unknowns, because it hasn't had the same
| number of hours of development time and usage.
|
| Have you ever used a language like Haskell in a formal
| verification environment? You still get memory issues but
| there are far less tools to tackle them.
| zppln wrote:
| I think my problem with writeups like these are that they
| attack the problem from the wrong (or uninteresting) angle.
| Like, say I'm writing software for an airplane then I'm gonna
| be chained to DO-178C. How will using Rust help me achieve all
| the objectives it requires for e.g. Level A? Is Rust gonna get
| me there cheaper (I think it might one day)? Is it gonna enable
| me to build systems that use constructs that I wouldn't have
| dared (due to complexity, safety or whatever)? Of course it's
| kind of hard to present this without a particular system design
| in mind (maybe it's PSAC for an abstract system I'm really
| after...). I suspect the situation is similar when getting some
| kind of security certification/accreditation (haven't seen much
| of that side of the coin). I'm not saying this project isn't
| valuable (it is), I just miss the top-down perspective of the
| language in this context. :)
___________________________________________________________________
(page generated 2022-03-28 23:01 UTC)