High Assurance Rust: Developing Secure and Robust Software

by sodality2 • 4 years ago

120 41 4 years ago

eminence322• 4 years ago

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• 4 years ago

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.

eminence322• 4 years ago

Indeed. But in this case, it took me a while to figure out what exactly "high assurance rust" actually is :)

titzer• 4 years ago

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• 4 years ago

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.

belter• 4 years 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

goodpoint• 4 years ago

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

You need Ada or other languages for that.

Veserv• 4 years 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.

zppln3• 4 years ago

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.

okl2• 4 years ago

Neither of which are ever fully solved at the software level anyway.

And not fully solvable at only the software level.

jerknextdoor• 4 years ago

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

okl2• 4 years ago

AdaCore != Ada

tbonesteaks• 4 years ago

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.

pjmlp5• 4 years ago

Search for high integrity computing, MISRA, CERT, AUTOSAR.

jksmith• 4 years ago

This. The tyranny of popularity continues with "c" sugared languages, among other factors.

tnballo3• 4 years ago

Author of the book here, thank you for your feedback!

Though not an Ada expert, I have used the SPARK subset. And I’ve worked on security assessment of military systems with components written in Ada. Although we looked at binaries and not source code, because our assurance model did not consider the Ada compiler to be part of the chain of trust (so we test the artifact the CPU will execute). I really like Ada and hope to use more of it in the future!

The HN community may be interested in this 1 hour presentation [1] on Nvidia's adoption of Ada, including why they chose it over Rust in 2019 (regulatory certification was one factor). There’s also a great academic paper [2] on the recent advances SPARK has made in heap memory verification, inspired in part by Rust’s type system.

There are currently efforts underway to certify Rust for usage in safety critical systems via an alternate, certified toolchain (among other pieces of the puzzle). Two related initiatives are linked through in FAQ question #7 (which someone already shared). I’ll be sure to add the Ferrous Systems and AdaCore collaboration when I have a chance to batch together some updates.

I, like many others, believe Rust is a technology that can deliver value in safety and mission critical verticals due to reduction in undefined behavior via principled static analysis (a type system for which there has been early success in formal verification of safety claims[3]). Looking forward to digging into Rust research tools for deductive verification in a later chapter(similar to SPARK - hand-written Hoare logic specifications, proven via SMT solving at compile-time).

We make comparisons to C and C++ in the book because they are the closest relatable analog for many developers. But I’m happy to add mention of Ada to not alienate potential readers like yourself, though my Ada knowledge is not currently deep enough to provide in-depth comparison.

This book is a best effort and an early-stage passion project. It strives to be technically accurate and data driven while remaining approachable to a range of readers. Like others have mentioned on this thread, this book does not claim to provide guidance for adherence with any particular standard or certification process. Although Chapter 3 does map concepts from MISRA C 2012 to Rust, in order to remain grounded in realistic, industry-adopted best practices.

The goal is to help readers build more secure and reliable software in general, to the furthest extent possible using entirely open-source tools. I look forward to iterating the content to meet high standards of quality, while keeping the entirety of the book freely available online.

Always open to critique and suggestions, thanks again!

[1] https://www.youtube.com/watch?v=2YoPoNx3L5E

[2] https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo...

[3] https://www.eurekalert.org/news-releases/610682

exdsq3• 4 years ago

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.

zppln3• 4 years ago

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

tnballo3• 4 years ago

Thank you for this perspective, it's one I'll try to incorporate more of in a future revision.

While the content aims to be generally applicable to a broad range of software, further contextualization against a specific standard like DO-178C might make for a valuable appendix section.

There's a bit of a balancing act, however, since Rust is, at present, not a certified choice for such use cases.

Ar-Curunir2• 4 years ago

ah yes, tried and tested C/C++ which has tons of memory-safety bugs leading to RCEs and more.

exdsq3• 4 years ago

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.

beepbooptheory• 4 years ago

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?

pjmlp5• 4 years ago

You can see that for yourself by getting a copy of MISRA C standard.

mprovost• 4 years ago

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.

tnballo3• 4 years ago

There is an "About the Team" page in Chapter 1 with short bios:

https://highassurance.rs/chp1/about_the_team.html

As a personal preference, I like to place the content front-and-center and not dwell on the individuals behind it :)

13415• 4 years ago

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.

High Assurance Rust: Developing Secure and Robust Software

Related Stories