Automatically deploying distributed Access Control Lists (ACLs) in a software-defined network can ensure their internal services and hosts connectivity, security and reliability. ACLs are often deployed in a switch using Ternary ContentAddressable Memory (TCAM). Since TCAM memory is often too limited to store a large ACL, one has to split the lists and distribute the parts on several switches in such a way that every packet travelling from a source to a destination undergoes the required match-action rules. In this paper, we develop and compare three algorithms based on graph theory and Reinforcement Learning (RL) techniques to automatically distribute ACLs across networks switches, while minimizing their TCAM memory occupancy. We compare the three algorithms on several network topologies to evaluate their efficiency in terms of memory occupancy.

Software Defined Networks (SDN) heavily rely on diverse management rules (ACL, traffic control, etc. ) to satisfy security and business requirements of their associated services. As these networks are increasing in size and complexity, their management rules configured in devices are becoming more complex. These rules are constantly growing in size and it is challenging to distribute them across network devices with limited capacities. The most challenging task is to deploy rules updates in a fast and efficient way to avoid a security breach or to meet a service needs. In this paper, we extend our previous work on network management rules distribution by introducing an efficient update strategy. Through extensive experiments on several rule sets with single and multiple path topologies, we evaluate and analyze the performance of our strategy. Our obtained results show a reduction of up to 90% in update time.

Socia1 media data has been mined over the years to predict individual sensitive attributes such as political and religious beliefs. Indeed, mining such data can improve the user experience with personalization and freemium services. Still, it can also be harmful and discriminative when used to make critical decisions, such as employment. In this work, we investigate social media privacy protection against attribute inference attacks using machine learning explainability and adversarial defense strategies. More precisely, we propose FOX (FOoling with eXplanations), an adversarial attack framework to explain and fool sensitive attribute inference models by generating effective adversarial reactions. We evaluate the performance of FOX with other SOTA baselines in a black-box setting by attacking five gender attribute classifiers trained on Facebook pictures reactions, specifically (i) comments generated by Facebook users excluding the picture owner, and (ii) textual tags (i.e., alttext) generated by Facebook. Our experiments show that FOX successfully fools (about 99.7% and 93.2% of the time) the classifiers, outperforms the SOTA baselines and gives a good transferability of adversarial features.

Software Defined Networks administrators can specify and smoothly deploy abstract network-wide policies. The rule sets of these policies are deployed in the forwarding tables of the available switches. In this paper, we propose a technique, named R2-D2, for decomposing and distributing a rule set on network switches of limited flow tables size, while preserving the network policy semantics. Through experiments on several rule sets with single dimension, we evaluate and analyse the performance of our rule decomposition techniques. Our results show that our technique is efficient in practice compared to existing techniques.

Software Defined Networks administrators can specify and smoothly deploy abstract network-wide policies, and then the controller acting as a central authority implements them in the flow tables of the network switches. The rule sets of these policies are specified in the forwarding tables, which are usually accessed using very expensive and power-hungry ternary content-addressable memory (TCAM). Consequently, a given table can only contain a limited number of rules. However, various applications need large rule sets to perform filtering on diverse flows. In this paper, we propose several algorithms for decomposing and distributing a rule set on network switches of limited flow tables size, while preserving the network policy semantics. Through experiments on several rule sets with single and multiple dimensions, we evaluate and analyse the performance of our rule placement techniques. Our results show that our proposals are efficient in practice.

Packet filtering is widely used in multiple networking applications, including firewalls, intrusion detection systems, routers and load balances, to decide whether to accept or deny an incoming packet. This mechanism relies on packet's header fields to filter such traffic by using range rules of IP addresses or ports. However, the set of packet filters has to handle a growing number of connected nodes and many of them are compromised and used as sources of attacks. For instance, IP filter sets available in blacklists may reach several millions of entries, and may require large memory space for their storage in filtering appliances. In this paper, we propose a new method based on a double mask IP prefix representation associated to a linear transformation algorithm to build a reduced set of range rules. Our experiments show that the proposed method achieves a reduction ratio of up to 74% on synthetic range rule sets.

The problem of private publication of graph data has attracted a lot of attention recently. The prevalence of differential privacy makes the problem more promising. However, a large body of existing works on differentially private release of graphs have not answered the question about the upper bounds of privacy budgets. In this paper, for the first time, such a bound is provided. We prove that with a privacy budget of O(log n), there exists an algorithm capable of releasing a noisy output graph with edge edit distance of O(1) against the true graph. At the same time, the complexity of our algorithm Top-m Filter is linear in the number of edges m. This lifts the limits of the state-of-the-art, which incur a complexity of O(n2) where n is the number of nodes and runnable only on graphs having n of tens of thousands.

Rather than anonymizing social graphs by generalizing them to super nodes/edges or adding/removing nodes and edges to satisfy given privacy parameters, recent methods exploit the semantics of uncertain graphs to achieve privacy protection of participating entities and their relationships. These techniques anonymize a deterministic graph by converting it into an uncertain form. In this paper, we propose a general obfuscation model based on uncertain adjacency matrices that keep expected node degrees equal to those in the unanonymized graph. We analyze two recently proposed schemes and their fitting into the model. We also point out disadvantages in each method and present several elegant techniques to fill the gap between them. Finally, to support fair comparisons, we develop a new tradeoff quantifying framework by leveraging the concept of incorrectness. Experiments on large social graphs demonstrate the effectiveness of our schemes.

Summary In recent years, important efforts have been made for offering a dedicated language for modelling and verifying security protocols. Outcome of the European project AVISPA, the high‐level security protocol language (HLPSL) aims at providing a means for verifying usual security properties (such as data secrecy) in message exchanges between agents. However, verifying the security protocol model does not guarantee that the actual implementation of the protocol will fulfil these properties. This article presents a model‐based testing approach, relying on the mutation of HLPSL models to generate abstract test cases. The proposed mutations aim at introducing leaks in the security protocols and represent real‐world implementation errors. The mutated models are then analysed by the automated validation of Internet security protocols and applications tool set, which produces, when the mutant protocol is declared unsafe, counterexample traces exploiting the security flaws and, thus, providing test cases. A dedicated framework is then used to concretize the abstract attack traces, bridging the gap between the formal model level and the implementation level. This model‐based testing technique has been experimented on a wide range of security protocols, in order to evaluate the mutation operators. This process has also been fully tool‐supported, from the mutation of the HLPSL model to the concretization of the abstract test cases into test scripts. It has been applied to a realistic case study of the Paypal payment protocol, which made it possible to discover a vulnerability in an implementation of an e‐commerce framework. Copyright © 2014 John Wiley & Sons, Ltd.

It is increasingly common to find XML views used to enforce access control as found in many applications and commercial database systems. To overcome the overhead of view materialization and maintenance, XML views are necessarily virtual. With this comes the need for answering XML queries posed over virtual views, by rewriting them into equivalent queries on the underlying documents. A major concern here is that query rewriting for recursive XML views is still an open problem, and proposed approaches deal only with non-recursive XML views. Moreover, a small number of works have studied the access rights for updates. In this paper, we present SVMAX (Secure and Valid MAnipulation of XML), the first system that supports specification and enforcement of both read and update access policies over arbitrary XML views (recursive or non). SVMAX defines general and expressive models for controlling access to XML data using significant class of XPath queries and in the presence of the update primitives of W3C XQuery Update Facility. Furthermore, SVMAX features an additional module enabling efficient validation of XML documents after primitive updates of XQuery. The wide use of W3C standards makes of SVMAX a useful system that can be easily integrated within commercial database systems as we will show. We give extensive experimental results, based on real-life DTDs, that show the efficiency and scalability of our system.

This paper describes the design and implementation of a Decentralized Shared Calendar (abbreviated as DeSCal), a distributed application which provides users a decentralized infrastructure to share their calendar events with selected users in a dynamic group. Although being a distributed application, DeSCal is as responsive as a personal calendar. It achieves this high responsiveness by keeping a local copy of the shared calendar at each participating user. Consistency of these replicated copies of the shared calendar is carried out in a decentralized fashion using Operational Transformation (OT) approach. OT allows users to concurrently modify the shared calendar and exchange their updates in any order since it ensures the convergence of copies of the shared calendar in all cases. To prevent unauthorized access by illegal users, DeSCal is endowed with access control mechanism on the local copy of the shared calendar. It employs a flexible access control model based on replicating the access data-structure at each user site to overcome the latency problem. Also, access control on the shared calendar events is dynamic i.e. users are able to change the access rights on their shared calendar events at any point of time after the creation of an event. In short, DeSCal is totally decentralized, scalable and self-configurable i.e., no need of a third party to manage it.

We address the insecurity problem for cryptographic protocols, for an active intruder and a bounded number of sessions. The protocol steps are modeled as rigid Horn clauses, and the intruder abilities as an equational theory. The problem of active intrusion -- such as whether a secret term can be derived, possibly via interaction with the honest participants of the protocol -- is then formulated as a Cap Unification problem. Cap Unification is an extension of Equational Unification: look for a cap to be placed on a given set of terms, so as to unify it with a given term modulo the equational theory. We give a decision procedure for Cap Unification, when the intruder capabilities are modeled as homomorphic encryption theory. Our procedure can be employed in a simple manner to detect attacks exploiting some properties of block ciphers.

Many decision problems on security protocols can be reduced to solving so-called intruder constraints in Dolev Yao model. Most constraint solving procedures for protocol security rely on two properties of constraint systems called monotonicity and variable-origination. In this work we relax these restrictions by giving an NP decision procedure for solving general intruder constraints (that do not have these properties). Our result extends a first work by L. Mazaré in several directions: we allow non-atomic keys, and an associative, commutative and idempotent symbol (for modeling sets). We also give several new applications of the result.

We propose a model for XML update primitives of the W3C XQuery Update Facility as parameterized rewriting rules of the form: "insert an unranked tree from a regular tree language L as the first child of a node labeled by a". For these rules, we give type inference algorithms, considering types defined by several classes of unranked tree automata. These type inference algorithms are directly applicable to XML static typechecking, which is the problem of verifying whether, a given document transformation always converts source documents of a given input type into documents of a given output type. We show that typechecking for arbitrary sequences of XML update primitives can be done in polynomial time when the unranked tree automaton defining the output type is deterministic and complete, and that it is EXPTIME-complete otherwise.

We present some decidability results for the universal fragment of theories modeling data structures and endowed with arithmetic constraints. More precisely, all the theories taken into account extend a theory that constrains the function symbol for

Cryptographic protocols are crucial for securing electronic transactions. The confidence in these protocols can be increased by the formal analysis of their security properties. Although many works have been dedicated to standard protocols like Needham-Schroeder very few address the more challenging class of group protocols. We have introduced in previous work a synchronous model for group protocols, that generalizes standard protocol models by permitting unbounded lists inside messages. This approach also applies to analyzing Web services manipulating sequences of items. In this model we propose now a decision procedure for the sub-class of well-tagged protocols with autonomous keys.

The recent and massive deployment of Voice over IP infrastructures had raised the importance of the VoIP security and more precisely of the underlying signalisation protocol SIP. In this paper, we will present a new attack against the authentication mechanism of SIP. This attack allows to perform toll fraud and call hijacking. We will detail the formal specification method that allowed to detect this vulnerability, highlight a simple usage case and propose a mitigation technique.

We show that the insecurity problem for protocols with modular exponentiation and arbitrary products allowed in exponents is NP-complete. This result is based on a protocol and intruder model which is powerful enough to uncover known attacks on the Authenticated Group Diffie-Hellman (A-GDH.2) protocol suite. To prove our results, we develop a general framework in which the Dolev-Yao intruder is extended by generic intruder rules. This framework is also applied to obtain complexity results for protocols with commuting public key encryption.

Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data s. Reachability-based secrecy means that s should never be disclosed while equivalence-based secrecy states that two executions of a protocol with distinct instances for s should be indistinguishable to an attacker. Although the second formulation ensures a higher level of security and is closer to cryptographic notions of secrecy, decidability results and automatic tools have mainly focused on the first definition so far. This paper initiates a systematic investigation of the situations where syntactic secrecy entails strong secrecy. We show that in the passive case, reachability-based secrecy actually implies equivalence-based secrecy for digital signatures, symmetric and asymmetric encryption provided that the primitives are probabilistic. For active adversaries, we provide sufficient (and rather tight) conditions on the protocol for this implication to hold.

