Subject: Talk - THURSDAY, Feb. 15
From: Carol Harlow (harlow@deas.harvard.edu)
Date: Thu Jan 25 2001 - 15:34:18 EST
http://www.deas.harvard.edu/colloquia/systems/lee01.pdf
----------------------------------------------------------------
Harvard University
Computer Science Colloquium Series
33 Oxford St., rm. 347, Cambridge, MA 02138
tel: (617) 496-1440 fax: (617) 495-9837
Colloquium
Certified Code
Professor Peter Lee
Carnegie Mellon University
THURSDAY, February 15, 2001
4:00PM
Maxwell Dworkin G125
(Tea at 5:00PM Breakout room G123)
Abstract
In recent years, several techniques have been developed for "infusing"
code
objects with small amounts of extra certification information. The
certificates allow program properties, even extremely complex ones, to
be
verified automatically. This includes properties of potentially great
practical value, such as adherence to safety and security policies. One
of
the first proposals to gain wide attention was proof-carrying code
(PCC),
and since then several variants of PCC as well as concepts such as typed
assembly language have emerged and are developing into more robust (and
sometimes commercially viable) implementations. The main practical
issue
now is how to create such certified code objects. Some of the problems
are
fundamental in nature, as they involve large-scale verification of
programs.
Other problems involve engineering issues such as the size of the
certificates and
the effort required to verify them.
This talk will provide a brief overview of these techniques and their
current status.
The focus of the talk will be on the state-of-the-art in certification
techniques, with
an emphasis on the technology of certifying compilers. Finally, the
talk will conclude
with prospects for the future.
Host: Professor Harry R. Lewis
This archive was generated by hypermail 2b28 : Thu Jan 25 2001 - 16:08:01 EST