Tuesday, January 11, 2005, 4:15-5:45, 3400 BH
 
Foundational Proof-Carrying Code

Andrew W. Appel
Princeton University

When software systems are built from modules and components from many
sources and then installed on your machine, you would like to know that the
software doesn't steal your data and trash your machine. The solution is to
use a protection mechanism; but the protection mechanism must be absolutely
correct, otherwise malicious attackers will analyze and exploit bugs in the
mechanism to write program components that evade the protection.  Thus we
need a formal proof of correctness.  I will explain one protection mechanism
-- language-based security -- and outline how its correctness can be
formally specified, and how its correctness proof can be designed,
engineered, verified, and trusted.  Formal verification as an engineering
discipline has come far in the last 30 years, and I also will talk about
what is now possible and what others in the field have achieved.

Andrew W. Appel is Professor of Computer Science at Princeton University.
He received his PhD from Carnegie Mellon University in 1985 for work on
semantics-directed compiling (and Rog-O-Matic).  He was a cofounder of the
Standard ML of New Jersey project, on which he worked from 1987 to 1996,
making safe programming languages go faster. He was editor-in-chief of ACM
Transactions on Programming Languages and Systems 1993-97, during which time
the "phone book" issue of that journal appeared.  In 1998 he was elected an
ACM Fellow.  Since 1997 he has worked on many aspects of computer security
and technologypolicy: using type theory to make safe languages go even
safer, doing logic-based reasoning about the security of enterprise
networks, investigating "light bulb" attacks on Java virtual machines,
testifying about free speech issues in distribution of cryptographic
software, and thinking about how to trust electronic voting machines.

Host: Jens Palsberg