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.