Almost without exception, as soon as a new security vulnerability is reported, people ask us, “Could a static analysis tool have found that bug?” Yesterday was no different when Poodle was announced.
Poodle, which stands for “Padding Oracle On Downgraded Legacy Encryption” is a new security vulnerability that was found by Bodo Möller, Thai Duong, and Krzysztof Kotowicz of Google who described it in their just published “This POODLE Bites: Exploiting The SSL 3.0 Fallback.”
I'm not going to attempt to explain how it works in this article. It is a cryptographical design flaw, and others with a lot more expertise in crypto have already posted detailed explanations. I can recommend the blog written by Matthew Green of Johns Hopkins, and the very readable description of how it works that Google's Adam Langley wrote. What I would like to discuss is the relationship between defects like this and static analysis.http://blog.cryptographyengineering.com/2014/10/attack-of-week-poodle.html
Static Analysis and Design Flaws
Poodle is not the sort of vulnerability that can be found by any static analysis tool, including CodeSonar. The defect is in the design and not the implementation. An implementation that supports SSLv3 can be 100% free of code-level defects, but it will still exhibit this vulnerability. It is even correct to say that all correct implementations of SSLv3 are required to have this defect. In contrast, Heartbleed was unambiguously a coding bug — the author neglected to check some input data and the consequent buffer overrun allowed an attacker to read sensitive information.
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. For example, although it is highly unlikely that a design would require a buffer overrun to occur, a bug such as a race condition may be present in an implementation because the specification is wrong. In such a case, the static analysis tool will be useful for finding the error.
There are other ways that static analysis tools can be useful for finding shortcomings in specifications. Specifications and designs are typically not very easy to analyze with automatic tools. The vast majority are written in informal natural languages and invariably contain omissions, inconsistencies, and ambiguities. The process of implementing a specification will iron out some of these wrinkles, but some defects may remain. The key thing, though, is that once you have an implementation, you at last have something concrete that you can analyze, and you can start asking questions about code properties that double as questions about the specification.
For example, many specifications talk about how the properties of an object should evolve over time in response to changing conditions. A reasonable implementation of such a specification is to encode the state as a field of a class that represents the objects, with methods to implement the transitions between states.
A static analysis tool can be used to answer questions about the sequence of transitions that are possible. Suppose there is a requirement that an object that starts in state A must not get to state C without passing through state B, and that the design is claimed to prevent that from happening. A static checker can be written that will explore paths through the program to determine if the code allows the forbidden state to be reached. It is of course possible that the error is in the implementation of the design, but it may also reveal that there is a subtle flaw in the design itself.
Similarly, if a design is claimed to prevent the flow of information from one part of the system to another, a static checker that uses taint analysis can uncover ways in which that property is violated.
Some static analysis tools allow you to do all this. CodeSonar, for example, allows you to write your own checkers for custom properties, and to make it easy, we allow you to piggyback on the whole-program interprocedural path-sensitive program-exploration algorithms. So very sophisticated queries can be written relatively easily.
Whether this approach might have been useful for Poodle remains to be seen. It is notoriously difficult to do precise static analysis on cryptographic algorithms – they are, after all, designed to scramble data and make it difficult to tease apart, so it may be a challenge to pose exactly the right question in a form that a static analysis tool would be able to give a useful answer.
And of course it would be much better for everyone if specifications and designs themselves could be checked directly. Formal methods aim to do just this, but there is still a lot of work to be done before such techniques are widely used.
We believe that moving the industry in this direction is important, which is why we're in the midst of several research projects, sponsored by NASA, the National Science Foundation, and the U.S. Navy, working on tool support for developing specifications and managing how they relate to the code. We'll report more on them in upcoming blog posts.
Paul Anderson is VP of Engineering at GrammaTech. He received his B.Sc. from Kings College, University of London and his Ph.D. in computer science from City University London. Paul manages GrammaTech’s engineering team and is the architect of the company’s static analysis tools. Paul has worked in the software industry for 20 years, with most of his experience focused on developing static analysis, automated testing, and program transformation tools. He can be contacted at firstname.lastname@example.org .