Zheng Cheng
email: zheng.cheng@inria.fr

Jean-Claude Royer
email: jean-claude.royer@imt-atlantique.fr

Massimo Tisi
email: massimo.tisi@imt-atlantique.fr

Efficiently Characterizing the Undefined Requests of a Rule-Based System

Rule-based systems are used to define complex policies in several contexts, because of the flexibility and modularity they provide. This is especially critical for security systems, which may require to compose evolving policies for privacy, accountability, access control, etc. The inclusion of conflicting rules in complex policies, results in the inability of the system to unambiguously answer to certain requests, with possibly unpredictable effects. The static identification of these undefined requests is particularly challenging for unconstrained rule-based systems, including quantifiers, computations and chaining of rules. In this paper we introduce a static method to precisely characterize the set of all undefined requests for a given unconstrained rule-based system, providing the user with a global view of the rule conflicts. We propose an enumerative approach, made usable in practice by two key performance optimizations: a finer classification of the rules and the resort of the topological sorting. We demonstrate its application on a well-known policy with more than fifty rules.

Introduction

Rule-based systems are widely used in very different contexts, ranging from knowledge representation and reasoning to system configuration, from logic programming to databases. Among these contexts, security systems are especially witnessing a significant growth in production of critical, complex and rapidly evolving rule-based policies aiming to offer strong guarantees (of privacy, accountability, etc.) in modern networking environments (including Internet of Things, Software-Defined Networks, etc.). A rule expresses in a concise and natural manner the link between some conditions and a conclusion. This if then else semantics is familiar to many software stakeholders, and allows for the definition of modular systems and their flexible evolution.

In this paper we consider a strict logical context, where a rule system is a finite set of logical implications and in conjunction with a request it ensures a reply. Efficient methods for verifying the correctness of such systems in practice is an important research subject [1]. We are particularly interested in one type of error, namely rule conflicts, that cause some requests to be undefined, i.e. to have several incompatible replies. The risk of rule conflicts is very relevant in modern security systems, that often compose independent and evolving policies. We are here interested in a general notion of conflicts entailing the system execution and leading to a runtime bug. We are not focusing on redundancies, misconfigurations or other similar problems which can be considered either as simplifications or holes in the rule system.

There are already several verification methods and algorithms for rule-based policies, in expert systems and databases [START_REF] Coenen | Verification, validation, and integrity issues in expert and database systems: Two perspectives[END_REF], for Web policies and contracts [START_REF] Paschke | Verification, validation and integrity of distributed and interchanged rule based policies and contracts in the semantic web[END_REF], and in the security domain [START_REF] Han | A survey on policy languages in network and security management[END_REF][START_REF] Hanamsagar | Firewall anomaly management: A survey[END_REF][START_REF] Aqib | Analysis and comparison of access control policies validation mechanisms[END_REF]. In this paper we will focus on formal methods and assume a formal policy written in a decidable logic. Moreover we will consider unconstrained systems with complex conclusions and chaining of rules (i.e. the conclusion of one rule can be used to match other rules and produce new derivations). For these systems we want to provide a precise characterization of the set of all undefined requests the user can present, that is in general an infinite set. This characterization constitutes a global view of the conflicts in the system, and a valuable aid in debugging extensive rule sets.

Techniques that have the potential to check for conflicts in unconstrained systems with chaining, divide in two categories. The testing method (e.g., [START_REF] Lin | Exam: a comprehensive environment for the analysis of access control policies[END_REF][START_REF] Hwang | Detection of multiple-duty-related security leakage in access control policies[END_REF]) computes the set of undefined requests by generating large sets of ground sentences as test requests, and checking the unsatisfiability of each of them in conjunction with the rule system. The testing method suffers from two main drawbacks: i) the global cost of the request generation and evaluation is very high and ii) the test set has finite coverage over the infinite set of undefined requests. The verification method (e.g., [START_REF] Montangero | Logic-based conflict detection for distributed policies[END_REF][START_REF] Halpern | Using first-order logic to reason about policies[END_REF][START_REF] Craven | Expressive policy analysis with enhanced system dynamicity[END_REF][START_REF] Turkmen | Analysis of XACML policies with SMT[END_REF]) considers consistency properties (e.g., it is not possible to deny and permit an access at the same time) and tries to prove these properties. It has similar drawbacks since it is generally costly, and does not aim at an exhaustive view of all possible conflicts.

Our contribution is to provide an enumerative method based on symbolic manipulation of the rules and a satisfiability procedure to exhaustively find the precise set of undefined requests in a rule system. The computation complexity is exponential, but we provide two optimization steps to enhance its practical applicability: an iterative method with rule classification and a sorting algorithm. Finally, we evaluate our approach on a well-known case study in XACML, translated into FOL. The experimentation shows that our method is suitable for the verification of rule systems of this size (i.e., 47 rules), where in less than one hundred seconds it produces and analyzes less than one thousand new rules (summarizing the analysis of 2 47 rule combinations).

The content of this paper is structured as follows. Section 2 describes related work in the area of rule-based systems and checking for conflicting rules. Section 3 presents a motivating example. Section 4 provides the necessary background and definitions to understand our approach. Section 5 illustrates our enumerative method and optimizations. In Section 6 we evaluate our method, based on a well-known case study. Lastly, In Section 7 we conclude and sketch future work.

An extensive literature studies the management of rule-based systems. The survey [1] shows that verification and validation of rule-based systems in practice is mainly based on testing or code review which are of course not sufficient to prove that a system is free from bugs. Validation and verification techniques for various kinds of rule-based systems have also been discussed in [START_REF] Coenen | Verification, validation, and integrity issues in expert and database systems: Two perspectives[END_REF] for expert systems and database management or [START_REF] Paschke | Verification, validation and integrity of distributed and interchanged rule based policies and contracts in the semantic web[END_REF] for Web policies and contracts. In the domain of security policies, the problem of conflicts has been intensively studied. In surveys on security [START_REF] Han | A survey on policy languages in network and security management[END_REF][START_REF] Hanamsagar | Firewall anomaly management: A survey[END_REF][START_REF] Aqib | Analysis and comparison of access control policies validation mechanisms[END_REF], conflict detection is a central problem but it is typically treated together with other tasks like finding bugs, redundancies, misconfigurations, etc. We propose a specific solution for static conflict detection, that we believe to be one of most critical issues in modern rule-based systems.

There are already some efficient algorithms to statically detect conflicts in access control policies [START_REF] Ni | Privacy-aware role-based access control[END_REF][START_REF] Neri | Conflict detection in security policies using semantic web technology[END_REF][START_REF] Armando | Automated and efficient analysis of role-based access control with attributes[END_REF][START_REF] Hu | Discovery and resolution of anomalies in web access control policies[END_REF][START_REF] Shaikh | A data classification method for inconsistency and incompleteness detection in access control policy sets[END_REF][START_REF] Deng | Elimination of policy conflict to improve the PDP evaluation performance[END_REF]. The method is generally to look for conflict in all combinations of a number of rules (often only two rules). However, most of these methods support only policies with discrete conclusions (like permit and deny) and even only handle discrete attributes as conditions (ABAC policies). Our approach is more general because, except decidabiblity of satisfiability, we do not assume constraints on the rule system, as we could have conditions, functions, any kind of conclusions, possibly with quantifiers and free variables. Even with unbounded rule systems we claim to generate all the undefined requests of the system.

In case of complex systems with predicates in conclusions and allowing the chaining of rules, the existing solutions are not numerous. There are approaches based on testing, used in different contexts, e.g. [START_REF] Lin | Exam: a comprehensive environment for the analysis of access control policies[END_REF][START_REF] Hwang | Detection of multiple-duty-related security leakage in access control policies[END_REF][START_REF] Xia | A conflict detection approach for XACML policies on hierarchical resources[END_REF][START_REF] Hu | Discovery and resolution of anomalies in web access control policies[END_REF]. A few studies rely on checking satisfiability as in [START_REF] Royer | AAL and static conflict detection in policy[END_REF], but it is too weak since satisfiability is always a system requirement. Other formal methods and verification, for instance [START_REF] Montangero | Logic-based conflict detection for distributed policies[END_REF][START_REF] Halpern | Using first-order logic to reason about policies[END_REF][START_REF] Craven | Expressive policy analysis with enhanced system dynamicity[END_REF][START_REF] Turkmen | Analysis of XACML policies with SMT[END_REF], use manual proof or derivation tools and are able to prove expected properties of the system (e.g., an access is never both permitted and denied). In practice these properties concern a finite set of authorizations, but in case of unrestricted obligations and chaining of rules the enumeration of the property of interest can be an issue. We do not expect to compete with these approaches on the side of efficiency in detecting a single conflict. Differently from these works, our method automatically computes all the conflicting requests of the system, even if it is not a finite set.

In the domain of constraint solving, we think that techniques for extracting minimal unsat core and maximal sat core are closely complementary to our work (e.g. [START_REF] Liffiton | Enumerating Infeasibility: Finding Multiple MUSes Quickly[END_REF][START_REF] Previti | Partial MUS Enumeration[END_REF]). We concretely show in this work how to encode the exhaustive conflict detection problem of security policies as a satisfiability problem. To make sure that the problem can be solved within reasonable time, we introduce performance optimizations as symbolic manipulations, before providing the problems to the constraint solver. We do not directly use minimal unsat core nor maximal sat core techniques to solve our problem. However, our manipulations can be also adapted for enhancing alternative solutions for conflict detection that rely on sat/unsat core (e.g. [START_REF] Wu | Finding achievable features and constraint conflicts for inconsistent metamodels[END_REF]).

To exemplify our approach, we refer to a very simple example of rule-based policy for a medical center, inspired from [START_REF] Adi | Typing for conflict detection in access control policies[END_REF]. The example is illustrated in Listing 1.1 using the syntax of the Z3 solver, where we represent implication as an infix operator. This example is a first-order example with predicates and free variables but our approach, detailed in the next section, is applicable to any decidable logic extending propositional logic. Here h, p are universally quantified variables (respectively for hospital personnel and patients) and other terms are predicates or boolean operators. The system decides about read and write access rights to the information of a patient (pread, pwrite). Hospital personnel comprises the doctor, nurse and chief roles. Personnel can be assigned to the ward of a patient (sameward). Despite representing a simple policy, user-defined rules in Listing 1.1 contain conflicts, missing information and redundancies. Briefly, hospital employees with multiple roles can not be assigned to the ward of any patient (rule 1), doctors have read and write access to any patient data (rule 2), nurses can not get information on patients from other wards (rule 3), a doctor can access data for the patients of his ward (rule 4), a chief has read access to any patient data (rule 5).

Listing 1.1. Input for the hospital example And ( doctor ( h ) , nurse ( h )) = > Not ( sameward (h , p )) doctor ( h ) = > And ( pread (h , p ) , pwrite (h , p )) And ( nurse ( h ) , Not ( sameward (h , p ))) = > Not ( pread (h , p )) And ( doctor ( h ) , sameward (h , p )) = > pread (h , p ) chief ( h ) = > pread (h , p )

We provide an automatic prototype that, given a system like the one in Listing 1.1, identifies all undefined requests, e.g. requests having multiple ambiguous answers because of rule conflicts. When provided with Listing 1.1, our prototype produces the output in Listing 1.2.

Listing 1.2. Prototype output for the example

[0 , 1 , 0 , -1 , -1]
And ( doctor ( h ) , Not ( nurse ( h ))) = > And ( pread (h , p ) , pwrite (h , p )) [0 , 0 , 1 , 0 , 0] And ( Not ( doctor ( h )) , nurse ( h ) , Not ( sameward (h , p )) , Not ( chief ( h ))) = > Not ( pread (h , p )) [0 , 0 , 0 , 0 , 1] And ( Not ( doctor ( h )) , Or ( Not ( nurse

( h )) , sameward (h , p )) , chief ( h )) = > pread (h , p ) # -----------Unsafe -------------- [1 , 1 , 1] And ( doctor ( h ) , nurse ( h ) , Not ( sameward (h , p ))) = > False [1 , 1 , 0]
And ( doctor ( h ) , nurse ( h ) , sameward (h , p )) = > False [0 , 0 , 1 , 0 , 1] And ( Not ( doctor ( h )) , nurse ( h ) , Not ( sameward (h , p )) , chief ( h )) = > False

The rule system in Listing 1.2 is logically equivalent to the original rule system and composed of pair-wise exclusive rules3 . Furthermore, each rule is prefixed by a sequence of digits indicating the combination of the original rules which produces this rule. For instance, the first rule in Listing 1.2 comes from the combination of the original rule 2 and negation of rule 1 and 3; -1 is a don't care digit for rule 4 and 5. The rules tagged as unsafe denote indeed set of undefined requests, for instance And(doctor(h), nurse(h), Not(sameward(h, p))) is undefined which results from the combination ([1, 1, 1]) of the three first rules. That means that its conjunction with the rule system is unsatisfiable. The other rules denote defined and undefined requests. On one side, the defined requests should intersect the conjunction of the rule condition and the rule conclusion.

On the other side, undefined requests are included, by implication, in the conjunction of the rule condition and the negation of the rule conclusion. Related to the first not unsafe rule, And(doctor(h), Not(nurse(h))) is a defined request and And(doctor(h), Not(nurse(h)), Not(pread(h, p))) is an undefined one.

With such information the user can exactly know what are all the conflicting problems, and then what are the requests that this rule system can handle. Furthermore, he can localize the problems in the rule system, by knowing what is the rule combination leading to undefined requests. For instance, the first unsafe rule comes from the combinations of rules 1, 2 and 3. It states that any request about a personnel member that is at the same time a doctor and a nurse will lead to a rule conflict, even if the person is not assigned to the ward of the patient. The conflict involves the first three rules, since chaining rule 1 with respectively rule 2 and 3 leads to contradictory answers, where the data from the patient can and can't be read at the same time (pread(h, p) and Not(pread(h, p))).

The next section will introduce the required concepts and Section 5 will present the principles of our algorithm.

Background and Definitions

In this section, we define a terminology that will be consistently used in the rest of the paper. Our focus are systems that process requests and produce replies. One important problem is due to requests leading to evaluation failures and often called conflict in the literature. Here we formalize the notion by defining the term undefined request. We focus on rule systems: a conjunction of rules, a rule is A => B with A and B in some logical language. Considering that satisfiability decision has made important progress, we expect to build a new management method of rule-based systems by reusing efficient tool support (e.g., Z3, SMT, SPASS, TSPASS).

Let R be a satisfiable policy system with its set of expected requests REQ. REQ is a finite set of satisfiable logical formulae that we are interested in answering. It represents the set of expected inputs to the policy system. Requests and replies are satisfiable logical expressions, they could be ground (without variables) or containing free variables (implicitly universally quantified) or quantified variables. Indeed all the expressions (requests, replies, conditions, conclusions, ...) are assumed to be written in a given logical language which may allow variables, quantifiers, modal operators, and so on, providing it has a satisfiability procedure.

Definition 1 (Rule-based system). A rule-based system ( R) consists of a finite conjunction of rules noted R = r 1≤i≤n , where each rule r i takes the format of D i => C i , where D i stands for the premise/condition of the rule, and C i stands for conclusion of the rule. In addition we assume that R is satisfiable and does not contain tautological rules.

We should note that a rule-based system is interesting if it is satisfiable and not valid. This means that it can derive non trivial facts from the request. Thus we assume that R is satisfiable and it does not contain tautological rules, that is D i ∧ ¬C i is satisfiable for all i. A request will be a satisfiable logical expression submitted to a rule-based system and leading to a reply, another logical expression. Note that a request should trigger at least one rule, otherwise its conjunction with the system is satisfiable but does not infer a reply. Thus we make the natural hypothesis that our requests are satisfiable and imply 1≤i≤n D i . We will say that a set of rules is exclusive if their conditions are pair-wise disjoint.

Definition 2 (Request evaluation in rule-based system). Let req be a logical expression, evaluating it against a given rep, called the reply, means that req ∧ R => rep is valid or equivalently req ∧ R ∧ ¬rep is unsatisfiable.

We are interested in the evaluation problem raised due to undefined requests.

Definition 3 (Undefined requests).

A req request is said undefined if and only if req and R are both separately satisfiable but req ∧ R is unsatisfiable.

An undefined request in fact leads to a problem since its evaluation leads to multiple incompatible replies. This definition is stricter than satisfiability and covers the usual notion of conflicts we found for instance in security policies [START_REF] Dunlop | Methods for conflict resolution in policybased management systems[END_REF][START_REF] Aqib | Analysis and comparison of access control policies validation mechanisms[END_REF]. This has two simple consequences: i) any useful system has undefined requests and ii) these undefined requests are included in 1≤i≤n D i . Furthermore any rule (D i => C i ) which is satisfiable and not valid has 1-undefined requests, that is requests invalidating this rule alone (in other words requests which imply D i ∧ ¬C i ). In this work, we aim to study a complete and efficient algorithm to ensure the safety of a given rule-based system (Definition 4).

Definition 4 (Safety of rule-based system). A rule-based system with its set of expected requests is safe if and only if it does not contain any undefined requests, that is for all satisfiable request req ∈ REQ implies req∧R is satisfiable.

As we can see this property assumes that the input system is satisfiable, and it is different from many approaches looking for logical inconsistencies in a system, for instance [START_REF] Montangero | Logic-based conflict detection for distributed policies[END_REF][START_REF] Halpern | Using first-order logic to reason about policies[END_REF][START_REF] Royer | AAL and static conflict detection in policy[END_REF].

The management of policies and requests requires to consider several activities: looking for the existence of one undefined request, checking a request, finding all the undefined requests, localizing the conflicting rules, resolving the undefined requests and evaluating a request. We here focus on finding all the undefined requests since this global knowledge is necessary to understand the failures in the system and to globally fix them. We do not study the fixing process but we will give a few related hints later. As we will see, one additional benefit of our method is to get localization of conflicting rules for free.

This section shows a decision procedure for the safety property (if satisfiability is decidable), its theoretical complexity is EXPSPACE. Our approach is based on transformations of the original rule-based system. It is important to preserve the conditions and conclusions of rules as they represent the expected requests and replies. Hence we will build new rules by mixing the conditions on the left hand side and conclusions on the right hand side.

The Enumerative Method with Exclusive Rules

Our enumerative method to compute undefined requests is based on rewriting the original rule system into its equivalent form in terms of exclusive rules.

A minor point of the method is to allow requests with variables. By considering requests with variables rather than ground requests, we aim to cover the whole (sometimes infinite) set of requests. For example, in Listing 1.1, a ground request like And(doctor(Jack), nurse(Jack), Not(sameward(Jack, May))) with constants Jack, and May is undefined. However, there are many other different ground requests that expose this problem. To capture the essence of these problems, we use the requests And(doctor(h), nurse(h), Not(sameward(h, p))), which is a short hand for (∀h, p • (doctor(h) ∧ nurse(h) ∧ ¬ sameward(h, p))).

Furthermore, an undefined request is unsafe in the sense that it contains (i.e., it is deducible by logical implication from) only undefined requests. However, defined requests are not safe in general, in the sense they are not maximally defined.

Definition 5 (Safe request). Let R be a rule system, a satisfiable request req is safe if and only if any satisfiable request which implies req is defined.

Second, Lemma 1 establishes that we can rewrite the original rule system into an equivalent form, namely exclusive rules. The lemma can be proved by recurrence on the size of rule system n.

Lemma 1 (Exclusive rules). Let R be a rule system, we have the equivalence 1≤i≤n

(D i => C i ) <=> I ((∧ i∈I D i ∧ j / ∈I ¬D j ) => ∧ i∈I C i )
where I is any non-empty subset of {1, ..., n}.

The rewriting of a rule system with n rules generates 2 n -1 exclusive rules.

The rule system is composed only of pair-wise disjoint rules, and preserves the original set of defined and undefined requests. For example, the rewriting applied to the rule system shown in Listing 1.1, results in a total of 31 exclusive rules (partially shown in Listing 1.3). As shown in Listing 1.3, first, we abbreviate each rule by its appearance order in Listing 1.1, e.g. R1 is And(doctor(h), nurse(h)) => Not(sameward(h, p)). Second, we use a D function to get the condition part of a rule, and a C function to get the conclusion part of a rule, e.g. D(R1) is And(doctor(h), nurse(h)) and C(R1) is Not(sameward(h, p)). For instance, in Listing 1.4 we show the non-abbreviated form of the first exclusive rule, corresponding to the first line of Listing 1.3. The condition is obtained by conjunction of the first original rule R1 's condition, with the negation of the conditions of the other rules (R2 -R5 ). The conclusion is simply the conclusion of R1. As we previously saw, a rule (if not valid) has always 1-undefined requests and the transformation above builds a system whose undefined requests are disjoint unions of 1-undefined requests.

Lemma 2 (Undefined requests of exclusive rules). req is an undefined request of an exclusive rule system R if and only it is a disjoint sum, req = 1≤j≤m req j , where is the accumulative exclusive-or operator, and each req j is satisfiable and 1-undefined for a given rule j.

Lemma 2 simply results from the exclusive rules and the partition of req into disjoint parts related to the conditions D i . Thus the set of safe requests is defined as the disjoint union of all the safe requests associated to each rule. For each rule the conjunction of the condition and the conclusion defines a safe request. The maximal safe request is saf e(R)

= I ∧ i∈I D i ∧ j / ∈I ¬D j ∧ i∈I C i . A request is safe if included in saf e(R), it is defined if it intersects saf e(R)
, and else it is an undefined request. From that the safety property can be checked by the satisfiability of elements in REQ against saf e(R).

Discussion. While existing testing methods for rule systems are generally able to show the existence of ground undefined requests, they can't prove that a given (unbounded) rule system is safe. The enumerative way has three main benefits:

it works with the same complexity in case of finite or infinite set of ground requests while the testing approach is not suitable with infinite sets, it does not depend on the set of requests thus it outperforms the testing approach in many non trivial examples, it may produce undefined requests with variables, that represent an abstraction of the system problems, with localization for free.

Compared to the verification approaches, our enumeration does not require a large set of interesting properties to prove. Moreover, if the property is not satisfied, in the best cases previous work on verification generates a counterexample. In general, it is not possible to produce a characterization of all the counter-examples as we did here.

On the performance side, the enumerative method implies the computation of all the rule combinations, which has an expensive cost. Furthermore, we check each rule for validity and valid rules are discarded as they do not contribute to the set of undefined requests. The enumerative method can have worse performance than the testing methods in case of propositional rule systems. However, we expect our method to perform better than exhaustive testing of rule systems with variables. For instance, with systems expressed in FOL, the exhaustive testing requires a maximal number of 2 P * D V test cases, where P is the number of predicate occurrences in R, D the size of the domain of arguments and V the number of arguments. The set of test cases is growing quickly, while the number of exclusive rules is only dependent on the number of rules in the input system.

Work on minimal unsat core and maximal sat core are closely related to our enumerative method [START_REF] Liffiton | Enumerating Infeasibility: Finding Multiple MUSes Quickly[END_REF][START_REF] Previti | Partial MUS Enumeration[END_REF]. For example, after our partition in order to identify all the undefined requests of a rule-based system, we could send each exclusive rule to a solver to extract all the minimal unsat cores. However, for the sake of performance, we only check exclusive rules for satisfiability, since theoretically, the problem of extracting minimal unsat core is harder than checking satisfiability.

The Iterative Method

We present a first improvement of the enumerative method, called the iterative method. It is based on adding iteratively a new rule at each step and eliminating some rules as soon as possible. The principle is based on the following property. Assuming that R is a list of exclusive rules computed with the enumerative method and r j a new rule. Note that each rule in R can be uniquely described by its binary characteristic which is a binary integer of length n (where n is the rule size of the initial rule system). Let b a binary integer we can construct a rule of R in the following manner: the condition is the conjunction of the conditions D i (respectively ¬D i ) if the i th digit of b is 1 (respectively 0). The conclusion is the conjunction of the conclusions of R for which digit is 1 in b. Thus speaking of an exclusive rule or its binary characteristic is equivalent. We will say that a rule i of the input system is active in an exclusive rule if the binary digit at position i is 1.

Property 1 (Iterative principle) Let R built from the enumerative method, then the enumerative result for R ∧r j is obtained from the binary characteristics of rules in R and for each b we will get two new binary characteristics 2 * b and 2 * b + 1 plus one single last characteristic equal to 1.

This results from a simple recursive analysis of the binary characteristics of R compared to that of R ∧ r j . That means that if R has m rules we will get 2 * m + 1 rule in R ∧ r j .

Furthermore, the main loop of the iterative method is based on the above principle and two optimizations.

Definition 6 (Obvious rule). A rule

D => C is an obvious rule iff D is unsatisfiable.
The first optimization is to discard obvious rules during the iterative method (Definition 6). Obvious rules are one specific kind of tautologies. Adding them during the iterative method offers no value, since they will just generate two new obvious exclusive rules and make no difference to the last generated exclusive rule that in negation form. Notice that we keep exclusive rules that are tautologies but not "obvious" during the iterative method. The reason is that they have an impact on the iteration, e.g. affect the last generated rule. An additional optimization is possible here but it is postponed to future work.

Definition 7 (Unsafe rule). A satisfiable rule

D => C is an unsafe rule iff it is equivalent to D => f alse.
The second improvement of the iterative method is to separate unsafe rules. An unsafe rule implies no defined request matching its condition. Checking it efficiently depends from the logical language used and should take care of quantifiers in case of free variables. If a rule is not unsafe then (D ∧ C) is a safe request and the rule has only 1-undefined requests in (D ∧ ¬C). A consequence of this classification is that now the maximal safe request (saf e(R)) is computed only from rules that are not unsafe.

The above definition paves the way to a further optimization, which is to check for unsafe rules and to store them separately from the others. Hence we stop processing unsafe rules and present them in the final result (possibly with a shorter binary characteristic w.r.t. not unsafe rules, e.g. see the first two unsafe rules of Listing 1.2). With the iterative method and the classification (obvious, unsafe and not unsafe) we expect to decrease the number of generated rules which is a critical factor of the enumerative approach.

