Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Rules for Writing Safety Critical Code (2006)

spinroot.com

Post reply on HN
Print view View original

71–80 of 82 posts

Re: Rules for Writing Safety Critical Code (2006)

#71

Post by qznc »

kccqzy wrote: post #6
huhtenberg wrote: post #3

An opinionated and needlessly specific list. For example, this Use minimally two assertions per function on average should've been Assert your invariants And this Do not use goto statements is a controversial advice at best, because there are several well-established goto-based patterns that produce a much cleaner code.

I would also say perhaps avoid recursion should be revised to avoid non-tail-call recursion Because the justification to avoid recursion is basically avoid running into the limit of stack, and tail-call recursion uses no stack space at all. Of course you still might end up with situations where the function does not terminate, but simple loops can do that too. In relation to Rule No.2, it is also possible to prove an…

In safety critical projects people often disable compiler optimizations. No tail call elimination.

Re: Rules for Writing Safety Critical Code (2006)

#72

Post by nstj »

mos_basik wrote: post #60
nstj wrote: post #27

Earlier quoted context omitted.

Space software? Nice! Going to check out MISRA now. FWIW the initial page just reflects the JPL publication "The Power of Ten – Rules for Developing Safety Critical Code" by Gerard Holzmann [0] [0]: http://spinroot.com/gerard/pdf/P10.pdf

Gerard Holzmann is the main author of the formal software verification tool "spin" as well as the owner of spinroot.com. I took a class on formal verification under him at Caltech.

I probably should have clicked around a bit to determine that he is the owner of that site :)

Re: Rules for Writing Safety Critical Code (2006)

#73

Post by achou »

Rules like this are much more useful if they're enforced. That's why efforts like the C Secure Coding Rules[1], which were designed with the capabilities of reasonably state of the art analyzers in mind, are a good idea. Like any standard designed by a committee, there are some unfortunate compromises.

Many commercial (and open source) static analyzers will have checks that are hard to codify in rules that are digestible by humans. For example, most analyzers that use sophisticated interprocedural analysis will not be easily described as a guideline for humans, unless those humans are compiler engineers. This is especially true for analyzers that have heuristics built in to minimize false positives, which is most often a real-world requirement.

[1] https://www.securecoding.cert.org/confluence/pages/viewpage....

Re: Rules for Writing Safety Critical Code (2006)

#74

Post by kazinator »

pjc50 wrote: post #58
vbtemp wrote: post #55

Why not just call it "Rules for Writing Code"? Who would ever, for example, consider checking the return value of some function but then think "ah, this isn't safety critical, I'm just skip writing a quick _if_ statement and then leave this as a place that mysterious bugs can arise"? Same thing with assertions.

Have you met programmers? Less snarkily, there are billions of lines of production code that don't check return values for malloc(), printf(), and so on because those failures are extremely rare and difficult to handle sensibly. Banning dynamic allocation would ban large areas of programming language - Lisp, Python, Javascript, and so on.

Even if you check the return value of malloc, that doesn't help when virtual memory is overcommitted. Malloc gets a valid pointer from mmap, but accessing the memory later crashes.

A system OOM may actually show a soft behavior, whereby the whole system thrashes more and more until it grinds to a halt. Whatever your program does is futile and irrelevant.

To QA the program for how it handles null out of malloc, you need to tweak the setup: disable overcommit and simulate low memory conditions. (Or even just switch to an alternative allocator that simulates failures.)

Checking the result of malloc for null is of course good for maximal portability: your code can be reused where the check actually means something.

Checking for null and not testing that logic is almost no better than not testing at all (in keeping with the general hypothesis that untested code is junk).

Re: Rules for Writing Safety Critical Code (2006)

#75

Post by jhomedall »

vbtemp wrote: post #59
4ad wrote: post #56

Earlier quoted context omitted.

Because these rules have a cost, and sometimes the cost is not worth it for non-safety critical code. It would be a PITA for general purpose code to avoid all dynamic memory allocation.

With the sole exception of item (3) in that list (pertaining to dynamic allocation), which others carry a cost?

Not allowing recursion makes functional programming impossible.

Giving all loops a fixed upper bound comes at a cost to code readability (consider the example of traversing a linked list, as given in the article).

