[Pl-seminar] Talk announcement: Danny Dubé, **tomorrow** 2/18, 3pm

[Aaron Turon]

**NOTE: nonstandard day and time**

NEU Programming Languages Seminar presents

Danny Dubé
Visiting NEU from Université Laval, Canada

Thursday, Feb 18, 2010
3:00-4:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Coffee, tea and cookies will be served.


Title:  Encoding the program correctness proofs as programs in PCC technology

Abstract:

One of the key issues with the practical applicability of
Proof-Carrying Code (PCC) and its related methods is the difficulty to
communicate the proofs, which are inherently large.  Previous
approaches to alleviate this problem suffer from drawbacks of their
own, especially the enlargement of the Trusted Computing Base, in
which any bug may cause an unsafe program to be accepted.  We propose
another approach: the Extended PCC framework (EPCC).  In EPCC, a proof
generator, which is a program itself, is transmitted instead of the
usual PCC proof.  EPCC provides the ability to execute the proof
generator and recover the original proof at the consumer side in a
secure manner via the use of the small and safe Virtual machine for
EPCC, the VEP.  The VEP is a minor TCB extension of less than 300
lines of C code.  It is a flexible solution that suits the needs of
the PCC variants.

After the presentation of EPCC, I will quickly mention my research
interests in programming languages.