For example, by applying our iterative method on the rule system shown in Listing 1.1, the first rule R1 is checked for its obviousness and unsafeness, and the checks succeed. Then, R1 becomes the first exclusive rule and the iteration starts. We show in Listing 1.5 the result of first iteration by adding R2 to the first exclusive rule. Since R2 also passes obviousness and unsafeness checks, three exclusive rules are built along with iterative method. Their binary characteristics are [1,1], [1,[START_REF]And ( Not ( D ( R1 ))[END_REF] and [START_REF]And ( Not ( D ( R1 ))[END_REF]1] respectively.

At the final iteration, we get a total of 6 exclusive rules (3 unsafe, 3 not unsafe, plus 4 eliminated as obvious), which results in a total of 16 unsat checks. Clearly, the iterative approach performs better than the enumerative approach (that in this example would generate 31 rules, by 31 unsat checks), and we anticipate that the effectiveness of the iterative approach would be more visible on larger examples. Note that the iterative method is a quite general solution which requires a logic extending propositional logic with a decision procedure for satisfiability.

The Sorting Method

The analysis of relations between rule conclusions can lead to significant performance improvements. We argue that in many practical examples, rule conclusions are built on a set of finite predicates, and several rule systems have some pairs of rules whose conclusions are related by inclusion. If we add in the iterative process a new rule D j => C j and if we know that it exists i < j such that C i => C j is valid then we can simplify the process using the following principle. Let cond ∧ D i => conc ∧ C i be the exclusive rule where rule i is active, in the step before the addition of rule j. By adding rule j, the iterative process would generate two rules cond

∧ D i ∧ D j => conc ∧ C i ∧ C j and cond ∧ D i ∧ ¬D j => conc ∧ C i .
Given the inclusion relation between C i and C j , instead of these two rules, the two rules simplify in cond ∧ D i => conc ∧ C i , that was already present before adding rule j. This rule will still be exclusive w.r.t. all the other rules generated during the addition of rule j. In the binary characteristic of this exclusive rule, we insert a -1 at position j, to indicate that the condition of rule j does not matter in this combination. This optimization eliminates two satisfiability checks, but most of all it decreases the number of generated exclusive rules.

With this optimization the size of the result depends on the order of rules. Thus, to take the maximal benefit from these relations, we sort the rules from minimal conclusions to maximal conclusions (w.r.t. the implication relation). We achieve this reordering by a simple adaptation of topological sorting, with a complexity in O(n 2 ) (where n being number of rules). The result of our topological sorting is that each rule is preceded by all the rules with a smaller conclusion than its proper conclusion. For example, the sorting result for our example shown in Listing 1.1 is R1, R3, R2, R4, R5.

The Algorithm

To sum up, in Algorithm 1 we sketch our process to efficiently compute exclusive rules and classify them as unsafe and not unsafe. Notations used in the algorithm require some explanation.

First, we use D and C to get the condition and conclusion of a rule respectively. Second, we inherit traditional list operators hd, tl and ++ for head, tail and concatenation of lists. Third, we use dict to initialize a dictionary, and use update to add a pair to a dictionary, and overload a[b] for element access in a dictionary (i.e. accessing element whose key is b in a dictionary a). Finally, three predicates specific to our algorithm are sort, isObvious and isUnsafe. They perform a topological sort of a list of rules w.r.t. implication between conclusions (Section 5.3), check whether the rule is an obvious tautology (Section 5.2), and check whether the rule is unsafe (Section 5.2), respectively.

The input of our algorithm is a list of rules, the output are classified exclusive rules. To compute from input to output, we use 4 global variables in our computation (line 1). NotUnsafes and Unsafes are dictionaries, which are used to keep track of the rules detected so far, that are unsafe and not unsafe. Notice that the key of these two dictionaries is the binary characteristic of each exclusive rule, and the value is the exclusive rule itself. Negs is a conjunction of formula that represents negated conditions for rules that previously iterated on. Zeros is synchronized with Negs to record binary characteristics. These two global variables are used when building exclusive rules in negative form on line 23.

Our iterative construction is performed to categorize rules that are unsafe or not unsafe (lines 2 -27). It internally uses our sorting method to optimize its efficiency (lines 17 -18), and uses BuildExRule to interact with the solver to check whether a newly constructed exclusive rule is unsafe (lines 29 -38). The whole process offers no surprise w.r.t. what we described in Section 5.2 and Section 5.3.

Once the two lists of rules NotUnsafes and Unsafes are computed by Algorithm 1, the set of undefined requests is precisely characterized as:

each unsafe exclusive rule denotes a set of undefined requests, i.e. all the requests included by implication in the rule condition, each exclusive rule that is not unsafe denotes a set of undefined requests, i.e. all the requests included by implication in the conjunction of the rule condition and the negation of the rule conclusion, no other undefined requests exist for the original system.

Evaluation and Discussion

We implement the three previous methods in Python 3 and we use the z3py interface to interact with the Z3 solver [START_REF] De Moura | Z3: An efficient SMT solver[END_REF]. Our input rules are defined using a class of rules reusing the logical expression defined by Z3. The code is available on our on-line repository4 with a set of examples. We prove, using the solver, that the original rule system is equivalent to the new generated one.

Our evaluation objective is to experiment with middle size examples to observe if the concrete performances are according to our expectations and suitable for a practical use. In our approach, we rely on the Z3 solver, but the solver can be changed as long as it provides a decision procedure for satisfiability suitable for the input rule system. Our method is not limited to pure predicates with free variables, however its success and efficiency depend on the ability of the solver to check such construction.

The CONTINUE Example

We describe here the case of the CONTINUE A policy already used in [START_REF] Fisler | Verification and change-impact analysis of access-control policies[END_REF][START_REF] Royer | AAL and static conflict detection in policy[END_REF] and dedicated to conference management. This policy5 is specified in 25 XACML files containing 44 rules. Our objective was not to exactly encode this policy but rather to validate that our optimizations are effective in case of a non trivial example. We deviate from the original CONTINUE example in several ways. First, we consider a pure logical translation and this introduces a difference as already discussed in [START_REF] Halpern | Using first-order logic to reason about policies[END_REF]. We do not take into account the combining algorithms since our objective is to observe the undefined requests occurring in the business rules, not to provide an ad-hoc automatic resolution. We also handle free variables and predicates (unary and binary), while this is not the case in the XACML language.

Our initial rule system has 47 rules, with two types, two free variables, 6 binary predicates and 29 unary ones. We start with this example without additional relations. Figures 1,2, and 3 depict the results we get with a MacBookPro under El Capitan, 2.5 GHz Intel Core i7 and 16 Go 1600 MHz DDR3 RAM. The resulting times were computed from an average of 10 runs.

In the figures we report the number of rules in the system and a few curves: correct is the number of non tautology in the system, time the time in second, exclusive, not unsafe, unsafe the number of exclusive, not unsafe and unsafe rules. We process the example by taking the first n rules from an arbitrary ordering. The correct curve shows that there is no tautology in this system.

The enumerative experiment (Figure 1) shows clearly an exponential growth in the number of generated rules and in the processing time. While the performances of the iterative method (Figure 2) are much higher, we still cannot process the full example in a reasonable time. The sorting method (Figure 3) provides more interesting results in such a case. CONTINUE has many inclusion relations among conclusions (653 relations), which explains the good performances by topological sorting. While this is not a universal property, in our experience, this is often the case in security systems. This is obvious when conclusions are only permit and deny as in some simple access control policies. More generally, in security we expect to control the possible outcomes of the rules, thus defining a limited set of replies. Each rule can then combined these outcomes and thus revealing relations between conclusions. We easily observe We should also note that some rules have a great impact on the behavior of the iterative and sorting methods. This is the case with predicate exclusivity which is often implicit. Indeed XACML, due to the use of the combining algorithms, does not make hypothesis about the disjunction of roles or permissions of different actions. To observe the stability of our performances we experiment adding a few new rules about roles in the system. For instance, it makes sense to consider that the PC chair is also a PC member and a subreviewer is not a PC member. There are also some relations related to resources, for example there are several different kinds of information about papers. These resources appears only in conditions and alone but never in a conjunction, thus we may consider these resources as disjoint. Adding these rules increases the size of the original system to 57 rules. As shown in the curves in Figure 4 these disjunctions decrease the number of rules that are not unsafe. With this setting we generate 776 rules (535 unsafe and 241 not unsafe) in nearly 100s, including the verification of the equivalence with the original system which takes 10s.

Listing 1.6. An example of conflicting rules // An unsafe case UNSAFE [0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 1 , 1 , 1 , 1] // The four active 10 -13 th rules ( other negative rules are omitted ) pcchair ( X ) = > pcmember ( X ) Or ( admin ( X ) , pcchair ( X ) , pcmember ( X ) , subreviewer ( X )) = > subject ( X ) And ( P a p e r A s s i g n m e n t s ( R ) , subject ( X ) , isConflicted ( X ))

= > And ( Not ( Pread (X , R )) , Not ( Pwrite (X , R )) , Not ( Pcreate (X , R ))) And ( P a p e r R e v i e w C o n t e n t ( R ) , pcmember ( X ) , isEQuserID ( X ))

= > And ( Pcreate (X , R ) , Pwrite (X , R ) , Pdelete (X , R ))

As an example of output in this scenario, Listing 1.6 shows the binary characteristic of one of the first unsafe rules detected (the 10 th ). As shown by the binary characteristic, this rule denotes a set of undefined requests coming from Listing 1.7. Two safety tests // Intersecting the maximal safe request it is a defined request ForAll ([ X , R ] , And ( Not ( PcMember ( R )) , P a p e r R e v i e w C o n t e n t ( R ) , pcmember ( X ) , Not ( subreviewer ( X )) , isEQuserID ( X ))) // It is contained in the negation of the maximal safe request // thus it is an undefined request ForAll ([ X , R ] , And ( P a p e r As s i g n m e n t s ( R ) , subject ( X ) , isConflicted ( X ) , P a p e r R e v i e w C o n t e n t ( R ) , pcmember ( X ) , isEQuserID ( X )))

Discussion

In summary, through our evaluation, we experiment our approach on a middlesize example, and observe its performances are according to our expectations and suitable for a practical use. There are also some lessons we learned.

Correctness. Decidability of the satisfiability is required for our approach to get an optimal rule classification and best performance. For example, we interact with solver to check conclusion implication, and whether a rule is obvious, unsafe or not unsafe. If the solver cannot give a reply to these questions within a given timeout, an unknown will be returned as result. This would degrade the precision of rule classification result and the performance of our approach. However, when unknown results occur, we always defensively categorize them as not unsafe, and thus will not give incorrect answers to the user.

Usability. It is important to simplify as much as possible the output, to facilitate the inspection of rule conflicts. Some simple cases are already handled in the iterative and sorting steps. For instance, two rules with equivalent conditions are simply merged into one rule with this condition and a conjunction of each conclusion. However, more aggressive simplifications are complex and time consuming. In our current solution, we think that it is better to first produce a result which alerts the user on the presence of undefined requests. In a second step, if the user wants to fix some problems we should provide a simplified version of the rules, and perhaps some hints for resolution of conflicts.

While we do not think that automatic resolution will always match users' expectation, our approach can be extended to suggest some automatic fixes to the user. For instance, the user may want to restrict its set of expected requests to the maximal set of safe requests.

Another idea is to add conditions occurring in the unsafe rules as extra conditions of the not unsafe rules. One approach is to introduce the input rules one by one and to resolve the generated unsafe cases. If the system has no chaining of rules then there is no further problem and this way will produce a safe system. In the more general chaining case, the user should always cope with 1-undefined requests.

Generalization. While the number of rules is related to the complexity of the rule system, they do not necessarily compromise the generalization of our approach, e.g. the algorithm could take advantage of more obvious rules, or there could have more implications between conclusions.

However, we do agree that more case studies are needed to confirm the generalization for the performance and practicability of our approach. We processed another example6 , consisting of 61 rules for managing resources, hierarchy of roles, permissions and revocation of permissions. The encoding of these rules are more complex than the CONTINUE example, e.g. predicates to represent discrete time. While the relationship between rules are more sparse (259 inclusion relations among conclusions), our sorting method is still much more efficient than the iterative one. For example, during the evaluation process, we observe that iterative method takes about 13000s to analysis 40 rules in this example. Our sorting method only takes 735s on the same set of rules. In our preliminary result on this example, we also observe a reasonable growth in its analysis time (5736s), and find 4 unsafe rules and 17085 not unsafe ones. The last unsafe rule reveals an unexpected conflict due to the hierarchy of resources and not seen in the original description.

Optimization. Currently, our approach produces a logically equivalent system for the input during its analysis. However, we think this restriction can be relaxed, e.g. a new system that is stronger than the original one could still be acceptable for analysis since it guarantees the behavior of the original. Our future work will explore new optimizations based on this kind of relaxation.

Another track of optimization could be decompose input system into subsystems, and pave its way for a map-reduce-flavor algorithm.

Conclusion

In this paper we provide a new way to compute all the conflicting problems occurring in a rule based system with chaining of rules. Our methods are rather general since they require a logic extending propositional logic and a decision procedure for its satisfiability. Existing methods rely either on testing or on formal verification but they are not suitable to find the exhaustive set of potential problems. Mixing symbolic manipulations and satisfiability, we provide a decidable enumerative approach to solve this problem but due to its exponential complexity we must provide optimizations. We study two optimizations in order to reduce the number of generated rules: an iterative method with a classification of rules and the use of the topological sorting to take the maximal advantage of relations between rule conclusions. As an evaluation we successfully apply our algorithm to a FOL rule system with more than forty rules. With this instance, rather than computing 2 47 new rules, we produce less than 1000 rules in less than 100s. Note that when the rule system is complex, it contains many relations between the predicates, and increases the risk of undefined requests. However, in this case our method, especially the sorting optimization, is particularly efficient. Our automatic method is able to handle middle size examples and more improvements are needed to solve larger examples in reasonable time. In our future work we expect to explore other practical optimizations, for instance by relaxing the relation of equivalence that we impose between the original rule system and its implementation. Another important research line will be to enrich our method with automatic or assisted ways to fix the detected problems.

Listing 1 . 3 .

 13 Part of abbreviated exclusive rules generated by our enumerative method for the example shown in Listing 1.1 And ( D ( R1 ) , Not ( D ( R2 )) , Not ( D ( R3 )) , Not ( D ( R4 )) , Not ( D ( R5 )) ) = > C ( R1 ) And ( D ( R1 ) , D ( R2 ) , Not ( D ( R3 )) , Not ( D ( R4 )) , Not ( D ( R5 )) ) = > And ( C ( R1 ) , C ( R2 ) ) And ( D ( R1 ) , D ( R2 ) , D ( R3 ) , Not ( D ( R4 )) , Not ( D ( R5 )) ) = > And ( C ( R1 ) , C ( R2 ) , C ( R3 )) ... Another 28 rules Listing 1.4. The first exclusive rule of Listing 1.3 in non-abbreviated form [1 , 0 , 0 , 0 , 0]And ( doctor ( h ) , nurse ( h )) , Not ( doctor ( h )) , Not ( And ( nurse ( h ) , Not ( sameward (h , p )))) , Not ( And ( doctor ( h ) , sameward (h , p ))) , Not ( chief ( h )) = > Not ( sameward (h , p ))

Fig. 1 .

 1 Fig. 1. Enumerative experiments

Fig. 2 .

 2 Fig. 2. Iterative experiments

Fig. 3 .Fig. 4 .

 34 Fig. 3. Sorting implementation

To improve readability, we simplify the actual output from our prototype in Listing 1.2. The complete output and our prototype can be found in https://github. com/atlanmod/ACP.

Efficiently characterizing the undefined requests of a rule-based system (on-line). https://github.com/atlanmod/ACP.git

http://cs.brown.edu/research/plt/software/margrave/versions/01-01/ examples/

RBAC and ARBAC policies for a small health care facility. http://www3.cs. stonybrook.edu/ ~stoller/ccs2007/


Jad Nassar
email: jad.nassar@yncrea@inria.fr

Nicolas Gouvy
email: nicolas.gouvy@yncrea.fr

Nathalie Mitton
email: nathalie.mitton@inria.fr

QoS-compliant Data Aggregation for Smart Grids

Keywords: Smart Grid, Data Aggregation, QoS, Wireless Sensor Networks

The Smart Grid (SG) aims to transform the current electric grid into a "smarter" network where the integration of renewable energy resources, energy efficiency and fault tolerance are the main benefits. A Wireless Sensor Network (WSN) controlling and exchanging messages across the grid is a promising solution because of its infrastructure free and ease of deployment characteristics. This comes at the cost of resource constrained and unstable links for such networks. The management of communication is then an issue: billions of messages with different sizes and priorities are sent across the network. Data aggregation is a potential solution to reduce loads on the communication links, thus achieving a better utilization of the wireless channel and reducing energy consumption. On the other hand, SG applications require different Quality of Service (QoS) priorities. Delays caused by data aggregation must then be controlled in order to achieve a proper communication. In this paper, we propose a work in progress, that consists of a QoS efficient data aggregation algorithm with two aggregation functions for the different traffics in a SG network. We expect to reduce the energy consumption while respecting the data delivery delays for the different SG applications.

I. INTRODUCTION

Wireless Sensor Networks (WSNs) are a potential candidate in the transition from the actual grid to the Smart Grid (SG), where the integration of renewable energy resources, energy efficiency and fault tolerance are the main benefits. On the other hand, WSNs are resource restrained entities with limited computing capabilities, even if in a SG electricity and energy exists, but connecting sensors to such high voltage with intermittent and ill-adapted energy levels is sometimes inappropriate. For that, battery-powered sensors must be deployed all over the grid alongside with the main-powered ones. This will raise a challenge in the data collection process, specially in a SG network where billions of packets with different sizes and priorities are frequently sent within the network. Data aggregation is a feasible paradigm that consists of combining data from multiple sensors across the network and sending the aggregated data to the base station. This will reduce loads on the communication links, thus achieving a better utilization of the wireless channel and reducing energy consumption. In a SG, different applications require different Quality of Service (QoS) priorities. Consequently, data aggregation must respect these requirements (i.e, delays caused by aggregating the packets) in order to ensure a proper communication. Therefore, in this paper, we propose a QoS efficient data aggregation algorithm for the different traffic in a SG network. The rest of the paper is organized as follows: Section II presents prior work on data aggregation in WSN. Section III describes our proposed solution. Section IV discusses some relevant issues about our proposal and expected results. Finally, section V concludes the paper.

II. RELATED WORKS

Many works addressed the data aggregation in WSNs and SGs. In [START_REF] Shiobara | Effective metering data aggregation for smart grid communication infrastructure[END_REF], two aggregation methods for processing data in smart meters were used: combining and manipulating. In the combining method, the concentrator removes all individual headers and includes only one single header for the large packet with no data modifications. The manipulating method consists of calculating the result of the messages thus reducing considerably the total size of the messages. Data packet concatenation in SGs was also addressed in [START_REF] Karimi | Scalable meter data collection in smart grids through message concatenation[END_REF], they achieved header compression on packets and formulated an optimization problem to optimally configure the sizes of the aggregated packets. However, they considered only overhead reduction, which may be insufficient alone in the presence of bigger data packets with smaller headers. Many other researches considered energy [START_REF] Uddin | Energy-aware optimal data aggregation in smart grid wireless communication networks[END_REF], delay guarantee [START_REF] Lee | On the capacity of smart grid wireless backhaul with delay guarantee and packet concatenation[END_REF] and other QoS requirements [5] [6] in data aggregation for SGs and sensor networks generally. However, none of these works addressed the challenge of having delay sensitive data traffic with different delivery priorities and sizes while reducing energy consumption and maximizing the available bandwidth.

III. PROPOSED SOLUTION

In our proposition, we consider a SG network consisting of several wireless sensors collecting data with different packet sizes and priorities. They can potentially act as aggregators, if they have enough resources, that receive the data and aggregate or concatenate it depending on their QoS requirements, and finally send the aggregated data across the network. We note that the routing process is mostly left unchanged, we only add the aggregation functionality when it is possible. Packets are generated with classifiers in their headers considering their type and criticality, we classify them into two levels: critical and regular. We note that these levels could be adjusted for other applications depending on the network characteristics. Two different queues are created on the aggregator level: Lossy and Lossless queue. The lossy queue contains delay insensitive data packets (regular) that are generally big in size [START_REF] Cam-Winget | Applicability statement for the routing protocol for low power and lossy networks (rpl) in ami networks[END_REF], which will allow us to aggregate the packets with the appropriate aggregation function [START_REF] Grabisch | Aggregation functions: means[END_REF]. The lossless queue contains delay sensitive data packets (critical) with critical priorities and with a header which represents a significant overhead compared to the payload size. Header compression is thus performed on the packets.

The proposed aggregation algorithm

In the following, we will explain the main functionality of the aggregation algorithm and its functions. The sender node sends and receives packets from other sensor nodes with different priorities included in their headers. Routes are constructed according to the existing routing protocol with no influence for the aggregation algorithm as already mentioned.

In figure 1 when an aggregator receives a packet it will firstly update its delivery time (Update_AD()) corresponding to the timestamp included in the header of the packet (maximum allowed delay) minus the time the packet spent to arrive to the aggregator. This will allow us to identify how much time the packet can stay in the aggregator. We store the value in the variable AD, we call it maximum allowed delay left. After that, the function Free_Space() will check whether the node can store more packets, and the function Battery_Node() will check whether the node has enough energy (more than a predefined threshold) to aggregate more packets. If these two conditions hold, we can aggregate packets and send the aggregated packets afterwards. If not, the packets are sent without aggregation. In the aggregate function, we check the Pkt_type and send it to the corresponding queue. If the packet is tagged regular, it is sent to the Lossy_Queue() (figure 2), where four conditions have to be validated in order to aggregate packets:

• Earliest_Deadline > Delivery_Threshold: aggregating if the packet with the earliest deadline in the aggregated packet is still within its allowed delay.

• AD > Delivery_Threshold: which means that the Delivery threshold from the aggregator to the sink must be smaller that the Maximum allowed delay left.

• AggrPktSize < MTU: aggregating as long the aggregated packet is smaller than the Maximum Transmission Unit (MTU) of the link.

• TTL > 0: If the above conditions were not valid yet and after a certain time we send the packet anyway on the link.

As long as these above conditions are valid, an arriving regular packet to the aggregator will undergo a lossy_aggregation(), and the timers are updated. Same applies for the Lossless_Queue() with a packet tagged critical. If not valid, we concatenate the incoming packet with the existing aggregated packet if possible and send it immediately. We note that the sink node will send back with the acknowledgment the time the packet spent from the aggregator to the sink in order to update the delivery threshold.

IV. DISCUSSION AND EXPECTED RESULTS

First of all aggregating packets will lead to less packets sent across the network and less bandwidth consumed, which will result in reducing the load on the communication links and achieving energy savings since the communication task consumes most of the energy in WSNs. Moreover, packets criticality and sizes are taken into consideration in our proposition. For that we expect that the packets will arrive within their deadlines, thanks to the different timers and thresholds across the network. We note that the delivery delays will be longer than a non aggregation scenario where packets are not stored in the queues. Packet delivery ratio might be affected also in our proposition, since aggregating means sending bigger packets thus resulting in more losses. We will deeply investigate this issue in order to mitigate these potential losses. Moreover, we will investigate in future works the impact of disaggregation at the destination node.

V. CONCLUSION In this paper, we propose a work in progress solution for data aggregation in SGs networks. QoS requirements of the different applications are taken into consideration by storing the packets in two different queues depending on their quality requirements. The expected results will reduce the energy consumption in a SG controlled by a WSN, while respecting the corresponding delays and QoS requirements. Several tests and investigations have to be performed (i.e, computer simulations) before the completion of this work, after that we will test our algorithm on a real test bed [START_REF] Adjih | Fit iot-lab: A large scale open experimental iot testbed[END_REF] to validate our theoretical approach.

Algorithm 1 :

 1 Aggregator node Update_AD() ; // AD= Maximum allowed delay -time from node to aggregator if Free_Space() AND Battery_Node > Threshold1 then Aggregate(); Send_AgPacket(); else Send_Packet(); end

Figure 1 .

 1 Figure 1. Aggregator node algorithm

Algorithm 2 :

 2 Lossy_Queue() Init: TTL if Earliest_Deadline > Delivery_Threshold AND AD > Delivery_Threshold AND AggrPktSize < MTU AND TTL > 0 then Lossy_Aggregation(); Update_Earliest_Deadline() ; // Earliest deadline in the aggregated packet TTL --; else Concatenate(); end

Figure 2 .

 2 Figure 2. Lossy queue algorithm

ACKNOWLEDGMENT

This work was partially funded by a grant from the MEL (Métropole Européenne de Lille), the SoMel SoConnected project (Ademe, PIA2), Yncréa Haut-de-France and CPER Data.


Anne Postec
email: annepostec@univ-amu.fr

Bernard Ollivier

Marie-Laure Fardeau

Objection to the proposition of the new genus Abyssivirga

Keywords:

Objection to the proposition of the new genus Abyssivirga Anne Postec,* Bernard Ollivier and Marie-Laure Fardeau

We have read with interest the recent paper published by Schouw et al. [START_REF] Schouw | Abyssivirga alkaniphila gen. nov., sp. nov., an alkanedegrading, anaerobic bacterium from a deep-sea hydrothermal vent system, and emended descriptions of Natranaerovirga pectinivora and Natranaerovirga hydrolytica[END_REF] in IJSEM (Vol 66, pp. 1724-1734) entitled: 'Abyssivirga alkaniphila gen. nov., sp. nov., an alkanedegrading, anaerobic bacterium from a deep-sea hydrothermal vent system, and emended descriptions of Natranaerovirga pectinivora and Natranaerovirga hydrolytica'.

We disagree with the proposal of Abyssivirga as a new genus due to phylogenetic considerations as shown below. Indeed, we noticed that a BLAST analysis of the Abyssivirga alkaniphila 16S rRNA gene sequence indicated 99.4 % similarity with Vallitalea guaymasensis isolated from sediments of the Guaymas Basin, and 96.1 % with Vallitalea pronyensis isolated from a hydrothermal chimney in Prony Bay. Both Vallitalea species have been fully characterized in IJSEM [START_REF] Lakhal | Vallitalea guaymasensis gen. nov., sp. nov., isolated from marine sediment[END_REF][START_REF] Aissa | Vallitalea pronyensis sp. nov., isolated from a marine alkaline hydrothermal chimney[END_REF].

Based on phylogenetic analyses, we believe that the proposal of the new genus Abyssivirga should be reconsidered. A. alkaniphila should be reassigned to the genus Vallitalea, and possibly as a novel species, 'Vallitalea alkaniphila', if demonstrated by significant DNA-DNA hybridization and phenotypic differences.

With the aim to clearly establish the phylogenetic position of A. alkaniphila and its effective affiliation to the genus Vallitalea, a phylogenetic tree is reconstructed here (Fig. 1).

Lachnospiraceae

Fig. 1 .

 1 Fig.1. Phylogenetic tree showing the position of Abyssivirga alkaniphila L81 T with the type strains of the closest described species. The neighbour-joining method was used, with Kimura's two-parameter model. Bootstrap values below 70 are not shown (from 1000 replicates). In total, 1211 positions were used in the final dataset. Bar, 0.02 changes per position.