Tue Feb 7, 4:15, 3400 Boelter Hall

What Are We Trying to Prove? Prospects for Certified Code

Peter Lee
CMU

Since 1996 there has been tremendous progress in developing the idea of
"certified code".  In a certified-code scheme, a certificate provides
easy-to-verify guarantees, for example that a program will definitely never
crash or that it obeys key security rules.  Almost magically, the guarantee
holds even if the code is  obtained from an untrustworthy source!  A
substantial amount of the research work in this area has been directed
towards the problem of how to make certified code a practical
technology---what one might call ``proof engineering.''  Thus, many of the
advances have been in methods for representing the certificates in the most
compact and efficiently checkable way.  Considerable effort has gone also
into the development of prototype tools that explore how to handle
realistic programs written in realistic languages.

In this talk, I will start with a brief tutorial on certified code and
describe the current state of these and related concepts in certified code.
Then, I will consider a very different but equally practical question: Just
what is it that we need to be able to prove, in order to be of practical
relevance?  And how far away are we from being able to prove these things?
While the safety properties provided by current certified code systems are,
in fact, of central importance to reliability and security, they also miss
many important properties, such as the absence of most kinds of trojan
horses, covert channels, or race conditions.  I will argue that there are
potentially great opportunities in tackling some new problems, and offer my
assessment for our chances for success in solving them.

About the speaker:  Peter Lee is a Professor of Computer Science at 
Carnegie Mellon University.  He joined the faculty of Carnegie Mellon's 
School of Computer Science in 1987, after completing his doctoral studies 
at the University of Michigan.  Dr. Lee is known internationally for 
his research contributions in areas related to information assurance, 
especially the application of programming language technology to 
operating systems design, networking, and computer security. 
He is perhaps best known for his co-invention of the "proof-carrying code"
technology for ensuring the safety and security of software obtained from 
untrustworthy sources.  In addition to being a Professor of Computer Science, 
Dr. Lee was also the Associate Dean for Undergraduate Education in Carnegie
Mellon's School of Computer Science.  In this capacity, Peter Lee was involved 
in the administration of Carnegie Mellon's undergraduate programs in Computer
Science.  Dr. Lee's tenure as Associate Dean saw the undergraduate program 
rise to national prominence, both for its intensive problem-oriented curriculum 
and for its success in attracting and retaining women into the field of 
Computer Science.  An award-winning teacher and lecturer, Peter Lee is 
called upon as an expert in diverse venues, including distinguished lectures 
at major universities, memberships on senior government advisory panels, 
and court testimony in the Sun v. Microsoft "Java lawsuit."  Dr. Lee is an 
elected Fellow of the Association for Computing Machinery and a member of the 
Board of Directors of the Computing Research Association.  He is a member of 
the Army Science Board and has served on panels for the Defense Science Board, 
the National Academies, the Defense Threat Reduction Agency, the senior advisory 
group for the DARPA Information Exploitation Office, and DARPA ISAT.  
In addition to holding M.S. and Ph.D. degrees in Computer and Communication 
Sciences, Peter Lee also earned a B.S. in Mathematics from the 
University of Michigan in 1982.  He has been a principal investigator on 
several DARPA, NSF, and NASA grants and contracts.  Peter Lee is a 
U.S. citizen of Korean descent, is married and has one child. 
He is an avid fan of auto racing and holds an SCCA competition license, 
which enables him to participate in both amateur and professional auto races.

Host: Jens Palsberg