7 ms·
Making robust software: the “Mars Code” talk (2012)
- noselasd 11y agoThere's also some similar talks/presentations on various topics related to software development for spacecrafts from the yearly Flight Software Workshop at APL: http://flightsoftware.jhuapl.edu/ http://flightsoftware.jhuapl.edu/
- adrianN 11y agoI wonder how much easier it would be to write the software in a language other than C/C++. Ada has a pretty mature toolchain for security critical software development. Where I work we still use C++, but mostly for political reasons. Rust also seems more suited for security critical engineering.
- seanmcdirmid 11y agoAt that level of reliability, language matters surprisingly little since everything is heavily tested, reviewed, hand verified, etc... Language safety is a cheap high-value solution, but might not make sense when coupled with other more expensive safety solutions (imagine wearing a simple seatbelt with a complete safety harness, they aren't additive). C/C++ have other benefits: minimal abstraction, lots of trained up talent.
- _yosefk 11y agoIf there are no bugs, you're right. However, every bug that does ship becomes harder to debug, and so does every bug you fight with during development. The impact of bugs becomes more severe and less predictable on average (dangling reference or buffer overflow can affect pretty much anything.) The more accurate analogy is seatbelts' utility in a car fitted with various collision avoidance devices all the way up to fully autonomous driving. I say you'd still want the seatbelt for when collision does occur after all.
- seanmcdirmid 11y agoAgain, the assurances you get from a seatbelt are dwarfed by the safety harness, they aren't additive. That is, you are going to have to check everything very carefully anyways, anything that allows you to be less careful then isn't very useful, and can actually be counterproductive. Continuing the analogy, the cheap seatbelt kills you when combined with a fancy safety harness/ejection system; it isn't helping, and it can actually hurt.
- adrianN 11y agoI agree that the resulting quality doesn't really depend on language choice. I just wonder about the development cost. For example, a lot of time can be spent reviewing code and checking that no unsafe constructs are used. A safe language makes that unnecessary. Some of those checks can be automated, but in my experience there is still a lot of manual checking going on. I think that the main advantage of C/C++ is the number of people who speak it. But my guess is that the time to train a competent programmer in a safe language can be easily saved in improved productivity.
- duhast 11y agoWhat safer languages you would recommend?
- draven 11y agoHe mentionned Ada and Rust in his initial comment.
- notalaser 11y agoThe main advantage of C (and, to a lesser, but still very significant degree, C++) in this field -- besides the number of people who speak it -- is the availability of a great deal of mature, well-tested compilers, static analysis tools and so on. We have about 40 years of experience writing C compilers today (and we still screw it up sometimes; C++ is... well, I mean, we have about 30 years of experience writing C++ compilers, but those are still in the "mostly right" state). Many subtleties of the language are well understood and many problems have had idiomatic, well-known, widely-used solutions for decades now. Ada would be a good choice for such projects but for the relative flimsiness of its ecosystem. It's a great language, but its development is fairly underfunded, and back when all this stuff was happening, its future was very uncertain (it still is, I guess). And when I say "fairly underfunded" and with a "very uncertain" future, you should understand that I mean "it used to be funded by the DoD, but with various levels of commitment" and "only a few companies, most of them government contractors, and maybe a few state institutions along with a small, but enthusiastic community were pushing for it". Its fame on HN and Reddit may not indicate it, but Rust fares even worse in this regard. Ten years from now, Rust may not even exist anymore. It's not only about technical merit. Projects like these would benefit a lot from being written in Ada (and Rust, too, I guess -- it's a great language), provided that there were such a well-developed ecosystem around either of them. But there isn't. E.g. when choosing their static analysis tools, these guys settled for the top 5 solutions. Top 5! They evaluated a bunch of programs and settled for the best 5. I don't think there are 5 static analysis solutions for Rust in total (and I'm pretty sure there are only two or three for Ada that have been maintained after 1999 or so).
- Sir_Cmpwn 11y agoC is the most widely used and deployed language in the world and it has a very long tenure. I would trust it much more with billions of dollars at stake than a less proven language like Rust. And as a C programmer, it's really not a bad language, and it makes sense for this application.
- deleted 11y ago[deleted]
- annnnd 11y agoExactly. Rust is great for deployments which can't afford such rigorous testing processes; for NASA however any abstraction above the bare minimum is just another risk.
- detaro 11y agoAnd still: The second was a software bug which led to a wrong file being deleted as part of regular housekeeping activities. The fix was straightforward and was applied and the MSL continues its investigation of life on Mars. (end of the article)
- duhast 11y agoI wonder: why this publicly funded code isn't available for download on GitHub or NASA website. Is this because Russians and Chinese can "steal" it and send another Curiosity to Mars?
- adrianN 11y agoIt probably contains lots of proprietary code to interface with the hardware.
- duhast 11y agoHardware was also funded by tax payers.
- humanrebar 11y agoNot a complete answer, but certain kinds of NASA tech undoubtedly has military applications. https://en.wikipedia.org/wiki/International_Traffic_in_Arms_Regulations https://en.wikipedia.org/wiki/International_Traffic_in_Arms_... I think your question is valid nonetheless, especially for the USPS, Dept. of Education, etc.
- fatlasp 11y agoThis. I work at a space research lab and we can't even let many of our employees view mission code; let alone the public. Violating export controls in any way could cost us our funding
- dimman 11y agoAnyone else than me (as a C programmer) that felt like: "Nice, most things mentioned are how I prefer to do it anyway"?
- efaref 11y ago> For example, coding standard says every "case" statement has to have a "default" switch. grep "case", grep "default", and you get wildly different numbers! I hope that's an error in the document. I assume they meant "$(grep -r 'switch (' . | wc -l) != $(grep -r 'default:' . | wc -l)".
- noselasd 11y agoIt's a summary of the talk at https://vimeo.com/84991949 https://vimeo.com/84991949 , where Holzmann just mentions the use of grep verbally, not giving the exact commands to run.
- deleted 11y ago[deleted]
- atsaloli 11y agoArticle author here. I'm a sysadmin so my programming mind may have translated "switch" (C) to "case" (bash). Fixed. Thanks for the catch!
- SeanDav 11y ago> "The color coding green/yellow/red had a psychological effect. The software developers worked really hard to make all the buttons go green." There is a possible risk element of Cargo Cult'ing here. I would hope that all programmers understood why the buttons weren't green. It sounds like they would have, having been certified, and in an environment that lives and breathes code safety, but it is always worth being aware that metrics like that can have hidden consequences.
- atsaloli 11y agoDr Holzmann's "The Power of 10: Rules for Developing Safety-Critical Code" was published in June 2006 issue of IEEE Computer Society "Computer" magazine. It is a small standard, easy to understand and remember; mechanically verifiable; and measurably effective. http://spinroot.com/gerard/pdf/P10.pdf http://spinroot.com/gerard/pdf/P10.pdf
- codemac 11y agoThe only one odd here for me is the ban on de-referencing more than one level. Even a simple linked list implementation uses double pointers to reset parent nodes.. Does anyone have insight into the risk in static analysis? Seems like it would be handled by whatever logic was handling normal pointer derefs. Seems like the only argument is the one against function pointers, which is a pretty amazing thing to ban but at least provides logic WRT static analysis.
- FLUX-YOU 11y agoWhen you can't use recursion, what data structures/algorithms do you use in place of the common data structures that often use recursion? I'm thinking of stuff like trees and quicksort. Do they even need these things?
- pieceof314 11y agoLoops. A recursive algorithm can be transformed into an iterative looping algorithm that uses a fixed stack of memory. There's probably no change in the algorithms. They just use non-recursive versions.
- marcosdumay 11y agoWhat's the gain? If you turn your recursive algorithm into an iterative one with a stack, you are sill subject to all the same problems. They probably don't use trees and quicksort at all.
- deleted 11y ago[deleted]
- ktRolster 11y ago> What's the gain? You can prove that you won't have a stack overflow. You can calculate the maximum depth of the stack at compile time, not runtime.
- dclowd9901 11y agoCan't you also just pass a bit through the recursion that contains its depth, and halt the recursion if that number gets too high?
- ktRolster 11y agoYes, but that depends on making sure you get the programming logic correct, whereas with banning recursion outright, it can be tested automatically.
- oxplot 11y ago> For example, coding standard says every "switch" statement has to have a "default" case. grep "switch", grep "default", and you get wildly different numbers! Standards were not being followed. Are they implying that MSL is the first time they used automated code checks?
- Tibbes 11y agoFor those interested in the "Static Source Code Analysis" section, "Semil" is a typo for "Semmle" [1] [1]: https://semmle.com/customers/code-exploration-at-nasa/ https://semmle.com/customers/code-exploration-at-nasa/
- nickpsecurity 11y agoVery good read. Thanks for submitting it. I like that there's significant overlap in the list in the summary and the list I produced of examples of techniques for improving software quality: http://pastebin.com/xZ6m4T8Z http://pastebin.com/xZ6m4T8Z Further validates those aspects of my list. I'll keep recommending them. Most tools and the rule list are available but I see no link for scrub on his website. Is it not going to be freely distributed or just not ready for public release? More tools for code review that are field-proven is A Good Thing to have.
- atsaloli 11y agoYay! Glad you enjoyed it.