Formal methods have proved to be very useful for analyzing cryptographic protocols. However, most existing techniques apply to the case of abstract encryption schemes and pairing. In this paper, we consider more complex, less studied cryptographic primitives like CBC encryption and blind signatures. This leads us to introduce a new fragment of Horn clauses. We show decidability of this fragment using a combination of several resolution strategies.As a consequence, we obtain a new decidability result for a class of cryptographic protocols (with an unbounded number of sessions and a bounded number of nonces) that may use for example CBC encryption and blind signatures. We apply this result to fix the Needham-Schroeder symmetric key authentication protocol, which is known to be flawed when CBC mode is used.

We provide a method for deciding the insecurity of cryptographic protocols in presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we ascertain that protocol insecurity is in NP for an intruder that can exploit the properties of the XOR operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. An immediate consequence of our proof is that checking whether a message can be derived by an intruder (using XOR) is in P. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).

replace me

Colloque avec actes et comité de lecture. internationale.

A term rewrite system (TRS) terminates if its rules are contained in a reduction ordering >. In order to deal with any set of equations, including inherently non-terminating ones (like commutativity), TRS have been generalised to ordered TRS (E, >), where equations of E are applied in whatever direction agrees with >. The confluence of terminating TRS is well-known to be decidable, but for ordered TRS the decidability of confluence has been open. Here we show that the confluence of ordered TRS is decidable if ordering constraints for > can be solved in an adequate way, which holds in particular for the class of LPO orderings. For sets E of constrained equations, confluence is shown to be undecidable. Finally, ground reducibility is proved undecidable for ordered TRS.

Proofs by induction arc important in many computer science and artificial intelligence applications, in particular, in program verification and specification systems. We present a new method to prove (and disprove) automatically inductive properties. Given a set of axioms, a well-suited induction scheme is constructed automatically. We call such an induction scheme a test set. Then, for proving a property, we just instantiate it with terms from the test set and apply pure algebraic simplification to the result. This method needs no completion and explicit induction. However it retains their positive features, namely, the completeness of the former and the robustness of the latter. It has been implemented in the theorem-prover SPIKE.

It is shown that unifiability is decidable in theories presented by a set of ground equations with several associative-communicative symbols (ground AC theories). This result applies, for instance, to finitely presented commutative semigroups, and it extends the authors' previous work (P. Narendran and M. Rusinwithch, 1991) where they gave an algorithm for solving the uniform word problem in ground AC theories.>

Much research has been devoted to diagnosis, where two main approaches have been pointed out: the empirical association-based diagnostic approach and the model-based diagnostic one. Both approaches can be characterized by the kind of knowledge that has to be specified and the diagnostic method that has to be used. However, it seems particularly difficult in real-world applications to obtain a complete description of the faulty (dually, correct) behavior of a system. This incompleteness of description is the reason why deductive reasoning alone is generally insufficient to point out the actual diagnosis. Deduction only allows one to generate some possible partial diagnoses. The latter must be selected and completed to get closer to the actual diagnosis. Both selection and completion require hypothetical reasoning and can be characterized by some preference criteria. The authors' contribution is twofold. A new diagnostic method based on deduction and abduction is then proposed, which is sufficiently flexible to deal with multiple knowledge representations.>

In this paper, a proof method based on a notion of transfinite semantic trees is presented and it is shown how to apply it to prove the completeness of refutational theorem proving methods for first order predicate calculus with equality.To demonstrate how this method is used, the completeness of two theorem-proving strategies, both refinements of resolution and paramodulation, are proved.Neither of the strategies need the functionally reflexive axioms nor paramodulating into variables.Therefore the Wos-Robinson conjecture follows as a corollary.Another strategy for Horn logic with equality is also presented.