Safety Verification for Software

When automakers are thinking about the safety of an embedded system in a car, while it’s good to know the hardware has been comprehensively tested for safety-specific requirements, that isn’t much help if the software component of the system is not supplied with similarly robust guarantees.

The challenge is that the software state space is invariably massively bigger than the hardware state space and much more dependent on external components – standard libraries and open source software for example. So traditional dynamic testing, while necessary, is even further from being sufficient than it has become for hardware. This problem highlights the importance of finding solutions which can provide more complete use-case-independent coverage, especially for safety-critical applications.

One partial solution is static verification. Linting has been the main workhorse and tools in this area have evolved considerably beyond the simple checks familiar from compiler warnings. But they still have significant limitations. Analysis is primarily structural (on a control/data-flow graph), complemented by peephole behavior views. Where correct understanding requires a broader behavioral view they tend to be noisy, producing lots of false violations. Equally they are likely to miss hazards apparent in a more global view of the code.

Formal analysis for software is always an active topic of research but has had a hard time making it into the production world. Challenges here are similar to those found in formal for hardware, amplified by massively increased state space. Successful demonstrations tend to be around highly constrained tests, raising concerns about the correctness of constraints and generally limiting confidence in coverage for real-world problems. As one example, the Synopsys Coverity product initially touted formal methods in their product but have since de-emphasized that capability.

Another direction is symbolic testing where you test with symbol values for variables, rather than actual values. This comes in two forms: dynamic symbolic execution (DSE) and static symbolic execution (SSE). In either case you can test safety assertions, much as you might in formal analysis. DSE in practice seems to combine symbolic values for some variables with actual values for others, and propagates formulae which can be tested against assertions. A challenge with DSE is explosion in the number of possible paths through everyday code. An alternative is static symbolic execution (SSE) which merges formulae through multiple paths simultaneously. A problem for SSE is that the formulae become very complex and difficult to solve.

DSE and SSE have been effective in finding some important bugs and security holes, in earlier versions of Windows for example (Microsoft is particularly active in this area). But alone neither scales well to most realistic programs. However a 2014 publication introduces a method called Veritesting which combines DSE and SSE methods in a (non-commercial) tool called MergePoint. MergePoint aims to minimize the difficult of solving formulae by alternating between DSE and SSE and allowing explicit values through DSE, where appropriate to limit the state-space search. Alternation makes analysis on realistic size code much more feasible.

An important advantage of this tool is that it can also be applied to directly to binaries without needing access to source (even for pre-processing). The authors have demonstrated the capabilities of MergePoint by applying it to Linux and Debian distributions with thousands of binaries. Their original work found over 10k bugs, of which already ~230 have been patched in those distributions (in other words, the bugs were agreed to be real and in need of fix).

While I’m sure this approach will not be the last word in safety/security-checking software, it does look like an important step forward. I have no idea if or when this might be commercialized but presumably you can contact the authors to learn more about how you can access their code. You can read more about Veritesting HERE.

More articles by Bernard…