Almost without exception, as soon as a new security vulnerability is reported, people ask us, “Could CodeSonar have found that bug?”
Our static analysis tool, CodeSonar, finds coding defects and security vulnerabilities, so it’s a perfectly logical question. However, Poodle is not the sort of vulnerability that can be found by CodeSonar, or indeed any other static analysis tool. The defect is in the design and not the implementation.
There is usually a clear difference between design defects and coding defects. Static analysis tools out-of-the-box are good at finding coding defects, and are generally not very helpful at finding design flaws unless the design flaw happens to trigger a bug as well.
In the wake of Poodle, I wrote this article on embedded.com, to address ways that static analysis tools can be useful for finding design defects.
The gist of the article is this: most specifications and designs are informal, so it is impossible to check them automatically. However, once you have an implementation, static analysis can reveal defects, some of which may indicate specification or design flaws.
The Poodle bug is a great example of why the development and adoption of formal methods is important to the industry. Here at GrammaTech, in addition to our commercial software, we are in the midst of numerous research projects, several of which aim to move the industry in this direction by working on tool support for developing specifications and managing how they relate to the code, sponsored by NASA, the National Science Foundation, and the U.S. Navy. We’ll report more on these projects in upcoming blog posts.