🚀 go-pugleaf

SDI/LCS and POP Seminar
Thursday, September 28, 2000
Noon - 1 pm
Hamerschlag Hall, Room D210
http://www.pdl.cs.cmu.edu/SDI/

contact: Stephen Miller (sm79@cs.cmu.edu) or
Karen Lindenfelser (karen@ece.cmu.edu)

Speaker:  Peter Lee

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.