Automated Verification of Security Chains in Software-Defined Networks with Synaptic

Nicolas Schnepf 1, 2 Rémi Badonnel 1 Abdelkader Lahmadi 1 Stephan Merz 2
1 MADYNES - Management of dynamic networks and services
Inria Nancy - Grand Est, LORIA - NSS - Department of Networks, Systems and Services
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by Satisfiability Modulo Theories (SMT) solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.
Type de document :
Communication dans un congrès
NetSoft 2017 - IEEE Conference on Network Softwarization, Jul 2017, Bologna, Italy. IEEE Computer Society, pp.1-9, 2017, 〈10.1109/NETSOFT.2017.8004195〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01630806
Contributeur : Stephan Merz <>
Soumis le : mercredi 8 novembre 2017 - 11:19:56
Dernière modification le : vendredi 10 novembre 2017 - 01:04:41

Fichier

camera-ready.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz. Automated Verification of Security Chains in Software-Defined Networks with Synaptic. NetSoft 2017 - IEEE Conference on Network Softwarization, Jul 2017, Bologna, Italy. IEEE Computer Society, pp.1-9, 2017, 〈10.1109/NETSOFT.2017.8004195〉. 〈hal-01630806〉

Partager

Métriques

Consultations de la notice

47

Téléchargements de fichiers

4