Coverity raises the bar for static analysis

The concept of Boolean satisfiability is being applied to identify "bugs" in software code and consequently establish to code writers' satisfaction that lines of code are predominantly bug-free.

At the 2007 Embedded Systems Conference, Coverity has unveiled what it claims to be the first source code analysis engine based on Boolean satisfiability (SAT). Coverity's SAT engine leverages its software DNA map, a highly accurate representation of any written software, to automatically, precisely and accurately identify defects in source code.

Embedded toolset
Coverity is a leader in enterprise applications. Customers for its static analysis software include 57 percent of software companies and 50 percent of computer peripheral companies listed among the Fortune 500. Its main product is the Prevent Software Quality System (SQS), which automates the detection of defects and security vulnerabilities in complex software by parsing and analyzing source code at compile time.

"Bringing SAT's proven capabilities to static code analysis will provide developers with an arsenal of new 'solvers' that uncover the toughest code defects. By leveraging technology that automates the accurate detection of defects, developers can stop wasting their valuable time tracking down bugs and can focus on bringing new software applications to market," said Ben Chelf, CTO of Coverity.

"Software developers today need static analysis to become more powerful, predictable and accurate to facilitate the acceleration of the overall software development cycle," said Theresa Lanowitz, founder of voke, a technology analyst firm.

Unlike current static analysis engines, which rely on data flow analysis and multiple checkers to identify software defects, the SAT engine is based on Boolean satisfiability and will enable multiple solvers to identify software defects.

This new technique of source code analysis is made possible by patent-pending technology from Coverity that creates a bit-accurate representation of a software system in which every relevant software operation is translated into Boolean values (true and false) and Boolean operators (AND, NOT, OR). This bit-accurate representation allows source code to be analyzed by SAT-based solvers, representing a first for commercial computer programming.

Over 300 customers already rely on Coverity Prevent SQS to analyze every path through their applications. By leveraging SAT, Prevent SQS can analyze not only every path but also every value in every computation within these paths. This exhaustive static code analysis results in the most accurate identification of critical performance and security vulnerabilities in the industry, says Chelf.

New paradigm
According to Chenxi Wang, principal analyst in the Security and Risk Management division at Forrester Research, the principle of "satisfiability" has been used for hardware verification for some time, but has previously never been applied to software verification.

"There are a number of reasons for that. First of all, software is generally more complex than hardware logic, and hence more difficult to do. Second, it's not immediately obvious that SAT is well suited for general software verification because you can't always make a good mapping from a generic software verification problem to a straightforward SAT problem," said Wang.

Wang thinks there is room for innovation, specifically in the area of embedded software. "Embedded software tends to be a bit more constrained than general application software both in terms of its complexity and the amount of state. Therefore, it's more likely that SAT can enhance the state of art for software verification in the area of embedded programming."

Chelf said that static analysis techniques have been successfully applied in the EDA industry at such companies as Synopsys and Cadence. "We are just applying the same software Boolean principles used in circuit design to the software code world."

The first solver to be released for Prevent SQS is the False Path Pruning Solver, which significantly lowers the number of false-positive results in static code analysis. By leveraging SAT to determine if the path to a potential software defect is feasible, the solver identifies and excludes unfeasible paths. By 'pruning' these unfeasible results, the solver increases the overall accuracy of the code analysis process and allows software developers to focus on those defects that pose the maximum threat to the success of their projects.

After testing on over 2 million lines of code from multiple applications of open-source software from Coverity's Scan project, the False Path Pruning Solver was found to reduce false-positive results by an average of 30 percent, according to Chelf.

Coverity plans to release two additional solvers in early 2008 that will allow customers to check code assertions statically and to detect critical types of bugs, including integer overflows. In addition, these solvers will expand Coverity's existing data flow analysis capabilities to identify an even greater number of buffer overflows while maintaining a low false-positive rate.

The foundational technology for Coverity Prevent SQS was developed in the late 1990s in the Computer Systems Laboratory at Stanford University, where Ben Chelf and others applied the technology for commercial use.

- Nicolas Mokhoff
EE Times