The C language has given the world many enduring gifts such as buffer overflows, uninitialized variables, and use-after-free errors. Since rewriting a code base in some other language is not easy, we’re often stuck trying to eliminate bugs in legacy C before they bite us, and of course bugs in network-facing code sometimes bite us very hard. In this post I’ll be discussing TrustInSoft’s Verification Kit for PolarSSL 1.1.8, which I’ll call “the report” throughout this post. Just to be clear, I’m not unbiased — I’m working for these folks this year — so I’ll try to keep the cheerleading to a minimum.
The crux is:
This report states the total immunity of the SSL server implemented by the PolarSSL 1.1.8 library to [CWE-119, CWE-120, CWE-121, CWE-122, CWE-123, CWE-124, CWE-125, CWE-126, CWE-127, CWE-369, CWE-415, CWE-416, CWE-457, CWE-476, CWE-562, and CWE-690] if it is deployed according to the Secure Deployment Guide detailed in section 4.4.
In other words, a collection of nasty undefined behaviors that are so hard to get rid of, have been gotten rid of — if you are careful to follow the instructions.
The thing that struck me while reading the report is that I’ve never seen a document quite like it. I’ll next try to nail down that idea by explaining what the report is not.
It’s not a piece of formal methods research, which would need to demonstrate the novelty and utility of a verification technique. Rather, the verification techniques are completely deemphasized in the report in order to concentrate on the code that is being verified. In fact, one of the things that bothers me about formal verification research is that so much of it is concerned with new notations and clever algorithms instead of focusing on the thing I’m interested in: the interplay between the verification techniques and the code being verified.
It’s neither a formal proof nor a code review. Rather, nearly all of the reasoning about code has been delegated to the analysis tool, which must be trusted to come to the right conclusions. Why would we trust a formal verification tool? For one thing, the analyzer has been validated on many other codes including programs generated by Csmith (we wrote a short paper about that work). For another, the analyzer identified some legitimate shortcomings in PolarSSL that needed to be fixed before the verification would go through (these are in Section 4.4.3). Additionally, a much more serious PolarSSL bug was found earlier in the verification process. It is not mentioned in this report since it had been fixed before version 1.1.8 was released.
Because it makes a guarantee, it is fundamentally different from a report based on unsound static analysis. By early 2014, OpenSSL had been examined by various unsound analyzers and yet none of them found Heartbleed. In contrast, if someone had used sound static analysis to verify OpenSSL 1.0.1f, it is a certainty that Heartbleed would have been among the defects that were discovered. (We have to be a little bit careful when making this kind of statement. For example, the bug won’t be discovered if the OpenSSL being verified was compiled using -DOPENSSL_NO_HEARTBEATS. The buggy code must lie within the verification perimeter that I’m about to discuss.)
So what is this report? It is, mainly, three things:
The definition of a perimeter within which its claims apply. This perimeter has three aspects. First, it excludes some parts of PolarSSL, such as X.509, that were not verified. Second, it excludes some ways in which the code could be used by defining drivers that exercise API calls in certain ways. For example, the server driver that spans pages 16 and 17 initializes the library, makes an arbitrary number of read and write calls, and then shuts it down. The guarantees in the report would not apply to a different usage, such as one that started writing data without properly initializing the library. Nor would they apply to usage of the library by a buggy program that corrupted PolarSSL’s state using a stray indirect write. Third, some configurations of the code are placed outside of the perimeter. The issue is that C code is implicitly parameterized by a collection of implementation defined behaviors, such as the representation of integers, and it is also typically explicitly parameterized by preprocessor directives. A real C program is actually a shorthand for a huge family of different programs; any formal verification effort either has to pin down which member of the family is being verified or else reason about the entire family. Reasoning about the entire family in a sound and precise way is an open problem.
A sketch of the verification strategy, which is divide and conquer. Each of chapters 5-10 describes the verification of a component. The interfaces between components are specified in ACSL, which is designed in such a way that when two components are verified against opposite sides of an interface, their overall verification can be taken for granted.
A justification of alarms. The analysis tool signals an alarm any time it fails to prove that an operation (for example, incrementing a signed integer) is safe. Each alarm must be investigated to determine if it is a true alarm (exposing a defect in the code) or a false alarm (exposing an imprecision in the analysis). Appendix A of the report contains this analysis. It turns out to be easy, in theory, to avoid the imprecisions that caused these alarms: the necessary techniques have been known for decades. The issue is that there are engineering reasons for avoiding these static analysis techniques: their results can be very difficult for people to understand and also they can be computationally expensive. An entertaining exercise would be to pick a few parts of Appendix A, download PolarSSL 1.1.8, and make sure you agree with the reasoning from the report.
That’s all there is to it, though if you read the report you’ll see that the reasoning sometimes becomes quite detailed and technical.
Finally I’ll try to anticipate a few questions the you might have at this point.
How much effort would be required to track the upstream PolarSSL (now mbed TLS)? A majority of local changes will just go through the verification automatically. Larger-scale changes might raise one or more new alarms that need to be investigated.
Under what conditions does the claim of “total immunity to UBs” apply? In addition to the conditions described in the report, the intellectual analyses in Appendix A must be correct, the verification tool must not have made a mistake, and the C compiler and the platform (OS + standard libs + hardware) must not make mistakes.
If we don’t want UBs, why not just use a TLS written in Java or C# or some other safe language? Of course that’s a fine idea! But we’ll have to somehow shoehorn a Java runtime onto those embedded processors with ~64 KB of RAM where PolarSSL / mbed TLS run. Also, I’m not sure that it is clear how to implement crypto in higher level languages in such a way that it resists timing attacks (this is hard enough in C). Finally, safe languages are only dynamically safe: a buffer overrun bug in a Java program will lead to an exception, and perhaps to a DoS attack. The report makes a guarantee of static safety, meaning that buffer overrun bugs do not exist.
Where is the corresponding document for OpenSSL? It doesn’t exist. Based on lines of code, it would probably be about four times longer than the PolarSSL report, and would require at least four times the effort to create.
What is the future of this kind of report? It’s all about economics. Given a piece of C code, we can choose to inspect it, to test it by hand, to fuzz it, to subject it to unsound static analysis, and to subject it to sound static analysis. Obviously, all of these validation techniques have merit — the question is how many resources to allocate to each of them. Larger, more rapidly evolving code bases tend to favor cheaper validation methods whereas smaller, security-critical codes are amenable to formal verification. The reach of formal verification techniques is increasing as techniques improve, but also software keeps getting bloatier.
How should I think or act differently based on the information in this report (and others like it)? Well, this is the central question. Formal verification has made major progress in the last 10-15 years and we now have extremely impressive technical results including CompCert and seL4. However, I think it’s fair to say that almost everyone is having trouble figuring out how to fit these results into the big picture. From the client’s point of view, formal verification tends to be somewhat mysterious, as if a mathematically adept wizard had sprinkled some magic verification dust over a source code repository, which now glows with correctness. Let’s take a quick look at this article about seL4 that appeared in New Scientist a few days ago. On Twitter, Gerwin Klein — the leader of the L4.verified project — said:
The sad truth is that this article is not that bad compared to others. I’ve seen way worse. Nuance is hard..
What he says is true: the article, while being sort of decent, is just extremely far from conveying accurate technical information. Here’s a more nuanced version.
The PolarSSL report can be best understood as providing details that are necessary for the next level of people to crack open the black box surrounding this particular formal verification effort. We didn’t need another article about abstract interpretation, we needed specific technical claims about a particular piece of source code, followed by details that back up the claim. Much more work on communicating verification results is needed, but this is a good piece of progress.