Hugo A López

Flemming Nielson

Hanne Riis Nielson

Enforcing Availability in Failure-Aware Communicating Systems

Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where the availability of components may change at runtime. We introduce the Global Quality Calculus (GCq), a process calculus featuring novel operators for multiparty, partial and collective communications; we provide a type discipline that controls how partial communications refer only to available components; and we show that well-typed choreographies enjoy progress.

Introduction

Choreographies are a well-established formalism in concurrent programming, with the purpose of providing a correct-by-construction framework for distributed systems [START_REF] Carbone | Structured communication-centered programming for web services[END_REF][START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF]. Using Alice-Bob's style protocol narrations, they provide the structure of interactions among components in a distributed system. Combined with a behavioral type system, choreographies are capable of deriving distributed (endpoint) implementations. Endpoints generated from a choreography ascribe all and only the behaviors defined by it. Additionally, interactions among endpoints exhibit correctness properties, such as liveness and deadlock-freedom. In practice, choreographies guide the implementation of a system, either by automating the generation of correct deadlock-free code for each component involved, or by monitoring that the execution of a distributed system behaves according to a protocol [START_REF] Carbone | Structured communication-centered programming for web services[END_REF][START_REF] Neykova | Timed runtime monitoring for multiparty conversations[END_REF][START_REF] Bocchi | Monitoring networks through multiparty session types[END_REF].

In this paper we study the role of availability when building communication protocols. In short, availability describes the ability of a component to engage in a communication. Insofar, the study of communications using choreographies assumed that components were always available. We challenge this assumption on the light of new scenarios. The case of Cyber-Physical Systems (CPS) is one of them. In CPS, components become unavailable due to faults or because of changes in the environment. Even simple choreographies may fail when including availability considerations. Thus, a rigorous analysis of availability conditions in communication protocols becomes necessary, before studying more advanced properties, such as deadlock-freedom or protocol fidelity.

Practitioners in CPS take availability into consideration, programming applications in a failure-aware fashion. First, application-based QoS policies replace old node-based ones. Second, one-to-many and many-to-one communication patterns replace peer-to-peer communications. Still, programming a CPS from a component viewpoint such that it respects an application-based QoS is difficult, because there is no centralized way to ensure its enforcement.

This paper advocates a choreography-based approach for the development of failure-aware communication protocols, as exemplified by CPS. On the one hand, interactions described in choreographies take a global viewpoint, in the same way application-based QoS describe availability policies in a node-conscious fashion. On the other hand, complex communication including one-to-many and many-to-one communications can be explicitly defined in the model, which is a clear advantage over component-based development currently used in CPS. Finally, choreographies give a formal foundation to practical development of distributed systems, with Chor [START_REF] Carbone | Chor: A choreography programming language for concurrent systems[END_REF], ParTypes [START_REF] López | Protocol-based verification of message-passing parallel programs[END_REF] and Scribble [START_REF] Yoshida | The scribble protocol language[END_REF].

Contributions. First, we present the Global Quality Calculus (GC q ), a process calculus aimed at capturing the most important aspects of CPS, such as variable availability conditions and multicast communications. It is a generalization of the Global Calculus [START_REF] Carbone | Structured communication-centered programming for web services[END_REF][START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF], a basic model for choreographies and the formal foundation of the Chor Programming language [START_REF] Carbone | Chor: A choreography programming language for concurrent systems[END_REF]. With respect to the Global Calculus, GC q introduces two novel aspects: First, it extends the communication model to include collective communication primitives (broadcast and reduce). Second, it includes explicit availability considerations. Central to the calculus is the inclusion of quality predicates [START_REF] Nielson | A calculus for quality[END_REF] and optional datatypes, whose role is to allow for communications where only a subset of the original participants is available.

Our second contribution relates to the verification of failure-aware protocols. We focus on progress. As an application-based QoS, a progress property requires that at least a minimum set of components is available before firing a communication action. Changing availability conditions may leave collective communications without enough required components, forbidding the completion of a protocol. We introduce a type system, orthogonal to session types, that ensures that well-typed protocols with variable availability conditions do not get stuck, preserving progress.

Document Structure In §2 we introduce the design considerations for a calculus with variable availability conditions and we present a minimal working example to illustrate the calculus in action. §3 introduces syntax and semantics of GC q . The progress-enforcing type system is presented in §4. Section §5 discusses related work. Finally, §6 concludes. Appendix includes additional definitions and proof sketches of the main results, and is intended only for reviewing purposes.

Towards a Language for CPS Communications

The design of a language for CPS requires a technology-driven approach, that answers to requirements regarding the nature of communications and devices in-volved in CPS. Similar approaches have been successfully used for Web-Services [START_REF] Carbone | A theoretical basis of communication-centred concurrent programming[END_REF][START_REF] Yoshida | The scribble protocol language[END_REF][START_REF] Montesi | Service-oriented programming with jolie[END_REF], and Multicore Programming [START_REF] López | Protocol-based verification of message-passing parallel programs[END_REF][START_REF] Cogumbreiro | Coordinating phased activities while maintaining progress[END_REF]. The considerations on CPS used in this work come from well-established sources [START_REF] Alur | Principles of Cyber-Physical Systems[END_REF][START_REF] Perillo | Wireless sensor network protocols[END_REF]. We will proceed by describing their main differences with respect to traditional networks.

Unique Features in CPS Communications

Before defining a language for communication protocols in CPS, it is important to understand the taxonomy of networks where they operate. CPS are composed by sensor networks (SN) that perceive important measures of a system, and actuator networks that change it. Some of the most important characteristics in these networks include asynchronous operation, sensor mobility, energy-awareness, application-based protocol fidelity, data-centric protocol development, and multicast communication patterns. We will discuss each of them.

Asynchrony. Depending on the application, deployed sensors in a network have less accessible mobile access points, for instance, sensors deployed in harsh environmental conditions, such as arctic or marine networks. Environment may also affect the lifespan of a sensor, or increase its probability of failure. To maximize the lifespan of some sensors, one might expect an asynchronous operation, letting sensors remain in a standby state, collecting data periodically.

Sensor Mobility. The implementation of sensors in autonomic devices brings about important considerations on mobility. A sensor can move away from the base station, making their interactions energy-intensive. In contrast, it might be energy-savvy to start a new session with a different base station closer to the new location.

Energy-Awareness. Limited by finite energetic resources, SN must optimize their energy consumption, both from node and application perspectives. From a nodespecific perspective, a node in a sensor network can optimize its life by turning parts of the node off, such as the RF receiver. From a application-specific perspective, a protocol can optimize it energy usage by reducing its traffic. SN cover areas with dense node deployment, thus it is unnecessary that all nodes are operational to guarantee coverage. Additionally, SN must provide self-configuration capabilities, adapting its behavior to changing availability conditions. Finally, it is expected that some of the nodes deployed become permanently unavailable, as energetic resources ran out. It might be more expensive to recharge the nodes than to deploy new ones. The SN must be ready to cope with a decrease in some of the available nodes.

Data-Centric Protocols. One of the most striking differences to traditional networks is the collaborative behavior expected in SN. Nodes aim at accomplishing a similar, universal goal, typically related to maintaining an application-level quality of service (QoS). Protocols are thus data-centric rather than node-centric. Moreover, decisions in SN are made from the aggregate data from sensing nodes,

