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:
- PCC scenarios (Gilles Barthe, INRIA)
A high-level overview of the Mobius goals and scientific objectives.
- 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.
- 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).
- 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.
- 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.
- 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.
- 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: