Invited speakers

Sophia Drossopoulou, Imperial College, UK (iFM invited speaker)

Towards Capability Policy Specification and Verification

The object-capability model is the de-facto industry standard widely adopted for the implementation of security policies for web-based software. Object-capabilities in various forms are supported by programming languages such as E, Joe-E, Newspeak, Grace, Cajita, and the newer versions of Javascript. Unfortunately, code written using capabilities tends to concentrate on the low-level mechanism rather than the high-level policy, and the part implementing the policy tends to be tangled with the part implementing the functionality. As a result, such code is not easy to understand or maintain. We argue that the policies which are intended by programs using object capabilities should be made explicit and written separately from the code implementing them. We also argue that the specification of such capability policies requires concepts which go beyond the features of current specification languages. Moreover, we argue that we need methodologies with which to prove that programs adhere to their capability policies as specified. We sketch such a capability policy specification language, and propose capability triples, which are a generalisation of Hoare logic triples. Capability triples consist of conditions, code and conclusions, but interestingly they allow the conditions as well as the conclusion to talk about the state before and after execution of the code, they allow the code to be existentially or universally quantified, and their interpretation quantifies over all modules extending the current module. Based on the famous mint example, we outline its capability policy specifications, we discuss the many possible different interpretations of the informal policies, and demonstrate how we can reason that it satisfies the capability policies. Interestingly, the reasoning makes use of restrictions imposed by the type system, such as final and private.

Helmut Veith, TU Wien, Austria (shared by iFM and FACS)

Shape and Content:
A database-theoretic perspective on the analysis of data structures

The verification community has studied dynamic data structures primarily in a bottom-up way by analyzing pointers and the shapes induced by them. Recent work in fields such as separation logic has made significant progress in extracting shapes from program source code. Many real world programs however manipulate complex data whose structure and content is most naturally described by formalisms from object oriented programming and databases. In recent work, we attempt to bridge the conceptual gap between these two communities. Our approach is based on Description Logics (DLs), a widely used knowledge representation paradigm which gives a logical underpinning for diverse modeling frameworks such as UML and ER. We show how DLs can be used on top of an existing shape analysis to add content descriptions to the shapes.

Rocco De Nicola, IMT Lucca, Italy (shared by FACS and iFM)

A formal approach to autonomic systems programming: The SCEL Language

The autonomic computing paradigm has been proposed to cope with size, complexity and dynamism of contemporary software-intensive systems. The challenge for language designers is to devise appropriate abstractions and linguistic primitives to deal with the large dimension of systems, and with their need to adapt to the changes of the working environment and to the evolving requirements. We propose a set of programming abstractions that permit to represent behaviours, knowledge and aggregations according to specific policies, and to support programming context-awareness, self-awareness and adaptation. Based on these abstractions, we define SCEL (Software Component Ensemble Language), a kernel language whose solid semantic foundations lay also the basis for formal reasoning on autonomic systems behaviour. To show expressiveness and effectiveness of SCEL's design, we present a Java implementation of the proposed abstractions and show how it can be exploited for programming a robotics scenario that is used as a running example for describing features and potentials of our approach.

Jean-Bernard Stefani, INRIA, France (FACS invited speaker)