Rules for Writing Safety Critical Code (2006)
spinroot.com
spinroot.com
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, printf. Most of the attempts at formal proof I've seen seem quite complex for very simple functions [1] and the next step up seems too complicated for me to follow [2]. I'm familiar with heuristic-based tools like clang analyser, coverity and flexelint - but none of those claim to produce any sort of proof. I'm also aware of MISRA but again, that doesn't claim to provide any sort of proof.
Those of you who are using formal methods: Is what I've seen really the state of the art? Or are there powerful tools I've overlooked?
[1] https://github.com/Beatgodes/klibc_framac_wp/blob/master/src... [2] https://github.com/seL4/l4v/blob/master/lib/Monad_WP/Strengt...
Both languages are being used in Project Everest [3], which is building a formally verified HTTPS stack, including a formally verified TLS implementation [4].
Unfortunately, there isn't a lot of documentation / beginner guides about these languages out there, but with the little there is, I was still able to start proving non-trivial (but still relatively easy-to-prove) code with them, even though I have no formal verification background whatsoever.
Just as a tip, I found the Dafny tutorial to be a lot easier to follow than F-Star's, but from what I could gather, F* appears to be slightly more general/sophisticated in what it can prove.
[1] https://github.com/Microsoft/dafny [2] https://www.fstar-lang.org [3] https://project-everest.github.io [4] https://mitls.org
And you wonder why you're not getting any traction.
Dafny, though, seems to have the right idea.
https://mathworks.com/products/polyspace-code-prover/
ou PolySpace bug finder :
As a concrete example, interactive theorem provers can prove the termination of Paxos for an arbitrary number of nodes (i.e., a system of `n` nodes will reach consensus, where `n` is a positive integer). But, automatically generating such a proof for something as complicated and parameterized as Paxos is an open problem ([1] describes an automatic tool working toward that goal).
Another thing to keep in mind is the goal of the tool: verification versus bug hunting. Verification aims to prove that a property will never be violated, while bug hunting aims to find a property violation. Here's a list of some types of tools off the top of my head.
Bounded model checkers such as CBMC [2] essentially search the entire state-space of the program; you can conceptually think of this as searching through a graph which has some start node, and you'd like to find a path from the start to an error. This is a bug hunting technique since the software/hardware may have an infinite state space (e.g., `while (true) ++i`), hence the search space must be bounded (e.g., unroll loops). For finite-state systems this can generate proofs of correctness. For infinite state systems, it can generate proofs up to a certain bound (e.g., correct for some number of clock cycles, correct for some number of loop iterations). The benefit of bounded model checkers is that when they find an error they generate a counter-example, which is essentially inputs to the program causing it to fail. So, you could use the counter-example as a concrete test case to fix the issue. Techniques such as counter-example guided abstraction refinement, and more recently IC3 and property-directed reachability make use of these counter-examples to generate proofs for infinite state systems.
A complementary technique is abstract interpretation, and numerical abstract interpretation in particular. One successful tool is Astree, though closed source, has been used to verify properties on Airbus planes. Abstract interpretation is complementary to something like bounded-model checking since it can be used to verify properties on infinite state systems. Numerical abstract interpretation can be used to generate numerical proofs such as, "on line 10, variable `x` is in the range `[-10, 10]`, or constraints between variables such as `x - y >= 10`. A difficult part with abstract interpretation, however, is that when it reports an error it may be the case that the error is a false-alarm and it doesn't actually exist. You can think of numerical abstract interpretation as typical "compiler algorithms" such as constant propagation but keeping track of much more complicated information.
Symbolic/Concolic execution, such as KLEE [4], Pex and Moles [5], and their successor IntelliTest [6], are sort of a middle ground between model checking, and traditional unit testing (i.e., hand writing inputs to the program to test it). The main goal is to automatically generate such tests in order to test behavior in the program (e.g., generate a set of test inputs to have 100% code coverage). The modern versions of these techniques make use of dynamic information (i.e., they actually execute the program under test), and use this information to make decisions about future executions. More concretely, you can imagine the program executing past some branch `if (c)` which was not taken (i.e., `c == false`) and then, the analysis asks the question: "what do the program inputs need to be such that `c == true`. An answer to this question generates new inputs and allows another test to be generated and explored.
Stateless model checking is another automated dynamic technique [7,8,9] used to explore non-determinism in concurrent programs. Essentially, it automatically generates "test cases" (i.e., new thread schedules) to efficiently explore the state space caused by a non-deterministic scheduler.
And there's a bunch of other techniques out there too (e.g., symbolic model checking). There's also a huge amount of work on practical test input generation for hardware. On top of all these techniques, there are there applications to solving specific problems, and heuristics to make them more practical and scalable. Overall, most of the techniques are niche and not widely used, but have been applied in various areas.
[1] https://www7.in.tum.de/~gleissen/papers/sharpie.pdf
[2] http://www.cprover.org/cbmc/
[5] https://www.microsoft.com/en-us/research/project/pex-and-mol...
[6] https://www.visualstudio.com/vs/release-notes/#Testing
[7] https://github.com/markus-kusano/SysTest
[8] http://www.srl.inf.ethz.ch/papers/oopsla15-modelchecking.pdf
FWIW the initial page just reflects the JPL publication "The Power of Ten – Rules for Developing Safety Critical Code" by Gerard Holzmann [0]
For writing safe code in C, you should also check Frama-C and CERT Secure Coding Standards.
https://www.securecoding.cert.org/confluence/display/seccode...
Even better, get the algorithms written in a theorem prover which is guaranteed to generate reliable safe C code.
This is approach taken by Microsoft with P Language(Windows USB device driver stack) and F* (new TLS implementation).
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.
Previous discussion: https://news.ycombinator.com/item?id=4339999
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....
Use minimally two assertions per function on average
Assert your invariants
Do not use goto statements
Not really. Gerard Holzmann is in charge of software at NASA/JPL. Each rule comes from experience with a mission loss that would have been prevented if people had implemented that rule. They also help static analysers become more accurate.
These rules are specific to ultra-reliable embedded software, flight software or software for life-critical equipment. They are not really relevant for most normal programming.
At the risk of stating the obvious, a "goto exit" pattern is the defacto standard for function cleanup in Linux kernel, which may not be flying every space probe, but it's still pretty damn ultra-reliable piece of software.
If the code has 100s of gotos and their paths are mapped out and its ramifications of the paths are clearly understood for all scenarios, then it is still reliable as its full behaviour is understood and is safe.
> a "goto exit" pattern is the defacto standard for function cleanup in Linux kernel
There are many ways to do error cleanup that do not involve goto, and there are many bad ways to use goto. A static analyser can't decide if you do "good goto" or "bad goto", but it's easy to ban goto outright and avoid all the "bad gotos". You pay the price in terms of programmer work (he has to do something different), but you gain better static analysis and eliminate a full class of bugs.
This tradeoff makes sense for JPL and other people who do mission-critical of life-critical software. It might not make sense for the Linux kernel or most C software.
Mission-critical is not the place where you want to rely on programmers to do their work correctly (goto fail anyone?). You rely on specific methodology, standards, and static analysis.
I think the point is that while it is potentially a good rule for mission critical code, it is not essential. There are other ways as well.
Operating systems like INTEGRITY RTOS are.
http://www.ghs.com/products/rtos/integrity.html
Which is why GNU/Linux gets packed into his own little sandbox running on top of INTEGRITY.
They use Linux for non-hard-real-time stuff. Their microcontrollers also do not use Linux.
Coincidentally, Tesla uses QNX.
That depends on the goto statement. A good static analyzer can certainly recognize a "goto exit" pattern. There is very little difference in a function graph between an if/then/else clause and a goto statement. In fact, most static analyzers perform a first pass that is pretty similar to a compiler so that it can build a function graph for performing data analysis along each of the potential branches. One this pass is performed, it doesn't matter if you used an if/then/else, a for/while/do-while, a switch statement, or a complex sequence of break or continue statements. A graph is a graph.
The more succinct question is, "What constitutes a 'good' goto statement?" From the perspective of a static analyzer, it would be applying the exact same analysis as it would for any other branch in the function graph. If it detects a memory leak, a use-after-free, or a use of data which isn't always initialized, it makes little difference whether this is because of a bad goto statement or a sloppy set of conditionals. Either the graph shows a problem, or it does not.
Are you sure?
http://arstechnica.com/security/2016/09/linux-kernel-securit...
http://www.cvedetails.com/product/47/Linux-Linux-Kernel.html...
It's really not. I don't think you have a good sense of how reliable the systems in this space really are. Firmwares and other ultra-reliable systems typically use microkernels, and there are billions of units of verified L4 microkernels out there. Linux can't even dream of approaching this level of reliability.
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/
avoid recursion
avoid non-tail-call recursion
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.
The fact that it's uglier suggests you'd have less of an idea how it's going to behave than simple tail recursion. That said, I agree with the idea that if you're after tail recursion, an annotation that the compiler checks that ensures the call is properly tail recursive is a good idea.
I'm happy to argue that in C, it's never neater to write a loop as a tail call. Tail calls aren't guaranteed to compile into a goto, so it can be difficult to say whether it's going to end up with a call or a goto - even on a case-by-case basis. And if you write a tail call expecting a goto, and you get a call, obviously you can't just give up and go home - you'll need to rewrite it as a loop, just like you could have done in the first place. This does not strike me as less ugly than just writing that loop.
I know people like to do things the roundabout way, by writing one thing, certain that the compiler will do something else, and then saying this code is more clear rather than less so - but I've never quite understood why. A better rule of thumb to my mind is that if you want something particular to happen: write the code that way.
(I'm not denying an annotation would help - because then at least you'd know statically when you need to rewrite your code as a loop, rather than having to wait until something bad happens. Though... maybe if nothing bad ever happens... it's fine after all...? Sheesh. Ask a philosopher. Too much for me!)
The whole point of these rules is defensive programming. Programming not what is correct but what is robust i.e. if anything breaks it still produces possibly suboptimal but not catastrophic results.
Not all compilers optimize tail-call recursion into - effectively - loops. And even those that can might only do so when certain compiler flags are active.
Opinionated, maybe (although it seems to me most rules are reasoned and a justification is given).
But something practical has to be specific.
It has happened time and again to come across something it appeared to me as an arbitrary an unnecessary rule, but with more experience I think it's better to have some "debatable" specific rules that something "open to interpretation", especially if many people will have to work on the same codebase.
These are reasoned, common sense measures, most of which I have seen in one form or another in the coding guidelines of the companies I have worked for as an embedded SW engineer.
Some of them are easy to enforce (no dynamic memory allocation, no recursion), other less so (using asserts, limit function size).
The worst is adding your rules-compliant code to messy and bloated legacy code :)
(The details for rule 5 and 8 mention testing)
DOORS is good for tracking and tracing requirements, but from what I can see doesn't do code parsing. This may have changed. However, my opinion of IBM software is irreparably broken so I don't have a huge amount of trust in it.
We use Reqtify to glue requirement documents to code. It also sucks, but I think it's still powerful. You just need to set up some regexes which can recognize your requirement identifier style and you're good to go.
Whoever comes up with a solution to glue DOORS requirements to Jira issues to code seamlessly is going to be fairly rich.
(Check out "Rules for Defensive C Programming" by Dinu Madau for starters.)
I referenced the paper mentioned in my literature review
I would not link it here to the world to see as it is just an undergraduate project and my research did not yield a highly quantitive result, but I am applying the technique on a project right now with good success
In his talks Holzmann always makes the point that a coding standard is a hard sell for most people, and JPL hadn't had any success until they could come up with something simple and concise.
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.
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).
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.
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).
2) Requiring a fixed upper bound when iterating a collection of objects is a direct contradiction of the ZOI rule[0]. Most programs should not place arbitrary boundaries on the number of objects they'll operate on. This is better adapted to systems with relatively fixed databases and a predictably low volume of operator and sensor input (i.e. flight management computers, train control systems) more than internet services.
7) "For this reason, most coding guidelines for safety critical software also forbid the use of all ansi standard headers like string.h, stdlib.h, stdio.h" should speak for itself.
9) Is pretty C/C++ specific.
I think this can be argued both ways. The classic stateless pipe programs, sure, they can take as many lines as you want. User-facing programs? It can be worth imposing fairly small limits just so you don't have to worry about pathological behavior and security risks. (What happens if someone pastes a million lines of text into a small box, etc)
1. printf almost never fails. If it does, I'm just going to re-run the program. If that doesn't work, I'll reboot and then re-run. On average, I waste less time with that approach than with checking the return value of printf.
2. If printf fails, what am I going to do? Print out an error message? But that might fail, too. Log something? That could also fail. Should I check the return values of those attempts, too?
But safety-critical code is usually not calling printf - it may not have a conventional output device at all. (It should have some mechanism for alerting the operator if there are failures, though.)