PCC on Friday, August 11th

Session 1: Welcoming and Keynote Address (09:15‑10:30)
Location: Metropolitan B

09:15‑09:30

Welcoming Remarks

09:30‑10:30

Andrew Appel (Princeton University) A Very Modal Model of a Modern, Major, General Type System Semantic approaches to machine-checkable proofs of type soundness for Proof-Carrying Code have not been easy---until now. We present a clean and powerful model of recursive and impredicatively quantified types with mutable references. Our model is less restrictive than previous models of impredicative references. We model all of the type constructors needed for typed intermediate languages and typed assembly languages for object-oriented and functional languages; our technique is applicable to any small-step semantics including lambda-calculus, labeled transition systems, and von Neumann machines. We have reduced the system to such a simple formulation that it becomes clear that what we have is a Kripke semantics of the Goedel-Loeb (GL) logic of provability. We have machine-checked proofs in Coq. This is joint work with Paul-André Melliès, Christopher D. Richards, and Jérôme Vouillon.

Break (10:30‑11:00)

Session 2: Invited Talks (11:00‑12:30)
Location: Metropolitan B

11:00‑11:30	Amal Ahmed (Harvard University)
11:30‑12:00	Adriana Compagnoni (Stevens Institute of Technology) Information Flow Analysis for Low-Level Languages This work addresses the problems raised by the study of confidentiality for Multi-Level Security systems in the context of low-level languages. In particular, we studied the vulnerabilities introduced by the absence of control flow constructs, the reuse of registers, and the manipulation of a control stack. In this talk, I will present language-based techniques used for the development of type systems for low-level languages that guarantee that well-typed programs preserve confidentiality.
12:00‑12:30	Dachuan Yu (Yale University) Toward More Typed Assembly Languages for Confidentiality [ppt] Low-level languages are starting to receive attention in the studies of information-flow questions, especially from the perspective of typed assembly languages and certifying compilation. In some recent work, type annotations are used to restore the missing abstractions in assembly code, and type-preserving compilation is used to preserve security evidence from the source to the target. By security-type checking directly at the target level, code consumers gain higher confidence on the behavior of untrusted code. Although a good start, existing work in this area has only focused on relatively simple settings, largely ignoring the timing behaviors of assembly programs. Unfortunately, timing behaviors, both external and internal ones, present some channels of information flow that can be easily exploited. This talk presents our progress toward addressing some of these covert information-flow channels in assembly code, including termination, timing, possibilistic and probabilistic channels. It is inspired by source-level information-flow type systems which account for program timing behaviors. On top of our previous work on a typed assembly language for confidentiality, we introduce additional annotations to document the timing of the program execution. These timing annotations are used to express various source-level constraints, such as the absence of high loops in any security contexts and the absence of any loops in high security contexts. We discuss how to accommodate these annotations in a type system and how to produce these annotations given securely typed source programs.

Lunch break (12:30‑14:00)

Session 3: Keynote Address (14:00‑15:00)
Location: Metropolitan B

14:00‑15:00

Ian Stark (University of Edinburgh) Resource Guarantees and PCC: 50 ways1 to say it with a proof [pdf] In collaboration with various 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. 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. 1. Note: Contents may vary.

Session 4: Posters (15:00‑15:30)
Location: Cedar

Break (15:30‑16:00)

Session 5: Posters (continued) (16:00‑16:30)
Location: Cedar

Session 6: Invited Talks (16:30‑17:30)
Location: Metropolitan B

16:30‑17:00

Tamara Rezk (INRIA) Certificate Translation [pdf] Program verification techniques based on programming logics and verification condition generators provide a powerful means to reason about programs. Whereas these techniques have very often been employed in the context of high-level languages in order to benefit from their structural nature, it is often required, especially in the context of mobile code, to prove the correctness of compiled programs. Thus it is highly desirable to have a means of bringing the benefits of source code verification to code consumers. We propose certificate translation, a mechanism that allows to transfer evidence from source programs to compiled programs. It builds upon the notion of certificate, which is used in Proof Carrying Code architectures to convey to the code consumer easily verifiable evidence that programs respect some policy. A certificate translator is an algorithm that turns certificates of source programs into certificates of compiled programs; its definition is tightly bound to the compiler used for programs, and the main difficulty in defining one stems from the optimizations performed by the compiler. In order to illustrate the feasibility of our approach, we build certificate translators for an optimizing compiler from a simple imperative language to an intermediate RTL language. Co-authors: G Barthe and B Gregoire and C Kunz and T Rezk

17:00‑17:30

Zhong Shao (Yale University) A Translation from Typed Assembly Languages to Certified Assembly Programming [ppt] Typed assembly languages (TAL) and certified assembly programming (CAP) are two new techniques for certifying assembly programs and for building proof-carrying code. TAL uses syntactic types (for reasoning) while CAP uses Hoare-style logic assertions. Because of the differences between type system and logic, TAL and CAP are suitable for different kinds of programming tasks. Previously, programs verified in TAL and CAP can not directly interoperate with each other so it is hard to integrate them into a single PCC system. In this talk we compare the TAL and CAP approaches and present a type-preserving translation from TAL to XCAP---a recent CAP language that provides modular support for embedded code pointers and impredicative polymorphism. Our translation supports other common language features such as general references and recursive types. Our paper gives a clear account of the relationship between type-based and logic-based approaches for certifying assembly programs. This is a joint work with Zhaozhong Ni at Yale University.