Re: Rules for Writing Safety Critical Code (2006)

#76

Post by Animats »

wizeman wrote: post #30
michaelt wrote: post #22

Rules like avoiding recursion and loop upper bounds are partly justified by helping code analyzers to prove executions are bounded. Does anyone have experience performing formal static analysis on code? And if so, are there any open-source examples of the state-of-the-art tools being used on nontrivial problems? I've been looking at this recently, but I've never seen a proof of reasonably standard function like, say,…

Take a look at dafny [1] and F* [2]. Both are open-source and it appears that both of them are able to prove code to be correct with considerably less proof code than traditional interactive theorem provers (such as Coq or Isabelle), mostly thanks to the use of an SMT solver (Z3, in both cases) to aid in proving. Both languages are being used in Project Everest [3], which is building a formally verified HTTPS stack,…

"F star is an ML-like functional programming language aimed at program verification. Its type system includes polymorphism, dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F star type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F star can be translated to OCaml or F# for execution."

And you wonder why you're not getting any traction.

Dafny, though, seems to have the right idea.

Re: Rules for Writing Safety Critical Code (2006)

#77

Post by mrlyc »

When I was writing safety-critical embedded programs for medical equipment and an air traffic control system, I found MISRA (https://en.wikipedia.org/wiki/MISRA_C) and Lutz's "Targeting Safety-Related Errors During Software Requirements Analysis" (http://trs-new.jpl.nasa.gov/dspace/bitstream/2014/35179/1/93...) useful.

Re: Rules for Writing Safety Critical Code (2006)

#78

Post by nickpsecurity »

JoachimSchipper wrote: post #70
naasking wrote: post #54

Earlier quoted context omitted.

seL4 is the big one: https://sel4.systems/ Here's a general reference of open source microkernel operating systems: http://www.microkernel.info/ Here's a general reference for open source real time operating systems: http://www.osrtos.com/

seL4 is really sexy, but I don't think it's anywhere near the most-used one?

OKL4 if we're going with the phone example. They stopped open-sourcing it by version 4.0 but someone should be able to dig up OKL4 3.0 somewhere.

Re: Rules for Writing Safety Critical Code (2006)

#79

Post by danjayh »

ti32x wrote: post #21

I work on software that goes to space. I believe we and NASA use the MISRA coding standard, which is effectively this but taken to extremes. If you actually want to create safety critical code I would recommend that you familiarize yourself with the MISRA ruleset and DO-178B.

I work for your friendly Aviation megacorp producing avionics-related widgets. We are currently transitioning to DO-178C. Fun anecdote: I took a training class on Peach Fuzzer last year & got to hear people from MS, Mozilla, etc. talk about the testing they do on their software. I asked them if they ever had to prove things like worst-case execution time, worst-case stack utilization, perform MC/DC analysis, perform source-to-object analysis, etc., etc. They did not ... and that, my friends, is why avionics software is so damned expensive compared to other software :)

EDIT: And to those of you debating whether all of these rules are necessary and good -- they are; however, they are a subset. We use an internal coding standard that resembles MISRA C but does have some modifications. The only rule of his that we don't do nearly the same way is the 60 line limit. We use code complexity metrics rather than a strict line limit, but it's the same idea.

Re: Rules for Writing Safety Critical Code (2006)

#80

Post by spc476 »

4ad wrote: post #36
pja wrote: post #29

Earlier quoted context omitted.

Manual conversion to a loop also destroys the same information, so it’s a wash either way on that front.

You can't convert arbitrary tail calls to a loop. You can only convert recursive tail calls to a loop. The information loss associated with non-recursive tail calls is great. It's true that recursive tail calls lose less information, but it is not true that it's equivalent to the information lost in a loop. In a loop you always have access to {head, current, tail} while in a tail call you might (subject to algorithm…

But I've found that non-recursive tail calls are great in handling state machines. I wrote a TFTP client and server in Lua [1] and the code was both much cleaner and more reusable between both client and server. Granted, Lua does proper TCO (as long as you properly code the return statement) and the lack of stack trace wasn't much of an issue there.

These rules are mostly geared towards C, which doesn't guarantee TCO at all.

[1] Partly as way to learn Lua and TCO, and as a way to manage Cisco router config files in a version control system.

Post reply on HN