Selected Papers of the Conferences FORTE and COORDINATION 2014

Editors: Erika Abraham, Eva Kühn, Catuscia Palamidessi, Rosario Pugliese, Vladimiro Sassone

This special issue contains revised and extended versions of six papers presented at FORTE 2014, the 34th International Conference on Formal Techniques for Distributed Objects, Components and Systems, and COORDINATION 2014, the 16th International Conference on Coordination Models and Languages, held as part of DisCoTec 2014, the 9th International Federated Conference on Distributed Computing Techniques, that took place in Berlin, Germany, during June 3--5, 2014. The DisCoTec series is one of the major events sponsored by the International Federation for Information Processing (IFIP) WG 6.1.

The papers collected in this special issue were invited by the guest editors, taking into account the opinions of the Program Committee members and the expert reviewers expressed during the paper selection process of the two conferences. They underwent a new and thorough reviewing and revision process, in accordance with the usual high standards of LMCS. We are grateful to all authors for their contributions and to the reviewers of the conferences and of this special issue for their thorough and valuable work.<7p>


1. Quantitative information flow under generic leakage functions and adaptive adversaries

Boreale, M. ; Pampaloni, Francesca.
We put forward a model of action-based randomization mechanisms to analyse quantitative information flow (QIF) under generic leakage functions, and under possibly adaptive adversaries. This model subsumes many of the QIF models proposed so far. Our main contributions include the following: (1) we identify mild general conditions on the leakage function under which it is possible to derive general and significant results on adaptive QIF; (2) we contrast the efficiency of adaptive and non-adaptive strategies, showing that the latter are as efficient as the former in terms of length up to an expansion factor bounded by the number of available actions; (3) we show that the maximum information leakage over strategies, given a finite time horizon, can be expressed in terms of a Bellman equation. This can be used to compute an optimal finite strategy recursively, by resorting to standard methods like backward induction.

2. A Program Logic for Verifying Secure Routing Protocols

Chen, Chen ; Jia, Limin ; Xu, Hao ; Luo, Cheng ; Zhou, Wenchao ; Loo, Boon Thau.
The Internet, as it stands today, is highly vulnerable to attacks. However, little has been done to understand and verify the formal security guarantees of proposed secure inter-domain routing protocols, such as Secure BGP (S-BGP). In this paper, we develop a sound program logic for SANDLog-a declarative specification language for secure routing protocols for verifying properties of these protocols. We prove invariant properties of SANDLog programs that run in an adversarial environment. As a step towards automated verification, we implement a verification condition generator (VCGen) to automatically extract proof obligations. VCGen is integrated into a compiler for SANDLog that can generate executable protocol implementations; and thus, both verification and empirical evaluation of secure routing protocols can be carried out in this unified framework. To validate our framework, we encoded several proposed secure routing mechanisms in SANDLog, verified variants of path […]

3. Type-based Self-stabilisation for Computational Fields

Damiani, Ferruccio ; Viroli, Mirko.
Emerging network scenarios require the development of solid large-scale situated systems. Unfortunately, the diffusion/aggregation computational processes therein often introduce a source of complexity that hampers predictability of the overall system behaviour. Computational fields have been introduced to help engineering such systems: they are spatially distributed data structures designed to adapt their shape to the topology of the underlying (mobile) network and to the events occurring in it, with notable applications to pervasive computing, sensor networks, and mobile robots. To assure behavioural correctness, namely, correspondence of micro-level specification (single device behaviour) with macro-level behaviour (resulting global spatial pattern), we investigate the issue of self-stabilisation for computational fields. We present a tiny, expressive, and type-sound calculus of computational fields, and define sufficient conditions for self-stabilisation, defined as the ability to […]

4. Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion

Debois, Søren ; Hildebrandt, Thomas ; Slaats, Tijs ; Yoshida, Nobuko.
We present the first session typing system guaranteeing request-response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (data-based) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.

5. Discovering, quantifying, and displaying attacks

Vigo, Roberto ; Nielson, Flemming ; Nielson, Hanne Riis.
In the design of software and cyber-physical systems, security is often perceived as a qualitative need, but can only be attained quantitatively. Especially when distributed components are involved, it is hard to predict and confront all possible attacks. A main challenge in the development of complex systems is therefore to discover attacks, quantify them to comprehend their likelihood, and communicate them to non-experts for facilitating the decision process. To address this three-sided challenge we propose a protection analysis over the Quality Calculus that (i) computes all the sets of data required by an attacker to reach a given location in a system, (ii) determines the cheapest set of such attacks for a given notion of cost, and (iii) derives an attack tree that displays the attacks graphically. The protection analysis is first developed in a qualitative setting, and then extended to quantitative settings following an approach applicable to a great many contexts. The […]

6. Multiparty Session Actors

Neykova, Rumyana ; Yoshida, Nobuko.
Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailboxes. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing communication safety of the participating entities. An actor can implement multiple roles in a similar way as an object can implement multiple interfaces. Multiple roles allow for cooperative inter-concurrency in a single actor. We demonstrate our framework by designing and implementing a session actor library in Python and its runtime verification mechanism. Benchmark results demonstrate that the runtime checks […]