start t0[M ]{Ac 0 }, t1[S]{Ac 1 }, t2[S]{Ac 2 }, t3[S]{Ac 3 } : temperature(k); t0{Ac 0 ; M s 0 } > &q 1 (t1{Ac 1 ; M s 1 }, t2{Ac 2 ; M s 2 }, t3{Ac 3 ; M s 3 }) : k[measure];
&q 2 (t1{Ms 1 ; E 1 }."1", t2{Ms 2 ; E 2 }."-2", t3{Ms 3 ; E 3 }."5") > t0{Ms 0 ; E 0 } : xm : k, avg ; 0 Fig. 1: Example: Sensor network choreography rather than the specific data of any of them [START_REF] Pattem | The impact of spatial correlation on routing with compression in wireless sensor networks[END_REF]. Collective decision-making based in aggregates is common in SN, for instance, in protocols suites such as SPIN [START_REF] Heinzelman | Adaptive protocols for information dissemination in wireless sensor networks[END_REF] and Directed Diffusion [START_REF] Intanagonwiwat | Directed diffusion: a scalable and robust communication paradigm for sensor networks[END_REF]. Shifting from node-level to applicationlevel QoS implies that node fairness is considerably less important than in traditional networks. In consequence, the analysis of protocol fidelity [START_REF] Honda | Language Primitives and Type Discipline for Structured Communication-Based Programming[END_REF] requires a shift from node-based guarantees towards application-based ones.

Multicast Communication. Rather than peer-to-peer message passing, one-tomany and many-to-one communications are better solutions for energy-efficient SN, as reported in [START_REF] Heinzelman | An applicationspecific protocol architecture for wireless microsensor networks[END_REF][START_REF] Deng | Balanced-energy sleep scheduling scheme for high-density cluster-based sensor networks[END_REF]. However, as the number of sensor nodes in a SN scales to large numbers, communications between a base and sensing nodes can become a limiting factor. Many-to-one traffic patterns can be combined with data aggregation services (e.g.: TAG [START_REF] Madden | TAG: A tiny aggregation service for ad-hoc sensor networks[END_REF] or TinyDB [START_REF] Madden | The design of an acquisitional query processor for sensor networks[END_REF]), minimizing the amount and the size of messages between nodes.

Model Preview

We will illustrate how the requirements for CPS communications have been assembled in our calculus through a minimal example in Sensor Networks (SN). The syntax of our language is inspired on the Global Calculus [START_REF] Carbone | Structured communication-centered programming for web services[END_REF][START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF] extended with collective communication operations [START_REF] López | Protocol-based verification of message-passing parallel programs[END_REF].

Example 1. Figure 1 portrays a simple SN choreography for temperature measurement. Line 1 models a session establishment phase between sensors t 1 , t 2 , t 3 (each of them implementing role S) and a monitor t m with role M . In Line 2, t m invoques the execution of method measure at each of the sensors. In Line 3, an asynchronous many-to-one communication (e.g. reduce) of values of the same base type (int in this case) is performed between sensors and the monitor. Quality predicates q 1 , q 2 model application-based QoS, established in terms of availability requirements for each of the nodes. For instance, q 1 = q 2 = ∀ only allows communications with all sensors in place, and q 1 = ∀, q 2 = 2/3 tolerates the absence of one of the sensors in data harvesting. Once nodes satisfy applications' QoS requirements, an aggregation operation will be applied to the messages received, in this case computing the average value.

One important characteristic of fault-tolerant systems, of which CPS are part, is known as graceful degradation. Graceful degradation allows a system to maintain functionality when portions of a system break down, for instance, when some of the nodes are unavailable for a communication. The use of different quality predicates q 1 = ∀, q 2 = 2/3 allow us to describe choreographies that gracefully degrade, since the system preserves functionality despite one of the nodes is unavailable.

Considerations regarding the impact of available components in a communication must be tracked explicitly. Annotations {X; Y } (in blue font) define capabilities, that is, control points achieved in the system. The X in t{X; Y } denotes the required capability for t to act, and Y describes the capability offered after t has engaged in an interaction. No preconditions are necessary for establishing a new session, so no required capabilities are necessary in Line 1. After a session has been established, capabilities (Ac i ) i∈{0...3} are available in the system. Lines 2 and 3 modify which capabilities are present depending on the number of available threads. For example, a run of the choreography in Figure 1 with q 1 = 2/3 will update capabilities from {Ac 0 , Ac 1 , Ac 2 , Ac 3 } to any of the sets {M s

0 , Ac 1 , M s 2 , M s 3 }, {M s 0 , M s 1 , Ac 2 , M s 3 }, {M s 0 , M s 1 , M s 2 , Ac 3 }, or {M s 0 , M s 1 , M s 2 , M s 3 }.
The interplay between capabilities and quality predicates may lead to choreographies that cannot progress. For example, the choreography above with q 2 = ∀ will be stuck, since three of the possible evolutions fail to provide capabilities {M s 0 , M s 1 , M s 2 , M s 3 }. We will defer the discussion about the interplay of capabilities and quality predicates to Section 4.

3 The Global Quality Calculus (GC q )

In the following, C denotes a choreography; p denotes an annotated thread t[A]{X; Y }, where t is a thread, X, Y are atomic formulae and A is a role annotation. We will use t to denote {t 1 , . . . , t j } for a finite j. Variable a ranges over service channels, intuitively denoting the public identifier of a service, and k ∈ N ranges over a finite, countable set of session (names), created at runtime. Variable x ranges over variables local to a thread. We use terms t to denote data and expressions e to denote optional data, much like the use of option data types in programming languages like Standard ML [START_REF] Harper | Programming in Standard ML[END_REF]. Expressions include arithmetic and other first-order expressions excluding service and session channels. In particular, the expression some(t) signals the presence of some data t and none the absence of data. In our model, terms denote closed values v. Names m, n range over threads and session channels. For simplicity of presentation, all models in the paper are finite.

Definition 1 (GC q syntax). A novelty in this variant of the Global calculus is the addition of quality predicates q binding vectors in a multiparty communication. Essentially, q determines when sufficient inputs/outputs are available. As an example, q can be ∃, meaning that one sender/receiver is required in the interaction, or it can be ∀ meaning that all of them are needed. The syntax of q and other examples can be summarised in Figure 2. We require q to be monotonic (in the sense that q( t r ) implies q( t s ) for all t s ⊆ t r ) and satisfiable.

| pr > &q( ps) : k[l] (select) [[∀]]( tr) = (|{ti ∈ tr | ti = tt}| = n|) n = | tr| [[∃]]( tr) = (|{ti ∈ tr | ti = tt}| ≥ 1|) n = | tr| [[m/n]]( tr) = (|{ti ∈ tr | ti = tt}| ≥ m|) n = | tr| (reduce)
We will focus our discussion on the novel interactions. First, start defines a (multiparty) session initiation between active annotated threads p r and annotated service threads p s . Each active thread (resp. service thread) implements the behaviour of one of the roles in A r (resp. A s ), sharing a new session name k. We assume that a session is established with at least two participating processes, therefore 2 ≤ | p r | + | p s |, and that threads in p r ∪ p s are pairwise different.

