Nicolas Schnepf
email: nicolas.schnepf@inria.fr

Rémi Badonnel
email: remi.badonnel@inria.fr

Abdelkader Lahmadi
email: abdelkader.lahmadi@inria.fr

Stephan Merz
email: stephan.merz@inria.fr

Generation of SDN Policies for Protecting Android Environments based on Automata Learning

Software-defined networking offers new opportunities for protecting end users and their applications. In that context, dedicated chains can be built to combine different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. To configure these security chains, it is important to have an adequate model of the patterns that end user applications exhibit when accessing the network. We propose an automated strategy for learning the networking behavior of end applications using algorithms for generating finite state models. These models can be exploited for inferring SDN policies ensuring that applications respect the observed behavior: such policies can be formally verified and deployed on SDN infrastructures in a dynamic and flexible manner. Our solution is prototypically implemented as a collection of Python scripts that extend our Synaptic verification package. The performance of our strategy is evaluated through extensive experimentations and is compared to the Synoptic and Invarimint automata learning algorithms.

I. INTRODUCTION

The increasing number of connected devices, such as smartphones, smart objects and sensors, is an important factor of Internet growth and dynamics. It also poses new challenges in terms of security management. These devices with restricted capacities generate a larger attack surface. A typical example is the recent attack against the DynDNS service, which exploited a botnet of infected smart objects to perform flooding. Malicious applications targeting these devices are also increasing massively every year. Preventive security methods that consist in analyzing the applications before their publication on markets are of limited effectiveness. For instance, analyses estimate that more than 3 million malwares were published on the official Google application market [START_REF] La Polla | A Survey on Security for Mobile Devices[END_REF], [START_REF] Faruki | Android Security, a Survey of Issues, Malware Penetrations and Defenses[END_REF]. Security mechanisms must be adjusted to threats dynamically. They are also constrained by the resources of devices that are often limited in terms of memory and CPU, making the local deployment of protective mechanisms more challenging.

In the meantime, the development of software-defined networking (SDN) provides new perspectives in terms of security, through an extended programmability of networks [START_REF] Feamster | The Road to SDN, an Intellectual History of Programmable Networks[END_REF], [START_REF] Feamster | Software-Defined Networks: Improving Network Management with SDN[END_REF]. The SDN architecture relies on the decoupling of the data and control planes of networks, the first consisting in programmable switches deployed in the network, and the second consisting in a central component, the controller, responsible for dynamically configuring the switches in response to network events. The interface between these planes is implemented by a dedicated protocol, such as OpenFlow, that can then serve as a support for deploying security rules from the controller to the switches. Programming the controller can benefit from high-level languages, such as Pyretic [START_REF] Foster | Languages for Software-Defined Networks[END_REF], part of the Frenetic family of languages [START_REF] Foster | Frenetic, a Network Programming Language[END_REF]. These languages allow the dynamics of the controller and the forwarding rules of the switches to be described as a Python program, before compiling them into low-level OpenFlow rules.

This programmability brings flexibility to the deployment and adjustment of security mechanisms in the network infrastructures. In this paper we propose an approach based on automata learning to capture the networking behavior of user applications; such models can be used for generating SDN policies in order to protect Android environments. More precisely, we build finite-state models that characterize the behavior of user applications through the analysis of flowbased interaction traces. We aim to infer SDN policies from these models in order to protect end users. Security policies can be expressed using Pyretic rules, for which formal verification methods are available that can help validating network policies. The verification of the control plane can be performed by model checking using the Kinetic extension [START_REF] Kim | Kinetic: Verifiable Dynamic Network Control[END_REF]. In addition, the data plane associated to Pyretic rules can be verified using our Synaptic checker described in [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF].

Our main contributions are: (i) designing an automated technique for learning the behavior of Android applications, (ii) developing practical algorithms for building the automata, (iii) prototyping our method based on Python scripts, and (iv) evaluating its performance through extensive experiments, with a comparison to other automata learning algorithms, namely Synoptic [START_REF] Beschastnikh | Synoptic: Studying logged behavior with inferred models[END_REF] and Invarimint [START_REF] Beschastnikh | Using declarative specification to improve the understanding, extensibility, and comparison of model-inference algorithms[END_REF].

The remainder of this paper is organized as follows. Section II gives an overview of existing related work. Section III describes the envisaged architecture for generating SDN policies and our algorithms for building finite state models. Section IV compares performance results obtained with different automata learning methods. Section V concludes and points out future research perspectives.

II. RELATED WORK

The widespread presence of malware applications on the Google market store has spurred research on the validation of Android applications. Asavoae et al. describe techniques for detecting collusion of Android malware applications based on their permissions [START_REF] Asavoae | Towards automated android app collusion detection[END_REF], but do not address the detection of attacks from a networking perspective. Similarly, Zhang et al. rely on the Android permissions for automatically generating security centric descriptions of applications [START_REF] Zhang | Towards automatic generation of security centric descriptions for android apps[END_REF], but also do not consider the validation of networking aspects. Mariconti et al. detect malware by building Markov models of the applications, but this approach requires downloading and executing the byte code of the application [START_REF] Mariconti | Mamadroid: Detecting android malware by building markov chains of behavioral models[END_REF]. Kim et al. mine the network protocols of an application from its executable, but the deployment of this approach is intractable in SDN networks [START_REF] Kim | Enabling automatic protocol behavior analysis for android applications[END_REF]. Finally, Xia et al. audit Android applications at runtime [START_REF] Xia | Effective real-time android application auditing[END_REF], and Ren et al. propose an approach for discovering personal data in the network traffic of an application [START_REF] Ren | Recon: Revealing and controlling privacy leaks in mobile network traffic[END_REF]; however, these approaches do not include automatic adjustments or the verification of network policies.

In our previous paper [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF] we introduce the Synaptic checker for the verification of both control and data planes of a software-defined network policy. This checker relies on the Pyretic programming language [START_REF] Foster | Languages for Software-Defined Networks[END_REF], part of the Frenetic family of languages for programming SDN controllers [START_REF] Foster | Frenetic, a Network Programming Language[END_REF]: Pyretic is implemented as a domain-specific language embedded in Python for the specification of chains of rules at an abstract level, from which low-level OpenFlow rules can be compiled. Pyretic is complemented by an extension, called Kinetic, for describing control plane policies; Kinetic also offers formal verification techniques based on model checking [START_REF] Kim | Kinetic: Verifiable Dynamic Network Control[END_REF]. Synaptic extends this formalism for verifying the correctness of both the control and data planes of Pyretic policies, before their deployment in the network.

To automate the protection of Android applications, we suggest here to complement our Synaptic checker by automata learning methods for obtaining a representation of the network behavior of Android applications. Automata learning methods can be classified into several categories: purely algorithmic, purely statistical or a mix of both. Among the purely algorithmic methods, the reference k-tails algorithm [START_REF] Biermann | On the synthesis of finite-state machines from samples of their behavior[END_REF] can mine exact, but potentially complicated, Markov models of applications. This algorithm underlies the Synoptic 1 tool [START_REF] Beschastnikh | Synoptic: Studying logged behavior with inferred models[END_REF] that can learn Markov models of processes. The Invarimint tool [START_REF] Kang | A Verification Method of SDN Firewall Applications[END_REF] is also based on k-tails but produces simpler, socalled declarative automata, without probabilities on the edges. In the field of statistical automata learning algorithms, there is the approach proposed by Carrasco [START_REF] Carrasco | Learning stochastic regular grammars by means of a state merging method[END_REF] for inferring grammar of languages by stochastic methods used in [START_REF] Cook | Discovering models of software processes from event-based data[END_REF] for learning inexact automata from logs of behaviors. Das and Mozer [START_REF] Das | A unified gradient-descent/clustering architecture for finite state machine induction[END_REF] suggest relying on neural nets for learning models of applications; this approach requires a learning session before producing the model of a system while exact approaches can be directly applied on logs without training phase.

III. AUTOMATA LEARNING STRATEGY FOR SUPPORTING ANDROID APPLICATION SECURITY

We propose in this paper an approach for learning interaction models of applications for protecting Android environments. More precisely, this approach consists in automatically profiling applications based on automata learning methods applied to network logs. We mainly focus on the network 1 Synoptic is an automata miner, while Synaptic is a checker. traces characterizing the behavior of applications, in contrast to Android permissions that focus on the services that applications can access directly on the smart device. One question to consider is whether application models should be built from packets or flows: a packet is the basic unit of data exchanged by applications during a communication whereas a flow is an aggregated and unidirectional collection of packets that can be used instead of packets for representing the network behavior of applications. We decided to build our models from flow traces, following Sperotto [START_REF] Sperotto | Flow-based intrusion detection[END_REF] who argues that using flows instead of packets presents several advantages from a security perspective. First of all, analyzing flows is faster than analyzing packets because we are interested in collections of packets sharing the same IP addresses and port numbers. A second advantage of this approach is higher confidentiality for end users: whereas an analysis at the level of packets can observe the data exchanged during a communication, the latter is hidden in the analysis of flows: one can only observe aggregate information such as the numbers of packets and of bytes but not what is transmitted over the network. We are mainly interested in the remote servers the application is communicating with, focusing on identifying communications that may present a risk for the safety of a smart environment.

The communication pattern of an application can conveniently be represented as a finite state automaton; in particular we consider hidden Markov models of applications because this representation captures interesting properties in terms of network security [START_REF] Sperotto | Flow-based intrusion detection[END_REF]. In addition to probabilistic aspects we are also interested in having quantitative information about the numbers of bytes and of packets sent or received by applications during their communications in order to capture abnormal behaviors and to adjust the chains accordingly when observing such events at the network level.

A. Underlying architecture

The overall architecture that supports our technique for protecting devices and applications in an SDN environment is depicted in Figure 1. It relies on a security manager that is responsible for the orchestration of security chains on top of an SDN controller. Our approach is organized into four major phases: netflow acquisition, netflow aggregation and automata learning. The acquisition probe is deployed directly on the smart device for collecting application flows. Using a dedicated protocol, these traces are sent to the security manager. After an aggregation phase (realized by an abstraction module), a process miner is applied during the automata learning phase for building a finite state machine that captures the communication behavior of the application.

B. NetFlow acquisition

The first phase relates to the acquisition of flow traces of applications that are collected on the end device. In the context of protecting Android devices, this acquisition is supported by Flowoid [START_REF] Lahmadi | A platform for the analysis and visualization of network flow data of android environments[END_REF], a probe developed in our research group. Deployed on Android devices, Flowoid collects traces of the network behavior of running applications and computes several statistics: the transmission of these traces to the security manager is based on NetFlow, a protocol specially designed for the acquisition of network flows over the network. In terms of information, Flowoid collects for each flow the IP addresses of the source and of the destination and the corresponding port numbers: it also provides information on the network protocol (TCP or UDP), a timestamp labeling the communication, its length, and the numbers of bytes and of packets transmitted. In order to build a model representing the behavior of applications, the fields that characterize the communications of an application must be identified: actually the IP source and its corresponding port number are not informative because they are bound to the smart device. The information about the network protocol and the numbers of bytes and packets are interesting but not sufficient for building a representative model of the communications of an application. The most relevant fields are the IP destination that defines the remote server that provides the service and the corresponding port number that defines this service. We will therefore initially consider only these fields for building the transitions of our model. The other informations are aggregated in order to infer properties of the traffic, as we describe next.

C. NetFlow aggregation

We rely on flows collected by Flowoid for inferring our application models: however, we need to define a way of aggregating these flows, in order to infer interesting properties on the traffic. If we directly use the IP addresses and port numbers contained in the logs, we obtain very precise application models. The problem of this approach is that whenever the IP address of a service changes, our models do not hold anymore. We therefore need to consider the traffic at a higher level of abstraction. An idea for solving this problem is to consider the type of service the application is communicating with, for instance google or amazon. In other words, we are interested in knowing the owner of the IP addresses contained in a log. This information can be collected by using whois requests: this command returns information about the organization owning the IP address in the field orgname but it can also return a more precise information, viz. the name of the network in the field netname. When whois returns both a netname and an orgname we have to decide which information to use for building the automaton: using only netnames could again result in a too precise automaton containing traces of networks appearing only once; using only orgnames could result in automata integrating many flows aggregated under very general services such as RIPE Network Coordination Centre. As a compromise between these two extremes, we decided to set a threshold n: if a netname appears more than n times in the overall log it is considered as significant and it is integrated into the model of the application; otherwise we integrate the orgname. We thereby limit the influence of netnames appearing only once or twice in the input log by setting a high value of n; conversely, we can avoid a too strong presence of generic orgnames by setting a lower value of n. We complement this strategy for aggregating IP addresses by another one for handling port numbers: although most Android applications only use HTTP or HTTPS ports and do not require such an aggregation strategy, some applications present a high disparity of port numbers that should be aggregated. In that case we can use the most frequent prefixes of port numbers in order to aggregate flows: this approach allows us to group together flows that have the same port number; moreover, when an application frequently communicates on a given port range we can aggregate these flows in order to get a more compact representation of the traffic of applications. The idea is again to only consider prefixes that appear more often than a certain threshold in order to limit the influence of port numbers appearing only once or twice in the flow.

D. Automata learning

The next phase consists in automata learning. The objective is to learn a Markovian model capturing the network behavior of an application. This automaton is implemented by two tables: States associates flows to their number of instances, while Transitions associates pairs of flows to their probability of succession. The arguments of our algorithm (see Algorithm 1) are the list noted Flows of extended flows computed by our aggregation module and the size N of this list; the local variables that we use are flow containing the orgname and the port number associated to a flow and transition containing two consecutive flows. Each state of the automaton is a class of flows defined by the name of the destination organization and the corresponding port number. Moreover, states can be enriched by auxiliary information in order to represent more details about the corresponding traffic. Concretely, we compute the following standard network information for each state of our automata:

• the maximum numbers of bytes and of packets sent during a flow; • the average length of the set of flows;

• the rates of TCP/UDP traffic.

As an example, we consider the logs of 275 flows generated by the pokemongo application: these traces contain communications of the application with 24 different hosts on the ports 80 and 443. Our aggregation strategy groups the 24 IP addresses of these logs under 7 different orgnames: based on this information we run our automata learning algorithm and obtain the automaton of Figure 3. This automaton contains 10 states and 33 transitions; to give a comparison, the automata mined directly from the IP addresses contains 26 states and 77 transitions. We also applied Invarimint and Synoptic to this example: Invarimint produces an automaton with 12 states and 32 transitions without probabilities and Synoptic produces an automaton with 28 states and 65 transitions.

IV. PERFORMANCE EVALUATION

We evaluated the performance of our prototype through several experiments. In particular, we wanted to compare the performances obtained with different methods of automata learning. The experimental setup was based on a MacBook Air laptop computer with an Intel Core i5 (1.7 GHz) processor and 4Gb of RAM. We considered the three following process/automata miners: Synoptic, its declarative version implemented in Invarimint, and finally our own generation method described in the previous section. For these experiments we used a set of 10 log files, described in Figure 2. From these log files we built the automata with the three methods that we selected, noting that we were not able to get the automata for the applications lequipe, skype and viber with Synoptic because of excessive memory consumption.

In order to compare the automata that we obtained we defined the following evaluation criteria:

• the simplicity of the resulting automata, expressed in terms of numbers of both states and transitions; • the precision of the model, expressed as the number of flows of other applications rejected by the automata.

A. Simplicity of automata

We only considered exact generation methods in this evaluation: the automata produced by such algorithms are guaranteed to accept all the logs used for learning. However, such automata can be quite complicated to read and to interpret, and their size has an influence on the number of SDN rules that are generated. We therefore chose their simplicity as an evaluation criterion, measured as the numbers of states and of transitions of an automaton. Because these metrics vary with both the method of generation and with the level of abstraction of the input logs, we compared the different methods by applying them on logs aggregated with different values of the threshold parameter n. The results of these experiments are presented in Figure 4.

Without aggregating IP addresses our approach produces automata with in average 105.2 states and 322.8 transitions for this data set. The automata produced by Invarimint and by our approach are of similar complexity on average, Invarimint produces automata that have two more states and one transition less than our approach. In contrast, Synoptic produces automata with in average 11.2 states and 29 transitions more than our approach. Indeed, the automata generated by Synoptic are always the most complex ones. Considering the performances of the aggregation strategy, the best improvement is obtained when replacing the IP addresses by their corresponding orgnames; concerning the influence of the value of n, the strongest impact is observed when aggregating the less frequent netnames, meaning that limiting the influence of values with low frequency of appearance is the most important factor for choosing the threshold value n.

For completing these results we also compared the automata sizes for our approach and for Invarimint when applying the port abstraction strategy on the logs of the three most complex applications: lequipe, skype and viber. During these experiments we considered the influence of the threshold on port numbers varying from 0 to 10. These results are described in Figure 5.

The high number of states and of transitions of these automata is caused by the complexity of the applications. The complexity of the automata decreases most significantly for threshold values between 0 and 3. This can be explained by the peer-to-peer profile of the considered applications that causes many port numbers to appear only one or two times. Port numbers appearing more than 4 or 5 times can be considered as being representative of the behavior of the application, nevertheless, for logs where such values would constitute an important part of the traffic it could be interesting to consider higher threshold values.

B. Precision of automata

The next criterion that we considered is the precision of the automata: given an application, we define the precision of its automaton as the percentage of logs of other applications that it rejects, in other words as the rate of foreign traffic rejected by the automaton. Having a high precision is important for ensuring that the traffic of an application will not be blocked by other automata. On the other hand, if two automata match the same traffic, their respective sets of rules could be joined into a set that is useful for both applications. We evaluated the precision of the automata generated by each method for the different applications, when using the orgname-based abstraction: these results are depicted in Figure 6. One can observe that the precision depends more on the type of application that is considered than on the method used for generating the automata. Moreover, for some applications, using the orgnames for computing the automata is sufficient for having a satisfactory precision. However for others, such as lequipe, precision is unsatisfactory. This difference is due to the fact that some applications only contact private services such as disney world wide service whereas others contact many public services such as Amazon or Google. For completing these results we ran another set of experiments with automata generated from the IP addresses of the remote hosts that the application contacts: these results are presented in Figure 7. Again, the precision depends more on the type of application that is considered than on the method used for generating the automata. We can see that the precision of the automata is better without abstracting the logs 2 : this fact confirms our strategy of using the IP addresses for matching the traffic at the network level. However, the strong overlaps observed when using the orgnames for generating the automata could be exploited for identifying sections of application traffic that can be protected by the same types of chains, so the 2 Observe the different scale of the ordinate axis in Figure 7. information on the IP addresses would be used for configuring these chains.

V. CONCLUSIONS AND FUTURE WORK

We propose in this paper a technique for learning the behavior of Android applications, as a starting point for generating SDN policies for protecting them. Our solution collects traces of NetFlow records of their applications, aggregates them, and finally builds finite-state models. We have described the architecture supporting our approach, as well as the interactions among its different components. We have designed and implemented aggregation and automata learning algorithms that allow precise and generic models of applications to be built, with the aim of using these models for configuring chains of security functions specified in the Pyretic language and verified with our Synaptic checker. We have developed a prototype of our solution implementing these algorithms, and evaluated its performances through a series of experiments based on the backend process miners Synoptic and Invarimint, in addition to our own algorithm. The experiments showed the benefits and limits of these methods in terms of simplicity, precision, genericity, and expressivity, while varying the level of aggregation of the input flow traces.

As future perspectives, we work on the generation or selection of chains of security functions, based on the inferred finite-state automata. We are also interested in further optimizing the formal models that we generate, based on the nature of the properties to ensure. Finally, we want to investigate further the integration of this automata learning method into the context of an automated management framework for security chains with our Synaptic checker.

Figure 1 .

 1 Figure 1. Overview of the proposed architecture for securing applications.

Figure 3 .

 3 Figure 3. Automaton describing the behavior of the pokemongo application.

Figure 4 .

 4 Figure 4. Simplicity of automata generated with the considered methods.

Figure 5 .

 5 Figure 5. Impact of port abstraction on the sizes of automata.

Figure 6 .

 6 Figure 6. Precision of orgname-based automata.

Figure 7 .

 7 Figure 7. Precision of automata based on IP addresses.


Nicolas Schnepf

Rémi Badonnel

Abdelkader Lahmadi

Stephan Merz

Synaptic: a Formal Checker for SDN-based Security Policies

Software-defined networking offers new opportunities for protecting end users by designing dynamic security policies. In particular, security chains can be built by combining security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. The configuration of these security functions and their associated policies is based on behavioural models of end-user applications when accessing the network. In this demo, we present our tool Synaptic, a SDN-based framework intended for the formal verification of security policies as well as for automatically generating such policies based on automata learning methods applied on NetFlow records of end-user applications collected at the device level.

I. BACKGROUND

The programmability that characterizes SDN [START_REF] Feamster | Software-Defined Networks: Improving Network Management with SDN[END_REF] simplifies the specification of network policies by decoupling the control and the data planes. Based on this paradigm, it is possible to enforce chains of security functions, such as described in [START_REF] Hurel | Towards Cloud Based Compositions of Security Functions for Mobile Devices[END_REF] for protecting end users. Such chains are composed of security functions, such as intrusion detection systems, firewalls or data leakage prevention mechanisms, combined in sequence or in parallel. However, due to their complexity and dynamics, these chains of security functions may give rise to misconfigurations in the network. Formal methods provide techniques that can help the validation of security chains before they are deployed. Formal verification of SDN policies is an important topic in the literature [START_REF] Al-Shaer | FlowChecker, Configuration Analysis and Verification of Federated OpenFlow Infrastructures[END_REF], [START_REF] Ball | Vericon: Towards Verifying Controller Programs in Software-Defined Networks[END_REF]. Current approaches focus mostly on the verification of the data plane, and miss aspects related to the control plane. Nevertheless, the Pyretic language [START_REF] Foster | Languages for Software-Defined Networks[END_REF], part of the Frenetic framework [START_REF] Foster | Frenetic, a Network Programming Language[END_REF], provides an intuitive way for specifying SDN security policies, and verification facilities are provided for the control plane, through its Kinetic extension [START_REF] Kim | Kinetic: Verifiable Dynamic Network Control[END_REF].

II. SYNAPTIC: GENERATING AND CHECKING POLICIES

Synaptic combines two functionalities. First, it provides techniques for verifying both the control and data planes related to security chains, as described in [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF]. These chains correspond to security policies combining security functions using software-defined networking. Second, it includes a component for profiling applications based on logs of their behavior, and for configuring SDN security policies from the inferred profiles. We developed the prototype using Python 2.7, as an extension of Pyretic and Kinetic. The interactions among the different components of Synaptic for the verification of a policy is depicted in Fig. 1. The input received by our checker is a security policy specified in Pyretic together with several logical properties. This input is then translated into either a SMTlib model that can be verified by SMT solving, or into a nuXmv model that can be verified by model checking. If the behavior of this policy is controlled by a Kinetic automaton, Synaptic will use the verification procedure implemented by this framework, then verify the correctness of each data plane policy used by this control automaton. Otherwise, Synaptic will directly verify the data plane policy that it receives. Concerning the possibilities in terms of formal verification, we integrated the following SMT solvers: CVC4 [START_REF] Barrett | CVC4[END_REF] v1.4 and veriT [START_REF] Bouton | veriT: An Open, Trustable and Efficient SMT-Solver[END_REF] v201506. We also included the nuXmv [START_REF] Cavada | The nuXmv symbolic model checker[END_REF] v1.0.1 model checker, as a backend of our tool. While the checker accepts arbitrary (such as hand-written) security policies expressed in Pyretic, we also support their automatic generation based on automata learning [START_REF] Schnepf | Towards generation of sdn policies for protecting android environments based on automata learning[END_REF]. Synaptic includes a component for learning a Markovian model that captures the networking behavior of an application and for deriving a corresponding security policy in Pyretic. This generation process is divided into four phases depicted in Fig. 2: NetFlow acquisition, NetFlow aggregation, automata learning and rule generation. NetFlow records are collected directly on the end-user device by a dedicated probe, such as Flowoid [START_REF] Lahmadi | A platform for the analysis and visualization of network flow data of android environments[END_REF] developed in our research team or from available datasets. Collected NetFlows are transmitted to the aggregation module deployed in the cloud: it will aggregate NetFlows based on the responses of whois requests for the IP addresses and on the ranges of ports contained in the traces. From the aggregated NetFlows, the automaton learning module will infer a Markov chain summarizing the behavior of the application: to do so, we create a state for each pair of netname/port range and we compute the probability of each outgoing transition. Finally, this automaton is provided to the rule generation module that will generate a Kinetic automaton matching the behavior of the application.

III. THE DEMONSTRATION

In this demo, we will present both the verification and the process learning features of Synaptic. The verification feature will be illustrated with several examples, including the verification of a Kinetic based control automaton or the verification of a stateless firewall. For each of these examples, we will show (1) the policy that input to Synaptic, (2) the properties to be verified, and (3) the verification options offered by Synaptic. We will exhibit correct and erroneous policies, show the corresponding responses of our checker, and provide timing information. For the automata learning feature, we collected traces of different applications. For each of them, we will show how Synaptic can be used for learning a probabilistic model of their networking behavior, and how this can be used to synthesize and then verify a security chain. Through these different examples, we will show how the complexity of NetFlow records influences the automata produced by Synaptic and the response time of the subsequent verification procedure. We will also show how to configure the aggregation module in order to reduce this complexity as much as possible. Finally, we will illustrate how automata can be stored in external files in order to be processed by other services: an example of such an automaton appears in Fig. 3.

Figure 1 .

 1 Figure 1. The verification steps of a SDN-based security policy.

Figure 2 .

 2 Figure 2. Generation and verification of SDN-based security policies based on application profiling.

Figure 3 .

 3 Figure 3. Automaton describing the behavior of the Dropbox application.


Nicolas Schnepf
email: nicolas.schnepf@inria.fr

Rémi Badonnel
email: badonnel@inria.fr

Abdelkader Lahmadi
email: lahmadi@inria.fr

Stephan Merz
email: stephan.merz@inria.fr

Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks

Keywords: Security Management, Software-Defined Networking, Android, Rule-Based Programming

Software-defined networks (SDN) offer a high degree of programmability for handling and forwarding packets. In particular, they allow network administrators to combine different security functions, such as firewalls, intrusion detection systems, and external services, into security chains designed to prevent or mitigate attacks against end user applications. These chains can benefit from formal techniques for their automated construction and verification. We propose in this paper a rulebased system for automating the composition and configuration of such chains for Android applications. Given the network characterization of an application and the set of permissions it requires, our rules construct an abstract representation of a custom security chain. This representation is then translated into a concrete implementation of the chain in Pyretic, a domain-specific language for programming SDN controllers. We prove that the chains produced by our rules satisfy a number of correctness properties such as the absence of black holes or loops, and shadowing freedom, and that they are coherent with the underlying security policy.

Introduction

Software Defined Networking (SDN) is a recent paradigm in the field of network management and security that promises to improve network programability by decoupling the data and control planes. In this context, the data plane consists in virtual switches and equipment responsible for forwarding traffic across the network, whereas the control plane consists in a single or multiple controllers, responsible for dynamically adjusting the configuration of the data plane in response to network events. The communication between the two planes is supported by a dedicated protocol, typically OpenFlow. SDN is oftenly used in conjunction with Network Function Virtualization (NFV) for supporting the automated deployment of more advanced security functions running in virtual machines in addition to virtual switches.

Based on these new networking paradigms, researchers proposed the concept of chains of security functions for protecting end user applications against attacks. These chains are composed of different security mechanisms such as intrusion detection systems (IDS) or firewalls in cloud infrastructures for the protection of end users. The programmability introduced by software defined networks helps greatly for automating the configuration, adjustment, and deployment of chains of security functions. Programming SDN controllers is made simpler by the introduction of domain-specific programming languages such as Pyretic designed for implementing chains of security functions at a high level of abstraction before compiling them into low-level OpenFlow configuration rules. Nevertheless, the validation of chains of security functions remains non-trivial: the complexity of their internal security functions makes it incredibly easy to introduce misconfigurations and security holes that can then be exploited by attackers targeting these networks and their users.

There exist several approaches for formally verifying chains of security functions a posteriori (cf. section 2). In this paper we propose an inference system based on Horn clauses for synthesizing chains of security functions in an automated manner, ensuring that the generated chains satisfy elementary correctness requirements. We specifically target the protection of network traffic generated by Android applications, taking into account security requirements derived from the observed networking behavior of an application and the set of operatingsystem level requirements that the application requires. We rely on our previous work [START_REF] Schnepf | Towards generation of SDN policies for protecting android environments based on automata learning[END_REF] for characterizing the networking behavior by learning a finite Markov chain that represents the network flows observed by a dedicated network probe. Using an inference system in order to construct a high-level representation of the security chain, we obtain a declarative description of the generation process that simplifies reasoning about the properties it guarantees, such as the consistency of the deployed security rules and the absence of loops.

Our contributions are threefold: (i) we design a system of Horn clauses for the inference of chains of security functions that ensure certain correctness properties and that can be translated directly into Pyretic implementations, (ii) we propose a new representation of security requirements of Android end users, (iii) we have implemented a prototype of our method in Prolog.

The remainder of this paper is organized as follows. Section 2 gives an overview of existing related work. Section 3 introduces background on network security. Section 4 describes the system of Horn clauses used for synthesizing SDN based chains of security functions. Section 5 discusses the correctness properties that are guaranteed by our solution. Section 6 concludes and points out future research perspectives.

Related work

Much work has been directed towards the detection of attacks: most approaches rely on packet analysis for detecting attacks [START_REF] Ain | Rank correlation for low-rate ddos attack detection: An empirical evaluation[END_REF][START_REF] Ensafi | Idle port scanning and noninterference analysis of network protocol stacks using model checking[END_REF][START_REF] Chen | Detecting early worm propagation through packet matching[END_REF]: these methods provide good accuracy; nevertheless the increasing mass of traffic to analyze in modern network require more efficient detection methods. In her PhD thesis, Anna Sperotto proposed to base the detection of attack on flow records instead of packet traces [START_REF] Sperotto | Flow-based intrusion detection[END_REF]: the objective of her work is to configure IDS depending on observed traces of attacks. Nevertheless, she does not consider data transmitted during exchanges and does not explore the possibility of deploying other security functions than IDS. Comparing detection methods requires dedicated datasets such as the CTU 13 [START_REF] García | An empirical comparison of botnet detection methods[END_REF] which contains botnet traces, but further datasets are necessary in order to capture other types of attacks such as DOS, port scanning or worm attacks.

New perspectives for the protection of end users are introduced by the SDN paradigm: one possible approach consists in composing different security functions into chains [START_REF] Hurel | Towards Cloud Based Compositions of Security Functions for Mobile Devices[END_REF][START_REF] Hurel | Behavioral and Dynamic Security Functions Chaining for Android Devices[END_REF]. There exists various work in the literature that addresses the formal verification of such chains. For instance, Vericon [START_REF] Ball | Vericon: Towards Verifying Controller Programs in Software-Defined Networks[END_REF] is a framework in which properties to be guaranteed by network policies can be expressed and verified. Al-Shaer and Hamed [START_REF] Al-Shaer | Discovery of policy anomalies in distributed firewalls[END_REF] propose another approach for the discovery of anomalies in distributed firewalls, targeting in particular contradictions in large firewall policies. Those approaches focus on the verification of the data plane of chains of security functions but do not cover the validation of aspects related to the control plane. In addition, while these approaches are useful for validating a posteriori the correctness of policies w.r.t. pre-established criteria, they do not generate a policy according to these criteria, and they may miss configuration errors that are not covered by the specified properties.

We previously [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF] introduced the Synaptic checker for the verification of both control and data plane properties of an SDN policy. This checker relies on the Pyretic programming language [START_REF] Foster | Languages for Software-Defined Networks[END_REF], part of the Frenetic family of languages for programming SDN controllers [START_REF] Foster | Frenetic, a Network Programming Language[END_REF]. Pyretic is implemented as a domain-specific language embedded in Python for describing chains of rules at a level of abstraction well above that of actual SDN protocols, but from which OpenFlow rules can be compiled. Pyretic is complemented by an extension, called Kinetic, for describing control plane policies; Kinetic also offers formal verification techniques based on model checking [START_REF] Kim | Kinetic: Verifiable Dynamic Network Control[END_REF]. Synaptic extends this formalism for verifying the correctness of both the control and data planes of Pyretic policies, before their deployment in the network. We also proposed [START_REF] Schnepf | Towards generation of SDN policies for protecting android environments based on automata learning[END_REF] an extension of the Synaptic checker with features for automatically learning network behaviors, represented as a Markov chain, of Android applications using their network flow traces. Our present paper is based on this technique and exploits it for the automatic generation of SDN policies satisfying the security requirements corresponding to such an application.

Most methods for the validation of chains of security functions consider their correctness a posteriori, using techniques such as model checking [START_REF] Clarke | The birth of model checking[END_REF][START_REF] Forejt | Automated verification techniques for probabilistic systems[END_REF] or SMT solving [START_REF] Biere | Handbook of satisfiability[END_REF]. In this paper, we suggest a declarative technique for the automatic synthesis of such chains, expressed at a high level of abstraction. We express our technique in terms of Horn clauses and have prototypically implemented it in Prolog. This representation makes it easy to modify the rules in order to take into account varying end-user requirements, rather than hard-coded policies defined by operators. It also helps for formally establishing a priori certain properties that the generated chains ensure.

Background on network security

We introduce some background regarding network security, with respect to the attacks we consider, network programmability, and Android environments.

Network flows and considered attacks

Our work is centered on the inference of chains of security functions based on a characterization of end-user applications in terms of network flows. According to RFC 5101 [START_REF] Claise | Specification of the IP Flow Information Export (IPFIX) Protocol for the Exchange of IP Traffic Flow Information[END_REF], network flows can be defined as "collections of IP packets passing through an observation point in the network during a certain interval". They are generally described by different properties such as IP version, source and destination IP addresses (srcaddr and dstaddr ), source and destination ports (srcport and dstport), network protocol (protocol ), and the numbers of packets and bytes (packets and bytes). In our context, they are collected directly on end-user devices [START_REF] Lahmadi | A platform for the analysis and visualization of network flow data of android environments[END_REF], and are extended with a timestamp (timestamp) and the name of the source application (appname). We furthermore complement this information with the name of the organization (orgname) responsible for the network that contains the destination IP address. As highlighted in [START_REF] Sperotto | Flow-based intrusion detection[END_REF], network flows are widely used for the detection of different categories of attacks, especially denial of service, port scanning, worms and botnets.

A denial of service (DoS) attack is characterized by "one or more machines targeting a victim and attempting to prevent the victim from doing useful work" [START_REF] Handley | Internet Architecture Board: Internet Denial-of-Service Considerations[END_REF]. In our context, we will consider DoS attacks that are observable from a networking point of view, such as SYN flood attacks where a high number of SYN packets are sent to the same host in order to overload the TCP stack with open connections that will never been closed. In a port scanning attack, an application initiates connections with a wide range of ports of a machine (or several machines) in order to detect which ports are open. We will consider port scanning techniques such as those generated by the nmap port scanner, available on standard Linux platforms. A worm is a program that can run independently, will consume the resources of its host in order to maintain itself, and can propagate a complete working version of itself to other machines [START_REF] Malkin | Internet Users' Glossary[END_REF]. Worms replicate by exploiting the vulnerabilities of applications and operating systems or by social engineering methods. We will consider worms that scan a certain port on many different machines in order to exploit a specific vulnerability on operating systems. A (potentially) malicious bot is a program that is installed on a system in order to enable that system to automatically (or semi-automatically) perform a task (or a set of tasks) typically under the command and control of a remote administrator, called "bot master" [START_REF] Barthel | Routing Metrics Used for Path Calculation in Low-Power and Lossy Networks[END_REF]. These bots can be detected based on the high volume of traffic they exchange with their controller or possibly by the use of network protocols that are not commonly observed in a given context.

Network programmability with Pyretic

Pyretic is a domain-specific programming language embedded in Python for the configuration of SDN controllers. It is based on fundamental blocks (called policies) that can be combined for generating more complex policies. In the remainder of this paper we will consider the following primitive policies and composition operators:

identity: forward all packets; drop: block all packets; match(x 1 = y 1 , . . . , x n = y n ): forward those packets whose header fields x i contain the values y i ; modify(x 1 = y 1 , . . . , x n = y n ): forward all packets but modifies their header fields x i to the values y i ; count packets(x 1 = y 1 , . . . , x n = y n ): count the number of packets whose header fields x i contain the values y i ; -LimitFilters(k, x 1 = y 1 , . . . , x n = y n ): forward a maximum of k packets whose header fields x i contain the values y i ; -RegexpQuery(pattern): forward packets whose payload matches the given pattern (a regular expression); sequential (p 1 , . . . , p n ): compose the policies {p 1 , . . . , p n } in sequence, also written p 1 p 2 for n = 2; parallel (p 1 , . . . , p n ): compose the policies {p 1 , . . . , p n } in parallel, also written p 1 + p 2 for n = 2; negate(p): forward packets that are blocked by the policy p, and block those that are forwarded by p, also written ∼ p.

This language and its primitives will serve as a support for building and composing security functions for software-defined networks.

Focus on Android environments

We will target the protection of Android devices and their applications. In particular, we will rely on the Flowoid probe [START_REF] Lahmadi | A platform for the analysis and visualization of network flow data of android environments[END_REF] dedicated to Android devices and will use it for exporting network flow records of applications running on these devices. Given its position as the market-leading operating system for smart devices and the limited effectiveness of preventive methods for proactively detecting malware applications, Android is particularly exposed to security attacks. For instance in 2016, Kaspersky Lab identified more than 3.5 million malware apps on the Google market store. In addition to the network flows previously mentioned, we will take into account the permissions that an application holds for accessing resources. An Android application must explicitly state the permissions it requires in its manifest file, and the security system of Android distinguishes between normal and (potentially) dangerous permissions. The former represents accesses to resources considered as non-critical, and they are automatically granted when requested. Dangerous permissions provide access to critical information such as user contacts, and they must be granted manually, when the application is installed. An application holding such a permission could use it to leak sensitive data to remote malicious servers. Therefore, the security chains that we generate include specific checks to prevent such attacks from occurring.

Automated network profiling of Android applications

We proposed in [START_REF] Schnepf | Towards generation of SDN policies for protecting android environments based on automata learning[END_REF] an algorithm for automatically learning a Markov model of the networking behavior of Android applications: this model is based on trace logs of the flows generated by an application, collected directly on the device by using a dedicated agent [START_REF] Lahmadi | A platform for the analysis and visualization of network flow data of android environments[END_REF] that can associate flows with applications depending on the name of the package producer. These flow records are then transmitted to a centralized platform by using the NetFlow protocol in order to learn the communication pattern of the application: the first stage of our learning algorithm consists in aggregating destination IP addresses of flows depending on common owning organizations. This information is obtained in the result of whois requests in the field called orgname or possibly in the field netname. Once flows have been completed by this information we build our Markov model of the application in the following manner: states are computed as collections of flows sharing the same orgname / netname; transitions are computed depending on the successions of orgname / netname in the input log; finally, probabilities are computed depending on the number of flow records in the input state and on the number of occurrences of the transition in the input log.

Automated synthesis of chains of security functions

We propose in this paper a strategy based on rule-based programming for the automated inference of chains of security functions, based on a characterization of an Android application in terms of its network behavior and the permissions it holds. Our approach consists in classifying the network traffic generated by an application, then to use logic programming for deriving the functional specification of the security chain to be deployed, and finally to generate an instance of such a chain using the Pyretic language for programming SDN controllers. Our work is presented in the context of Android protection, although it can be extended to any systems using similar permissions for protecting user data. Similarly, it is possible to consider other formats or implementations for the generation of chains of security functions, for instance by exploiting Network Function Virtualization (NFV) facilities.

Representing flows, traces, and security functions

Recall that flows are collections of packets sharing certain properties. We summarize a flow in a record that contains the key attributes of a flow. In the following, N and R + denote the sets of natural and non-negative real numbers, Addr = {0, 1} 32 and Port = {1, . . . , 65535} the sets of IP addresses and ports, Prot = {TCP , UDP , ARP , ICMP , . . .} the set of networking protocols and String the set of (ASCII) character strings. Definition 1. A flow f is a record that contains the following attributes and maps them to values in the corresponding domains:

f.timestamp ∈ R + f.srcaddr ∈ Addr f.dstaddr ∈ Addr f.srcport ∈ Port f.dstport ∈ Port f.bytes ∈ N f.packets ∈ N f.protocol ∈ Prot f.appname ∈ String f.orgname ∈ String
A flow trace is a sequence of flows such that time stamps are strictly increasing along the sequence. By abuse of notation, we will write f ∈ t to indicate that flow f appears as an element of the sequence t. Given two traces t 1 and t 2 , their merge t 1 ⊕ t 2 corresponds to the unique trace formed by the elements of t 1 and t 2 in increasing order of time stamps, with the proviso that whenever t 1 and t 2 contain flows f 1 and f 2 with f 1 .timestamp = f 2 .timestamp, then f 1 appears in t 1 ⊕ t 2 while f 2 is dropped. For an application app we will note t app a flow trace such that f.appname = app for all flows f in the trace, and P app the list of permissions it requests. We let D stand for the set of Android permissions qualified as dangerous.

Our approach aims at constructing a chain of security functions for protecting a specific application. Security functions transform network traffic, i.e. sequences of packets. Packets contain header fields similar to flows, except those that contain aggregate information such as packets and bytes, but they also contain a packet payload (field payload ) that represents the actual information transmitted in a packet. We overload the merge operation ⊕ to apply to sequences of packets as well as to flow traces.

Security functions are built by combining in parallel basic building blocks, called security rules, and they in turn give rise to chains by applying parallel or sequential composition. Rules, security functions, and chains transform flow traces, in particular through blocking certain traffic and modifying the values of certain header fields. Definition 2. A security function s is a function from traffic (i.e., a sequence of packets) to traffic. For an integer n ∈ N, the function cut(t, n) returns the prefix of traffic t consisting of at most n packets. Given a predicate pred (p) on packets, we define the function restrict(t, pred ) that returns the subsequence of traffic t consisting of those packets satisfying pred .

Security functions can be composed in sequence (• ) or in parallel (• + ) where

(s 1 • s 2 )(t) = s 2 (s 1 (t)) (s 1 • + s 2 )(t) = s 1 (t) ⊕ s 2 (t)
and these operators generalize to n-ary compositions and + .

Classifying flows for learning security requirements

Our first objective is to classify the flows observed for an application according to the attack types mentioned in section 3.1. As described in our previous work [START_REF] Schnepf | Towards generation of SDN policies for protecting android environments based on automata learning[END_REF], we construct a Markov chain from a trace t app obtained from observing an application. The locations L app of the Markov chain correspond to (not necessarily contiguous) sub-traces of t app consisting of flows with the same orgname attribute. Transitions T app of the Markov chain are triples (l, p, l ) for locations l, l ∈ L app and a probability value p ∈ [0; 1]. Observe that for any flow f ∈ t app , there is a unique location l ∈ L app (corresponding to f.orgname) such that f ∈ l; we denote this location as l f . For example, Fig. 1 depicts the automaton obtained for the application Pokemon Go from a flow trace containing 150 flow records. It represents the connections that the application establishes to addresses associated with different organizations. The analysis of the transition probabilities, and in particular those associated with self-loops, is at the basis of detecting potential attacks such as denial of service, port scanning or worm traffic.

We thus classify flows, and by extension their destination addresses, based on the following metrics defined for a flow trace t of length n > 1:

avg interval (t) = n i=2 t i .timestamp -t i-1 .timestamp n -1 avg size(t) = n i=1 t i .packets n count(x , t) = |{i ∈ 1 .. n : t i .dstaddr = x ∨ t i .dstport = x}| ports(t) = {p ∈ Port : ∃i ∈ 1 .. n : t i .dstport = p} protocols(t) = {p ∈ Prot : ∃i ∈ 1 .. n : t i .protocol = p}
In addition, bgp ranking(ip) denotes a value corresponding to a trust ranking measure of the IP address ip. In practice, this value is obtained by contacting a remote service.

We associate the following thresholds to the above metrics; appropriate values for these thresholds are defined by the network operators and administrators.

attack limit: maximum probability of self looping transitions for considering a location of the automaton as normal; min interval : minimum acceptable interval time between the arrival of packets in a flow; min size: minimum number of packets in a flow; ip limit: maximum number of occurrences of an IP address; port limit: maximum number of occurrences of a port number; port scan limit: minimum number of port numbers contacted in a trace for considering it as a port scanning trace; unsafe threshold : maximum value of bgp ranking for considering an IP address as safe.

At the core of our approach lies a classification of the destination addresses a appearing in flows in t app according to the following predicates that indicate whether a is suspected to be the target of an attack of the various types we consider:

dos(a) ≡ f ∈ t app ∧ a = f.dstaddr ∧ (l f , p, l f ) ∈ T app ∧ p ≥ attack limit ∧ count(a, l f ) ≥ ip limit ∧ avg interval (l f ) ≤ min interval ∧ avg size(l f ) ≤ min size port scan(a) ≡ f ∈ t app ∧ a = f.dstaddr ∧ (l f , p, l f ) ∈ T app ∧ p ≥ attack limit ∧ count(a, l f ) ≥ ip limit ∧ avg interval (l f ) ≤ min interval ∧ avg size(l f ) ≤ min size ∧ | ports(l f ) | ≥ port scan limit worm(a, pt) ≡ f ∈ t app ∧ a = f.dstaddr ∧ (l f , p, l f ) ∈ T app ∧ p ≥ attack limit ∧ pt = f.dstport ∧ count(pt, l f ) ≥ port limit botnet(a, pt) ≡ f ∈ t app ∧ a = f.dstaddr ∧ count(a, l f ) ≥ ip limit ∧ pt = f.dstport ∧ protocols(l f ) ∩ {"tcp", "udp"} = ∅ ⇒ avg interval (l f ) ≤ min interval unsafe(a) ≡ f ∈ t app ∧ a = f.dstaddr ∧ bgp ranking(a) ≥ unsafe threshold safe(a) ≡ ¬dos(a) ∧ ¬port scan(a) ∧ ¬worm(a, pt) ∧ ¬botnet(a, pt) ∧ ¬unsafe(a) danger (a, pm) ≡ f ∈ t app ∧ a = f.dstaddr ∧ pm ∈ P f.appname ∩ D
In words, an address is considered to be the target of a potential attack if there exists a flow in t app for which certain threshold values are exceeded. Addresses that are not the target of an attack are considered safe. In addition, the predicate danger records addresses that receive flows from an application that holds dangerous permissions. For example, a few properties derived for the Pokemon Go application, based on its automaton are given in Listing 1.1.

Inferring a high-level representation of the chain

We now present a rule-based program for inferring the chain of security functions that should be deployed on the basis of the observed trace, making use of the classification of flows that occur in the trace. In a nutshell, we start by associating elementary security rules with addresses that occur in the trace. These will be composed in parallel to build security functions such as firewalls or intrusion detection systems, which in turn are composed sequentially to form entire chain. In the present section, security functions are represented symbolically; we will explain in section 4.4 how we translate this representation into the Pyretic language.

The elementary security rules make use of the following predicates that are defined externally:

regexp(s, pm): true if the string s (representing the packet payload) matches a regular expression associated with the permission pm; tcp check (t): true if the network traffic t is a valid TCP connection; udp check (t): true if the network traffic t is a valid UDP connection; http check (s): true if the string s (representing the packet payload) is a valid HTTP request; inspect payload (s): true if the string s (representing the packet payload) passes deep packet inspection.

Our system is based on the following elementary security rules:

forward (a, t) = restrict(t, λpk : pk.dstaddr = a) block (a, pt, t) = restrict(t, λpk : pk.dstaddr = a ∧ pk.dstport = pt) limit(a, n, t) = cut(forward (a, t), n)

filter (a, pm, t) = restrict(t, λpk : pk.dstaddr = a ∧ regexp(pk.payload , pm))

inspect(a, t) = restrict(t, λpk : pk.dstaddr = a ∧ inspect payload (pk.payload ))

tcp(a, pt, t) =    restrict(t, λpk : pk.dstaddr = a ∧ pk.dstport = pt) if tcp check (t) otherwise udp(a, pt, t) =    restrict(t, λpk : pk.dstaddr = a ∧ pk.dstport = pt) if udp check (t) otherwise
http(a, pt, t) = restrict(t, λpk : pk.dstaddr = a ∧ pk.dstport = pt ∧ http check (pk.payload ))

