DATE: Thursday, September 28, 2000
TIME: Noon - 1 pm
PLACE: Hammerschlag Hall, D210

SPEAKER:
Peter Lee
Professor and Associate Dean for Undergraduate Education,
School of Computer Science, CMU

TITLE:
A Certifying Compiler for Java

ABSTRACT:
It is a well-known fact that it is usually easier to check a proof than to generate one. This idea is used in a mechanism called proof-carrying code. Using PCC, the designer of a host system defines a safety policy and makes it public. Then, using this policy, any application writer can provide binaries in a special form that contains, in addition to the native code, a formal proof of that the code adheres to the safety policy. The host system can then quickly and easily validate the proof without using cryptography and without consulting any external trusted entities. If the validation succeeds, the code is guaranteed to respect the safety policy without relying on run-time checks. This guarantee holds even if the certificate or native code are tampered with.

One of the major tools for creating PCC binaries is the certifying compiler. A certifying compiler starts with a high-level source language - in this case, Java - and compiles it into optimized native code with an attached proof of safety. This talk will describe a certifying compiler for Java, including an overview of its internal structure and a short demonstration of how it works. This will be followed by a brief discussion of the benefits that PCC provides in compiler construction, and directions for future work.

BIO:
Peter Lee is a Professor of Computer Science and Associate Dean for Undergraduate Programs at Carnegie Mellon University. He is also the President of Cedilla Systems Incorporated, a company he co-founded in 1998.

After receiving his Ph.D. at the University of Michigan in 1987, Peter Lee's research and teaching have been devoted to improving the reliability, security, and performance of computer systems. His approach of applying theoretical ideas in programming language design to practical systems has led to numerous research contributions in the areas of programming language design, compiler technology, networking, and operating systems. Most recently, he has focused his attention on developing Proof-Carrying Code (PCC), a technique which uses program verification in a practical way to enhance the performance and safety of mobile code. Recently, he has directed Cedilla Systems Incorporated in the development of industrial-strength tools and infrastructure for exploiting PCC.

For Further Seminar Info:
Visit http://www.pdl.cmu.edu/SDI/