What's the Difference Between Sound and Unsound Static Analysis? (.PDF Download)
Static analysis has established itself as a "must-have" for the verification of critical software. Notably, it can find problems that are hard to uncover by testing, such as concurrency issues and security vulnerabilities. Many static analyzers can now associate CWE entries (for Common Weakness Enumeration,1 a well-known classification of security vulnerabilities) to their messages, to help users review all messages related to a given vulnerability. For example, CWE-120 is the classic buffer overflow.
But, in general, there’s no guarantee that the code is immune from classic buffer overflows even after reviewing all messages associated with CWE-120. Indeed, most static analyzers are "unsound" in their verification; that is, unable to report all potential problems. This has led projects to use a combination of static analyzers to detect as many security vulnerabilities as possible. For example, Mozilla uses Clang Analyzer, clang-tidy, their own checkers, and Coverity on its C/C++ code.2
But this still doesn’t provide any guarantee that a given vulnerability has been fully covered. Enter sound static analysis. Some static analyzers are "sound" in their verification and can guarantee that a given vulnerability isn’t present in some piece of software. In practice, sound static analyzers output an exhaustive list of places where the vulnerability could occur, most of which are false alarms or "false positives" that need to be reviewed.
While more demanding for users, these static analyzers make it possible to achieve higher levels of confidence than is possible with their unsound counterparts, which makes them attractive in a security context. A recent workshop at NIST focused on "Sound Static Analysis for Security"3 with presentations from providers and users of such tools showing the maturity of that field. In this article, we draw on that workshop’s results and our experience building both sound and unsound static analyzers to explain why their difference matters—and when you should use which tool.
Definition of Sound Analysis
A sound analyzer is correct with respect to a class of defects it can detect in a safe and exhaustive way. It offers the guarantee that it will detect any such vulnerability occurring during run-time. This is in contrast with an unsound analyzer, which might not flag faulty code lines (in order to limit the number of warnings returned to the user).
In addition, a sound analyzer is guaranteed to be exhaustive, at the expense of possible false positives: warnings emitted on code for which no problem actually occurs at execution time. As explained by David Wheeler in his talk about verification of legacy software,4 exhaustiveness is a large commitment, which can hardly be made by any other verification technique.