The language features broadcast, reduce and selection as collective interactions. A broadcast describes one-to-many communication patterns, where a session channel k is used to transfer the evaluation of expression e (located at p r ) to threads in p s , with the resulting binding of variable x i at p i , for each p i ∈ p s . At this level of abstraction, we do not differentiate between ways to implement one-to-many communications (so both broadcast and multicast implementations are allowed). A reduce combines one-to-many communications and aggregation [START_REF] Madden | TAG: A tiny aggregation service for ad-hoc sensor networks[END_REF]. In & q ( p r .e r ) > p s : x : k, op , each annotated thread p i in p r evaluates an expression e i , and the aggregate of all receptions is evaluated using op (an operator defined on multisets such as max, min, etc.). Interaction p r > & q ( p s ) : k[l] describes a collective label selection: p r communicates the selection of label l to peers in p s through session k.

Central to our language are progress capabilities. Pairs of atomic formulae {X; Y } at each annotated thread state the necessary preconditions for a thread to engage (X), and the capabilities provided after its interaction (Y ). As we will see in the semantics, there are no associated preconditions for session initiation (i.e. threads are created at runtime), so we normally omit them. Explicit x@p/e@p indicate the variable/boolean expression x/e is located at p. We often omit 0, empty vectors, roles, and atomic formulae {X; Y } from annotated threads when unnecessary.

The free term variables fv(C) are defined as usual. An interaction η in η; C can bind session channels, choreographies and variables. In start, variables { p r , a} are free while variables { p s , k} are bound (since they are freshly cre-

T(η) # T(η ) η; (η ; C) C η ; (η; C) p /
∈ T(η) if e@p then η; C1 else η; C2 C η; if e@p then C1 else C2 p = r if e@p then (if e @r then C1 else C2) else

(if e @r then

C 1 else C 2 ) C
if e @r then (if e@p then C1 else C 1 ) else (if e@p then C2 else C 2 )

Fig. 3: Swap congruence relation, C ated). In broadcast, variables x s are bound. A reduce binds {x}. Finally, we assume that all bound variables in an expression have been renamed apart from each other, and apart from any other free variables in the expression.

Expressivity The importance of roles is only crucial in a start interaction. Technically, one can infer the role of a given thread t used in an interaction η by looking at the start interactions preceding it in the abstract syntax tree. GC q can still represent unicast message-passing patterns as in [START_REF] Carbone | Structured communication-centered programming for web services[END_REF]. Unicast communication p 1 .e > p 2 :

x : k can be encoded in multiple ways using broadcast/reduce operators. For instance, p

Semantics

Choreographies are considered modulo standard structural and swapping congruence relations (resp. ≡, C ). Relation ≡ is defined as the least congruence relation on C supporting α-renaming, such that (C, 0, +) is an abelian monoid. The swap congruence [START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF] provides a way to reorder non-conflicting interactions, allowing for a restricted form of asynchronous behavior. Non-conflicting interactions are those involving sender-receiver actions that do not conform a control-flow dependency. For instance, t A .e A > & q1 (t B : x B ) :

k 1 ; t C .e C > & q2 (t D : x D ) : k 2 C t C .e C > & q2 (t D : x D ) : k 2 ; t A .e A > & q1 (t B : x B ) : k 1 .
Formally, let T(C) be the set of threads in C, defined inductively as

T(η; C) def = T(η) ∪ T(C), and
T(η) def = i={1..j} t i if η = t 1 [A 1 ].e > & q (t 2 [A 2 ] : x 2 , .
. . , t j [A j ] : x j ) : k (similarly for init, reduce and selection, and standardly for the other process constructs in C). The swapping congruence rules are presented in Figure 3.

A state σ keeps track of the capabilities achieved by a thread in a session, and it is formally defined as set of maps (t, k) → X. The rules in Figure 4 define state manipulation operations, including update (σ[σ ]), and lookup (σ(t, k)).

Because of the introduction of quality predicates, a move from η; C into C might leave some variables in η without proper values, as the participants involved might not have been available. We draw inspiration from [START_REF] Nielson | A calculus for quality[END_REF], introducing effect rules describing how the evaluation of an expression in a reduce 5) describes how evaluations are partially applied without affecting waiting threads. Label ξ records the substitutions of atomic formulae in each thread.

Y = X if (t, k, X) ∈ σ Y = ∅ o.w. σ(t, k) = Y δ = {(t, k, X) | (t, k, X) ∈ σ ∧ (t, k, Y ) ∈ σ } σ[σ ] = (σ\δ), σ
x : k, op ei@ti ↓ vi Xi ∈ σ(ti, k) σ = σ[(ti, k) → [[Xi; Yi]](σ(ti, k))] i∈{1...j} σ, η; C (t i ,k) : X i ::Y i --------→ →
Finally, given φ ∈ {tt, ff}, the relation β :: φ θ tracks whether all required binders in β have been performed, as well as substitutions used θ. Binder β is defined in terms of partially evaluated outputs c:

sc ::= p.e | p.some(v) c ::= & q (sc 1 , . . . , sc n )
The rules specifying β :: φ θ appear in Figure 6. A substitution θ = [(p 1 , some(v 1 )), . . . , (p n , some(v n ))/x 1 @p 1 , . . . , x n @p n ] maps each variable x i at p i to optional data some(v i ) for 1 ≤ i ≤ n. A composition θ 1 • θ 2 (x) is defined as θ 1 • θ 2 (x) ::= θ 1 (θ 2 (x)), and q(t 1 , . . . , t n ) = i∈1≤i≤n t i if q = ∀, q(t 1 , . . . , t n ) = i∈1≤i≤n t i if q = ∃, and possible combinations therein. As for process terms, θ(C) denotes the application of substitution θ to a term C (and similarly for η).

We now have all the ingredients to understand the semantics of GC q . The set of transition rules in λ -→ is defined as the minimum relation on names, states, and choreographies satisfying the rules in Figure 7. The operational semantics is given in terms of labelled transition rules. Intuitively, a transition (ν m) σ, C λ -→ (ν n) σ , C expresses that a configuration σ, C with used names m fires an action λ and evolves into σ , C with names n. We use the shorthand notation A # B to denote set disjointness, A ∩ B = ∅. The exchange function [[X; Y ]]Z returns (Z\X)∪Y if X ⊆ Z and Z otherwise. Actions are defined as λ ::= {τ, η}, where η denotes interactions, and τ represents an internal computation. Relation e@p ↓ v describes the evaluation of a expression e (in p) to a value v.

We now give intuitions on the most representative operational rules. Rule

Init models initial interactions: state σ is updated to account for the new threads in the session, updating the set of used names in the reductum. Rule Bcast models broadcast: given an expression evaluated at the sender, one needs to check that there are enough receivers ready to get a message. Such a check is performed by evaluating q(J). In case of a positive evaluation, the execution of the rule will:

p.e ::ff [ ] p.some(v) ::tt [(p, some(v))] sc1 ::t 1 θ1 . . . scn ::t n θn &q(sc1, . . . , scn) :: q(t 1 ,...,tn) θ1 • . . . • θn Fig. 6: Rules for β :: φ θ (1) update the current state with the new states of each participant engaged in the broadcast, and (2) apply the partial substitution θ to the continuation C. The behaviour of a reduce operation is described using rules RedD and RedE : the evaluation of expressions of each of the available senders generates an application of the effect rule in Figure 5. If all required substitutions have been performed, one can proceed by evaluating the operator to the set of received values, binding variable x to its results, otherwise the choreography will wait until further inputs are received (i.e.: the continuation is delayed).

Remark 1 (Broadcast vs. Selection). The inclusion of separate language constructs for communication and selection takes origin in early works of structured communications [START_REF] Honda | Language Primitives and Type Discipline for Structured Communication-Based Programming[END_REF]. Analogous to method invocation in object-oriented programming, selections play an important role in making choreographies projectable to distributed implementations. We illustrate their role with an example. Assume a session key k shared among threads p, r, s, and an evaluation of e@p of boolean type. The choreography p.e > r : x : k; if (x@r) then (r.d > s : y : k) else (s.f > r : z : k) branches into two different communication flows: one from r to s if the evaluation of x@r is true, and one from s to r otherwise. Although the evaluation of the guard in the if refers only to r, the projection of such choreography to a distributed system requires s to behave differently based on the decisions made by r. The use of a selection operator permits s to be notified by r about which behavior to implement: p.e > r : x : k; if (x@r) then (p > r : k[l 1 ]; r.d > s : y : k) else (p > r : k[l 2 ]; s.f > r : z : k) Remark 2 (Broadcast vs. Reduce). We opted in favor of an application-based QoS instead of a classical node-based QoS, as described in Section 2. This consideration motivates the asymmetry of broadcast and reduce commands: both operations are blocked unless enough receivers are available, however, we give precedence to senders over receivers. In a broadcast, only one sender needs to be available, and provided availability constraints for receivers are satisfied, its evolution will be immediate. In a reduce, we will allow a delay of the transition, capturing in this way the fact that senders can become active in different instants.

The reader familiar with the Global Calculus may have noticed the absence of a general asynchronous behaviour in our setting. In particular, rule:

(ν m) σ, C λ -→ (ν n) σ , C η = start snd(η) ⊆ fn(λ) rcv(η) # fn(λ) n = m, r ∀ r∈ r (r ∈ bn(λ) r / ∈ fn(η)) (ν m) σ, η; C λ -→ (ν n) σ , η; C Asynch η = tr[Ar]{Xr; Yr} start ts[Bs]{Ys} : a(k) σ = [(ti, k) → Yi] | tr |+| ts| i=1 n = ts, {k} n # m (ν m) σ, tr[Ar]{Yr} start ts[Bs]{Ys} : a(k); C η -→ (ν m, n) σ[σ ], C Init η = tA[A]{XA; YA}.e > &q( tr[Br]{Xr; Yr} : xr) : k J ⊆ tr q(J) e@tA ↓ v ∀i∈{A}∪J : Xi ⊆ σ(ti, k) ∧ σ (ti, k) = [[Xi; Yi]](σ(ti, k)) ∀i∈ tr : θ(xi) = some(v) i ∈ J none o.w. (ν m) σ, tA[A]{XA;YA}.e > &q( tr[Br]{Xr;Yr} : xr) : k ; C θ(η) ---→ (ν m) σ[σ ], θ(C) Bcast η = tA[A]{XA; YA} > &q( tr[Br]{Xr; Yr}) : k[l h ] J ⊆ tr q(J) ∀i∈{A}∪J : Xi ⊆ σ(ti, k) ∧ σ (ti, k) = [[Xi; Yi]](σ(ti, k)) (ν m) σ, tA[A]{XA; YA} > &q( tr[Br]{Xr; Yr}) : k[l h ] ; C η -→ (ν m) σ[σ ], C Sel η = &q( tr[Ar]{Xr; Yr}.er) > tB[B]{XB; YB} : x : k, op σ, η; C ξ -→ → σ , η ; C η ::ff θ (ν m) σ, η; C τ -→ (ν m) σ , η ; C RedD η = &q( tr[Ar]{Xr; Yr}.er) > tB[B]{XB; YB} : x : k, op σ, η; C ξ -→ → σ , η ; C η :: φ θ (tB, k, XB) ∈ σ (ν m) σ, η; C θ(η ) ---→ (ν m) [[(tB, k, XB); (tB, k, YB)]]σ , C[op(θ)/x@tB] RedE C R C (ν m) σ, C λ -→ (ν n) σ , C C R C R ∈ {≡, C } (ν m) σ, C λ -→ (ν n) σ , C Cong i = 1 if e@t ↓ tt, i = 2 o.w. (ν m) σ, if e@t then C1 else C2 τ -→ (ν m) σ, Ci If (ν m) σ, Ci λ -→ (ν n) σ , C i∈{1,2} (ν m) σ, C1 + C2 λ -→ (ν n) σ , C
Sum Fig. 7: GC q : Operational Semantics corresponding to the extension of rule C |ASYNCH in [START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF] with collective communications, is absent in our semantics. The reason behind it lies in the energy considerations of our application: consecutive communications may have different energetic costs, affecting the availability of sender nodes. Consider for example the configuration

(ν m) σ, (tA[A]{X; Y }.e > & ∃ ( tr[Br] : xr) : k); tA[A]{X; Y }.e > & ∀ ( ts[Bs] : xs) : k with t r # t s and X ⊆ σ(t A , k).
If the order of the broadcasts is shuffled, the second broadcast may consume all energy resources for t A , making it unavailable later. Formally, the execution of a broadcast update the capabilities offered in σ for t A , k to Y , inhibiting two communication actions with same capabilities to be reordered. We will refrain the use Rule Asynch in our semantics.

... Lines 1,2 in Figure 1.

3 & ∃ (t1{Ms 1 ; E 1 }."1", t3{Ms 3 ; E 3 }."5") > tm{Ms 0 ; E 0 } : x0 : k, avg ; 0
(ν m) σ, C λ -→ (ν n) σ , C
, for all σ, m.

Type-checking Progress

One of the challenges regarding the use of partial collective operations concerns the possibility of getting into runs with locking states. Consider a variant of Example 1 with q 1 = ∃ and q 2 = ∀. This choice leads to a blocked configuration.

The system blocks since the collective selection in Line (2) continues after a subset of the receivers in t 1 , t 2 , t 3 , have executed the command. Line (3) requires all senders to be ready, which will not be the most general case. The system will additionally block if participant dependencies among communications is not preserved. The choreography in Figure 8 illustrates this. It blocks for q 1 = ∃, since the selection operator in Line 2 can proceed by updating the capability associated to t 2 to M s 2 , leaving the capabilities for t 1 , t 3 assigned to Ac 1 , Ac 3 . With such state, Line 3 cannot proceed. We introduce a type system to ensure progress on variable availability conditions. A judgment is written as Ψ C, where Ψ is a list of formulae in Intuitionistic Linear Logic (ILL) [START_REF] Girard | Linear logic[END_REF]. Intuitively, Ψ C is read as the formulae in Ψ describe the program point immediately before C. Formulae ψ ∈ Ψ take the form of the constant tt, ownership types of the form p : k [A] X, and the linear logic version of conjunction, disjunction and implication (⊗, ⊕, ). Here p : k [A] X is an ownership type, asserting that p behaves as the role A in session k with atomic formula X. Moreover, we require Ψ to contain formulae free of linear implications in Ψ C.

Figure 9 presents selected rules for the type system for GC q . The full definition is included in Appendix A.1. Since the rules for inaction, conditionals and non-determinism are standard, we focus our explanation on the typing rules for communications. Rule TInit types new sessions: Ψ is extended with function init( t p [A]{X}, k), that returns a list of ownership types t p : k [A] X. The condition { t s , k} # (T(Ψ ) ∪ K(Ψ )) ensures that new names do not exist neither in the threads nor in the used keys in Ψ .

The typing rules for broadcast, reduce and selection are analogous, so we focus our explanation in TBcast . Here we abuse of the notation, writing Ψ C to denote type checking, and Ψ ψ to denote formula entailment. The semantics of ∀ ≥1 J s. x@tB : opt.data

Ψ
] ; C Tsel Ψ 0 Tinact Ψ C1 Ψ C2 Ψ if e@t then C1 else C2 Tcond Ψ = ψ ⊕ ψ ψ C ψ C Ψ C + C
Tsum Fig. 9: GC q : Type checking rules (excerpt): Premises for Tsel are the same as for Tbcast , without opt.data premises succeeds if environment Ψ can provide capabilities for sender t A [A] and for a valid subset J of the receivers in t r [B r ]. J is a valid subset if it contains enough threads to render the quality predicate true (q(J)), and the proof of ψ A , (ψ j ) j∈J t A : k [A] X A j∈J (t j : k [B j ] X j ) is provable. This proof succeeds if ψ A and (ψ j ) j∈J contain ownership types for the sender and available receivers with corresponding capabilities. Finally, the type of the continuation C will consume the resources used in the sender and all involved receivers, updating them with new capabilities for the threads engaged.

Example 2. In Example 1, tt

C if (q 1 = ∀) ∧ (q 2 = {∀, ∃}). In the case q 1 = ∃, q 2 = ∀, the same typing fails. Similarly, tt C if q 1 = ∃, for the variant of Example 1 in Figure 8.

A type preservation theorem must consider the interplay between the state and formulae in Ψ . We write σ |= Ψ to say that the tuples in σ entail the formulae in Ψ . For instance, σ |= t : k The decidability of type checking depends on the provability of formulae in our ILL fragment. Notice that the formulae used in type checking corresponds to the Multiplicative-Additive fragment of ILL, whose provability is decidable [START_REF] Lincoln | Deciding provability of linear logic formulas[END_REF]. For typing collective operations, the number of checks grows according to the amount of participants involved. Decidability exploits the fact that for each interaction the number of participants is bounded.

[A] X iff (t, k, X) ∈ σ. Its formal definition is included in Appendix A.1. Theorem 1 (Type Preservation). If (ν m) σ, C λ -→ (ν n) σ , C , σ |= Ψ ,
Theorem 3 (Decidability of Typing). Ψ C is decidable

Related Work

Availability considerations in distributed systems has recently spawned novel research strands in regular languages [START_REF] Abdulla | What's decidable about availability languages[END_REF], continuous systems [START_REF] Alur | Principles of Cyber-Physical Systems[END_REF], and endpoint languages [START_REF] Nielson | A calculus for quality[END_REF]. To the best of our knowledge, this is the first work considering availability from a choreographical perspective.

A closely related work is the Design-By-Contract approach for multiparty interactions [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF]. In fact, in both works communication actions are enriched with pre-/post-conditions, similar to works in sequential programming [START_REF] Hoare | An axiomatic basis for computer programming[END_REF]. The work on [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF] enriches global types with assertions, that are then projected to a session π-calculus. Assertions may generate ill-specifications, and a check for consistency is necessary. Our capability-based type system guarantees temporalsatisfiability as in [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF], not requiring history-sensitivity due to the simplicity of the preconditions used in our framework. The most obvious difference with [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF] is the underlying semantics used for communication, that allows progress despite some participants are unavailable.

Other works have explored the behavior of communicating systems with collective/broadcast primitives. In [START_REF] Hüttel | Broadcast and aggregation in BBC[END_REF], the expressivity of a calculus with bounded broadcast and collection is studied. In [START_REF] López | Protocol-based verification of message-passing parallel programs[END_REF], the authors present a type theory to check whether models for multicore programming behave according to a protocol and do not deadlock. Our work differs from these approaches in that our model focuses considers explicit considerations on availability for the systems in consideration. Also for multicore programming, the work in [START_REF] Cogumbreiro | Coordinating phased activities while maintaining progress[END_REF] presents a calculus with fork/join communication primitives, with a flexible phaser mechanism that allows some threads to advance prior to synchronization. The type system guarantees a node-centric progress guarantee, ideal for multicore computing, but inadequate for CPS. Finally, the work [START_REF] Kouzapas | Session types for broadcasting[END_REF], present endpoint (session) types for the verification of communications using broadcast in the Ψ -calculus. We do not observe similar considerations regarding availability of components in this work.

The work [START_REF] Castagna | On global types and multiparty session[END_REF] presented multiparty global types with join and fork operators, capturing in this way some notions of broadcast and reduce communications, which is similar to our capability type-system. The difference with our approach is described in Section 3. On the same branch [START_REF] Denielou | Multiparty session types meet communicating automata[END_REF] introduces multiparty global types with recursion, fork, join and merge operations. The work does not provide a natural way of encoding broadcast communication, but one could expect to be able to encode it by composing fork and merge primitives.

Conclusions and Future Work

We have presented a process calculus aimed at studying protocols with variable availability conditions, as well as a type system to ensure their progress. It constitutes the first step towards a methodology for the safe development of communication protocols in CPS. The analysis presented is orthogonal to existing type systems for choreographies (c.f. session types [START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF].) Our next efforts include the modification of the type theory to cater for recursive behavior, the generation of distributed implementations (e.g. EndPoint Projection [START_REF] Carbone | Structured communication-centered programming for web services[END_REF]), and considerations of compensating [START_REF] Carbone | Session-based choreography with exceptions[END_REF][START_REF] Carbone | Structured interactional exceptions in session types[END_REF][START_REF] López | Time and Exceptional Behavior in Multiparty Structured Communications[END_REF] and timed behavior [START_REF] Bocchi | Timed multiparty session types[END_REF][START_REF] Bocchi | Meeting deadlines together[END_REF]. Type checking is computationally expensive, because for each collective interaction one must perform the analysis on each subset of participants involved. The situation will be critical once recursion is considered. We believe that the efficiency of type checking can be improved by modifying the theory so it generates one formulae for all subsets.

Traditional design mechanisms (including sequence charts of UML and choreographies) usually focus on the desired behavior of systems. In order to deal with the challenges from security and safety in CPS it becomes paramount to cater for failures and how to recover from them. This was the motivation behind the development of the Quality Calculus that not only extended a π-calculus with quality predicates and optional data types, but also with mechanisms for programming the continuation such that both desired and undesired behavior was adequately handled. In this work we have incorporated the quality predicates into choreographies and thereby facilitate dealing with systems in a failure-aware fashion. However, it remains a challenge to incorporate the consideration of both desired and undesired behavior that is less programming oriented (or EndPoint Projection oriented) than the solution presented by the Quality Calculus. This may require further extensions of the calculus with fault-tolerance considerations.

  (Choreographies) C ::= η; C | C + C | if e@p then C else C | 0 (Annotated threads) p, r ::= t[A]{X; Y } (Interactions) η ::= pr start ps : a(k) (init) | pr.e > &q( ps : xs) : k (broadcast) | &q( pr.er) > ps : x : k, op

Fig. 2 :

 2 Fig. 2: Quality predicates: syntax q and semantics [[q]].

  1 .e > & ∀ (p 2 : x) : k and & ∀ (p 1 .e) > p 2 : x : id, k are just a couple of possible implementations. The implementation of unicast label selection p > r : k[l] can be expressed analogously.

