MOBIUS TUTORIAL at ETAPS 07 (Sunday April 1, 2007)

This tutorial introduces participants to the central security architecture of Mobius as well as type systems, logics, and tools that enable static verification of Java source and bytecode.

You can download the brochure :

Contents

The proposed tutorial consists of the following units:

1. PCC scenarios (Gilles Barthe, INRIA) A high-level overview of the Mobius goals and scientific objectives.
2. Type systems I: Secure information flow (David Pichardie, IRISA) We will present an information flow type system for a sequential JVM-like language that includes classes, objects, arrays, exceptions and method calls, and prove that it guarantees non-interference.
3. Type systems II: Resource control (David Aspinall, Univ. of Edinburgh) An overview of type systems (and related static analysis tools) developed in Mobius for resource control. These include mechanisms for managing heap space consumption, access controls, and external resources (e.g. billable events).
4. Type systems III: Ownership (Peter Müller, ETH Zurich) An introduction to ownership type systems for alias control, in particular, the Universe type system, and their application to program verification.
5. Mobius logics (Lennart Beringer, LMU Munich) An introduction to the base formalisms underlying the Mobius verification architecture: operational model of Java bytecode, program logic for verification of JML-like specifications, representation of (resource) type systems in program logics.
6. Mobius tool suite (Joe Kiniry, UC Dublin) We will review the primary features of the Mobius Program Verification Environment, which is based upon the Eclipse platform. In particular, we will review the environment's "lightweight" features that support writing, modifying, and checking annotations (statically and at runtime), and "heavyweight" features that focus upon program verification with integrated automatic and interactive theorem provers.
7. Perspectives (Gilles Barthe, INRIA) How the results presented in the tutorial fit into the wider view of Mobius; conclusion, ongoing work, and future work.

Learning Objectives

The objective of this tutorial is to get an overview of state-of-the-art techniques and tools for reasoning about security and functional correct properties of object-oriented code as well as their application to Proof-Carrying Code.

Intended Audience

The target audience of the tutorial consists of researchers and practitioners interested in Proof-Carrying Code, type systems, program verification.

The Mobius project will hold its annual End User Panel meeting in conjunction with ETAPS and invite all members of the End User Panel to the tutorial. However attendance is OPEN.

Participants should have interest in security, formal methods and object-oriented programming. Experience with a particular language, formalism, or tool is not required.

Registration

Registration are closed.

Agenda

9:00 - 9:45 PCC scenarios and platform (Gilles Barthe)

9:45 - 10:30 Type systems I: Secure information flow (David Pichardie)

10:30 - 11:00 break

11:00 - 11:45 Type systems II: Resource control (David Aspinall)

11:45 - 12:30 Type systems III: Ownership (Peter Müller)

14:00 - 14:45 Mobius logics (Lennart Beringer)

14:45 - 15:30 Mobius tool suite (Joe Kiniry)

16:00 - 16:45 Perspectives (Gilles Barthe)

16:45 - 17:30 Discussion (Peter Müller)

Slides

• You can download the complete presentation from the following link: