Evgenii Vinarskii

Andrey Laputenko
email: laputenko.av@gmail.com

Nina Yevtushenko
email: evtushenko@ispras.ru

Using an SMT solver for checking the completeness of FSM-based tests

Keywords: FSM based testing, SMT solver, Fist order logic formulas

Deriving tests with guaranteed fault coverage by FSM-based test methods is rather complex for systems with a large number of states. At the same time, formal verification methods allow to effectively process large transition systems; in particular, SMT solvers are widely used to solve analysis problems for finite transition systems. In this paper, we describe the known necessary and sufficient conditions of completeness of test suites derived by FSM-based test methods via the first-order logic formulas and use an SMT solver in order to check them. In addition, we suggest a new sufficient condition for test suite completeness and check the corresponding first-order logic formula via the SMT solver. The results of computer experiments with randomly generated finite state machines confirm the correctness and efficiency of a proposed approach.

Introduction

Finite state machines (FSM) based test derivation is well-known in the software testing of communication protocols and other reactive systems [START_REF] Chow | Test design modeled by finite-state machines[END_REF][START_REF] Dorofeeva | An improved conformance testing method[END_REF][START_REF] Fujiwara | Test selection based on finite state models[END_REF][START_REF] Vasilevskii | Failure diagnosis of automata[END_REF]. In this case, the behavior of the specification as well as of an implementation under test (IUT) is modeled by a corresponding FSM and testing is performed for determining whether the implementation conforms to the specification. As the number of input sequences is infinite, different limitations are imposed for an implementation under test [START_REF] Chow | Test design modeled by finite-state machines[END_REF][START_REF] Koufareva | A novel modification of w-method[END_REF][START_REF] Vasilevskii | Failure diagnosis of automata[END_REF][START_REF] Yevtushenko | Failure diagnosis of automata[END_REF] when deriving finite tests with guaranteed fault coverage. One of the well known limitations is to assume that the number of states of an implementation FSM is not bigger than the number of states of the specification and methods for deriving such tests are developed for various kinds of FSMs, complete and partial, deterministic and non-deterministic as well as for various kinds of conformance relations [START_REF] Dorofeeva | An improved conformance testing method[END_REF][START_REF] Petrenko | Nondeterministic state machines in protocol conformance testing[END_REF][START_REF] Yevtushenko | Failure diagnosis of automata[END_REF].

Most methods are developed for initialized complete deterministic FSMs where the conformance means the equivalence. Despite the big number of derivatives of such methods the necessary and sufficient conditions for a finite test suite to be a complete test suite are still unknown.

This work is partly supported by RFBR project No 18-01-00854.

The main idea when deriving a complete test suite, is to establish an isomorphic relationship between state sets of the specification and an implementation under test. For this purpose, so-called state identification sequences of the specification FSM are utilized [START_REF] Chow | Test design modeled by finite-state machines[END_REF][START_REF] Dorofeeva | An improved conformance testing method[END_REF][START_REF] Vasilevskii | Failure diagnosis of automata[END_REF][START_REF] Yevtushenko | Failure diagnosis of automata[END_REF], especially, distinguishing or separating sequences. Intuitively, a distinguishing sequence is a sequence that being applied at two different states provides different output sequences and, thus, for a deterministic machine, different states can be implicitly distinguished without their direct observation. In [START_REF] Chow | Test design modeled by finite-state machines[END_REF][START_REF] Dorofeeva | An improved conformance testing method[END_REF][START_REF] Koufareva | A novel modification of w-method[END_REF][START_REF] Vasilevskii | Failure diagnosis of automata[END_REF], it is shown that the use of distinguishing sequences allows constructing a complete rather reduced test suite without explicit enumeration of all implementations of the fault domain. However, as an example in [START_REF] Dorofeeva | An improved conformance testing method[END_REF] demonstrates, the conditions based on distinguishing sequences are not necessary. The idea of the example is to show that two implementation states still can be implicitly distinguished without applying distinguishing sequences at these states. Such distinguishing sequences can be applied at appropriate predecessors or successors of these states. Since this fact is difficult to express as an analytical feature, we turned our attention to the formal verification that now is widely used for checking appropriate properties of different kinds of discrete event and hybrid systems [START_REF] Fujiwara | Test selection based on finite state models[END_REF].

In this paper, we use the following steps to verify that a test suite T S is or is not complete, i.e., whether requested fault coverage is guaranteed: (1) Given necessary or sufficient conditions for the test suite completeness and a test suite T S, we represent the conditions as a first-order logic formula. If the formula is true, then the T S satisfies the conditions, and if the formula is false then the T S does not satisfy the conditions. (2) The formula satisfiability is checked by the Z3 solver [START_REF] Yurichev | SAT/SMT by Example[END_REF]. In addition, we suggest a new sufficient condition for the test suite completeness, describe this condition via a firstorder logic formula and check this formula via the Z3 solver. This formula becomes true for the example in [START_REF] Dorofeeva | An improved conformance testing method[END_REF], i.e., a considered test suite is complete according to this formula.

This paper is organized as follows. Sections 2 and 3 briefly describe finite state machines and properties of a test suite with guaranteed fault coverage as well as include first-order logic formulas for describing some necessary and sufficient conditions for the test suite completeness. Section 4 contains the preliminary experimental results of using Z3 solver for checking the test suite completeness and Section 5 concludes the paper.

Deriving test suites using Finite State Machine based methods

The section briefly presents the preliminary concepts that are used in the paper. Most of the definitions are taken from [START_REF] Dorofeeva | An improved conformance testing method[END_REF][START_REF] Gill | Introduction to the theory of finite-state machines[END_REF].

In this paper, a Finite State Machine (FSM) is an initialized complete deterministic machine, i.e., a 6-tuple M = S, I, O, δ M , λ M , s 0 [START_REF] Gill | Introduction to the theory of finite-state machines[END_REF], where S is a finite set of states with the designated initial state s 0 , I and O are finite input and output alphabets, δ M : S ×I → S is the next state (or transition) function, λ M : S ×I → O is the output function.

In the usual way, both functions are extended to input sequences. In this paper, we consider (initially) connected FSMs, i.e., we assume that each state is reachable from the initial state via an appropriate input sequence.

A set SC of input sequences is called a state cover set of FSM M if SC has the empty sequence ε and for each state s i of S, there is an input sequence α ∈ SC that takes FSM M from the initial state to state s i . If the FSM is connected then such a state cover set always exists. As usual, seq = seq.i specifies that a sequence seq is the concatenation of sequences seq and i and SC.I is the set {seq.i ∈ I | seq ∈ SC&i ∈ I}. A set TC of input sequences is a transition cover set if for each state s ∈ S and each input i ∈ I there exists sequence seq ∈ TC such that seq = seq 1 .i where δ M (s 0 , seq 1 ) = s.

Given two complete deterministic FSMs M and P over the same input and output alphabets, two states s i of M and p j of P are equivalent, written s i ∼ = p j , if for each input sequence α ∈ I * it holds that λ M (s i , α) = λ P (p j , α). Otherwise, we say that states s i and p j are distinguishable, written s i ∼ = p j [5]. FSMs M and P are equivalent, written M ∼ = P , (distinguishable, written M ∼ = P ) if their initial states are equivalent (distinguishable). Given distinguishable states s i of M and p j of P , an input sequence α ∈ I * such that λ M (s i , α) = λ P (p j , α) is said to distinguish states s i and p j , written s i ∼ =α p j .

An input sequence that distinguishes the initial states of distinguishable FSMs M and P distinguishes FSMs M and P , written M ∼ =α P . FSM M is reduced if each two different states s, s of M are distinguishable. For each initialized complete deterministic FSM, there exists a reduced connected equivalent FSM [START_REF] Gill | Introduction to the theory of finite-state machines[END_REF] and in this paper, we assume that all the FSMs are connected and reduced unless the contrary is explicitly stated.

Let M be the specification FSM with n states, n > 0; a test suite T S is a finite set of finite input sequences of the specification FSM M . Given an implementation FSM P over alphabets I and O, the FSMs M and P are T S-equivalent if for each input sequence of T S, the output responses of both machines coincide. A test suite T S is n-complete if, for each implementation P with at most n states that is distinguishable from M , there exists a sequence in T S that distinguishes M and P . In other words, in this paper, we assume that the number of states of an implementation FSM is not bigger than that of the specification. We now present some conditions when a test suite is or is not n-complete. Let T S = {α 1 , . . . , α k } be a test suite that is checked for the n-completeness where α 1 , . . . , α k are test sequences. One of the known necessary (Proposition 1) conditions for a test suite to be n-complete is to contain a state / transition cover of the specification FSM. Proposition 2 gives sufficient conditions for a test suite T S to be n-complete [START_REF] Dorofeeva | An improved conformance testing method[END_REF].

Proposition 1. Given the complete deterministic reduced connected specification FSM M with n states and a test suite T S, if T S does not contain the state cover set SC (the transition cover set TC) of M , then T S is not n-complete. Proposition 2. Given the complete deterministic reduced connected specification FSM M with n states and a state cover set SC of M , let T S be a finite set of finite input sequences of M that contains the set SC.I. The test suite T S is n-complete if the following conditions hold:

1. For each two different states of M there exist sequences α and β in SC such that T S has sequences α.γ and β.γ where γ is a distinguishing sequence of the states δ M (s 0 , α) and δ M (s 0 , β).

2. For each sequence α.i, α ∈ SC, that takes the specification FSM M from s 0 to state s, T S has sequences α.i.γ and β.γ, where β ∈ SC, δ M (s 0 , β) = s, and γ is a distinguishing sequence of states s and δ M (s 0 , β).

According to Proposition 2, given a state s of M , different state identification sequences can be used when checking incoming transitions to state s, i.e. distinguishing sequences for the ending state of a transition can be derived on-the-fly using already a constructed part of a test suite. Based on the above proposition the algorithm has been developed for deriving an n-complete test suite, called the improved H-method [START_REF] Dorofeeva | An improved conformance testing method[END_REF]. Note that since an implementation FSM has at most n states, the fulfillment of the first condition implies that an implementation under test has exactly n different states. However, the conditions of Proposition 2 are not necessary conditions for a test suite to be n-complete and this fact is illustrated by the example of the specification FSM in Figure 1 taken from [START_REF] Dorofeeva | An improved conformance testing method[END_REF]. Consider a test suite T S = {raaa, rabb, rbaba, rbbab}. By direct inspection, one can assure that Proposition 2 does not hold, since states 2 and 3 that are reachable through sequences a and b are not distinguished with suffixes aa, bb and aba, bab. Nevertheless, if an implementation FSM P reaches the same state under input sequences a and b, then this machine reaches the same state under input sequences aa, ba and ab, bb. The latter means that P has four different responses to the set {a, b} of input sequences and thus, the deterministic machine P has more than three states. This example shows that states of an IUT reached by two sequences of SC can be implicitly distinguished not only after applying a distinguishing sequence exactly at these states. This intuition leads to a new statement written as Proposition 3.

Proposition 3. Given the reduced connected specification FSM M with n states and an FSM P with at most n states, let T S be a finite set of finite input sequences of M such that FSMs M and P are T S-equivalent. The FSMs M and P are equivalent if the following conditions hold:

1. For each state s and an input sequence α such that δ M (s 0 , α) = s there exist input sequences β 1 , . . . , β n-1 such that all the states reached from the initial state p 0 in P via input sequences β 1 , . . . , β n-1 are pair-wise different.

2. Given a sequence α.i, i ∈ I, such that δ M (s 0 , α) = δ M (s 0 , α.i) = s, the states reached from the initial state p 0 in P via input sequences α, β 1 , . . . , β n-1 are pairwise different. 3. Given a sequence α.i, i ∈ I, such that δ M (s 0 , α.i) = δ M (s 0 , β t ) = s for t ∈ {1, . . . , n -1}, the states reached from the initial state p 0 in P via input sequences α.i, β 1 , . . . , β t-1 , β t+1 , . . . , β n-1 are pair-wise different.

Sketch of the Proof. Indeed, if the condition (1) of the above proposition holds then there exists the one-to-one correspondence between sets of states of M and P .

The conditions (2) and (3) of the proposition show that this correspondence is valid for all transitions of M . Consider again the example in Figure 1. Condition 1 of Proposition 3 holds for the state cover set ε, a, b due to the above comments. The final states of the transitions under inputs a and b from a state reached after applying input sequence a are different from states reached under input sequences of the set ε, b according to an input sequence a that distinguishes state 1 from states 2 and 3. The final states of the transitions under inputs a and b from a state reached after applying input sequence b are different from states reached under input sequences of the set ε, a according to input sequences ba and ab that distinguish state 1 from states 2 and 3, i.e., Conditions 2 and 3 of Proposition 3 also hold. Therefore, according to Proposition 3, the T S is a 3-complete test suite. We still do not know whether the conditions of Proposition 3 are necessary and sufficient conditions for the test suite completeness. However, this novel definition of determining different states of an implementation under test without using distinguishing sequences directly at these states, opens new directions to find sufficient (necessary and sufficient) conditions for the test suite completeness. In order to check the above properties, we use the Z3 solver which has already illustrated its effectiveness when solving formal verification problems.

First-order formulas and complete test suites

In order to verify that appropriate properties hold for a given test suite (Propositions 1-3), we use first-order logic formulas. The notion of a first-order logic formula includes the notions of predicate symbols, functional symbols and constants [START_REF] Huth | Logic in Computer Science: Modelling and reasoning about systems[END_REF]. Formally, a term t ::= x|c| f (t, . . . ,t) where x ranges over a set of variables, c is a constant and f is a functional symbol. Then a first-order (quantified) logic formula is a formula ϕ ::

= P(t 1 , . . . ,t n ) | (¬ϕ) | (ϕ ∧ ϕ) | (∀xϕ) | (∃xϕ)
where P is a predicate of arity n ≥ 1 and t i is a term over functional symbols and variables.

We now describe conditions for the test suite completeness of Propositions 1, 2, 3 via first-order logic formulas. Given FSM M = S, I, O, δ M , λ M , s 0 , |S| = n, T S = {t 1 , t 2 , . . . ,t m } is a test suite for FSM M , where t j , j ∈ {1, 2, . . . , m}, is a test sequence, with length |t j |. Let SS = {θ 1 , θ 2 , . . . , θ m } (OS = {ζ 1 , ζ 2 , . . . , ζ m }) be a set of sequences of states (sequences of outputs) which an FSM M passes when a corresponding test sequence is applied. For j ∈ {1, . . . , m} and k ∈ {1, . . . , |t j |} we define a k-th element in a sequence t j as t k j . Then the formula for Proposition 1 can be as follows: ∀s ∈ S, i ∈ I, ∃ j ∈ {1, . . . , m}, ∃k ∈ {1, . . . , |t j |}((s = θ k j ) ∧ (i = t k j )). This formula is described in python language and verified via Z3 solver. The corresponding source code is available in [START_REF] Laputenko | Vinarskii[END_REF].

The formula for Proposition 2 is more complex (available in [START_REF] Laputenko | Vinarskii[END_REF]) and we first describe the set of predicates for its simplification: (i) Predicate sub seq(seq, T S) means that sequence seq = a 1 . . . a k is a subsequence of some sequence t j of T S; predicate sub seq(seq, T S) can be expressed via first-order logic as follows: ∃ j ∈ {1, . . . , m}∃d ∈ {1, . . . , In addition, for each state s, we determine the set of all sequences of T S which take the specification FSM from the initial state to state s. If S = {s 0 , . . . , s n-1 }, then SC s j = {seq ∈ I * | sub seq(seq, T S) ∧ reach(s 0 , s j , seq)} for each j ∈ {0, . . . , n -1}. The formula for Proposition 2 For checking the conditions of Proposition 2 the following formula can be used: ∃seq 0 ∈ SC s 0 . . . ∃seq n-1 ∈ SC s n-1 (home(s 0 , s 0 , seq 0 , T S) ∧ . . . ∧ home(s 0 , s n-1 , seq s n-1 , T S)) ∧ ∀ j ∈ {0, . . . , n -1} ∧ ∀i ∈ I ∧ ∀k ∈ {0, . . . , n -1}((s = δ M (s 0 , seq s j .i)

|t j | -k}((a 1 = t d j ) ∧ • • • ∧ (a k = t d+k j )). (ii)
∧ ( = k)) → (∃di f f seq ∈ I * (sub seq(seq s j .i.di f f seq, T S) ∧ di f f (s , s k , di f f seq)))).
The formula for Proposition 3 is rather complex for the analytic description; the source code is available in [START_REF] Laputenko | Vinarskii[END_REF]. The main idea of this formula is as follows. Consider the maximal subset of states S ⊆ S such that for each state s ∈ S there exists a sequence seq for which home(s 0 s, seq, T S) is true and the non-empty subset S of states for which this does not hold. Let s α ∈ S , s β ∈ S be states reachable in M via sequences α and β. If the formula is satisfiable then the following holds: if an implementation under test passes the test suite T S and implementation states reachable via sequences α and β coincide, then the implementation has more than n states.

Experimental results

In this section, we describe how fast the conditions of Propositions 1 and 2 can be checked when using the Z3 solver. Preliminary experiments were performed with randomly generated FSMs using FSM generator from the FSMTestOnline [START_REF]Test generation for finite state machine[END_REF] web-service, which also allows deriving a complete test suite by various FSM-based methods. Experiments showcased that for each generated FSM and complete test suite each formula turned out to be satisfiable, as well as for an incomplete test suite the formula was unsatisfiable. For FSMs with 100 states and 8 inputs, the average time in seconds spent on checking the formula is 219.98 when the formula is satisfiable and 113.24 when the formula is unsatisfiable. The average time for checking the formula according to Proposition 2 was much bigger: for FSMs with five states and two inputs, the average time in seconds spent on checking the formula was 1203.01 when the formula is satisfiable and 18951.48 when the formula is unsatisfiable. For Proposition 3, the formula was checked only for the example of [START_REF] Dorofeeva | An improved conformance testing method[END_REF] where this formula was satisfiable illustrating that a considered test suite is 3-complete. To conduct experiments, a python script was developed that uses API for SMT solver Z3. The experiments were carried out using virtual machine with a AMD Ryzen 5 2500U CPU @ 2.0 GHz running OS GNU/Linux Ubuntu 16.04 with 7 GB RAM.

Conclusion

In this paper, we have described the known necessary or sufficient conditions for an FSM-based test suite to have guaranteed fault coverage via first-order logic formulas and checked these formulas using Z3 solver. In addition, we have suggested a new sufficient condition for the implicit distinguishability of implementation states. In the future, we are going to use this condition for deriving shorter complete test suites as well as for checking the completeness of a given test suite.

Fig. 1 :

 1 Fig. 1: The example of the specification FSM.

  Predicate reach(s 0 , s, seq) means that state s is reached from state s 0 via sequence seq in FSM M . (iii) Predicate di f f (s, s , seq) means that sequence seq is a distinguishing sequence for states s and s . (iv) Predicate home(s 0 , s, seq, T S) = reach(s 0 , s, seq) ∧ ∀s ∈ S (s = s → ∃di f f seq ∈ I * (sub seq(seq.di f f seq, T S) ∧ di f f (s, s , di f f seq))) means that state s is reached from state s 0 via sequence seq in FSM M and for each state s ∈ S, the test suite T S has a sequence which distinguishes states s and s .


Enrico Russo

Luca Verderame

Alessio Merlo

Enabling Next-Generation Cyber Ranges with Mobile Security Components

Keywords: Cyber Range, Mobile Security, Cybersecurity Training

The number of security incidents involving mobile devices has risen in the past years. This means that organizations must seriously consider such devices within their threat landscape and prepare their cybersecurity operators to prevent, identify, and manage security issues involving them. Nowadays, cyber ranges represent the most effective and versatile systems for training skills in the cybersecurity domain as they provide hands-on experiences in large, sophisticated infrastructures. Nevertheless, cyber ranges are capable of emulating components and interactions of the Information and Operational Technology domains, but they lack the support of mobile devices with the same effectiveness and realism. In this paper, we propose an enhancement of the architecture and the training environments of an existing cyber range, which properly integrates mobile security components. The effectiveness of such an integration is due to a thorough review of the mobile threat landscape and the functional components of a cyber range.

Introduction

Cyber ranges are virtualized environments that allow defining specific training in cybersecurity for a plethora of different students. A cyber range emulates an actual cybersecurity-relevant scenarios (e.g., the ICT deployment of a corporation or a small city) in which teams of several trainees compete to reach different (and conflicting) aims. A typical (and simplified) cyber range deployment involves a simulated ICT environment in which all components of the environment suffer from specific vulnerabilities, properly inserted before the competition start. On one side, a red team is aimed at discovering and exploiting such vulnerabilities, while, on the other side, a blue team aims to discover and fix the same vulnerabilities, before the red one can exploit them.

The granularity of the exercises, as well as the kind of vulnerabilities to play with, depends on the number and kind of emulated ICT infrastructures in the cyber range. A missing brick is the mobile component of the emulated ICT infrastructure. As a consequence, a lot of high impact vulnerabilities and attack patterns cannot be tried in current cyber ranges. In fact, a vulnerable mobile node may act as a Trojan Horse to contact other connected devices, perform harmful commands or spread malicious software. Furthermore, a compromised mobile device may allow the attacker to steal, publicly reveal, or sell any personal information extracted from the device and the installed apps, including the user's information, information about contacts, or credentials.

To try bridging this gap, in this paper we discuss the importance of adding mobile components in actual cyber ranges, by illustrating a training motivating scenario (Section 2). Then, we point out the mobile threat landscape (Section 3) in order to identify the most promising family of vulnerabilities and attack patterns that can be fruitfully ported on cyber ranges. Furthermore, we detail a taxonomy and an architectural model of a generic cyber range (Section 4), before pointing out how such architectures can be extended and integrated with a mobile component (Section 5). Finally, we discuss some related work and some future steps towards the implementation of a next-generation cyber range emulating mobile components.

Motivating Scenario

In this section, we introduce a motivating scenario concerning a security testing against the employees and the Information Technology (IT) infrastructure of an enterprise.

A Penetration Testing Activity

A penetration test [START_REF] Bishop | About Penetration Testing[END_REF], also knows as a pentest, is a simulation of an attack against a given system or environment. The purpose of a pentest activity is identifying weaknesses and vulnerabilities in the target before an attacker can identify and exploit them for malicious activities.

This scenario is inspired by [START_REF] Pierini | From APK to Golden Ticket[END_REF] and refers to the pentest conducted to find possible ways to steal reserved documents from a target enterprise. The initial conditions require the actors, namely the pentesters, to have no internal knowledge of the target system and negligible privileges. In detail, the pentesters have only a time-limited access to the guest network, i.e., the wireless network granting visitors access to the Internet and isolated from corporate resources. Nevertheless, the entire attack sequence led to the gain of the admin rights and the creation of a special Kerberos ticket, namely the Golden Ticket [START_REF] Soria-Machado | Kerberos golden ticket protection. Mitigating Pass-the-Ticket on Active Directory[END_REF], which guarantees a long-term and hard-to-detect persistence. For the sake of presentation, here we only report the relevant steps that involve the mobile components.

First, the pentesters leverage their connection to execute a quick scan of the network and discover that even the employees use the guest wireless. In particular, they discover that the receptionist accesses the guest network to connect her own personal smartphone to the Internet.

Then, they exploit social engineering techniques [START_REF]Conduct social engineering[END_REF] against the receptionist and gather the information that (i) she has a young daughter and (ii) often uses the connected smartphone to make the daughter play with some games inside. This information allows the pentester to conduct a spear phishing [START_REF]Phishing: Spearphishing Link[END_REF] campaign to invite the receptionist to download and install an Android application for children. The suggested application is a real puzzle for children but modified with an injected code to grant the attackers a shell access to the mobile device.

The success of the phishing campaign provides a more stable link to the guest network through the receptionist's smartphone. This connection enables the pentesters to obtain a more in-depth knowledge of the network configuration, as depicted in Figure 1. Notice that the connected device can contact a name resolution server, namely dns, and a web server, namely www, hosted in a different network, probably the corporate Intranet. Moreover, a misconfiguration on the corporate firewall allows the guest hosts to access the login page of the manager application of the www server.

The pentesters use the smartphone as a gateway for attacking the www server. In particular, they obtain the admin password with a brute force attack [START_REF]Brute Force[END_REF], upload a web shell, and gain access to the Intranet.

A sequence of further lateral movements leads to the achievement of admin rights. We refer the interested reader to [START_REF] Pierini | From APK to Golden Ticket[END_REF] for a detailed description of these steps.

The Mobile Threat Landscape

The involvement of vulnerable mobile devices in an attack can have severe consequences. Indeed, the attack discussed in Section 2 underlines the strategic importance of including mobile devices and applications in a cyber range exercise.

From a general standpoint, mobile devices share the same IT infrastructure of other connected devices. As shown in Figure 2, the device can connect through a Wi-fi or cellular network to the Enterprise systems and consequently to the exposed Back-end Services such as Email servers, File Shares, and Enterprise App servers. Furthermore, the mobile device may host third-party apps retrieved by either Public or Enterprise App Stores. To cope with the complexity of evaluating the security risks posed by such a mobile ecosystem, several initiatives propose frameworks and procedures for the threat modeling and the vulnerability assessment and penetration testing of mobile apps and devices. Notable examples include the Mobile Applications Security Verification Standard (MASVS) from the OWASP consortium [START_REF]OWASP: OWASP Mobile Security Testing Guide[END_REF] and the Mobile Threat Catalogue by NIST [START_REF]Mobile Threat Catalogue[END_REF].

For instance, Figure 3 depicts the Threat Model Diagram for a mobile app that can interact with a company workstation and its back-end services [START_REF] Sethi | The Developer's Guide to Securing Mobile Applications: Threat Modeling[END_REF]. The diagram details the Assets controlled or accessed by the app, the possible Threat Agents that can interact with the ecosystem and, finally, describes a set of Controls that enable the mitigation of security breaches.

We can use the Threat Model Diagram to map the attack exploited in the Motivating Scenario: the attacker crafted a malicious app without specific permissions (TA04 -Malicious App (Sandboxed)) and then delivered it to the victim using a phishing message (e.g., [START_REF] Aonzo | Phishing attacks on modern android[END_REF]). Once installed, the app grants access to the device functionalities and the credentials of the victim (A06 -A03). After this Fig. 3: Example of a Threat Model Diagram of a mobile app, taken from [START_REF] Sethi | The Developer's Guide to Securing Mobile Applications: Threat Modeling[END_REF] stage, the mobile app acted as a Trojan Horse to contact other connected devices, perform harmful commands, or spread malicious software.

Cyber Ranges

In this section, we provide a taxonomy and an architectural model of a generic cyber range. The overall layout and its key components, core technologies, and capabilities are inspired by [START_REF] Yamin | Cyber ranges and security testbeds: Scenarios, functions, tools and architecture[END_REF][START_REF] Gonzalez | Cyber Range The Future of Cyber Security Training[END_REF].

In detail, the architectural scheme of a cyber range is depicted in Figure 4. It represents the two main levels, namely the Management and the Training Environment level, the core functionalities and related components. Two specific functionalities, i.e., the Orchestration and the Data Collection, enables interfacing between the two levels. A description of the above elements follows.

Management Level

The Management Level supports the planning and execution of the activities conducted within the cyber range. It can be accessed through a standalone User Interface (UI) or through an Application Program Interface Gateway (API GW). UI simplifies human interaction with the management functionalities. API GW provides a unified entry point for integrating external entities. This level makes Exercise Design. The outcomes of the activities carried out in a cyber range are highly correlated to the quality of the training scenario. This means that the exercise designers must be able to build complex and heterogeneous infrastructures and reproduce events that characterize them, e.g., the users' activity. The Exercise Design functionality includes all the facilities to help designers to create training environments complying with the above constraints.

The definition of the infrastructure and its initial configuration is handled through the Scenario and Content Development (SCD) component. The primary function of SCD is allowing exercise designers to compose scenarios without having to know the underlying technologies and the complexity to configure the running environment. A common solution is to provide SCD with a domain-specific language (see, for example, [START_REF] Russo | Building Next Generation Cyber Ranges with CRACK[END_REF][START_REF] Fite | Simulating Cyber Operations: A Cyber Security Training Framework[END_REF]) for detailing the training environments of a cyber range. In particular, the above language, also identified as the Scenario Definition Language (SDL), allows the declarative specification of the scenario elements (e.g., a server, a firewall, or an IoT device), and their (mis)configurations (e.g., the installed software, the configured users, or the affected vulnerabilities).

A further component, namely the Workflow Management (WM), is in charge of scheduling and programming events, i.e., scenario injections, that are performed during the simulation. The WM supports the configuration of scenario injections through an extension of SDL, namely extended SDL (eSDL), that resembles the languages for business process modeling. Briefly, an exercise designer can use eSDL to configure (a combination of) activities, e.g., a scenario element that generates Internet traffic, and the conditions allowing their executions, e.g., a time constraint.

Finally, the Orchestrator functionality receives the outputs from the Exercise Design components. First, it interacts with the Scenario components and creates the sandbox defined with the SDL specification. Then, it handles tasks and condition defined with eSDL and, when required, execute a specified activity interacting with the Support Services component.

Competency Management. The Competency Management functionality includes systems used to manage a competence program. In particular, the above systems allow an organization to perform the skill gap analysis, user profiling, and, consequently, define learning paths and competence assessment.

A first component, i.e., the Scoring and Reporting Dashboards (SRD), scores trainee during their interaction with the cyber range. The main outcome of the scoring system is monitoring the progression of activities and showing a timeline of performances of individual users or teams. SRD also reports the real-time situational awareness,e.g., the impact of tools used, and action taken by the users during the exercise.

A further core component that integrates the Competency Management functionality is the Learning Management System (LMS). LMS is required for the administration, documentation, tracking, reporting, and delivery of learning and assessment content.

The Data Collection functionality extracts from the training environment most of the data used by these components, e.g., services status, generated traffic, memory dumps, logs, or other artifacts.

Training Environment

The Training Environment level represents the sandbox in which teams and individual users carry out their activities during the exercise execution. It includes the Scenario along with the Support Services and Toolsets functionalities.

Scenario. The Scenario functionality includes the digital infrastructure where all the activities are staged as well as all the game-specific aspects such as targets, vulnerabilities and rules of engagement. To this aim, it mainly leverages Virtualization and Cloud Computing components to host the virtual instance of all the required components.

Nevertheless, the Scenario may also require the inclusion of physical devices such as network equipment or IoT systems. The Physical Hardware (PH) component manages the interfacing with these hardware items.

PH also enables the Hardware-in-the-Loop (HITL) capability and allows real systems to interact with virtual stimuli received from the training environment.

Support services. Actions performed by the Support Services functionality take place during the execution of the exercise and help to improve the realism of the training experience. Support Services interact directly with the Scenario and include the following components.

-End-User Simulation (EUS). It simulates the presence and behavior of benign users in the training environment. User simulation may refer to both internal users or fictitious clients accessing exposed services of the simulated environment. Examples of such user activity can include browsing the Internet, sending emails, or interacting with cloud or external services. -Traffic Generator (TG). This component is capable of automatically generating both benign and malicious traffic. The function of traffic generators is crucial as the ability to identify and react to attacks by defense systems and operators lies in the precision with which traffic can be distinguished. -Attack Simulation (AS). It refers to the ability to simulate attacks within and to the simulated environment. This component made available an attack library which contains a list of pre-defined attacks together with the ability to import/create custom operations. Attacks are performed interacting with the Red Team Toolset, and they may aim at exploiting vulnerabilities, executing lateral movements, and injecting malware or backdoors. -Simulated Internet. It provides services outside the main simulated environment that are required for the realization of specific use cases. For example, this component can simulate social media (e.g., Twitter, Facebook, or LinkedIn), internet routing protocols, global services such as name resolution, remote API endpoints, or update and software repositories for various operating systems.

Toolsets. A cyber range is also equipped with state-of-the-art attack and defense tools made available to attackers (red team) and defenders (blue team) by the Red Team (RTB) and Blue Team Toolsets (BTT), respectively. RTB consists of a collection of tools that aid in attacker operations, e.g., reconnaissance, weaponization, command-and-control, escalate privileges, lateral movements, or data exfiltration.

BTT includes services for the identification and prevention of intrusions, e.g., anti-malware or intrusion detection systems [START_REF] Migliardi | Improving energy efficiency in distributed intrusion detection systems[END_REF][START_REF] Migliardi | Modeling the energy consumption of distributed ids: A step towards green security[END_REF], and tools for carrying out analysis and managing security incidents, e.g., a System Information and Event Management (SIEM) software or digital forensic tools.

Extending Cyber Ranges with Mobile Ecosystems

As previously discussed, one of the main strengths of cyber ranges is the execution of exercises with a high degree of realism. Unfortunately, state-of-the-art cyber ranges cannot easily cope with a scenario that comprises mobile devices and apps. Indeed, current cyber ranges threat models do not include mobile ecosystems specifically, and thus the corresponding Assets, Threats, and Controls are coarse-grained and inaccurate. This implies that designers cannot create mobile-first exercises -like the one presented in Section 2 -and thus, red and blue teams cannot train their attack and defense skills in a mobile ecosystem.

To this aim, we define and present here an extension of the cyber range architectural model to support mobile ecosystems.

Mobile-Aware cyber range Architecture

The support of the mobile ecosystem requires a revision of the components of a cyber range (see Section 3) following the analysis of their functionalities that need to be updated or added. In table 1, we summarize the results of the above analysis presenting the required integration tasks for revising each component.

b. Attack Simulation

-T.2b: supporting the interaction with mobilespecific attack tools. c. Simulated Internet -T.2c: introducing the mobile-specific components. 3. Toolsets a. Blue Team -T.3a: extending the weapon rack with mobilespecific tools for BTs. a. Red Team -T.3b: extending the weapon rack with mobilespecific attack tools.

Scenario and Content Development. A major set of updates concerns functionalities providing facilities for personnel involved in designing exercises, i.e., the SCD and WM components.

A first update consists of extending SDL languages to support the addition of mobile components and their configurations in the scenario specification (Task M.a1.1). For instance, cyber ranges can use easily expandable languages, e.g., CRACK SDL [START_REF] Russo | Building Next Generation Cyber Ranges with CRACK[END_REF], to reproduce mobile elements and configurations through typed nodes. Figure 5 depicts the CRACK SDL diagram for the receptionist's smartphone as described in the motivating scenario. In detail, the device and guestwifi nodes represent components of the existing Compute and Network types, respectively. They represent the compute node, i.e., a virtual machine, connected to the guest network. The System.Android, Android.Cfg.Mail, and Android.Vuln.ExtSrc types are an example of an extension of the existing CRACK SDL. The smartphone node is the instance of the Android system running on the compute node. Its type allows the designer to specify the Android version through the version property. The mailbox node represents an Android configuration. In particular, it configures the mailbox used by the receptionist for reading emails on the smartphone. Its type allows the designer to specify the credential for accessing the mailbox through the user and pass properties. The vuln1 node is a vulnerability that arises from a misconfiguration of the smartphone.

In addition to the support of an extended SDL language, the SCD needs to associate a corresponding configuration script to each new component (Task M.a1.2). For example, the Android.Vuln.ExtSrc type presented in Figure 5 must be translated into a sequence of operations required on Android for allowing the installation of apps from unknown sources.

Scenario. Hence, the scenario deployment is handled by an SDL Orchestrator that (i) parses the specification, (ii) selects all the configuration scripts associated with the scenario, and (iii) executes the script on the related System node.

Typically, the execution phase is managed using automation IT tools, e.g., Ansible [START_REF] Hat | [END_REF], that use Secure Shell (SSH) daemons to access each compute node and execute the scripting operations to configure the scenario. However, mobile OSes do not support by default the SSH connectivity, and thus, it is not the best method to configure them. For example, the Android debug bridge [START_REF]Android: Android Debug Bridge[END_REF] (ADB) can run over a TCP connection and facilitates a variety of device configuration and actions.

To this aim, the Orchestrator must be extended to support specific connectivity methods (i.e., an ADB plugin) for configuring mobile devices (Task T.1a).

The operations described above apply to mobile OSes running inside a virtual machine. Unfortunately, in some cases, mobile OSes can not be executed inside a virtual environment. For instance, this is due to a licensing problem, virtual hardware incompatibility, or because designers want to include a physical mobile device in the exercise scenario. For this reason, the PH component must be extended to support the interfacing with physical mobile devices (Task T1.b). A suitable solution for this extension could be (i) having the management interface through a USB cable and (ii) providing the connectivity to the training environment using a wireless access to the scenario networks.

Workflow Management. As it happened for the SDL language, a further update consists in extending eSDL in the Workflow Management to support activities and conditions related to a mobile ecosystem (Task M.b2.1). As an example, Figure 6 depicts the eSDL diagram of the spearphishing attack described in the motivating example. The diagram represents an injection event that is programmed to possibly occurs during the running exercise. Differently from the traditional eSDL language, we introduced two activities, A1 and A2, to mimic the user operations on Android devices. The A1 activity download and read an email using the Android mail app. The A2 activity download and install an app from a HTML link in input and install it on Android. Support Services. As detailed in Section 4, eSDL activities are executed in the running environment by the Orchestrator but through the EUS and TG com-ponents of the Support Services. Therefore, EUS and TG must be extended to execute mobile-specific actions on running devices (Task T.2a). To do so, the Support Services need to include specific software to interact and simulate the user interaction, such as the monkeyrunner tool [4] and DroidBot [START_REF] Li | Droidbot: a lightweight ui-guided test input generator for android[END_REF] for Android OS.

Another fact that features the mobile ecosystem is its close relationship with Internet services. As described in Section 3, apps installed on mobile devices are typically retrieved from stores hosted on the public Internet. Moreover, many mobile apps implement their functionalities interacting with remote API services exposed by servers from the Internet. For this reason, the SI component must be integrated with services that simulate App Stores and remote API services (Task T.2c). For instance, the SI can include a customized application market based on the F-Droid [START_REF] Limited | F-Droid[END_REF] open-source marketplace and a system to mock remote API services based on the Mocky [START_REF] Lafont | Mocky.io[END_REF] tool.

Toolsets. Concerning the Toolsets component, the cyber range needs to include mobile-specific tools for both the Red and Blue teams (Tasks T.3a and T.3b).

For example, as described in the motivating scenario, the red team could use an injection tool, namely Metasploit framework [START_REF]Rapid7 LLC: Metasploit Framework[END_REF], to generate a malicious payload and pack it into a legitimate Android application as a Trojan to compromise the user device. Other red team tools can include Owasp ZAP Proxy [START_REF]Open Web Application Security Project: Zed Attack Proxy[END_REF], zAnti [START_REF]Zimperium: zAnti[END_REF], and iNalyzer [START_REF]AppSec Labs: iNalyzer[END_REF].

Notice that some of these attacking tools need to be integrated with the AS component (Task T2.b) if they are used to perform operations during automatic attacks.

On the other hand, blue teams can use vulnerability assessment tools, e.g., apktool [START_REF] Tumbleson | Apktool[END_REF], jadx [START_REF]Skylot[END_REF], and Mobile Security Framework (MobSF) [START_REF] Abraham | Mobile Security Framework[END_REF], to detect vulnerabilities and patch mobile apps [START_REF] Aonzo | Obfuscapk: An opensource black-box obfuscation tool for android apps[END_REF].

Competency Management. Mobile-aware cyber ranges requires also to extend the Competency Management. In particular, trainees must practice on topics and hands-on specific to mobile security before tackling an exercise on a complex and mixed scenario. These new resources need to be added to the LMS component (Task M2.b). For example, the contents hosted by LMS could be enriched with documentation and related exercises about the security of mobile ecosystems, such as fundamentals of decompilation of mobile apps, static analysis techniques, fundamentals of app repackaging and instrumentation, how to intercept the network traffic of an app, or forensic techniques for mobile devices.

Similarly, the rating of the trainees' performances must be extended according to their activities related to the mobile environment. In detail, the SRD score must include the goals that involve mobile assets (Task M.2a). For example, a red team's goals could include taking control of a mobile device, exfiltrate data from smartphones and apps, or threaten the overall service availability shutting them down. On the other side, new blue team goals could be reporting how they hardened flaws in mobile devices' configuration or how they analyzed and patched an installed app.

Related Work

The increasing popularity of Cyber Ranges is pushing the research community to design and build advanced Cyber Ranges architectures. More in detail, most of the attention is devoted to the building and deployment of complex and heterogeneous training scenarios to reduce the learning curve of students. The KYPO cyber range [START_REF] Vykopal | Kypo cyber range: Design and use cases[END_REF] is a cyber exercise and research platform where security experts can carry out exercises and experiments in a secure and isolated environment. KYPO simulates complex scenarios through virtual environments hosting different types of infrastructural components. These scenarios can also include mobile devices running virtual machines with Android images.

ADLES [START_REF] Conte De Leon | ADLES: Specifying, deploying, and sharing hands-on cyber-exercises[END_REF], CyRIS [START_REF] Beuran | Cybersecurity education and training support system: CyRIS[END_REF], CRACK [START_REF] Russo | Building Next Generation Cyber Ranges with CRACK[END_REF] are tools for creating cyber range scenarios and use virtualization for deploying them. Like [START_REF] Vykopal | Kypo cyber range: Design and use cases[END_REF] they can potentially emulate mobile devices running Android in the instantiated virtual machines.

Unlike [START_REF] Vykopal | Kypo cyber range: Design and use cases[END_REF][START_REF] Conte De Leon | ADLES: Specifying, deploying, and sharing hands-on cyber-exercises[END_REF][START_REF] Beuran | Cybersecurity education and training support system: CyRIS[END_REF][START_REF] Russo | Building Next Generation Cyber Ranges with CRACK[END_REF], a proficient training on mobile security can not be limited only to the integration of Android virtual machines in the running scenario. It requires at least the support of specific configurations and vulnerabilities, the emulation of their strong relationship with the user activity through adhoc runtime injections, and the support of targeted tools like the preliminary proposal we discussed here.

Many other initiatives offer hands-on solutions for training security experts on mobile security. Among them, the MSTG Playground [START_REF]Open Web Application Security Project: MSTG Hacking Playground[END_REF], the Android Security Sandbox [START_REF] Toledo | Android Security Sandbox[END_REF], DIVA Android [START_REF]DIVA Android[END_REF] and InsecureBankv2 [START_REF] Shetty | InsecureBankv2[END_REF] provide vulnerable apps to be used as the target of VAPT sessions. Other similar forms of hands-on activities are Capture the Flag (CTF) challenges like UnCrackable Mobile Apps [START_REF]OWASP: UnCrackable Mobile Apps[END_REF], KGB Messenger [START_REF] Lambert | KGB Messenger[END_REF] and Mobile CTF [START_REF] Rodriguez | Mobile CTF[END_REF].

However, although these hands-on solutions represent an effective way to learn mobile security, they are unable to cover the comprehensive process of cybersecurity defense like Cyber Ranges and our proposal do.

Conclusion

This paper is an early step towards enhancing generic cyber ranges with the full integration of the mobile security ecosystem in their training environments. We briefly reviewed the mobile threat landscape along with the component and functionalities of the current state-of-the-art cyber ranges. The above analysis allowed us to detail a list of tasks and examples to simplify and carry out such an integration. This project is still on-going and we identify the following main next steps.

First, a complete implementation of the proposal on an existing and running cyber range. During this activity, we strongly require to focus our effort on extending the SDL and its orchestrator engine with the support of a rich catalog of configurations, vulnerabilities and runtime actions for mobile components.

Then, after a survey of real-world case studies involving the use of mobile components in complex IT infrastructures, we need to identify key aspects to be reproduced in training exercises. This effort should lead us to proficiently extend the current training scenarios with mobile components and make the most of the new features.

Finally, we need to validate our proposal by using an extended scenario and evaluating the training outcome after an exercise session.

Fig. 1 :

 1 Fig. 1: The diagram of the penetration testing scenario.

Fig. 2 :

 2 Fig. 2: Mobile ecosystem landscape.

Fig. 4 :

 4 Fig. 4: The architectural scheme of a cyber range.

Fig. 5 :

 5 Fig. 5: An excerpt from the CRACK SDL diagram for the motivating scenario.

Fig. 6 :

 6 Fig. 6: A eSDL diagram for the spearphishing attack of the motivating scenario.

Table 1 :

 1 Integration tasks for mobile security components.

	Management level (M)
	1. Exercise Design
	a. Scenario and Content De-	-M.a1.1: extend SDL with new components.
	velopment	-M.a1.2: add configuration script for new compo-
		nents.
	b. Workflow Management	-M.b1.1: extend SDL+ with new actions and condi-
		tions.
	2. Competency Management
	a. Scoring and Reporting	-M.2a: extend goals and metrics with ones related
		to mobile components.
	b. Learning and Management	-M.2b: introducing learning material and hands-on
	System	specific to mobile security.
	Training environment (T)
	1. Scenario
	a. Virtualization/Cloud	-T.1a: extend automation tool for supporting
		mobile-specific connectivity.
	b. Physical Hardware	-T.1b: support the interfacing with physical mobile
		devices.
	2. Support services
	a. End-Users Simulation/-	-T.2a: execute mobile-specific actions.
	Traffic Generator

Acknowledgement

This work was partially funded by the Horizon 2020 project "Strategic Programs for Advanced Research and Technology in Europe"(SPARTA) and by the Italian Ministry of Defense PNRM project "UNAVOX".


Luca Verderame

Davide Caputo

Andrea Romdhana

Alessio Merlo

APPregator: a Large-scale Platform for Mobile Security Analysis *

Keywords: App Analysis, Static and Dynamic Analysis, Security & Privacy

The Google Play Store currently includes up to 2.8M apps. Nonetheless, it is rather straightforward for a user to quickly retrieve the app that matches her tastes, as Google provides a reliable search engine. However, it is likewise almost impossible to select apps according to a security footprint (e.g., all apps that enforce SSL pinning). To overcome this limitation, this paper presents APPregator, a platform which allows security analysts to i) download apps from multiple app stores, ii) perform automated security analysis (both static and dynamic), and iii) aggregate the results according to user-defined security constraints (e.g., vulnerability patterns). The empirical assessment of APPregator on a set of 200.000 apps taken from the Google Play Store and Aptoide suggests that the current implementation grants a good level of performance and reliability. APPregator will be made freely available to the research community by the end of 2020.

Introduction

Risk assessment is crucial for IT systems, and it became a key issue for mobile apps, which are increasingly used every day for private or working activities. To deal with app security problems, several tools for the analysis of vulnerabilities have been proposed over the years. Despite this, such efforts did not provide a solution allowing to build a global view of the security status over a set of arbitrarily selected mobile apps. In particular, some research projects produced datasets that allow performing analysis on the security features of apps, however, these projects are focused mainly on malware. Indeed, automatic techniques are especially used to study malware and prevent its spread, but the same effort is not applied to find vulnerabilities exposed in apps that could be exploited both by malicious apps or external attackers (i.e., confused deputy attacks). Albeit there exist some proposals that allow assessing the number of apps affected by a specific vulnerability, the results and the tools are kept mostly private so that only a few information is available and the tools cannot be used to replicate the analysis in the wild. To overcome previous limitations, we designed and implemented a large scale platform for mobile security analysis called APPregator. The purpose of AP-Pregator is to help researchers and developers to discover new vulnerabilities in Android apps, allowing them to aggregate and analyze a subset of Android apps that match specific security and privacy constraints as well as examining the distribution of security flaws. The proposed platform can automatically download apps from multiple stores and aggregate information about them, perform automated security analysis (both static and dynamic), and moreover, it is able to notify the results of the security analysis to apps' developers in a fully automatic way. Furthermore, our proposal allows researchers to aggregate the results according to defined security constraints and privacy. To prove the scalability and reliability of our proposal, we collected in one month 200, 000 apps information from app stores and we performed a security analysis on 3, 500 apps. Furthermore, the 3, 500 apps were subjected to statistical analysis with the aim of examining the distribution of security flaws (i.e., insecure connections, privacy leaks, and hard-coded keys).

Structure of the paper

The rest of the paper is organized as follows: Section 2 introduces the vulnerability assessment of mobile apps, while Section 3 presents the current state of the art. Section 4 defines the requirements of a large-scale platform, Section 5 presents the design of APPregator. Section 6 discusses the implementation choices for APPregator, while Section 7 shows the capabilities of the platform proposed. Finally, the Section 8 concludes the paper and points out some extensions of this work.

Vulnerability Assessment of Android Apps

The vulnerability assessment of Android apps is based on two main approaches: static and dynamic analysis. Static analysis techniques enable the evaluation of an app by examining the source code and the package content without executing it. Static analysis examines all possible execution paths and variable values, not just those invoked during execution. Thus, it can reveal errors and vulnerabilities that may not manifest themselves during the code execution, thereby leading to false positives. Dynamic analysis techniques, instead, explore and evaluate the behavior of the app during its execution. Unfortunately, its effectiveness is influenced by the current limitations imposed by automated testing techniques that fail to analyze the whole app surface, leading to false negatives. To this aim, the typical assessment workflow combines both the approaches, and it is composed of the following steps:

-APK Reverse Engineering. In this step, the Android Package (APK) is unpacked to retrieve manifest, resources, certificate and the app compiled code (dex files). The compiled code can be disassembled or decompiled. In the first case, the dex files are transformed using a disassembler (e.g., apktool [START_REF]Apktool[END_REF]) in order to obtain a human-readable representation of the dex format called Smali [START_REF] Smali | [END_REF]. In the second case, the dex files are reconverted in the original source code (or a representation of it) using tools like dex2jar [START_REF]Dex2jar[END_REF] or jadx [START_REF] Jadx | [END_REF]. -Static Analysis. The app code is analyzed to evaluate the presence of security misconfigurations, vulnerable APIs, and security patterns. Static analysis of an app package often relies on the model representation of the app logic (e.g., through control flow graphs or call graphs [START_REF] Yang | Appcontext: Differentiating malicious and benign mobile app behaviors using context[END_REF][START_REF] Armando | Enabling byod through secure meta-market[END_REF]). Furthermore, static analysis techniques also evaluate non-code elements, i.e., the manifest file and all the resources files. These files are analyzed to detect misconfiguration or essential information about the app (e.g., exported activities, debug information, hard-coded keys, etc.). The most famous used tools are FlowDroid [START_REF] Arzt | Flowdroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps[END_REF], TaintDroid [START_REF] Enck | Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones[END_REF] and AmanDroid [START_REF] Wei | Amandroid: A precise and general inter-component data flow analysis framework for security vetting of android apps[END_REF]. -Dynamic Analysis. During the dynamic analysis, the app is installed and executed in a controlled environment (usually a virtual machine) in order to monitor its runtime behavior. During this phase, the behavior observed is the interaction with the file system, with the OS (i.e., all APIs invoked at runtime), and with the network by sniffing and collecting all traffic exchanged by the app during the execution. The app is stimulated using automatic tools that simulates human behavior like Droidbot [START_REF] Li | Droidbot: a lightweight ui-guided test input generator for android[END_REF] or Monkey [START_REF]Monkey runner[END_REF].

Related Work

The typical vulnerability assessment workflow has been adopted by several frameworks and tools to either evaluate the security state of the apps (e.g., SCanDroid [START_REF] Fuchs | Scandroid: Automated security certification of android applications[END_REF], CHEX [START_REF] Lu | Chex: statically vetting android apps for component hijacking vulnerabilities[END_REF], DroidChecker [START_REF] Chan | Droidchecker: analyzing android applications for capability leak[END_REF], DroidSafe [START_REF] Gordon | Information flow analysis of android applications in droidsafe[END_REF], AppAudit [START_REF] Xia | Effective real-time android application auditing[END_REF]) or to monitor apps behavior (e.g, ProfileDroid [START_REF] Wei | Profiledroid: multi-layer profiling of android applications[END_REF], CopperDroid [START_REF] Tam | Copperdroid: Automatic reconstruction of android malware behaviors[END_REF], AppIntent [START_REF] Yang | Appintent: Analyzing sensitive data transmission in android for privacy leakage detection[END_REF], Droid-Miner [START_REF] Yang | Droidminer: Automated mining and characterization of fine-grained malicious behaviors in android applications[END_REF], AsDroid [START_REF] Huang | Asdroid: Detecting stealthy behaviors in android applications by user interface and program behavior contradiction[END_REF]). However, all the above solutions focus on the security evaluation of a single app and do not provide mechanisms to i) retrieve sets of apps automatically, ii) evaluate the app's security posture in the different versions and the various application stores, and iii) prune, query and filter apps according to their security evaluation.

In the last years, both the scientific and industrial communities have proposed datasets that collect security information about apps. In [START_REF] Geiger | Datasets of android applications: a literature review[END_REF] the authors identified that there are five datasets that collect information of more than 1 million of apps: Appannie [START_REF]Appannie[END_REF], AppBrain [START_REF]App brain[END_REF], AndroZoo [START_REF] Li | Androzoo++: Collecting millions of android apps and their metadata for the research community[END_REF], AndroVault [START_REF] Platzer | Andrubis -1,000[END_REF], and Andrubis [START_REF] Meng | Androvault: Constructing knowledge graph from millions of android apps for automated computing[END_REF]. While the first two are commercial data aggregation tools that use the information to study clients' competitors and improve their market position, the others have a research purpose and provide collections of apps enriched with some metadata and analyzed with several static or dynamic analysis techniques.

For instance, AndroZoo collects information from: (1) the Google Play Store,

(2) the manifest file, (3) the classes.dex files, (4) the presence of native and encrypted code, and (5) the reports of the antivirus and vulnerabilities detection services. Unfortunately, Meng et al. [START_REF] Meng | Androvault: Constructing knowledge graph from millions of android apps for automated computing[END_REF] claim that it is complex to extract valuable information from the AndroZoo dataset and therefore they build a graph of attributes to extract these data. Androvault and Andrubis are two datasets that also perform dynamic analysis. Still, in the former, the authors were unable to execute the dynamic analysis of many apps due to time and technological constraints. The latter, instead, is discontinued and it is no longer updated from 2015. All in all, the primary purpose of those datasets is to analyze and study mobile malware, where most of them are obtained from alternative app stores or virus collections. To the best of our knowledge, there are no solutions able to aggregate apps coming from several stores (including the Google Play Store) and perform both static and dynamic analysis in order to make available to the researchers and developers community the security state of the app and its evolution.

4 Requirements for a Large-scale Platform

In this section, we identify the requirements for a large-scale platform with the capability to perform automated security analysis (both static and dynamic) and aggregate the results according to user-defined security constraints. In detail, the aim of our proposal is to design and implement an architecture that is able to:

1. automatically collect a large set of mobile apps from several app stores; 2. perform static and dynamic analysis of those apps following the typical workflow, as described in Section 2; 3. store all the security-relevant information of the analysis to build a security dataset that can be queried and used to infer statistical results; 4. automatically check the release of app updates to create a security history of mobile apps releases, and 5. automatically notify the developers about security issues founded in their apps.

Apps Collection, Update & Filtering. Since the architecture needs to retrieve large sets of apps from the application stores automatically, it must crawl and download app packages from the leading Android app stores, i.e., Google Play and Aptoide [START_REF]Aptoide[END_REF]), being two of the most widespread Android market places.

For each analyzed app, the architecture should also collect a set of app metadata, to enable fine-grained filtering of the dataset. In detail, we are interested in recording: (1) package name, (2) title, (3) icon, (4) category, (5) developer, (6) number of installs, (7) privacy policy, (8) number of ratings, (9) average ranking, (10) existence of advertising, (11) timestamp of the last update, (12) market of origin, (13) app version, ( 14) file hash, and (15) the analysis date.

Security Analysis. The architecture needs to perform a systematic security evaluation of the Android apps, thereby adopting the workflow described in Section 2. To this aim, the platform needs to perform Reverse Engineering, Static Analysis, and Dynamic Analysis. The reverse engineering step is necessary to obtain information about the files that compose the app and the structure of the app itself (i.e., activities, services, providers, and receivers).

Regarding the static analysis, we are interested in evaluating the following information:

the permissions (used and requested), the invoked APIs; the presence of patterns that could bring to security vulnerabilities. Such a vulnerability analysis should follow security frameworks and standards, e.g., the OWASP Mobile Applications Security Verification Standard (MASVS) [START_REF]OWASP: OWASP Mobile Security Testing Guide[END_REF] and the NIST Mobile Threat Catalogue [START_REF]Mobile Threat Catalogue[END_REF]; the usage of third-party libraries or frameworks; the obfuscation level; the presence of malicious code.

Regarding the dynamic analysis techniques, our platform needs to cover all of the main security measurements. Since most apps communicate over the Internet, the security assessments of network traffic and the communication protocols [START_REF] Armando | From modelchecking to automated testing of security protocols: Bridging the gap[END_REF] is an essential feature. Among the possible checks, the platform needs to evaluate the absence of unencrypted communication and the presence of miss configuration, such as permissive certificate checks or the lack of security enforcement mechanisms (e.g., SSL Pinning) [START_REF] Fahl | Why eve and mallory love android: An analysis of android ssl (in)security[END_REF]. Furthermore, the platform should also identify the domain reputation of all the accessed URLs. Such a feature would help to detect privacy and security leaks affecting multiple apps by checking if they interact with the same unsafe endpoint. The proposed platform also needs to detect all vulnerable third-party components since unpatched and obsolete third-party libraries are the primary source of security vulnerabilities in mobile apps, as described in [START_REF] Backes | Reliable third-party library detection in android and its security applications[END_REF][START_REF] Derr | The impact of third-party code on android app security[END_REF][START_REF] Verderame | On the (un)reliability of privacy policies in android apps[END_REF]. The platform should also report the usage of tracking or advertising libraries to evaluate the presence of potential privacy leaks. Furthermore, the dynamic analysis performed by the platform should also include additional information such as i) the application access to internal and external memory files, ii) the disclosure of sensitive information in the system and application logs, and iii) the use of hard-coded keys, passwords, or private token. Besides the filtering and sorting features, the system should also provide general security statistics such as the most commonly used libraries and contacted domains or the most requested files and leaks found at the same location reported for more apps.

Developers Notification. The platform needs to follow the responsible disclosure guidelines imposed by both application stores and the involved vendors. In detail, we designed our platform to be compliant with the Google's vulnerability disclosure policy [START_REF]Google's vulnerability disclosure policy[END_REF]. In order to meet the requirements, after each security analysis, the platform automatically notifies the app's developer, waiting for 90 days for the inclusion in the dataset. The developer will be able to evaluate the security analysis and apply the required fixes to their apps within that time.

Platform Requirements. To formalize the platform requirements, we organize its features in functional requirements (FUNR), security measures (SECM), and statistical measures (STAT). The first group indicates the primary functionalities of our platform; the second one includes all the security measurements that need to be extracted by the mobile apps, while the last group collects the global metrics that can be computed by the platform. Table 1 presents the full list of requirements and their corresponding IDs.

ID Description FUNR1 Filter apps using the package name or a keyword in the title. FUNR2 Filter apps from a specific developer or category. FUNR3 Filter apps by the number of installations or their score. FUNR4 Filter apps that do not include a privacy policy on the Google Play Store page. FUNR5 Filter apps that requires a specific permission. FUNR6 Filter apps that use a certain category of APIs. FUNR7 Filter apps that include a specific library. FUNR8 Filter apps that use a low obfuscation level. FUNR9 Filter apps that interact with a specific internet domain. FUNR10 Filter apps that use insecure connections. FUNR11 Filter apps that access to a specific file path. FUNR12 Filter apps for which a leak is reported or an hard-coded key is found. FUNR13 Notify the app developers of security issues found in their app. SECM1 The list of components included in an app SECM2 The list of permissions required by an app. SECM3 The list of APIs used by an app. SECM4 The list of libraries included in an app. SECM5 The request to read the Device ID. SECM6 The list of vulnerabilities reported for an app. SECM7 The obfuscation level of an app. SECM8 The probability for an application to be a malware. SECM9 The list of hosts contacted by an app with network security settings. SECM10 The list of files in the external memory used by an app. SECM11 The list of leaks found for an app. SECM12 The list of hard-coded keys reported for an app. STAT1 The most required permissions. STAT2 The most used APIs. STAT3 The most imported libraries. STAT4 The most common vulnerabilities. STAT5 The most contacted domains. STAT6 The domains most involved in a leak. STAT7 The most used files. STAT8 The files most involved in a leak.

Table 1: Platform Requirements

5 APPregator: a large-scale platform for mobile security analysis

In order to meet all requirements described in the previous section, we propose a modular architecture called APPregator. APPregator is composed of several modules, namely Database, Crawler, Worker, and Server. These modules allow to retrieve app information, to analyze its security, and to manage the obtained reports and statistics.

The Database stores all apps information, while the Crawler module identifies and collects the mobile apps. The Crawler also keeps track of the various versions of the apps. The Worker downloads the apps and performs the security analysis. A set of rest API is exposed by the Server to interact with the platform; moreover, the Server features a responsive GUI to extract and filter the data. Figure 1 depicts the modules of APPregator. Worker. The Worker is structured as a micro-service, where each security measure is conducted by a specific sub-module (Figure 1). The Manifest module retrieves information about app components and permissions (SECM1, SECM2).

The API & Strings module is able to retrieve all APIs and string used by the app dividing them into categories (SECM3). The list of libraries included in the app are retrieved by two sub-modules: the Libraries and the Tracking Libraries (SECM4). The Vulnerable Code sub-module reports all vulnerabilities found in the app (SECM6), together with the obfuscation level of the app code (SECM7). The virus scan is performed by the Malware sub-module (SECM8). The Dynamic sub-module performs the dynamic analysis and stores the list of: (1) the host contacted by the app (SECM9),(2) the files used by the app (SECM10) and (3) the information leaked (SECM11). The Device ID access (SECM5) can be retrieved combining the information obtained from Vulnerable Code module and the Dynamic module, while the HardCoded Keys module detects the usage of hard-coded keys (SECM12).

The Download service downloads apps and checks if the latest version available in Google Play Store matches the one in Aptoide. The comparison is done through a specific API [5]. The version of an app is denoted by a name (verName) and a code (verCode). The Worker compares the SHA-2 of the downloaded APKs from the Play Store with those that have the same verName coming from unofficial markets. If the hashes are different, the Worker performs a new security analysis.

If the apps have the same verName and the same verCode but a different hash, the Worker executes the malware analysis, to detect whether those apps are embedding malicious code.

Once the analysis is completed, the Worker uses the Notification sub-module to send the analysis result to the app developer. At last, the Worker publishes the results on the platform, after the 90-day period imposed by the Google policy has expired (FUNR13).

Database. The Database stores the information collected during the analysis and provides the server with data which allows the user to execute the queries. The stored data are organized into two tables. One contains information available in app stores about apps (i.e., Play Store, Aptoide), in which each app is identified by the appId (package name). The other one contains the results of the security analysis, which has a unique verCode (version) for each app associated to the source store. The schema of the Database is described in Figure 2. The Server also adopts operators typically implemented in the query language, such as count, limit and offset, in order to improve user experience and prevent Fig. 3: Example of APPregator Web Interface the retrieving of large sets. If the client filters the data, an estimate of the number of query results is returned. Several navigation buttons allow to navigate through the results (Figure 3). In addition, the server offers the possibility to download all the filtered results which could also represent the entire dataset: the server provides a stream from the database to the client to avoid storing the object in the main memory.

Implementation

The APPregator platform has been designed by leveraging state-of-the-art technologies and tools. The following section explains the implementation of each module.

Worker. The Worker consists of a set of micro-services developed in Java and Python languages. The security analysis is performed through Approver, a Saas developed by Talos [START_REF]Talos sec[END_REF]. Approver consists of:

- Moreover it categorizes the Android API calls contained in the app. -Permission Checker. It produces a list of permissions, taking into account both those used in the code and those declared in the manifest. -Library Detector. This module searches for known third-party libraries inside the app.

-Vulnerability Checker. It identifies code patterns that could be considered as security risks, classifying their severity according to the OWASP Mobile Top 10 [START_REF]Owasp mobile top 10[END_REF]. -Dynamic Analysis. This module stimulates the app by simulating human behavior. The aim is to evaluate as many app features as possible to monitor and analyze all API invocations, file system interactions, and network traffic generated. This information is required to identify security vulnerabilities or privacy leaks (e.g., SSL pinning misconfiguration, phone number leaks, etc.). Dynamic Analysis is the most expensive module in terms of resources and time.

The Worker uses a heuristic based on the results of the API & String module in order to perform the Dynamic Analysis module only when it is necessary.

In detail, the Worker executes it only if the app uses at least one APIs in at least three of the following categories: INTERNET, FILE, CRYPTO, and PHONE. The Worker is composed also by another module named HardCoded Keys. It verifies the presence of hard-coded keys and monitors the functions categorized as CRYPTO. In details, this module compares the strings extracted from the app with the arguments passed to the caller. We decided to ignore arguments with fewer than four characters in order to reduce false positives, because they were too short to be considered as tokens. We also saved the most frequent results for creating lists of exclusion and false-positive.

