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 […]

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 […]

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 […]

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 […]

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 […]

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 […]