Gilles Barthe: An Overview of Certificate Translation

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. This talk will provide an overview of certificate translation, a mechanism that allows to transfer evidence from source programs to compiled programs.

Rocco De Nicola: ULTRAS: Unified Labelled Transition Systems

Rate Transition Systems (RTS) are special kind of transition systems introduced for defining stochastic behaviour of processes and for associating Continuous Time Markov Chains to process terms. The transition relation associates to each process, for each action, the set of possible futures paired with a measure indicating their rates. RTS have been used for providing an operational semantics to stochastic extensions of classical process algebras. We will introduce ULTRAS as a generalization of RTS that can be used to uniformly describe also the nondeterministic, probabilistic and timed variants of process algebras. We shall then introduce a general notion of equivalences that can instantiated to capture the classical notions, but also stochastic, timed, and probabilistic trace, testing and bisimulation equivalence.

Ugo Montanari: Toward a Game-Theoretic Model of Grid Systems

Both Grid and Global Computing try to address the problem of utilizing scattered idle resources connected across a network. The former aims at creating an illusion of a simple yet large virtual computer from a large set of heterogeneous computers sharing various resource types to benefit a (virtual) organization. Here we consider a Grid structure in the style of the Worldwide LHC Computing Grid, a global organization linking grid infrastructures and computer centers worldwide for the purpose of distributing, storing and analyzing the immense amount of data being generated by Large Hadron Collider (LHC) at the European Organization for Nuclear Research (CERN). The Grid consists of several `sites', each of which may provide computational and data-storage resources for user submitted jobs. Besides the sites, the Grid includes a central `global scheduler' that is responsible for the allocation of jobs to sites, with the main goal of improving the overall throughput of the Grid.

Game theory is a mathematical-economic discipline that studies situations in which multiple independent agents - possibly featuring different or conflicting goals - take decisions and try to maximize their returns. A central notion in Game theory is that of `Nash equilibrium', a situation in which no player can improve its own payoff by unilaterally changing its strategy.

Distributed computing and game theory share common problems, such as dealing with systems where many agents face uncertainty, and possibly have different goals. In such non-cooperative systems, optimization does not amount to maximizing/minimizing a unique common function but rather to find a `stable' situation in which, for instance, sites guarantee to equally treat remote and local jobs, i.e. a Nash Equilibrium. To this purpose, we formulate a repeated non-cooperative Grid scheduling game in which Grid sites are considered as the players of the game, and the actions that are available to players range over various job scheduling policies. We prove that the situation in which every player plays Earliest Response Time (ERT) is a Nash equilibrium, thus achieving a model in which a strategy that essentially contributes to the well-functioning of the Grid is indeed convenient for every player.

Giuseppe Persiano: Predicate Encryption for Secure Remote Storage

Predicate encryption is a special encryption method that allows one to release keys to compute specific predicates of the plaintext without having to decrypt. This cryptographic primitive is instrumental for executing search on encrypted data and enables remote storage of data. Predicate encryption dispenses with the need of downloading and decrypting the whole data set whenever a search needs to be performed.

In this talk, I overview security models and constructions proposed and suggest a few applications.

Davide Sangiorgi: Higher-order concurrency: termination and liveness properties

A higher-order concurrent language is one that combines message-passing and functional constructs. In the talk, I discuss type systems that guarantee termination on the (internal) computations of programs in these languages. I first illustrate the interest of the problem, including the possibility of combining the termination analysis with deadlock analysis so to obtain a powerful analyser for general liveness properties.

I then review two approaches to termination. The first one draws on the method of logical relations, a well-known technique from higher-order sequential languages. The second approach exploits notions from term rewriting. Finally I show how to combine the two approaches and discuss the usefulness of this.

Don Sannella: Techniques for Resource Analysis of Java Bytecode

Recent work in resource analysis has translated the idea of amortised resource analysis to imperative languages using a program logic that allows mixing of assertions about heap shapes, in the tradition of separation logic, and assertions about consumable resources. Separately, polyhedral methods have been used to calculate bounds on numbers of iterations in loop-based programs. We are attempting to combine these ideas to deal with Java programs involving both data structures and loops, focusing on the bytecode level rather than on source code.

Vladimiro Sassone: Trust in Crowds: Probabilistic Behaviour in Anonymity Protocols

The existing analysis of the Crowds anonymity protocol assumes that a participating member is either 'honest' or 'corrupt.' We generalise this by assuming members to maliciously disclose the identity of other nodes with a probability determined by their vulnerability to corruption. We use this enhanced, probabilistic model to study the anonymity guarantees of Crowds, and formulate the necessary conditions to achieve 'probable innocence.' Using such conditions, we then propose a generalised protocol which uses trust information to achieve 'probable innocence' for principals exhibiting probabilistic malicious behaviour.