Improving Program Robustness
via Static and Dynamic Analysis

We have developed a new framework, based on the concept of deductive databases, for context-sensitive program analysis. In this framework, all program information is stored as relations; data access and analyses are written as Datalog queries. To handle the large number of contexts in a program, the database represents relations with binary decision diagrams (BDDs). The system we have developed, called bddbddb, automatically translates database queries into highly optimized BDD programs.

Our preliminary experiences suggest that a large class of analyses involving heap objects can be described succinctly in Datalog and implemented efficiently with BDDs. To make developing application-specific analyses easy for programmers, we have also created a language called PQL that makes a subset of Datalog queries more intuitive to define. We have used the language to find many security holes in Web applications.

We designed a program representation, called IPSSA, for capturing intraprocedural and interprocedural definition-use relationships of directly and indirectly accessed memory locations. This representation makes it easy to create demand-driven path-sensitive and context-sensitive analyses.

We demonstrated how a program checker based on IPSSA can be used to find security violations. Our checker, when applied to 10 programs, found 6 new violations and 8 previously reported ones. The checker generated only one false warning, suggesting that our approach is effective in creating practical and easy-to-use bug detection tools.

Memory leaks and double deletes in large C++ programs are hard to find; detecting them require not just local analysis, but whole program analysis. We have made formal an object ownership model that is commonly used in practice. Objects in this model are owned at all times. The ownership may be held by a parent object, or by a variable in a method, and can be transferred during the lifetime of the object.

We have developed an algorithm that can automatically identify objects that follow the model and locate potential memory leaks and deletions of dangling pointers in C++ programs, without requiring user intervention. The algorithm uses a fully flow-sensitive and context-sensitive analysis to derive the likely object invariants and to check that the objects are used consistently throughout the program. The algorithm has been implemented in a tool called Clouseau.

Previous attempts to model memory management with linear types were too restrictive to be useful on real-life programs. To create a practical model, we allow object ownership be transferred optionally in assignments and parameter passing. We use an automatic procedure to determine if there are any inconsistencies in transfers of ownership. We make ownership inferencing feasible by introducing an object invariant that is often found in good object-oriented programming practice. Namely, members of a class are classified as either "owned" or "not owned"; i.e. a member is either "always owned" or "never owned" by the parent object at all public method boundaries. This approach results in an efficient whole-program flow-sensitive and context-sensitive analysis, which takes less than 8 minutes on a PC to analyze a program with over 100,000 lines of code.

Clouseau successfully identifies tens of errors in our SUIF2 research compiler, and several bugs each in the open-source Mozilla web browser and the OpenOffice productivity suite. In addition, it found numerous classes in most of the systems where system extenders could easily misuse the class implementations because of undocumented interface restriction on the object. Besides producing a useful tool, this research contributes to our understanding of deep program analysis by producing one of the fully flow-sensitive and context-sensitive analysis tools that works on large real-life C++ programs.

System software often obey rules such as "accesses to variable A must be guarded by lock B". We have developed an approach called metacompilation where programmers can add simple system-specific compiler extensions that check their code. We have written roughly fifty checkers to find errors in operating systems such as Linux and OpenBSD. We have also developed techniques to automatically extract such rules from the program.

Metacompilation checkers find many serious errors in complex, real systems code. We have written roughly 50 checkers that in aggregate have found thousands of errors in widely-used systems such as Linux and OpenBSD. Many errors were the worst type of systems bugs: those that crash the system, but only after it has been running continuously for days. We have validated the results by reporting the errors to the main system developers, spurring hundreds of fixes (not all errors have been fixed --- there were so many that the backlog could easily take over a year to process).

Many checkers are less than 100 lines of code; some of the most effective are less than 20. MC checkers are easily written. Most of our checkers were written by programmers who had only a passing familiarity with the systems that they checked. Extension writers also need little background knowledge of compilers in order to write checkers. A good example of this can be seen in that an undergraduate with no real knowledge of Linux and OpenBSD and no compiler experience implemented an MC checker that found roughly two hundred security holes in these systems in a few months (which is likely a world record for security holes per unit of time, if not close to the record for sheer numbers).

CRED is implemented as an extension of the GNU C compiler version 3.3.1. The simplicity of our design makes possible a robust implementation that has been tested on over 20 open-source programs, comprising over 1.2 million lines of C code. CRED proved effective in detecting buffer overrun attacks on programs with known vulnerabilities, and is the only tool found to guard against a testbed of 20 different buffer overflow attacks. Finding overruns only on strings impose an overhead of less than 26% for 14 of the programs, and an overhead of up to 130% for the remaining six, while the previous state-of-the-art bounds checker by Jones and Kelly breaks 60% of the programs and is 12 times slower. Incorporating well-known techniques for optimizing bounds checking into CRED could lead to further performance improvements.

Automatically extracted models are useful as documentation or constraints to be enforced by a static or dynamic checker; developers can check the models to ensure that they match the original design intents and testers can use them to evaluate the completeness of a test suite. Techniques developed include static analyses to deduce illegal call sequences in a program, dynamic instrumentation techniques to extract models from the execution runs, and finally a dynamic model checker that ensures that the code conforms to the model.

We have tested our model extraction tools over 1.2 millions of lines of code. The model automatically extracted for the socket implementation in java.net captures the essence of the class effectively. The models extracted for the standard Java libraries are useful as documentation and can be used by static tools to look for errors in programs. The scalability of the dynamic analysis tool is demonstrated by running it on the million-line J2EE enterprise edition platform. The extracted models convey interesting information about the program being tested and the test suite itself. Finally, when applied to the joeq virtual machine, the tools found discrepancies betwen the intended and implemented API. This information is helpful in the evolution of programs.

Limited hardware support has been provided in the past for performance monitoring. Here, we are interested in monitoring the execution for the sake of software reliability, as such, the support must be more flexible. The program-specific monitor functions are executed in parallel with the continuation of the normal execution. Because the hardware buffers up all the side effects of the speculative execution of the normal thread, the monitoring functions can simply assume they are operating on the state in which the function is invoked. Because the side effects of the monitoring functions seldom affect the normal threads, it is often possible to execute the normal threads in parallel. In the rare occasion where the monitoring threads wish to raise an exception, the hardware can simply discard the speculative state. For error recovery, we advocate the use of fine-grain transactions in our programming. We execute the code within the transaction in a speculative thread. The side effects of the transactions are committed if the thread completes normally, and discarded otherwise.

We have measured the effectiveness of our proposal by experimenting with a number of case studies including the implementation of DIDUCE and Purify, and code to recover from buffer overruns. Our preliminary results suggest that instrumented code indeed has more parallelism. For example, our proposed architectural feature manages to execute 80% more instructions with no performance degradation in one of our test cases. Also, we showed that the speculative thread support allows computations to recover quickly and thus fends off denial-of-service attacks that try to crash the processes of an application.

This work suggests a new direction in architectural research. There has been so much energy devoted to squeezing the last drop of performance out of existing applications, we are seeing diminishing returns. Instead of tuning the micro-architecture to speed up existing applications, we propose that we look to the future to promote emerging programming paradigms that enhance reliability and productivity, and which may be too expensive on today's architecture.