Copenhagen Programming Language Seminar
In collaboration with a number of European partners, the
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.
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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org