8 ms·

High Assurance Rust: Developing Secure and Robust Software

120 points by sodality2 5y ago

eminence32 5y 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 5y ago
  This sort of book is common in the Rust community, eg https://doc.rust-lang.org/book/ https://doc.rust-lang.org/book/ and https://serde.rs/ https://serde.rs/ are two more examples many Rust programmers will come across.
  - eminence32 5y ago
    Indeed. But in this case, it took me a while to figure out what exactly "high assurance rust" actually is :)
titzer 5y 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.
- tnballo 5y 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 https://www.youtube.com/watch?v=2YoPoNx3L5E [2] https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memory-Management-in-Ada-and-SPARK.pdf https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo... [3] https://www.eurekalert.org/news-releases/610682 https://www.eurekalert.org/news-releases/610682
- sodality2 5y ago
  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
- zppln 5y 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.
  - okl 5y ago
    > Neither of which are ever fully solved at the software level anyway. And not fully solvable at only the software level.
    - exdsq 5y ago
      Especially when you see hidden opcodes at the CPU level - if you can't trust the hardware how can you trust the software?
- jerknextdoor 5y 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-forces-to-support-rust https://blog.adacore.com/adacore-and-ferrous-systems-joining...
  - okl 5y ago
    AdaCore != Ada
- tbonesteaks 5y 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.
  - pjmlp 5y ago
    Search for high integrity computing, MISRA, CERT, AUTOSAR.
    - estebank 5y ago
      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-Rules.md 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%3Ahttps%3A%2F%2Fwww.autosar.org%2Fnews-events%2Fdetails%2Fautosar-announces-new-working-group-for-programming-language-rust-in-automotive-software-context-202%2F https://webcache.googleusercontent.com/search?q=cache%3Ahttp... but it is still available as a PDF https://www.autosar.org/fileadmin/user_upload/20220308_RustWorkingGroup_Announcement_EN.pdf https://www.autosar.org/fileadmin/user_upload/20220308_RustW...
      - pjmlp 5y ago
        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.
- jksmith 5y ago
  This. The tyranny of popularity continues with "c" sugared languages, among other factors.
exdsq 5y 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.
- zppln 5y 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. :)
  - tnballo 5y 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.
    - zppln 5y ago
      Well, in my experience it is possible to claim Level A despite not using a certified compiler. Perhaps not if you're building a civilian airliner and you're probably still gonna have to do some kind of activities to show what goes into the compiler comes out as expected. So although certification may be an ultimate goal, I don't think I'd consider it to be a complete showstopper when it comes to getting Rust airborne and keeping whatever it executes on so. :)
beepbooptheory 5y 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?
- pjmlp 5y ago
  You can see that for yourself by getting a copy of MISRA C standard.
mprovost 5y 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.
- tnballo 5y ago
  There is an "About the Team" page in Chapter 1 with short bios: https://highassurance.rs/chp1/about_the_team.html 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 5y 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.

120 points by sodality2 5y 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 5y ago
This sort of book is common in the Rust community, eg https://doc.rust-lang.org/book/ https://doc.rust-lang.org/book/ and https://serde.rs/ https://serde.rs/ are two more examples many Rust programmers will come across.
- eminence32 5y ago
  Indeed. But in this case, it took me a while to figure out what exactly "high assurance rust" actually is :)

titzer 5y 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.

tnballo 5y 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 https://www.youtube.com/watch?v=2YoPoNx3L5E [2] https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memory-Management-in-Ada-and-SPARK.pdf https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo... [3] https://www.eurekalert.org/news-releases/610682 https://www.eurekalert.org/news-releases/610682
sodality2 5y ago
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
zppln 5y 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.
- okl 5y ago
  > Neither of which are ever fully solved at the software level anyway. And not fully solvable at only the software level.
  - exdsq 5y ago
    Especially when you see hidden opcodes at the CPU level - if you can't trust the hardware how can you trust the software?
jerknextdoor 5y 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-forces-to-support-rust https://blog.adacore.com/adacore-and-ferrous-systems-joining...
- okl 5y ago
  AdaCore != Ada
tbonesteaks 5y 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.
- pjmlp 5y ago
  Search for high integrity computing, MISRA, CERT, AUTOSAR.
  - estebank 5y ago
    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-Rules.md 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%3Ahttps%3A%2F%2Fwww.autosar.org%2Fnews-events%2Fdetails%2Fautosar-announces-new-working-group-for-programming-language-rust-in-automotive-software-context-202%2F https://webcache.googleusercontent.com/search?q=cache%3Ahttp... but it is still available as a PDF https://www.autosar.org/fileadmin/user_upload/20220308_RustWorkingGroup_Announcement_EN.pdf https://www.autosar.org/fileadmin/user_upload/20220308_RustW...
    - pjmlp 5y ago
      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.
jksmith 5y ago
This. The tyranny of popularity continues with "c" sugared languages, among other factors.

exdsq 5y 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.

zppln 5y 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. :)
- tnballo 5y 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.
  - zppln 5y ago
    Well, in my experience it is possible to claim Level A despite not using a certified compiler. Perhaps not if you're building a civilian airliner and you're probably still gonna have to do some kind of activities to show what goes into the compiler comes out as expected. So although certification may be an ultimate goal, I don't think I'd consider it to be a complete showstopper when it comes to getting Rust airborne and keeping whatever it executes on so. :)

beepbooptheory 5y 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?

pjmlp 5y ago
You can see that for yourself by getting a copy of MISRA C standard.

mprovost 5y 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.

tnballo 5y ago
There is an "About the Team" page in Chapter 1 with short bios: https://highassurance.rs/chp1/about_the_team.html 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 5y 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.