Fig. 4 :

 4 Fig. 4: State lookup and update rules

Fig. 8 :

 8 Fig. 8: Variant of Example 1 with locking states

  t. C : D is given by ∀J s.t. C : D ∧ ∃J s.t. C. The judgmentΨ (t A [A]{X A ; Y A }.e > & q ( t r [B r ]{X r ; Y r } : x r ) : k); C Choregraphy Formation (Ψ C), Ψ, init( tr[Ar]{Yr}, ts[Bs]{Ys}, k) C { ts, k} # (T(Ψ ) ∪ K(Ψ )) Ψ tr[Ar]{Yr} start ts[Bs]{Ys} : a(k); C Tinit ∀ ≥1 J. s.t. J ⊆ tr ∧ q(J) ∧ Ψ = ψA, (ψj)j∈J , Ψ ∧ ψA, (ψj)j∈J tA : k [A] XA j∈J (tj : k [Bj] Xj) : tA : k [A] YA, (tj : k [Bj] Yj) j∈J , Ψ C e@tA : opt.data ( xi@ti : opt.data) | tr | i=1 Ψ tA[A]{XA; YA}.e > &q( tr[Br]{Xr; Yr} : xr) : k ; C Tbcast ∀ ≥1 J. s.t. J ⊆ tr ∧ q(J) ∧ Ψ = ψB, (ψj) |J| j=1 , Ψ ∧ ψB, (ψj) |J| j=1 tB : k [B] XB j∈J (tj : k [Aj] Xj) : tB : k [B] YB, (tj : k [Aj] Yj) |J| j=1 , Ψ C ( ei@ti : opt.data) | tr | i=1

  and Ψ C, then ∃Ψ . Ψ C and σ |= Ψ . Theorem 2 (Progress). If Ψ C, σ |= Ψ and C ≡ 0, then C progresses.

  &q( tr[Ar]{Xr; Yr}.er) > tB[B]{XB; YB} : x : k, op ; C

		Tred
		((as in Tbcast * ))
	Ψ	tA[A]{XA; YA} > &q( tr[Br]{Xr; Yr}) : k[l h

Acknowledgments. We would like to thank Marco Carbone and Jorge A. Pérez for their insightful discussions, and to all anonymous reviewers for their helpful comments improving the paper. This research was funded by the Danish Foundation for Basic Research, project IDEA4CPS (DNRF86-10). López has benefitted from travel support by the EU COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (BETTY).

A Additional Definitions

A.1 Type System Figure 10 presents the complete type system for GC q . Definition 3 (State Satisfaction). The entailment relation between a state σ and a formula Ψ , and between σ and a formula ψ are written σ |= Ψ and σ |= ψ, respectively. They are defined as follows:

x@t B : opt.data


Francesco Mercaldo
email: fmercaldo@unisannio.it

Vittoria Nardone
email: vnardone@unisannio.it

Antonella Santone
email: santone@unisannio.it

Aaron Corrado

Visaggio
email: visaggio@unisannio.it

Ransomware Steals your Phone. Formal Methods Rescue it

Keywords: Malware, Android, Security, Formal Methods, Temporal Logic

Ransomware is a recent type of malware which makes inaccessible the files or the device of the victim. The only way to unlock the infected device or to have the keys for decrypting the files is to pay a ransom to the attacker. Commercial solutions for removing ransomware and restoring the infected devices and files are ineffective, since this malware uses a very robust form of asymmetric cryptography and erases shadow copies and recovery points of the operating system. Literature does not count many solutions for effectively detecting and blocking ransomware and, at the best knowledge of the authors, formal methods were never applied to identify ransomware. In this paper we propose a methodology based on formal methods that is able to detect the ransomware and to identify in the malware's code the instructions that implement the characteristic instructions of the ransomware. The results of the experimentation are strongly encouraging and suggest that the proposed methodology could be the right way to follow for developing commercial solutions that could successful intercept the ransomware and blocking the infections it provokes.

Introduction and Motivation

Ransomware is a recent kind of malware that spread out mainly in last couple of years, and it is particularly aggressive for two reasons: on one hand it uses very effective mechanisms of infection based mainly on techniques of social engineering like sophisticated phishing (by mail or chat), and on the other hand it makes completely inaccessible the data on the infected machine, as it cyphers all the files with a strong asymmetric key cryptographic algorithm.

The ransomware is still increasing its capability to harm the victim's device, prevent the restore of the data or device, and evade detection. As a matter of fact, the more recent releases of this malware are able to recognize when they are executed in a virtual environment, which is often used for creating a sandbox where safely executing a program for studying its behavior and understanding if it launches a malicious payload or not. Additionally, recent ransomware is equipped with anti-debugging techniques, which is another way to evade detection as hindering the scanning of anti-malware.

Statistics from US governative agencies show that Cryptolocker infected in 2014: 336,856 machines in USA, 4,593 in UK, 25,841 in Canada, 15,427 in Australia, 1,832 in India, 100,448 in other countries. At its peak, CryptoLocker, a kind of ransomware, was infecting around 50,000 computers per month. According to SCMagazine1 the CryptoWall, another ransomware, in a roughly fivemonth period infected 625,000 victims worldwide, encrypting 5.25 billion files, collecting more than $1.1 million in ransoms. The malware tries to delete shadow copies of the system through vssadmin.exe, so that the victim cannot return to previous system restore points too.

Moreover ransomware is invading the smartphone world: Kaspersky labs found 1,113 new ransomware samples targeting Android devices in the first quarter of 2015, which is a 65% increase in the number of mobile ransomware samples with respect to those collected in 20142 . This is a dangerous trend since ransomware is designed to extort money, damage personal data, and block infected devices. Once the device is infected, the attacker asks the victim to pay a ransom in order to obtain the key for decrypting the files or restoring the control of the smartphone.

As the evidence of the high infections rate demonstrates, commercial antimalware solutions are mainly ineffective to detect ransomware.

For this reason we propose a technique for specifically detecting ransomware on smartphone devices that is completely based on formal methods. The technique has been proved to be very effective as the evaluation produced an Fmeasure of detection equal to 0.99 on a dataset of 2, 477 samples. Additionally, the technique is able to localize in the code the peculiar instructions that implement the stages of infection, and the activation of the payload, which provides fundamental pieces of information to build both effective detectors and removal systems for ransomware. Moreover, at the best knowledge of the authors, literature counts only two works that propose a method to detect mobile ransomware [START_REF] Andronio | Heldroid: Dissecting and detecting mobile ransomware[END_REF][START_REF] Yang | Automated detection and analysis for android ransomware[END_REF] and that are compared with ours in the section of related work.

The paper proceeds as follows: Section 2 describes and motivates our detection method; Section 3 illustrates the results of experiments; Section 4 discusses the related work; finally, conclusions are drawn in Section 5.

The Methodology

In this section we present our methodology for the detection of Android ransomware malware using model checking. While model checking was originally developed to verify the correctness of systems against specifications, recently it has been highlighted in connection with a variety of disciplines see [START_REF] Anastasi | Efficient verification of a multicast protocol for mobile computing[END_REF][START_REF] Ceccarelli | Infer gene regulatory networks from time series data with probabilistic model checking[END_REF] Moreover, great advancements have been made to tackle the limitation of this technique due to its high time and memory requirements, see [START_REF] Barbuti | LORETO: A tool for reducing state explosion in verification of LOTOS programs[END_REF][START_REF] De Francesco | Heuristic search for equivalence checking[END_REF][START_REF] Francesca | Ant colony optimization for deadlock detection in concurrent systems[END_REF][START_REF] Francesco | State space reduction by non-standard semantics for deadlock analysis[END_REF]. In this paper we present the use of model checking in the security field.

Formal Methods for Ransomware Detection

The approach is structured in three main sub-processes.

Formal Model Construction. This first sub-process aims at deriving formal models starting from the Java Bytecode. The Bytecode of the app under study is parsed and suitable formal models of the system are produced. More precisely, the bytecode of the analysed app that resides in a class folder or in JAR files is fed to a custom parser, based on the Apache Commons Bytecode Engineering Library (BCEL) 3 . The parsed Java Bytecode of the .class files are successively translated into formal models. In our approach Calculus of Communicating Systems (CCS) [START_REF] Milner | Communication and concurrency[END_REF] has been exploited. CCS [START_REF] Milner | Communication and concurrency[END_REF] is one of the most well known process algebras. A Java Bytecode-to-CCS transforming function has been defined for each instruction of the Java Bytecode. We associate a new CCS process to each Java Bytecode instruction. This translation has to be performed only one time for each app to be analysed and it has been completely automated. Each Java Bytecode instruction that is not a (conditional or unconditional) jump is represented by a process that, using the operator ("."), invokes the process corresponding to its successive instruction. Conditional jumps are instead specified as non-deterministic choices. An unconditional jump is represented by a CCS process that invokes the corresponding process of the jump target.

Temporal Logic Properties Construction. This second sub-process aims to define the characteristic behaviour of a ransomware by means of the construction of the temporal logic properties. This step tries to recognize specific and distinctive features of the ransomware behaviour with respect to all the other malware families and to goodware too. Thus, this specific behaviour is written as a set of properties. To specify the properties, we manually inspected a few samples in order to find the ransomware malicious behavior implementation at Bytecode level. In our approach, the mu-calculus logic [START_REF] Stirling | An introduction to modal and temporal logics for ccs[END_REF] is used, which is a branching temporal logic to express behavioural properties.

Ransomware Family Detection. Finally, a formal verification environment, including a model checker, is invoked to recognise the ransomware family. This sub-process checks the sets of logic properties obtained from the ransomware malware family characterization against the CCS model of the app. In our approach, we invoke the Concurrency Workbench of New Century (CWB-NC) [START_REF] Cleaveland | The ncsu concurrency workbench[END_REF] as formal verification environment. When the result of the CWB-NC model checker is true, it means that the app under analysis belongs to the ransomware family, false otherwise. Thanks to very detailed CCS model and the logic formulae we are able to reach a good accuracy of the overall results, as explained in the following section.

To the Authors' knowledge, model checking has never used before for the ransomware detection. The main distinctive features of the approach proposed in this paper are the use of formal methods, the identification of the ransomware through the Java Bytecode and the definition of a fully static approach. More precisely, our methodology exploits the Bytecode representation of the analysed apps. Detecting Android ransomware through the Bytecode and not directly on the source code has several benefits: (i) independence of the source programming language; (ii) recognition of malware families without decompilation even when source code is lacking; (iii) easiness of parsing a lower-level code; (iv) independence from obfuscation.

Another important feature of our approach is that we try to reuse existing model checkers avoiding the design of custom-made model checker. In fact our goal is to recognise ransomware with the criteria of reusing existing checking technologies. Model checkers, especially the most widely used ones, are extremely sophisticated programs that have been crafted over many years by experts in the specific techniques employed by the tool. A re-implementation of the algorithms in these tools could likely yield worst performance.

Results and Discussion

Empirical Evaluation Procedure

To estimate the detection performance of our methodology we compute the metrics of precision and recall, F-measure (Fm) and Accuracy (Acc), defined as follows:

P R = T P T P + F P ; RC = T P T P + F N ;

F m = 2P R RC P R + RC ; Acc = T P + T N T P + F N + F P + T N
where T P is the number of malware that was correctly identified in the right family (True Positives), T N is the number of malware correctly identified as not belonging to the family (True Negatives), F P is the number of malware that was incorrectly identified in the target family (False Positives), and F N is the number of malware that was not identified as belonging to the right family (False Negatives).

Experimental Dataset

The real world samples examined in the experiment were gathered from three different datasets. The first one is a collection of freely available 672 samples4 and 11 5 Android ransomware samples. The samples are labelled as ransomware, koler, locker, fbilocker and scarepackage [START_REF] Andronio | Heldroid: Dissecting and detecting mobile ransomware[END_REF] and appeared from December 2014 to June 2015. The second one is the Drebin project's dataset [START_REF] Arp | Drebin: Efficient and explainable detection of android malware in your pocket[END_REF][START_REF] Spreitzenbarth | Mobilesandbox: Looking deeper into android applications[END_REF], a very well known collection of malware used in many scientific works, which includes the most diffused Android families. Each malware sample in these datasets is labelled according to the malware family it belongs to: each family comprehends samples which have in common the same payload. This collection does not contain ransomware samples: we use this dataset to check the true positives.

The last one is a dataset of trusted applications crawled from Google Play6 , by using a script which queries a python API7 to search and download apps. The trusted applications were collected between April 2015 and January 2016 and were later analysed with the VirusTotal service8 , a service able to run 57 different antimalware software (i.e., Symantec, Avast, Kasperky, McAfee, Panda, and others) on the app: the analysis confirmed that the crawled applications did not contain malicious payload. We use this dataset to check the true positives.

Furthermore, we developed a framework9 able to inject several obfuscation levels in Android applications: (i) changing package name; (ii) identifier renaming; (iii) data encoding; (iv) call indirections; (v) code reordering; (vi) junk code insertion.

These injections were aimed at generating morphed versions of the applications belonging to the ransomware dataset. Previous works [START_REF] Canfora | Obfuscation techniques against signature-based detection: a case study[END_REF] demonstrated that antimalware solutions fail to recognize the malware after these transformations. We applied our method to the morphed dataset in order to verify if it loses its effectiveness, too, or it keeps on recognizing the malware also after they have been altered. Table 1 provides the details of the full collection of 2,477 samples used to test the effectiveness of our method. Regarding the ransomware samples, Table 1 shows the number of original and morphed samples we tested; in some cases our framework was not able to disassemble some of the selected samples, this is the reason why we had to discard them and we consider a lower number of morphed samples if compared with original ones. In order to test the capacity of our rules to identify exclusively ransomware samples, we include in the dataset both trusted and malware samples from other families (respectively Trusted and Other Malware).

Table 2 provides a brief description of the payload brought by the malware families labelled as Other Malware, i.e., malware that is not ransomware.

We test 60 samples for each family. The malware was retrieved from the Drebin project [START_REF] Arp | Drebin: Efficient and explainable detection of android malware in your pocket[END_REF][START_REF] Spreitzenbarth | Mobilesandbox: Looking deeper into android applications[END_REF] (we take into account the top 10 most populous families).

Evaluation

As a baseline for evaluating the performances of our solution, we compare the results obtained with our method with those produced by the top 10 ranked mobile antimalware solutions from AVTEST10 , an independent Security Institute which each year provides an analysis of the performances of the antimalware software. We built this baseline, by submitting our original and morphed samples to the VirusTotal API 11 , which allows to run the above mentioned antimalware.

Table 3 shows the evaluation between the top 10 antimalware solutions and our method with the original ransomware samples and with the morphed ones.

We consider only the samples and the percentage identified in the right family (column "ident" and the percentage in column "%ident") in Table 3. We also report the samples detected as malicious but not identified in the right family and the samples not recognized as malware (column "unident").

With regards to Table 3 we notice that BitDefender shows better performance in family identification for Ransomware original samples. Instead, with regards to morphed samples, antimalware performance decreases dramatically, indeed BitDefender is able to identify only 86 samples. The worst antimalware in Ransomware identification is Alibaba, able to correctly classify just 3 original samples and 0 morphed samples. Due to the novelty of the problem, antimalware solutions are not still specialized in family identification; this is the reason why most of antimalware are unskilled to detect families. Another problem is that current antimalware are not able to detect malware when the signature mutates: their performance decreases dramatically with morphed samples. On the contrary, the detection done by our method is barely affected by the code transformations, so it is independent from the signature.

Table 4 shows the results obtained using our method. We consider the sum of original and morphed samples: the detail about the number of original and morphed samples is shown in Table 1.

Results in Table 4 seems to be very promising: we obtain an Accuracy and a F-measure equal to 0.99. Concerning the ransomware results, we are not able to identify the malicious payloads of just 6 samples (i.e., 3 originals and 3 morphed) on 1, 277.

Related Work

In this section we review the current literature related to ransomware detection and formal methods applied to the detection of mobile malware.

As we stated previously, literature counts only two works about the detection of Android ransomare.

The first one proposes HelDroid [START_REF] Andronio | Heldroid: Dissecting and detecting mobile ransomware[END_REF]: the approach includes a text classifier based on NLP features, a lightweight Smali emulation technique to detect locking strategies, and the application of taint tracking for detecting file-encrypting flows. The main weakness of HelDroid is represented by the text classifier: the authors train it on generic threatening phrases, similar to those that typically appear in ransomware or scareware samples. In addiction, like whatever machine learning approach, HelDroid needs to train the classifier in order to label a samples as a ransomware: the detection capability of the model is related to the training dataset.

The other work in literature exploring the ransomare detection in mobile world is [START_REF] Yang | Automated detection and analysis for android ransomware[END_REF]. The authors illustrate a possible design of a static and dynamic analysis based solution, without implementing it. Their goal is to build a better performance tool in order to help to understand what should to approach for a successful detection of Android ransomware.

Formal methods have been applied for studying malware in some recent papers, see [START_REF] Jacob | Formalization of viruses and malware through process algebras[END_REF][START_REF] Kinder | Detecting malicious code by model checking[END_REF][START_REF] Song | Pommade: Pushdown model-checking for malware detection[END_REF][START_REF] Song | Model-checking for android malware detection[END_REF]. Recently, the possibility to identify the malicious payload in Android malware using a model checking based approach has been explored in [START_REF] Battista | Identification of android malware families with model checking[END_REF][START_REF] Mercaldo | Download malware? No, thanks. How formal methods can block update attacks[END_REF]. Starting from payload behavior definition they formulate logic rules and then test them by using a real world dataset composed by DroidKungFu, Opfake families and update attack samples. However, as it emerges from the literature in the last years, formal methods have been applied to detect mobile malware, but at the best knowledge of the authors they have never been applied for identifying specifically the ransomware attack on Android malware.

Conclusions

Ransomware is a new type of malware that restricts access to the infected smartphone and it demands the user to pay a ransom to the attacker in order to remove the restriction. Ransomware samples are able to encrypt files on the infected device, which become difficult or impossible to decrypt without paying the ransom for the encryption key.

In this paper we propose a technique based on formal methods able to detect ransomware behaviour in Android platform. We obtain encouraging results on a dataset of 2,477 samples: 1 precision and 0.99 recall, overcoming in terms of effectiveness the top 10 popolous commercial antimalware.

As future work we are going to extend our solution using a ransomware dataset for different environment, like Windows Mobile and iOS in order to experiment the portability of our method.

  The downloaded applications belong to all the 26 different available categories (i.e., Books & Reference, Lifestyle, Business, Live Wallpaper, Comics, Media & Video, Communication, Medical, Education, Music & Audio, Finance & News, Magazines, Games, Personalization, Health & Fitness, Photography, Libraries & Demo, Productivity, Shopping, Social, Sport, Tools, Travel, Local & Transportation, Weather, Widgets). The applications retrieved were among the most downloaded in their category and were free.

Table 1 :

 1 Dataset used in the Experiment

	Dataset	Original Samples Morphed Samples #Samples for Category
	Ransomware	683	594	1,277
	Other Malware	600	0	600
	Trusted	600	0	600
	Total	1,883	594	2,477

Table 2 :

 2 Families in Drebin dataset with details of the installation method (standalone, repackaging, update), the kind of attack (trojan, botnet), the events that trigger the malicious payload and a brief family description.

	Family	Installation Attack	Activation	Description
	FakeInstaller	s	t,b		server-side polymorphic family
	Plankton	s,u	t,b		it uses class loading to forward details
	DroidKungFu	r	t	boot,batt,sys	it installs a backdoor
	GinMaster	r	t	boot	malicious service to root devices
	BaseBridge	r,u	t	boot,sms,net,batt	it sends information to a remote server
	Adrd	r	t	net,call	it compromises personal data
	Kmin	s	t	boot	it sends info to premium-rate numbers
	Geinimi	r	t	boot,sms	first Android botnet
	DroidDream	r	b	main	botnet, it gained root access
	Opfake	r	t		first Android polymorphic malware

Table 3 :

 3 Top 10 Signature-Based Antimalware Evaluation Against Our Method.

	Antimalware		Original			Morphed
		%ident. #ident. #unident. %ident. #ident. #unident.
	AhnLab	13.76%	94	589	5.22%	31	563
	Alibaba	0.44%	3	680	0%	0	594
	Antiy	13.18%	90	593	4.04%	24	570
	Avast	27.52%	188	495	6.4%	38	556
	AVG	3.22%	22	661	1.51%	9	585
	Avira	19.76%	135	548	12.46%	74	520
	Baidu	14.34%	98	585	6.7%	41	553
	BitDefender	28.26%	193	490	14.47%	86	508
	ESET-NOD32 20.35%	139	544	8.58%	51	543
	GData	27.96%	191	492	7.91%	47	547
	Our Method 99.56% 680	3	99.49% 591	3

Table 4 :

 4 Performance Evaluation

	Formula	# Samples TP FP FN TN PR RC Fm Acc
	Ransomware	2,477	1,271 0	6 1,200 1 0.99 0.99 0.99

http://www.scmagazine.com/cryptowall-surpasses-cryptolocker-in-infectionrates/article/368920/

2 https://securelist.com/analysis/quarterly-malware-reports/69872/it-threatevolution-in-q1-2015/

http://commons.apache.org/bcel/

http://ransom.mobi/

http://contagiominidump.blogspot.it/

https://play.google.com

https://github.com/egirault/googleplay-api

https://www.virustotal.com/

https://github.com/faber03/AndroidMalwareEvaluatingTools

https://www.av-test.org/en/antivirus/mobile-devices/