PCC 2008
Second International Workshop on Proof-Carrying Code

22 June 2008

Carnegie Mellon University
Pittsburgh, Pennsylvania, USA

Registration · Programme

PCC 2008 is a joint LICS and CSF affiliated workshop on Proof-Carrying Code.

Proof-carrying code is an important and distinctive approach to enhancing trust in programs. It provides a practical framework for independent assurance of program behaviour; especially where source code is not available, or the code author and user are unknown to each other.

The workshop will address theoretical foundations of proof-carrying code as well as practical examples and work on alternative application domains. Here "proof" is construed broadly, to include not just mathematical derivations but any formal evidence that supports the static analysis of programs. That is, evidence about an intrinsic property of code and its behaviour that can be independently checked by any user, intermediary, or third party. These manifest guarantees mean that PCC raises trust in the code itself, distinct from and complementary to any existing trust in the creator of the code, the process used to produce it, or its distributor.

Topics include:

• PCC addressing properties of safety, security, and correctness such as:

  Memory safety, information flow, declassification, resource management, access control, protocol enforcement, functional correctness.

• Examples of PCC in application domains, including but not limited to:

  Mobile code, mobile devices, operating systems, grid computing, peer-to-peer computing, active networks, embedded systems, cloud computing, databases, e-Science.

• Probabilistically-checkable proofs, zero-knowledge proofs, proof-on-demand.
• Trust and policy frameworks; supporting modular and extensible systems; compositionality in code and proofs.
• Certifying compilation, proof-transforming compilation, certified verifiers.
• Logics and notions of certificate specific to proof-carrying frameworks.

PCC 2008 follows on from the successful PCC 2006 workshop in Seattle.

Programme

Links: Full schedule of talks; Abstracts

Invited Speakers

• Thomas Jensen Static Analysis for Extended Byte Code Verification
• Zhong Shao Modular Development of Certified System Software

Contributed Papers

• Comparing Semantic and Syntactic Methods in Mechanized Proof Frameworks
  Christian Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel and David Walker
• Noninterference for Mobile Code with Dynamic Security Domains
  Robert Grabowski
• A Logic for Reasoning About Faulty Programs
  Matthew L. Meola, Frances Perry and David Walker.

Workshop Talks

• Limin Jia AURA: A Programming Language for Authorization and Audit
• Robert Atkey A Practical PCC Framework for Java Bytecode
• Andrei Sabelfeld Tight Enforcement of Flexible Information-Release Policies for Dynamic Languages

Registration

Registration is being handled centrally by CMU for CSF, LICS, and all associated workshops. All registrations include lunch, refreshment breaks and wireless internet access for each day of attendance. You can book dorm accommodation on campus with conference registration. In addition, LICS and CSF have also reserved blocks of rooms with local hotels.

• The deadline for early registration is 1 June 2008.
• The deadline for late online registration is 10 June 2008.
• After June 10 you must make special arrangements with the conference organizers to register on-site.

Links: Online registration, LICS hotels, CSF hotels

Programme Committee

• David Aspinall, University of Edinburgh (co-chair)
• Gilles Barthe, INRIA Sophia-Antipolis / IMDEA Software, Madrid
• Nick Benton, Microsoft Research Cambridge
• Adriana Compagnoni, Stevens Institute of Technology
• Karl Crary, Carnegie Mellon University
• Ewen Denney, NASA Ames
• Hans-Wolfgang Loidl, LMU Munich
• George Necula, UC Berkeley / Rinera Networks
• Ian Stark, University of Edinburgh (co-chair)
• Stephanie Weirich, University of Pennsylvania

Important Dates

Organisers

David Aspinall and Ian Stark
Laboratory for Foundations of Computer Science
School of Informatics
The University of Edinburgh

James Clerk Maxwell Building
The King's Buildings
Mayfield Road
Edinburgh EH9 3JZ
Scotland

Contact email: pcc08@easychair.org

Affiliation

LICS 2008: Twenty-Third Annual IEEE Symposium on Logic in Computer Science

CSF: 21st IEEE Computer Security Foundations Symposium

Mobius: Mobility, Ubiquity, Security
Enabling proof-carrying code for Java on mobile devices

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336

Page last modified: Monday 16 June 2008