, Nos trois critères d'optimisation sont antagonistes : minimiser l'utilisation du réseau conduit à grouper les règles sur quelques switches et donc à maximiser la congestion du service et sa probabilité de disponibilité. Pour gérer ce problème nous calculons le front de Pareto représentant l

, Automated Verification of Security Chains in Software-Defined Networks with Synaptic, Nous reprenons ici les publications internationales résultant de notre travail de thèse, nous les citons par ordre chronologique : -Nicolas Schnepf, Stephan Merz, Rémi Badonnel, and Abdelkader Lahmadi, vol.6, 2017.

-. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, Towards Generation of SDN Policies for Protecting Android Environments based on Automata Learning, Proceedings of the 16th Network Operations and Management Symposium (IEEE/IFIP NOMS'18), 2018.

-. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, Synaptic : a Formal Checker for SDN-based Security Policies, Proceedings of the 16th Network Operations and Management Symposium (IEEE/IFIP NOMS'18), 2018.
URL : https://hal.archives-ouvertes.fr/hal-01892397

-. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks, Proceedings of the 18th International Workshop on Automated Verification of Critical Systems (AVOCS'18), 2018.
URL : https://hal.archives-ouvertes.fr/hal-01892423

, Automated Factorization of Security Chains in Software-Defined Networks, Réponses apportées à la problématique -Nicolas Schnepf, Stephan Merz, Rémi Badonnel, and Abdelkader Lahmadi, 2019.

-. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, A Tool Suite for the Automated Synthesis of Security Function Chains, Proceedings of the 16th IFIP/IEEE Symposium on Integrated Network and Service Management, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02111658

, Réponses apportées à la problématique

, Android permissions's system

, Configuration Analysis and Verification of Federated OpenFlow Infrastructures, Proceedings of the 3rd ACM Workshop on Assurable and Usable Security Configuration (CCS'10), 2010.

S. Ehab, H. H. Al-shaer, and . Hamed, Discovery of Policy Anomalies in Distributed Firewalls, Proceedings of the Twenty-third Annual Joint Conference of the IEEE Computer and Communications (INFOCOM'04), 2004.

R. Alur, R. Bodík, G. Juniwal, M. M. Martin, M. Raghothaman et al., Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis, FMCAD, pp.1-8, 2013.

D. Angluin, Learning regular sets from queries and counterexamples, Inf. Comput, vol.75, issue.2, pp.87-106, 1987.

J. Antunes, N. Neves, and P. Verissimo, Reverse engineering of protocols from network traces, Proceedings of the 2011 18th Working Conference on Reverse Engineering, WCRE '11, pp.169-178, 2011.

J. Irina-mariuca-asavoae, T. M. Blasco, . Chen, I. Harsha-kumara-kalutarage, and . Muttik, Hoang Nga Nguyen, Markus Roggenbach, and Siraj Ahmed Shaikh. Towards automated android app collusion detection, Proc. 1st Intl. Wsh. Innovations in Mobile Privacy and Security (IMPS 2016), volume 1575 of CEUR Workshop Proceedings, pp.29-37, 2016.

, smtlib, the satisfiability modulo theory library

Z. Ayyub and R. Miao, Simple-fying middlebox policy enforcement using sdn, ACM SIGCOMM Computer Communication Review, 2013.

M. Backes, S. Bugiel, E. Derr, P. Mcdaniel, D. Octeau et al., On demystifying the android application framework : re-visiting android permission specification analysis, Proceedings of the 25th USENIX Security Symposium (NSDI 2016), 2016.

T. Ball, N. Bjørner, A. Gember, S. Itzhaky, A. Karbyshev et al., Vericon : Towards Verifying Controller Programs in Software-Defined Networks, Proc. 35th ACM SIGPLAN Intl. Conf. Programming Language Design (PLDI'14), pp.282-293, 2014.

C. W. Barrett, D. L. Dill, and J. R. Levitt, A decision procedure for bit-vector arithmetic, Proceedings of the 35th Annual Design Automation Conference, DAC '98, pp.522-527, 1998.

C. W. Barrett, R. Sebastiani, A. Sanjit, C. Seshia, and . Tinelli, Satisfiability modulo theories, Handbook of Satisfiability, vol.185, pp.825-885, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

D. Barthel, K. Vasseur, M. Pister, N. Kim, and . Dejean, Routing Metrics Used for Path Calculation in Low-Power and Lossy Networks, RFC, vol.6551, 2012.

R. Beckett, Network Control Plane Synthesis and Verification, 2018.

I. Beschastnikh, J. Abrahamson, Y. Brun, and M. D. Ernst, Synoptic : Studying Logged Behavior with Inferred Models, Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, ESEC/FSE '11, pp.448-451, 2011.

I. Beschastnikh, Y. Brun, J. Abrahamson, M. D. Ernst, and A. Krishnamurthy, Using Declarative Specification to Improve the Understanding, Extensibility, and Comparison of Model-Inference Algorithms, IEEE Transactions on Software Engineering, vol.41, pp.408-428, 2015.

I. Beschastnikh, Y. Brun, M. D. Ernst, and A. Krishnamurthy, Inferring models of concurrent systems from logs of their behavior with csight, Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, pp.468-479, 2014.

A. Biere, M. Heule, T. Hans-van-maaren, and . Walsch, Handbook of satisfiability, 2008.

A. W. Biermann and J. A. Feldman, On the Synthesis of Finite-State Machines from Samples of Their Behavior, IEEE Transactions on Computers, 1972.

N. Bjorner, A. Phan, and L. Fleckenstein, vz -an optimizing smt solver, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol.9035, pp.194-199, 2015.

J. Blendin, J. Rückert, N. Leymann, G. Schyguda, and D. Hausheer, Position paper : software defined network services chaining, Proceedings of the Third European Workshop on Software Defined Networks (EWSDN 2014), 2014.

W. Scott, B. E. Brim, and . Carpenter, Middleboxes : Taxonomy and Issues, RFC, vol.3234, 2002.

M. Canini, D. Venzano, P. Pereskini, D. Kostic, and R. Jennifer, A Nice Way to Test OpenFlow Applications, Proceedings of the 9th USENIX conference on Networked Systems Design and Implementation (NSDI'12), 2012.

C. Rafael, J. Carrasco, and . Oncina, Learning stochastic regular grammars by means of a state merging method, 2nd Intl. Coll. Grammatical Inference and Applications (ICGI-94), vol.862, 1994.

N. M. Mosharaf-kabir-chowdhury and R. Boutaba, A survey of network virtualization, Comput. Netw, vol.54, issue.5, pp.862-876, 2010.

B. Claise, Specification of the IP Flow Information Export (IPFIX) Protocol for the Exchange of IP Traffic Flow Information, RFC, vol.5101, 2008.

B. Claise, Cisco Systems NetFlow Services Export Version 9, vol.3954, 2004.

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst, vol.8, issue.2, pp.244-263, 1986.

E. M. Clarke, The birth of model checking, 25 Years of Model Checking, vol.5000, pp.1-26, 2008.

J. Cui, W. Kannan, and H. Wang, Discoverer : Automatic protocol reverse engineering from network traces, Proceedings of the 16th USENIX Security Symposium, 2017.

S. Dai, A. Tongaonkar, X. Wang, A. Nucci, and D. Song, Networkprofiler : Towards automatic fingerprinting of android apps, Proceedings of IEEE InfoCom 2013 (INFOCOM 2013), 2013.

G. B. Dantzig, Linear programming and extensions. Rand Corporation Research Study, 1963.

G. B. Dantzig, A history of scientific computing. chapter Origins of the Simplex Method, pp.141-151, 1990.

S. Das, C. Michael, and . Mozer, A unified gradient-descent/clustering architecture for finite state machine induction, Advances in Neural Information Processing Systems, vol.6, pp.19-26, 1994.

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Commun. ACM, vol.5, issue.7, pp.394-397, 1962.

M. Davis and H. Putnam, A computing procedure for quantification theory, J. ACM, vol.7, issue.3, pp.201-215, 1960.

J. Dilip and S. Ion, Modeling middle boxes, IEEE Network : The Magazine of Global Internetworking archive, 2008.

P. Faruki, A. Bharmal, V. Laxmi, V. Ganmoor, M. S. Gaur et al., Android Security, a Survey of Issues, Malware Penetrations and Defenses, IEEE Communications Surveys & Tutorials, 2015.

K. Seyed, V. Fayaz, and . Sekar, Testing Stateful and Dynamic Data Plane with FlowTest, Proceedings of the third Workshop on Hot Topics in Software-Defined Networking (HotSDN'14), 2014.

N. Feamster and H. Kim, Software-Defined Networks : Improving Network Management with SDN, IEEE Communications Magazine, 2013.

N. Feamster, J. Rexford, and E. Zegura, The Road to SDN, an Intellectual History of Programmable Networks, SIGCOMM Computer Communication Review, vol.44, issue.2, pp.87-98, 2014.

V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker, Automated verification techniques for probabilistic systems, Formal Methods for Eternal Networked Software Systems (SFM'11), vol.6659, pp.53-113, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00648037

N. Foster, M. J. Freedman, A. Guha, R. Harrison, C. Naga-praveen-kata et al., Languages for Software-Defined Networks, Software Technology Group, 2016.

N. Foster, M. J. Freedman, R. Harrison, C. Monsanto, and D. Walker, Frenetic, a Network Programming Language, Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP'11), 2011.

N. Foster, J. Mcclurg, H. Hojjat, and P. Cerny, Efficient Synthesis of Network Updates, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), 2015.

N. Foster, C. Monsanto, J. Reich, R. Jennifer, and D. Walker, Composing software defined networks, Proceedings of the 10th USENIX conference on Networked Systems Design and Implementation (NSDI 2013), 2013.

J. François, L. Dolberg, O. Festor, and T. Engel, Network Security through Software Defined Networking : a Survey, IIT Real-Time Communications (RTC) Conference -Principles, Systems and Applications of IP Telecommunications (IPTComm), 2014.

S. García, M. Grill, J. Stiborek, and A. Zunino, An empirical comparison of botnet detection methods, Comput. Secur, vol.45, pp.100-123, 2014.

, GData. Mobile malware report, 2018.

A. Gorla, I. Tavecchia, F. Gross, and A. Zeller, Checking app behavior against app description, Proceedings of international Conference of Software Engineering (ICSE 2014), 2014.

J. Mark and . Handley, Eric Rescorla, and Internet Architecture Board. Internet Denial-of-Service Considerations, RFC, vol.4732, 2006.

L. Frank and . Hitchcock, The distribution of a product from several sources to numerous localities, Journal of Mathematics and Physics, vol.20, issue.1-4, pp.224-230, 1941.

A. Horn, On sentences which are true of direct unions of algebras, J. Symb. Log, vol.16, issue.1, pp.14-21, 1951.

H. Hu, W. Han, G. J. Ahn, and Z. Zhao, Flowgard : building robust firewalls for software defined networks, Proceedings of the third workshop on Hot topics in software defined networking (SIGCOMM 2014), 2014.

G. Hurel, R. Badonnel, A. Lahmadi, and O. Festor, Behavioral and Dynamic Security Functions Chaining for Android Devices, Proceedings of the 11th IFIP/IEEE/ACM SIGCOMM International Conference on Network and Service Management (CNSM'15), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01231173

G. Hurel, R. Badonnel, A. Lahmadi, and O. Festor, Towards Cloud Based Compositions of Security Functions for Mobile Devices, IFIP/IEEE International Symposium on Integrated Network Management (IM'15), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01093041

M. Kang, J. Choi, I. Kang, H. H. Kwak, S. J. Ahn et al., A Verification Method of SDN Firewall Applications, IEICE Transactions on Communications, 2016.

L. V. Kantorovich, Mathematical methods of organizing and planning production, Manage. Sci, vol.6, issue.4, pp.366-422, 1960.

A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P. Brighten, VeriFlow : Verifying Network-wide Invariants in Real Time, Proceedings of the first Workshop on Hot Topics in Software-Defined Networks (HotSDN'12), 2012.

C. Kilinc, T. Booth, and K. Andersson, Walldroid : cloud assisted virtualized application specific firewalls for the android os, Proceedings of IEEE 11th International Conference on Trust, Security and Privacy in Computing and Communications (TRUSTCOM 2012), 2012.

H. Kim, J. Reich, A. Gupta, M. Shahbaz, N. Feamster et al., Kinetic : Verifiable Dynamic Network Control, Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation (NSDI'15), 2015.

J. Kim, H. Choi, H. Namkung, W. Choi, B. Choi et al., Enabling automatic protocol behavior analysis for android applications, Proceedings of the 12th International on Conference on Emerging Networking EXperiments and Technologies, CoNEXT '16, pp.281-295, 2016.

J. Kronqvist, D. E. Bernal, A. Lundell, and I. E. Grossmann, A review and comparison of solvers for convex minlp, 2018.

H. Kuai, F. Alajaji, and G. Takahara, A lower bound on the probability of a finite union of events, Discrete Math, vol.215, issue.1-3, pp.147-158, 2000.

F. Mariantonietta-la-polla, D. Martinelli, and . Sgandurra, A Survey on Security for Mobile Devices, IEEE Communications Surveys & Tutorials, 2012.

A. Lahmadi, F. Beck, E. Finickel, and O. Festor, A platform for the analysis and visualization of network flow data of android environments, IFIP/IEEE International Symposium on Integrated Network Management (IM), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01242911

T. Liang, A. Reynolds, N. Tsiskaridze, C. Tinelli, C. Barrett et al., An efficient smt solver for string constraints, Form. Methods Syst. Des, vol.48, issue.3, pp.206-234, 2016.

A. O. Adetokunbo, A. Makanju, E. E. Zincir-heywood, and . Milios, Clustering event logs using iterative partitioning, Proceedings of the 15th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD '09, pp.1255-1264, 2009.

S. Gary, T. Malkin, and . Parker, Internet Users' Glossary. RFC 1392, 1993.

E. Mariconti, L. Onwuzurike, P. Andriotis, E. De-cristofaro, G. J. Ross et al., Mamadroid : Detecting android malware by building markov chains of behavioral models, 2016.

N. Mckeown and G. Parulkar, openflow, enabling innovation in campus networks, ACM SIGCOMM Computer Communication Review, 2008.

D. Miller and G. Nadathur, Programming with Higher-Order Logic, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

S. Nain and M. Y. Vardi, Branching vs. linear time : Semantical perspective, Proceedings of the 5th International Conference on Automated Technology for Verification and Analysis, ATVA'07, pp.19-34, 2007.

R. Neisse, G. Steri, and G. Baldini, Enforcement of security policy rules for the internet of things, Proceedings of the 10th IEEE International Conference on Wireless and Mobile Computing, Networking and Communications (WiMob'14), 2014.

J. Oberheide, K. Veeraraghavan, E. Cooke, J. Flinn, and F. Jahanian, Virtualized incloud security services for mobile devices, Proceedings of the First Workshop on Virtualization in Mobile Computing, MobiVirt '08, pp.31-35, 2008.

J. Oberheide, K. Veeraraghavan, E. Cooke, J. Flinn, and F. Jahanian, Virtualized incloud security services for mobile devices, Proceedings of the first workshop on virtualization in mobile computing (MOBIVIRT 2008), 2008.

F. Andrés, J. Ocampo, P. H. Gil-herrera, M. C. Isolani, J. F. Neves et al., Optimal Service Function Chain Composition in Network Functions Virtualization, Proceedings of the IFIP International Conference on Autonomous Infrastructure, Management and Security (IFIP AIMS'17), pp.62-76, 2017.

T. Ohmann, M. Herzberg, S. Fiss, A. Halbert, M. Palyart et al., Behavioral resource-aware model inference, Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE '14, pp.19-30, 2014.

A. Porter-felt, E. Chin, S. Hanna, D. Song, and D. Wagner, Android permission demystified, dings of the 18th ACM conference on Computer and communications security, 2011.

C. Prakash, J. Lee, Y. Turner, J. Kang, A. Akllia et al., Pga : using graphs to express and automatically reconcile network policies, Proceedings of the 2015 ACM Conference on Special Interest Group on Data communication (SIGCOMM 2015), 2015.

J. Ren, A. Rao, M. Lindorfer, A. Legout, and D. R. Choffnes, Recon : Revealing and controlling privacy leaks in mobile network traffic, 2015.

J. A. Robinson, A machine-oriented logic based on the resolution principle, J. ACM, vol.12, issue.1, pp.23-41, 1965.

F. Rossi, T. Peter-van-beek, and . Walsh, Handbook of Constraint Programming, 2006.

A. Rozinat, M. Veloso, and W. M. Van-der-aalst, Evaluating the Quality of Discovered Process Models, Proceedings of the ECML-PKDD Workshop on Induction of Process Models (IPM08), pp.45-52, 2008.

A. Sapio, M. Liao, Y. , G. Ranjan, F. Risso et al., Per-user policy enforcement on mobile apps through network virtualization, Proceedings of the 9th ACM workshop on Mobility in the evolving internet (MOBIARCH 2014), 2014.

N. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, Automated Verification of Security Chains in Software-Defined Networks with Synaptic, Proceedings of the 3rd IEEE Conference on Network Softwarization (NetSoft'17), Acceptance Rate of 18.6%, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01630806

N. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks, Proceedings of the 18th International Workshop on Automated Verification of Critical Systems (AVOCS'18), 2018.
URL : https://hal.archives-ouvertes.fr/hal-01892423

N. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, Synaptic : a Formal Checker for SDN-based Security Policies, Proceedings of the 16th Network Operations and Management Symposium (IEEE/IFIP NOMS'18), Demonstration, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01892397

N. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, Towards Generation of SDN Policies for Protecting Android Environments based on Automata Learning, Proceedings of the 16th Network Operations and Management Symposium (IEEE/IFIP NOMS'18, 2018.

N. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, A Tool Suite for the Automated Synthesis of Security Function Chains, Proceedings of the 16th IFIP/IEEE Symposium on Integrated Network and Service Management, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02111658

N. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, Automated Factorization of Security Chains in Software-Defined Networks, Proceedings of the 16th IFIP/IEEE Symposium on Integrated Network and Service Management, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02111656

R. Sebastiani and P. Trentin, Optimathsat : A tool for optimization modulo theories, Journal of Automated Reasoning, 2018.

J. Sherry and A. Krishnamurthy, Making middleboxes someone else's problem : network processing as a cloud service, ACM SIGCOMM Computer Communication Review, 2012.

J. Sherry, C. Lan, A. Raluca, S. Popa, and . Ratnasamy, Blindbox : Deep packet inspection over encrypted traffic, Proceedings of the 2015 ACM Conference on Special Interest Group on Data Communication, SIGCOMM '15, pp.213-226, 2015.

A. P. Sistla and E. M. Clarke, The complexity of propositional linear temporal logics, J. ACM, vol.32, issue.3, pp.733-749, 1985.

A. Sperotto, Flow-based Intrusion Detection, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01529782

X. Wei, Profiledroid : Multi-layer profiling of android applications, Proceedings of the 18th annual international conference on Mobile computing and networking (MOBICOM 2012), 2012.

M. Xia, L. Gong, Y. Lyu, Z. Qi, and X. Liu, Effective real-time android application auditing, Proceedings of the 2015 IEEE Symposium on Security and Privacy, SP '15, pp.899-914, 2015.

M. Zhang, Y. Duan, Q. Feng, and H. Yin, Towards automatic generation of security centric descriptions for android apps, dings of the 22nd ACM SIGSAC Conference on Computer and Communications Security (CCS 2015), 2015.

Y. Zheng, V. Ganesh, S. Subramanian, O. Tripp, M. Berzish et al., Z3str2 : An efficient solver for strings, regular expressions, and length constraints, Form. Methods Syst. Des, vol.50, issue.2-3, pp.249-288, 2017.

S. Zonouz, A. Houmansadr, R. Berthier, N. Borisov, and W. Sanders, Secloud : A cloud-based comprehensive and lightweight security solution for smartphones, Comput. Secur, vol.37, pp.215-227, 2013.