Assistant Professor (EECS), Computer Science Division Office, University of California, Berkeley, US.
·CCured is a tool that processes C applications and analyzes them for type safety. Where the analysis fails, Ccured adds run-time checks to guarantee the safety of the application at a cost that ranges from 10-70%. Because CCured has access to the source code it can find more errors than Purify can find and at an order-of-magnitude lower run-time code. Using CCured we have found several new errors in SPEC95 programs that have been used widely for many years.
·Random Interpretation is a program analysis technique that relies on executing a program fragment on a number of random inputs. The obvious problem with a naïve implementation of such random testing is that it lacks soundness. We have shown that for certain program properties the interpretation can be suitably modified such that we can make the probability of unsound results very small.
·CIL (C Intemediate Language) is a high-level representation along with a set of tools that permit easy analysis and source-to-source transformation of C programs. CIL is both lower-level than abstract-syntax trees, by clarifying ambiguous constructs and removing redundant ones, and also higher-level than typical intermediate languages designed for compilation, by maintaining types and a close relationship with the source program. The main advantage of CIL is that it compiles all valid C programs into a few core constructs with a very clean semantics. Also CIL has a syntax-directed type system that makes it easy to analyze and manipulate C programs. Furtheremore, the CIL front-end is able to process not only ANSI-C programs but also those using Microsoft C or GNU C extensions.
·Proof-Carrying Code (PCC) is a technique for safe execution of untrusted code. The basic idea is to require the code producer to generate a formal proof that the code meets the safety requirements set by the code receiver. The code receiver can easily check the proof by using a simple and easy-to-trust proof checker. Due to the separation of the difficult task of verifying the code from the easy task of validating the proof of verification, PCC can be used efficiently even for optimized assembly language. Check out my papers on this subject.
·Translation Validation for Optimizing Compilers. Compilers are an indispensable tool in software engineering because they bridge the abstraction gap between high-level languages and machine code. But they also introduce a semantic gap between the source programs that we design, analyze and reason about and the compiled programs that we actually run and care about. Everything would be fine if we could trust that compilers are perfect. But they are far from perfect. To make matters worse advanced optimizing compilers are notoriously hard to test and debug and there is little help that we can verify them formally. Translation validation is a promising technique that proposes to verify the correctness of each compilation as is happens. This seems to be must easier that verifying the compiler. To experiment with translation validation in a real world setting we are building a translation validator for the GNU C compiler. Our preliminary results are promising.
·Open Source Quality Project. This project investigates techniques and tools for assuring software quality: finding and removing defects in software systems, as well as improving current methodology for designing high-quality software systems at the outset. The project consists of both experimental and theoretical components. The foundational work in this project combines expertise in the three branches of the discipline of the analysis of software: formal verification and theorem proving, model checking, and large-scale software analysis. These three areas have developed rapidly in recent years, seeing both significant theoretical and practical advances. A central thesis of this project is that significant further advances are possible by bringing together these areas to work on a common set of problems.
2001 ACM Grace Murray Hopper Award "For his seminal work on the concept and implementation of Proof Carrying Code, which has had a great impact on the field of programming languages and compilers and has given a new direction to applications of theorem proving to program correctness, such as safety of mobile code and component-based software."