Finding bugs in software is no easy task. One of the most popular methods is
something known as static-code analysis, which typically involves a data-flow
analysis that looks for defects along a code path. The problem is that data-flow analysis on its own can potentially yield false positives.
Code-analysis vendor Coverity claims to have a solution for lowering false
positives and finding even more bugs. The key is seeing whether variables and equations can be solved, which could ultimately lead to a
revolution in how software bugs are validated.
“With data-flow analysis we’re able to get 100 percent path coverage,
analyzing all the paths through code,” said Ben Chelf, CTO of Coverity. “With
this new technology based on Boolean satisfiability we’ll be able to also
get 100 percent value coverage so we’ll be able to dig into all the possible
variables and values along the path.”
Whereas traditional static-code analysis has checkers that validate code,
with Boolean satisfiability there are solvers, as the notion is all about
Chelf said that Boolean satisfiability asks if a
given formula is satisfiable. A formula could consist of variables that can
be either true or false and a developer uses “and,” “or” and “not” as the
operations on them.
So for example the developer says: X and Y or not Z. If the formula is
satisfiable it means there is a way that the developer can assign values
so that the whole expression evaluates to “True.”
“The biggest source of false positives for any data-flow analysis is a path
that can’t actually exist when you run the code,” Chelf said. “What we’re
now able to do is plug all the conditions that would lead to a bug report
into the SAT solver and then ask if it’s actually possible to satisfy the
The idea is for developers to spend less time on false bugs, as well as
making code analysis more precise.
Though Coverity is officially announcing the technology today, it has tested
it among its users, specifically those open source projects that it analyzes
for code defects as part of a multi-year agreement with the Department of Homeland Security (DHS). Chelf claimed
that, as a result of using the SAT solver on the DHS open source projects,
they have been able to reduce the false-positive rate by 30 percent.
That’s not to say that Coverity had a high false-positive rate before.
According to Chelf, without SAT, four out of five bugs are valid, while with SAT, nine out of 10 bugs are valid.
“From a philosophical point of view we have always hung our hat on the low
false-positive rate,” Chelf said. “The reason why SAT is important is not
just false positives, though that’s a great first application for it. But
it’s also going to open up a world of new defects. For us we’re always
trying to find as many defects as possible with the lowest false-positive