The inference system below determines which security rules to deploy for addresses appearing in the given flow trace. For each of the elementary security rules r above, a corresponding predicate deploy r indicates if the rule is to be instantiated, with additional parameters corresponding to the relevant IP address, port etc. deploy block (a, ← worm(a, pt)

deploy block (a, pt) ← botnet(a, pt)
deploy forward (a) ← ¬worm(a, pt) ∧ ¬botnet(a, pt) deploy limit (a, ip limit) ← dos(a) deploy limit (a, ip limit) ← port scan(a)

deploy tcp (a, pt) ← f ∈ t app ∧ a = f.dstaddr ∧ pt = f.dstport ∧ f.protocol = "tcp" deploy udp (a, pt) ← f ∈ t app ∧ a = f.dstaddr ∧ pt = f.dstport ∧ pt = 80 ∧ pt = 443 ∧ f.protocol = "udp" deploy http (a, 80) ← f ∈ t app ∧ a = f.dstaddr ∧ f.dstport = 80 deploy http (a, 443) ← f ∈ t app ∧ a = f.dstaddr ∧ f.dstport = 443
deploy filter (a, pm) ← unsafe(a) ∧ danger (a, pm)

deploy inspect (a) ← unsafe(a)
Based on the predicates deploy r inferred to be true from a given trace t app characterizing the network behavior of the application we wish to protect, we now construct security functions by composing elementary rules in parallel.

stateless firewall (t) =

+ { forward (a, t) : deploy forward (a), a ∈ Addr } • + + { block (a, pt, t) : deploy block (a, pt), a ∈ Addr, pt ∈ Port } ids(t) = + { limit(a, n, t) :

deploy limit (a, n), a ∈ Addr, n ∈ N } stateful firewall (t) = + { tcp(a, pt, t) : deploy tcp (a, pt), a ∈ Addr, pt ∈ Port } • + + { udp(a, pt, t) : deploy udp (a, pt), a ∈ Addr, pt ∈ Port } • + + { http(a, pt, t) : deploy http (a, pt), a ∈ Addr, pt ∈ Port } dpi (t) = + { inspect(a, t) : deploy inspect (a), a ∈ Addr } dlp(t) = + { filter (a, pm, t) : deploy filter (a, pm), a ∈ Addr, pm ∈ D }
Continuing our example of the Pokemon Go application, we obtain a chain containing the following security functions. (We omit the full definitions since the inference system generated too many security rules, but show the overall structure of each security function.) For the Pokemon Go application, we should deploy the chain corresponding to unsafe traffic. However, given that no dangerous permission is declared in the manifest file of this application, the DLP component of that chain is trivial and can be omitted in order to reduce the overall complexity of flow evaluation.

stateless

Generation of a Pyretic implementation of the chain

The last step of our approach consists in generating the Pyretic code implementing the abstract functions that we previously computed. Below we provide rewriting rules to derive Pyretic implementations corresponding to the elementary security rules introduced in section 4.3. In these rewrites, the argument of the security rules corresponding to the traffic t remains implicit in the Pyretic translation, which is applied to the current stream of packets. The functions DPIQuery, TCPFilter , UDPFilter , and HTTPFilter are part of our Synaptic checker [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF] using dynamic query policies that Pyretic provides. The translations of the overall chains is then obtained by composing the Pyretic code sequentially or in parallel using the combinators and + of Pyretic To illustrate this last step of our inference system let us consider again our running example, the Pokemon Go application. The security functions introduced previously are converted into the following chain of security functions. The construction of security chains based on a high-level representation guarantees certain correctness properties that we now discuss. The evaluation of the performances of the chains generated using our inference system will be discussed in further work.

Packet routing

Two elementary desirable properties of packet routing in networks are the absence of black holes and of loops. A black hole arises if packets are sent to a link at which no actual routing function is installed. A loop refers to a cycle in routing policies, so that packets may be sent back to a security function that they have already passed. Our security functions avoid these problems by construction.

Lemma 1. The security chains generated by the approach described in section 4 are free of black holes and of loops.

Proof. In our setup, security functions are total functions on sequences of packets, and they are built up from elementary security rules using parallel and sequential composition. In particular, every constituent of our chains is fully defined before it is used, so black holes do not exist at the abstract level of the descriptions of the chains. Similarly, the high-level definitions of chains do not involve fixpoint operators or similar looping constructs. Finally, we rely on the close correspondence between the abstract chains and their Pyretic implementation and on the correctness of the Pyretic translator in order to ensure that the latter does not introduce black holes or loops.

Shadowing freedom and coherence

The two main correctness properties of chains of security functions that we are interested in are shadowing freedom and coherence. Shadowing freedom means that whenever two rules are composed in parallel within a chain, only one of them actually applies. This property ensures that there is no confusion in the sense that two rules could be applied with potentially conflicting results. In particular, this property implies the consistency of the rules, which requires that whenever two rules apply, they result in the same decisions. Coherence means that the traffic after applying the security chains satisfies the security requirements: safe traffic passes unchanged, whereas potentially dangerous traffic is either blocked or limited within acceptable bounds.

Lemma 2. The security chains generated by the approach described in section 4 guarantee shadowing freedom.

Proof. Elementary security rules are composed in parallel in the definitions of the basic security functions stateless firewall , ids, stateful firewall , dpi , and dlp.

The definition of stateless firewall composes in parallel rules forward and block , which are potentially in contradiction. However, this is possible only if both deploy forward (a) and deploy block (a, pt) are true for some address a and port pt, and this is impossible due to the definitions of these predicates.

Similarly, the parallel composition of the elementary security rules tcp, udp, and http in the definition of stateful firewall is unproblematic because the definitions of the corresponding predicates deploy tcp , deploy udp , and deploy http are mutually exclusive. We now show that our security chains are coherent with the security policy determined on the basis of the trace t app underlying their generation. Lemma 3. Given a trace t app characterizing the network traffic generated by an application, the security chains generated by the approach described in section 4 transmit unchanged the traffic towards addresses considered as safe but block or limit network traffic towards other addresses.

Proof. An address is considered as potentially not safe if t app contains some flow towards that adress classified as worm, botnet, dos, port scanning or unsafe. The stateless firewall applied as the first security function in the chain will directly block packets towards IP addresses associated with worm and botnet traffic.

Concerning traffic directed to addresses associated with DoS or port scanning attacks, it will pass the stateless firewall and will subsequently be transmitted to the IDS. The traffic will then be limited to a number of packets bounded by the fixed threshold ip limit, considered to be acceptable by the security policy.

For addresses associated with unsafe flows, i.e., network traffic potentially compromising sensitive data, the security chains contain the security functions DPI and DLP that check the payload of packets. These apply the security policy by blocking packets that do not match the criteria defined by the predicates regexp (associated with Android permissions) and inspect payload .

Traffic towards addresses classified as safe is only subject to the stateless firewall, which lets it pass unchanged.

Conclusions and future work

We proposed in this paper a system based on inference rules for automating the generation of chains of security functions, based on the requirements of end users. This inference system is intended to protect Android applications, by taking into account both their networking behavior and the OS-level permissions that they request. By using first-order predicates for classifying network traffic observed in the flow trace -rather than for example finite state machines -the composition and factorization of security chains to be applied for several applications becomes straightforward. Our system infers a high-level representation of the security functions, which can be translated into a concrete implementation in the Pyretic language for programming software-defined networks. We showed that the generated chains satisfy several desirable properties such as the absence of black holes and of loops, shadowing freedom, and that they are consistent with the underlying security policy.

Further correctness properties of the chains can be verified using our Synaptic checker [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF] based on symbolic model checking and SMT solving. The main assumption underlying our approach is that the network-level behavior of Android applications can be characterized in terms of flow traces that are collected before the security chains are generated, and that are analyzed offline, as described in our previous work [START_REF] Schnepf | Towards generation of SDN policies for protecting android environments based on automata learning[END_REF] on process learning. This assumption holds for many, but not all Android applications, a Web browser being a typical counter-example. In that case, network administrators must install a default security chain.

An interesting extension of our present work would be to consider which parts of the analysis are sufficiently lightweight to be performed online. As further perspectives, we are also planning to work on optimizing and improving the parameterization of the security chains that are generated by our inference system. In addition, we are interested in investigating to what extent our solution is compatible with network function virtualization techniques (NFV) to implement security functions, such as firewalls and intrusion detection systems.

Fig. 1 .

 1 Fig. 1. Automaton describing the behavior of an Android application.

  These security functions are in turn composed into chains to be applied to the network traffic of the different types: safe chain = stateless firewall • stateful firewall unsafe chain = stateless firewall • stateful firewall • dpi • dlp dos chain = stateless firewall • ids • stateful firewall port scan chain = dos chain worm chain = stateless firewall botnet chain = stateless firewall These chains are deployed for filtering traffic generated by the target application by subjecting addresses to the chains associated with the classes to which the address belongs.

  . The following definitions indicate the implementations of the elementary security rules; forward (a, t) ; match(dstaddr = a) block (a, pt, t) ; ∼ match(dstaddr = a, dstport = pt) limit(a, n, t) ; LimitFilters(n, dstaddr = a) filter (a, pm, t) ; match(dstaddr = a) RegexpQuery(regexp(pm)) inspect(a, t) ; match(dstaddr = a) DPIQuery tcp(a, pt, t) ; match(dstaddr = a, dstport = pt) TCPFilter udp(a, pt, t) ; match(dstaddr = a, dstport = pt) UDPFilter http(a, pt, t) ; match(dstaddr = a, dstport = pt) HTTPFilter

  stateless firewall = match(dstaddr = 169 .45 .223 .16 ) + match(dstaddr = 169 .45 .223 .20 ) + . . . stateful firewall = match(dstaddr = 169 .45 .223 .16 , dstport = 80 ) TCPFilter + match(dstaddr = 169 .45 .223 .20 , dstport = 80 ) TCPFilter + . . . + match(dstaddr = 169 .45 .223 .20 , dstport = 80 ) HTTPFilter + . . . dpi = match(dstaddr = 169 .45 .223 .16 ) DPIQuery+ match(dstaddr = 169 .45 .223 .20 ) DPIQuery + . . . chain = stateless firewall stateful firewall dpi 5 Correctness properties of the generated chains

  firewall (t) = forward (169 .45 .223 .16 , t) • + forward (169 .45 .223 .20 , t) • + . . . stateful firewall (t) = tcp(169 .45 .223 .16 , 80 , t) • + tcp(169 .45 .223 .20 , 80 , t) • + . . . http(169 .45 .223 .20 , 80 , t) • + . . . dpi (t) = inspect(169 .45 .223 .16 , t) • + inspect(169 .45 .223 .20 , t) • + . . .