Selected Papers of the Conferences FORTE and COORDINATION 2014

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

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

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

2. A Program Logic for Verifying Secure Routing Protocols

Chen Chen ; Limin Jia ; Hao Xu ; Cheng Luo ; Wenchao Zhou ; Boon Thau Loo.
The Internet, as it stands today, is highly vulnerable to attacks. However,little has been done to understand and verify the formal security guarantees ofproposed secure inter-domain routing protocols, such as Secure BGP (S-BGP). Inthis paper, we develop a sound program logic for SANDLog-a declarativespecification language for secure routing protocols for verifying properties ofthese protocols. We prove invariant properties of SANDLog programs that run inan adversarial environment. As a step towards automated verification, weimplement a verification condition generator (VCGen) to automatically extractproof obligations. VCGen is integrated into a compiler for SANDLog that cangenerate executable protocol implementations; and thus, both verification andempirical evaluation of secure routing protocols can be carried out in thisunified framework. To validate our framework, we encoded several proposedsecure routing mechanisms in SANDLog, verified variants of path authenticityproperties by manually discharging the generated verification conditions inCoq, and generated executable code based on SANDLog specification and ran thecode in simulation.

3. Type-based Self-stabilisation for Computational Fields

Ferruccio Damiani ; Mirko Viroli.
Emerging network scenarios require the development of solid large-scalesituated systems. Unfortunately, the diffusion/aggregation computationalprocesses therein often introduce a source of complexity that hamperspredictability of the overall system behaviour. Computational fields have beenintroduced to help engineering such systems: they are spatially distributeddata structures designed to adapt their shape to the topology of the underlying(mobile) network and to the events occurring in it, with notable applicationsto pervasive computing, sensor networks, and mobile robots. To assurebehavioural correctness, namely, correspondence of micro-level specification(single device behaviour) with macro-level behaviour (resulting global spatialpattern), we investigate the issue of self-stabilisation for computationalfields. We present a tiny, expressive, and type-sound calculus of computationalfields, and define sufficient conditions for self-stabilisation, defined as theability to react to changes in the environment finding a new stable state infinite time. A type-based approach is used to provide a correct checkingprocedure for self-stabilisation.

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

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

5. Multiparty Session Actors

Rumyana Neykova ; Nobuko Yoshida.
Actor coordination armoured with a suitable protocol description language hasbeen a pressing problem in the actors community. We study the applicability ofmultiparty session type (MPST) protocols for verification of actor programs. Weincorporate sessions to actors by introducing minimum additions to the modelsuch as the notion of actor roles and protocol mailboxes. The framework usesScribble, which is a protocol description language based on multiparty sessiontypes. Our programming model supports actor-like syntax and runtimeverification mechanism guaranteeing communication safety of the participatingentities. An actor can implement multiple roles in a similar way as an objectcan implement multiple interfaces. Multiple roles allow for cooperativeinter-concurrency in a single actor. We demonstrate our framework by designingand implementing a session actor library in Python and its runtime verificationmechanism. Benchmark results demonstrate that the runtime checks inducenegligible overhead. We evaluate the applicability of our verificationframework to specify actor interactions by implementing twelve examples from anactor benchmark suit.

6. Discovering, quantifying, and displaying attacks

Roberto Vigo ; Flemming Nielson ; Hanne Riis Nielson.
In the design of software and cyber-physical systems, security is oftenperceived as a qualitative need, but can only be attained quantitatively.Especially when distributed components are involved, it is hard to predict andconfront all possible attacks. A main challenge in the development of complexsystems is therefore to discover attacks, quantify them to comprehend theirlikelihood, and communicate them to non-experts for facilitating the decisionprocess. To address this three-sided challenge we propose a protection analysisover the Quality Calculus that (i) computes all the sets of data required by anattacker to reach a given location in a system, (ii) determines the cheapestset of such attacks for a given notion of cost, and (iii) derives an attacktree that displays the attacks graphically. The protection analysis is firstdeveloped in a qualitative setting, and then extended to quantitative settingsfollowing an approach applicable to a great many contexts. The quantitativeformulation is implemented as an optimisation problem encoded intoSatisfiability Modulo Theories, allowing us to deal with complex coststructures. The usefulness of the framework is demonstrated on a national-scaleauthentication system, studied through a Java implementation of the framework.