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.
SDI / LCS Seminar Questions?
Karen Lindenfelser, 86716, or visit www.pdl.cmu.edu/SDI/