Electronic Design Interviews U. of Virginia Computer Prof

ED: Can you give a little overview and history of Splint?

Back in 1993, I was a student at MIT and took a seminar on formal methods taught by Professors John Guttag and Jeanette Wing. One of the things covered in the seminar was the Larch family of specification languages (see http://mms.lcs.mit.edu/Larch/history.html for a brief history of Larch) and the LCL interface language for C. I was looking for a topic for my Master's research at the time, and discussed with Guttag who became my research advisor, the possibility of building a tool that checked an implementation for consistency with an LCL specification. The tool I developed to do that became LCLint (a name that merged LCL for the specification language) with the C program checking tool, lint. At this point, LCLint was focused primarily on enforcing data abstraction in C programs. A paper (co-authored with John Guttag, Jim Horning, and Yang Meng Tan) was published in the SIGSOFT Foundations of Software Engineering conference in December 1994.

After people began using LCLint, it became clear that needing a separate LCL specification limited both the potential audience that would use it and the kinds of constraints that could be expressed and checked. So, I added support for expressing specifications using structured comments (annotations) in the source code. The first version of LCLint was released sometime in 1994, and as various groups started to use it more features were added. In 1995-1996, motivated mostly by my own difficulties dealing with memory management problems in the increasingly complex LCLint code, I developed annotations for describing common memory management strategies and associated checks. This was the focus of a paper published in the SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96).

After 1996, I focused on other work (which became my PhD thesis), and I joined the University of Virginia in 1999. My first graduate student there, David Larochelle, worked on extending LCLint to support checking for security-related implementation flaws (including buffer overflow vulnerabilities). To reflect the new focus on security, we renamed LCLint as "Splint".

ED: What were some of the lessons gained from developing and using Splint?

One main lesson is that a little bit of redundancy has a lot of value. When we began the project, the goal was to surreptitiously lead developers into using more complete formal methods. This turned out to not be successful; very few Splint users ended up even writing separate LCL specifications, let alone using more advanced formal methods. On the other hand, the very minimal specifications supported by Splint have proven to be quite useful in detecting programming bugs, producing programs more efficiently, and leading to better documented, more understandable programs. The value of these types of simple annotations has also been confirmed by their widespread use at Microsoft with PREfix and PREfast. In most of the important projects at Microsoft, developers are now required to annotate their code sufficiently to pass checking done by these tools.

Another lesson is that the prevailing academic view that implementations and specifications should be separated is not the best view for helping developers. Although there are good aesthetic and elegance reasons to have a clear separation between a specification and implementation, such a separation limits the number of developers who will create any kind of formal specification at all, and limits what can be expressed in the specification. By embedding the specification directly in the code as comments, we made Splint much more accessible to typical developers than any approach that requires a separate specification.

ED: Can you comment on the current state of affairs with respect to static analysis tools?

A great deal of progress has been made since the 1990s both in terms of the quality of available tools and their widespread use. In the mid-1990s, I don't think there were any companies whose primary business was software checking tools and security analysis; now, there are scores of companies selling software checking tools and services, and many of these are quite successful. The other major change, at least with software vendors, is making security and dependability priorities in a more mature software development process. This is perhaps best exemplified by the philosophical change at Microsoft (and other companies) that has lead to security being incorporated throughout the design and development process, instead of something that is attempted to be tacked on at the end. This attitude does not seem to have reached most web application companies yet, though.

ED: Has the increase of applications requiring higher levels of safety and reliability affected the importance of static analysis tools?

Yes, many developers have come to the realization that all programs are now security-critical. Since essentially all programs now run on networked computers, bugs in non-critical programs can often be exploited just as easily as bugs in critical servers. The emergence of a software security industry speaks to the understanding, at least of some segment of the software industry, that spending effort on security and reliability is necessary and important.

ED: How have improvements in IDEs and system performance affected the adoption of static analysis tools?

Program analysis tools that can be easily incorporated into a build process are much more widely used than tools that require special extra efforts on the part of developers. Many of the checks that were done in the first versions of LCLint are now done by default by most compilers—other checks are done by compilers if flags like -Wall are used. The incorporation of more advanced analysis tools into IDEs (e.g., PREfast in Visual Studio) and SDKs (e.g., the Static Driver Verifier in device driver development) greatly increases the number of developers benefiting from static analysis.