Databases. The Database Management System of APPregator relies on Mon-goDB. The choice of a document-based solution (i.e., MongoDB) allow clients to query nested values efficiently. The database empowers multi-key index to seamlessly support the addition of new analysis modules or a new crawler. This solution prevents already existing data from being invalidated.

Crawler & Server. APPregator exploits the npm library google-play-scraper 3 , and the query-to-mongo library4 to extract app data from the Google Play Store. In this way, the users can filter the apps in the Database that match specific security-constraint. As a result of the libraries' choice, we used Node.JS and the framework Express for the HTTP server. We used Docker [START_REF] Docker | [END_REF] in order to provide portability and fast deployment of the platform. Docker allows to stop (and eventually restart) the containers when a failure occurs or when a task is completed, thereby reducing memory usage.

APPregator Query Capabilities

We tested APPregator, on real-world apps extracted from the app stores between November 2019 and February 2020. The analysis has been carried out on a single machine with a quadcore 3.40 GHz processor, an SSD with 256 GB of storage, and 24GB of RAM. Using this setup, we were able to collect in one month 200.000 apps information from the market and analyzed 3500 different app versions from the app stores. All queries described in this section were executed in a time-span between 200ms and 800ms. The analysis was carried out inspecting two different aspects of mobile apps: Privacy and Security.

Privacy

Using the Web Server Interface, the user can filter the apps that do not contain a field just using the search bar. For example, if the operator wants to filter apps that do not include a privacy policy on the Play Store page (FUNR4), he can execute the search !policy. If he also wants to find the subset which declared to include advertisements, he can append a semicolon with the new command ads=true, as shown in Code-Snippet 1. By using Code-Snippet 1 query on !policy; ads=true

Code-Snippet 1: Query to find apps with advertising and without a privacy policy the entire dataset, APPregator reports that almost 13.000 apps do not include a privacy policy in the Play Store page on the last check, and about 7.000 of these use advertising anyway. Furthermore, we can sort them out by the number of installations by clicking on the table column name (FUNR3): four apps have at least 100 or 50 million users (Figure 4), 35 apps have more than 10 million installations, 350 more than 1 million installations, and more than 1.500 have at least 100.000 users. Using a search bar the operator can look for apps involved Fig. 4: Top 4 most installed apps without a privacy policy on the Google Play Store in a leak (FUNR12) by using the leaks keyword in the search bar. By using this query on the dataset of analyzed apps, we discovered 21 apps with a potential leak, 17 of which come from the Play Store. In detail, 12 privacy leaks are saved to file, 12 exposed on the net, 19 refer to the device ID, and 5 to the user email. Since the Android best practices for unique identifiers [START_REF]Best practices for unique identifiers[END_REF] recommends developers to avoid using hardware identifiers like the device ID and use GUIDs to identify app instances uniquely, we inspected the collected dataset. Figure 5 presents the results obtained by the query in the Code-Snippet 2: 9 Google Play Store apps send the Device ID to a server.

leaks.net.category=device; store=play

Code-Snippet 2: Query to find Device ID leaks via net in the Play Store Such an issue is particularly relevant when using advertisement libraries as a user-resettable identifier needs to be used. Despite this, the authors of Ad IDs Behaving Badly [START_REF] Egelman | Ad ids behaving badly[END_REF] reported to Google how ads libraries transmit over the net the device ID instead of a user-generated Advertising ID. The results obtained by APPregator confirm, one year later, the worries pointed out in the report, thereby also proving the usefulness of the website search feature (FUNR9) since some of the domains involved are the same reported in the study. Further we tested some of the capabilities offered by APPregator to evaluate the security of the app.

Insecure Connections. To find the usage of insecure connections (FUNR10), the security operator can execute the query net.plain-http. By using the collected dataset, the query reports 7 results. Among the vulnerable apps, six of them come from the Play Store and have between 10 and 100 million installations. On of them apps is a web browser and reading its description in the store, we noticed that one of the features offered is the advertising block during the navigation. However, the app itself contains ads and tracking libraries, which is a behavior far from a privacy-oriented adblocker. Studying connections in a browser app is especially tricky due to the strong dependency on the user input for the URL browsing. However, also the static code analysis reports the presence of http URLs.The connection is related to the usage of the Tencent Login library [16], indeed APPregator also collects the reference to which part of code is involved to facilitate researchers to discover security issues.

Vulnerable Libraries. Another operation that we tested regards finding the usage of a vulnerable library just by inserting its package name (FUNR7) or searching its common name. For instance, 50 apps of the dataset include Tencent Login, but the version described above is used only by the web browser app. Unfortunately, APPregator does not always provide information about the library version, due to the current limitation of the library recognition technology. Indeed, library recognition is not precise due to obfuscation techniques (see, e.g., [START_REF] Aonzo | Obfuscapk: An opensource black-box obfuscation tool for android apps[END_REF]) or the lack of libraries signatures. To mitigate such an issue, some additional filter operations should be performed and to help in this process, the permissions related to the methods used in the instance of the library for a specific app are saved.

Malware. The malware field is a probability obtained by adding up the number of positive responses between different antivirus services and dividing the result for the total number of scans. In our dataset, we only find 5 occurrences with malware>0 raging from 0.016 to 0.032, i.e., a minimal probability. By using the same approach of Meng et al. [START_REF] Meng | Androvault: Constructing knowledge graph from millions of android apps for automated computing[END_REF] that allows identifying repackaging of an app by checking the developer certificate w.r.t. the one in the Play Store, we identify an app between the possible malware with a different value of the certificate. This information is included in the vulnerabilities field with the flag level=Info.

Looking for the hash value of apps on Virus Total, we have retrieved an app analysis that reports an Android.PUA.DebugKey issue. This issue indicates that the app has a debug certificate: the Play Store would not have allowed the app upload, which is instead possible on Aptoide. However, the differences between the app within Play Store and within Aptoide are all related to third parties libraries: it looks like a patched version of the app with ads removed. The other 4 results are false positives.

Hard-coded Keys. APPregator reports 8 apps that contain hard-coded keys (FUNR12): as explained in Section 5, we inserted a check in the code to exclude configuration parameters and manually remove the most frequent values like HmacSHA1 or HmacSHA256. The platform collects the string, the method, and the number of the parameter: the most common method is javax.crypto.spec-.SecretKeySpec, which is used to construct a Secret key starting from the string. This method should be used to store keys generated at run time as authentication tokens, but these strings are inserted into the code and therefore, could represent a security vulnerability depending on the specific case. Usually, the main problem is the usage of API keys for third-party services, that are saved within this method, to be used later in the code. The best practice is to perform the requests server-side, but also string obfuscation is often used.

Conclusion

In one month, APPregator was able to collect information from almost 200.000 apps and performed the security analysis on the 2.000 most installed apps in the Play Store, using only a single machine. It saved more than 3.500 database entries and APK files, including updates and the Aptoide app versions. The aim of this work was to build a platform able to manage large scale studies, and therefore we used technologies optimized for big data and we designed the platform with a distributed architecture. Other works (Section 3) collected a lot of more data, but reached one million results only after a couple of years [START_REF] Platzer | Andrubis -1,000[END_REF] or three million in several months using seven nodes and starting from other datasets [START_REF] Allix | AndroZoo: collecting millions of Android apps for the research community[END_REF]. While finding information about new apps from the store becomes more difficult over time since repetitions often occur, the number of results produced in the analysis step is constant and depends on the performance of the computer (more than 100 new analyses per day in our case). After comparing the library statistics with the AppBrain [START_REF]App brain[END_REF] list of top development and advertising tools, we noticed that we obtained equivalent results also concerning the order of the elements, especially in the first positions. Consequently, the analyzed apps are relevant for this metric, and therefore also the other measures could be valid for a larger set of apps. In any case, our objective was to build an architecture able to download, analyze, aggregate a large number of apps in a totally automatic way. The produced results by our architecture show how the static analysis is useful for computing general statistics, while the dynamic tests are essentials to find security and privacy vulnerabilities.

Future Work. First, we aim to make APPregator available to the research community by the end of 2020. APPregator can be extended with new modules in order to carry out new types of analysis. Furthermore, APPregator can be extended to retrieve apps from other stores (e.g., APK Mirror, Amazon, Galaxy Store, or F-Droid) and to support iOS apps. The main limitation of our proposal is related to the results obtained during the dynamic analysis, as a full exploration of the app requires to bypass login activities with valid user's credentials. Currently, APPregator is unable to bypass this step. However, we argue that new modules, leveraging machine learning techniques to identify the fields to fill, can overcome this limitation.

Fig. 1 :

 1 Fig. 1: APPregator architecture

Fig. 2 :

 2 Fig. 2: Conceptual Schema

  The Decompiler. It extracts the code and the resources from the app. The code is disassembled from .dex to Smali format. The resources (e.g., the Android manifest and the accessible strings) are stored on the disk. -Manifest Parser. It analyzes the Android manifest and produces a JSON file containing permissions, activities, services, version and name of the app. -String & API Analysis. This module analyzes the code searching for strings.

Fig. 5 :

 5 Fig. 5: Play Store apps that send the Device ID to a server

https://github.com/facundoolano/google-play-scraper

https://www.npmjs.com/package/query-to-mongo

* This work was partially funded by the Horizon 2020 project "Strategic Programs for Advanced Research and Technology in Europe"(SPARTA).