Copenhagen Programming Language Seminar

Resource Guarantees and PCC: 50 ways to say it with a proof

I. Stark
University of Edinburgh

Wedensday, October 3, 10:00-11:00
ITU , Rued Langgaards Vej 7, Room 4A.14


In collaboration with a number of European partners, the
Mobility+Security group at Edinburgh have been investigating the use
of Proof-Carrying Code to implement "Resource Guarantees" for the Java Virtual Machine.

Proof-carrying code is a technology for assuring the safety and security of mobile applications. Conventional cryptographic digital signatures tell us who supplied a program --- who to blame if it goes wrong. Proof-carrying code complements this with digital evidence about the program itself, which can be checked by the user or any third party.

I'll describe and demonstrate a working implementation of this, where Java class files carry certificates of their heap space usage that are independently verified before execution. These certificates are generated during compilation of an ML-like source language into Java bytecodes; using resource types, inferred from the source program, that capture the required information about heap usage. Code consumers may specify resource policies against which incoming class files are checked; where both certificates and policies are expressed in a general bytecode logic that can capture various different kinds of resource.

More generally, I'll discuss associated work on some of the very many different ways to engage PCC: such as wholesale code certification for application distributors; tactic-carrying code; algebras of resources; validation of optimising compilation; adaptive proofs for heterogeneous clients; languages for resource policies; probabilistically checkable proofs; and PCC in large scientific databases.

This work is part of the MRG, ReQueST and Mobius projects funded by the UK EPSRC and the European Commission Framework Programme.

Note: Contents can vary. May not actually contain 50 ways.

Scientific host:Thomas Hildebrandt and Lars Birkedal The Programming, Logic and Semantics (PLS) research group at ITU.. Administrative host: Annette Enggaard . All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org