6 ms·

> 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

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

by titzer 5y ago

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.