>X-NS-Transport-ID: 080020884593011F51FB
>Date: Tue, 21 Sep 1999 00:22:42 PDT
>From: Drew Dean <ddean@parc.xerox.com>
>Subject: 9/23 PARC Forum: Proof-Carrying Code: Design, Implementation and
>Applications
>To: OpenPARCForum.PARC@xerox.com
>Sender: owner-colloq-ext@lists.Stanford.EDU
>Precedence: bulk
>
>XEROX PARC FORUM
>Thursday, September 23, 1999
>4:00 - 5:00 p.m.
>
>Proof-Carrying Code: Design, Implementation and Applications
>
>George C. Necula, Assistant Professor of Electrical Engineering and
>Computer Science, University of California, Berkeley
>
>In an environment where more and more code cannot be trusted to
>behave safety it is becoming necessary to employ mechanisms for
>detecting and preventing unsafe program behavior. Proof-Carrying Code
>is such a technique that allows a code receiver to verify statically
>that the code has certain required properties, which are stated in the
>form of a trusted safety policy. To make this possible the code is
>accompanied by a representation of an easily checkable formal proof of
>compliance with the safety policy. This talk discusses first the
>general properties of the Proof-Carrying Code technique and then
>explores a particular implementation of the idea using verification
>condition generators.
>
>There are two major challenges in using Proof-Carrying Code. One lies
>in producing the necessary formal compliance proofs. The talk will
>describe briefly an optimizing compiler that, while compiling a safe
>subset of the C programming language, produces proofs of type safety
>for the resulting machine code.
>
>The final part of the talk will give a hint of how Proof-Carrying
>Code could be used to enforce more that just type safety. This will be
>done for an example of a safety policy for active network packets that
>imposes running time and bandwidth usage limitations.
>
>Part of this work has been done jointly with Peter Lee from Carnegie
>Mellon University. Further information and an online demo can be
>found at http://www.cs.berkeley.edu/~necula/pcc.html
>
>
>This Forum is OPEN to the public.
>
>
>Refreshments will be served from 3:45 to 4:00.
>
>The George Pake Auditorium is located at Xerox PARC, 3333 Coyote Hill
>Road in Palo Alto, off of Page Mill Road.
>
>>From Page Mill Road, turn South on Foothill Expressway, then right on
>Hillview, and take the second entrance to the right.
>
>Park in the large parking lot and enter the auditorium at the upper
>level of the building. The auditorium is located to the left of and
>down the stairs from the main entrance.
>
>There is a map to PARC at:
>
>http://www.parc.xerox.com/images/maptoparc.gif.
>
>
>Note to Xerox employees and contractors: remember to bring your badge
>for re-entry to building 35.
>
>
>Forum Coordinator:
> Drew Dean <ddean@parc.xerox.com>
> Phone: 650 812-4415
>
>Xerox employees may purchase a copy of the forum videotape by
>contacting Mimi Gardner, mgardner@parc.xerox.com. A circulation copy
>will be available to Palo Alto employees through the PARC Information
>Center, library@parc.xerox.com.
>
>
>PARC Forum Web addresses:
> External: http://www.parc.xerox.com/forum
> Internal: http://parcweb.parc.xerox.com/events/forum
>
>[-- For mailing list administrative requests, please send mail to Drew Dean
> <ddean@parc.xerox.com>. Please understand that the PARC Forum
> announcements get forwarded via many mailing lists, and I may be unable
> to help you. Thanks. --DD]
>
Bill Frantz | Macintosh: Didn't do every-| Periwinkle -- Consulting (408)356-8506 | thing right, but did know | 16345 Englewood Ave. frantz@netcom.com | the century would end. | Los Gatos, CA 95032, USA
