{"id":1249,"date":"2020-02-27T15:51:29","date_gmt":"2020-02-27T14:51:29","guid":{"rendered":"https:\/\/samovar2022.int-evry.fr\/index.php\/2020\/02\/27\/caracterisation-de-la-securite-de-la-migration-de-reseaux-virtuels-sdn-approche-formelle-et-optimisation-des-ressources\/"},"modified":"2020-09-04T18:45:17","modified_gmt":"2020-09-04T16:45:17","slug":"caracterisation-de-la-securite-de-la-migration-de-reseaux-virtuels-sdn-approche-formelle-et-optimisation-des-ressources","status":"publish","type":"post","link":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/2020\/02\/27\/caracterisation-de-la-securite-de-la-migration-de-reseaux-virtuels-sdn-approche-formelle-et-optimisation-des-ressources\/","title":{"rendered":"Caract\u00e9risation de la s\u00e9curit\u00e9 de la migration de r\u00e9seaux virtuels SDN: Approche formelle et Optimisation des ressources"},"content":{"rendered":"<p>L&rsquo;Ecole doctorale : Ecole Doctorale de l&rsquo;Institut Polytechnique de Paris<\/p>\n<p>et le Laboratoire de recherche SAMOVAR<\/p>\n<p>pr\u00e9sentent<\/p>\n<p>l\u2019AVIS DE SOUTENANCE de <strong>Monsieur Fabien CHARMET<\/strong><\/p>\n<p>Autoris\u00e9 \u00e0 pr\u00e9senter ses travaux en vue de l\u2019obtention du Doctorat de l&rsquo;Institut Polytechnique de Paris, pr\u00e9par\u00e9 \u00e0 T\u00e9l\u00e9com SudParis en :<br \/>\nInformatique<br \/>\n\u00ab Caract\u00e9risation de la s\u00e9curit\u00e9 de la migration de r\u00e9seaux virtuels SDN: Approche formelle et Optimisation des ressources \u00bb<\/p>\n<p>le <strong>MARDI 25 F\u00e9VRIER 2020 \u00e0 14h00 &#8211; Salle C06<\/strong><\/p>\n<p>\u00e0<\/p>\n<p>T\u00e9l\u00e9com SudParis &#8211; 9 Rue Charles Fourier 91000 Evry-Courcouronnes<\/p>\n<p><strong>Membres du jury :<\/strong><\/p>\n<p>M. Abdallah M&rsquo;HAMED, Ma\u00eetre de conf\u00e9rences, T\u00e9l\u00e9com SudParis, FRANCE &#8211; Directeur de th\u00e8se<br \/>\nMme Val\u00e9rie VIET TRIEM TONG, Professeure, Centrale Sup\u00e9lec Rennes, FRANCE &#8211; Rapporteur<br \/>\nM. Ahmed MEDDAHI, Professeur, IMT Lille Douai, FRANCE &#8211; Rapporteur<br \/>\nM. Jean LENEUTRE, Ma\u00eetre de Conf\u00e9rences, T\u00e9l\u00e9com Paris, FRANCE &#8211; Examinateur<br \/>\nMme Nesrine KAANICHE, Lecturer, The University of Sheffield, ROYAUME-UNI &#8211; Examinatrice<br \/>\nMme Hind CASTEL, Professeure, T\u00e9l\u00e9com SudParis, FRANCE &#8211; Examinatrice<br \/>\nM. Rami LANGAR, Professeur, Universit\u00e9 Paris-Est Marne-la-Vall\u00e9e, FRANCE &#8211; Examinateur<br \/>\nM. Christophe KIENNERT, Ma\u00eetre de Conf\u00e9rences, T\u00e9l\u00e9com SudParis, FRANCE &#8211; Encadrant de th\u00e8se<\/p>\n<p><strong>R\u00e9sum\u00e9 :<\/strong><\/p>\n<p>Cette th\u00e8se explore la s\u00e9curit\u00e9 de la migration de r\u00e9seaux virtuels. Au cours des ann\u00e9es, la virtualisation a \u00e9t\u00e9 utilis\u00e9e pour optimiser l&rsquo;usage des ressources informatiques et pour supporter les infrastructures des entreprises. La virtualisation consiste \u00e0 allouer une partie des ressources d&rsquo;une machine physique \u00e0 un utilisateur (sous la forme d&rsquo;une machine virtuelle) pour qu&rsquo;il puisse l&rsquo;exploiter. Les machines virtuelles sont utilis\u00e9es pour h\u00e9berger des services op\u00e9rationnels comme un serveur internet ou une base de donn\u00e9es. La virtualisation des r\u00e9seaux n&rsquo;a pas profit\u00e9 du m\u00eame int\u00e9r\u00eat de la part des chercheurs et des acteurs industriels. Le paradigme du Software Defined Networking a introduit de nouvelles possibilit\u00e9s pour impl\u00e9menter la virtualisation r\u00e9seau et fournir aux utilisateurs une solution flexible pour leurs besoins m\u00e9tiers. Les r\u00e9seaux virtuels sont utilis\u00e9s pour interconnecter des machines virtuelles, et ils peuvent \u00eatre configur\u00e9s avec des r\u00e8gles de routages ou des protocoles de s\u00e9curit\u00e9 sp\u00e9cifiques. Dans l&rsquo;\u00e9ventualit\u00e9 o\u00f9 un \u00e9quipement r\u00e9seau tomberait en panne ou sous le coup d&rsquo;une attaque informatique, le syst\u00e8me d&rsquo;hypervision va migrer les ressources afin de pr\u00e9server la disponibilit\u00e9 des services utilisateurs. La s\u00e9curit\u00e9 des machines virtuelles et de leur migration est un domaine de recherche qui a \u00e9t\u00e9 grandement explor\u00e9 par le pass\u00e9, tandis que la virtualisation r\u00e9seau et plus sp\u00e9cifiquement la migration de r\u00e9seaux virtuels restent encore des domaines de recherche assez jeune et o\u00f9 beaucoup reste \u00e0 faire. La surface d&rsquo;attaque de la virtualisation r\u00e9seau est similaire en nature \u00e0 celle de la virtualisation traditionnelle, mais elle pr\u00e9sente un aspect suppl\u00e9mentaire d\u00fb \u00e0 l&rsquo;usage du paradigme du Software Defined Networking. La motivation de notre travail est d&rsquo;\u00e9tudier la s\u00e9curit\u00e9 du processus de migration des r\u00e9seaux virtuels, dans le contexte du Software Defined Networking. Nous proposons d&rsquo;atteindre cet objectif en trois phases. Tout d&rsquo;abord, nous d\u00e9finissons le p\u00e9rim\u00e8tre de cette \u00e9tude, et nous concentrons sur l&rsquo;aspect r\u00e9seau de la migration. Ensuite, nous d\u00e9crivons le mod\u00e8le d&rsquo;attaquant afin de compromettre la migration des r\u00e9seaux et nous concevons un m\u00e9canisme de d\u00e9tection contre les attaques envers l&rsquo;infrastructure de virtualisation. Enfin, nous am\u00e9liorons le m\u00e9canisme de d\u00e9fense en optimisant le d\u00e9ploiement des ressources de d\u00e9tection afin d&rsquo;obtenir une couverture optimale de l&rsquo;infrastructure. Dans la premi\u00e8re partie de cette th\u00e8se, nous proposons une approche formelle pour d\u00e9crire les diff\u00e9rents composants de l&rsquo;infrastructure de virtualisation. Nous utilisons un formalisme de logique du premier ordre pour d\u00e9crire diff\u00e9rentes propri\u00e9t\u00e9s de s\u00e9curit\u00e9 sous la forme de pr\u00e9dicats bool\u00e9ens. Cette mod\u00e9lisation inclut la repr\u00e9sentation des donn\u00e9es des utilisateurs finaux ainsi que l&rsquo;infrastructure de virtualisation. Une trace d&rsquo;ex\u00e9cution est g\u00e9n\u00e9r\u00e9e pendant la migration d&rsquo;un r\u00e9seau virtuel, et est ensuite utilis\u00e9e par un prouveur de th\u00e9or\u00e8me afin de v\u00e9rifier formellement si la s\u00e9curit\u00e9 de la migration a \u00e9t\u00e9 respect\u00e9e. Le mod\u00e8le formel est bas\u00e9 sur la supposition que la trace d&rsquo;ex\u00e9cution est g\u00e9n\u00e9r\u00e9e par un outil de supervision exempt de tout d\u00e9faut. Ceci implique que la preuve formelle est compl\u00e8te. Nous levons cette hypoth\u00e8se en mod\u00e9lisant un probl\u00e8me d&rsquo;allocation de ressources afin de d\u00e9terminer quels \u00e9quipements r\u00e9seau devraient \u00eatre charg\u00e9s de la d\u00e9tection d&rsquo;attaques pour une couverture optimale. Nous r\u00e9solvons ce probl\u00e8me en utilisant un processus de d\u00e9cision markovien. Nous concluons notre optimisation en proposant un d\u00e9ploiement statique des ressources, en amont de toute migration.<\/p>\n<p><strong>Abstract :<\/strong><\/p>\n<p>This thesis investigates the security of virtual network migration. Over the years, virtualization has been used to optimize physical resources and to support businesses\u2019 infrastructure. Virtualization consists in exposing a fraction of a resource for a user to operate. Virtual Machines are used to host business services like web servers or a backup service. Network virtualization has not benefited from the same interest from researchers and the industry. The Software Defined Networking paradigm has introduced new possibilities to implement network virtualization and provide users with a flexible network, decoupled from the physical equipment. Virtual Networks are used to interconnect Virtual Machines and can be configured with specific routing policies or security protocols. In case of a failure of the resource, either accidental or intentional, the virtualization infrastructure will migrate the resource to maintain the service provided. The security of Virtual Machines and their migration is a well-researched topic that has been widely in the past, while the study of network virtualization and especially the migration process only are at an early stage. The attack surface of network virtualization is similar in nature to the virtualization of legacy resources, and presents an additional aspect because of the use of Software Defined Networking. The motivation of this research is to investigate the security of the virtual network migration process in the context of Software Defined Networking. In order to do so, we first define the scope of the study and focus on the networking aspect of the migration. Then, we outline the threat model of the migration process and devise a detection mechanism against attacks in the virtualization infrastructure. Finally, we optimize the previous mechanism by optimizing the deployment of network monitoring resources for an optimal coverage. In the first part of this thesis we propose a formal approach to describe the different aspects of the virtualization infrastructure. We use a first order formalism to model several security properties as a set of logical predicates. These predicates account for both physical and virtual elements of the virtualization infrastructure, and the data use by both end users and the infrastructure owner. An execution trace is generated during the migration of a virtual network, and will be used by a theorem prover to compute a formal proof to verify if a security violation occurred. The first order model is based on the assumption that the execution trace is generated using perfect monitoring. This implies that the proof is complete and that the networking monitoring is always done under optimal conditions. We alleviate this assumption by modeling a resource allocation problem to determine how the monitoring resources should be deployed and which network nodes provide the best coverage. We solve this problem using a Markov Decision Process, and determine a dynamic deployment of monitoring resources during the migration. We conclude our optimization with a proposition of a static deployment of the resources prior to the migration.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>L&rsquo;Ecole doctorale : Ecole Doctorale de l&rsquo;Institut Polytechnique de Paris et le Laboratoire de recherche SAMOVAR pr\u00e9sentent l\u2019AVIS DE SOUTENANCE de Monsieur Fabien CHARMET Autoris\u00e9 \u00e0 pr\u00e9senter ses travaux en vue de l\u2019obtention du Doctorat de l&rsquo;Institut Polytechnique de Paris, pr\u00e9par\u00e9 \u00e0 T\u00e9l\u00e9com SudParis en : Informatique \u00ab Caract\u00e9risation de la s\u00e9curit\u00e9 de la migration [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"ocean_post_layout":"","ocean_both_sidebars_style":"","ocean_both_sidebars_content_width":0,"ocean_both_sidebars_sidebars_width":0,"ocean_sidebar":"","ocean_second_sidebar":"","ocean_disable_margins":"enable","ocean_add_body_class":"","ocean_shortcode_before_top_bar":"","ocean_shortcode_after_top_bar":"","ocean_shortcode_before_header":"","ocean_shortcode_after_header":"","ocean_has_shortcode":"","ocean_shortcode_after_title":"","ocean_shortcode_before_footer_widgets":"","ocean_shortcode_after_footer_widgets":"","ocean_shortcode_before_footer_bottom":"","ocean_shortcode_after_footer_bottom":"","ocean_display_top_bar":"default","ocean_display_header":"default","ocean_header_style":"","ocean_center_header_left_menu":"","ocean_custom_header_template":"","ocean_custom_logo":0,"ocean_custom_retina_logo":0,"ocean_custom_logo_max_width":0,"ocean_custom_logo_tablet_max_width":0,"ocean_custom_logo_mobile_max_width":0,"ocean_custom_logo_max_height":0,"ocean_custom_logo_tablet_max_height":0,"ocean_custom_logo_mobile_max_height":0,"ocean_header_custom_menu":"","ocean_menu_typo_font_family":"","ocean_menu_typo_font_subset":"","ocean_menu_typo_font_size":0,"ocean_menu_typo_font_size_tablet":0,"ocean_menu_typo_font_size_mobile":0,"ocean_menu_typo_font_size_unit":"px","ocean_menu_typo_font_weight":"","ocean_menu_typo_font_weight_tablet":"","ocean_menu_typo_font_weight_mobile":"","ocean_menu_typo_transform":"","ocean_menu_typo_transform_tablet":"","ocean_menu_typo_transform_mobile":"","ocean_menu_typo_line_height":0,"ocean_menu_typo_line_height_tablet":0,"ocean_menu_typo_line_height_mobile":0,"ocean_menu_typo_line_height_unit":"","ocean_menu_typo_spacing":0,"ocean_menu_typo_spacing_tablet":0,"ocean_menu_typo_spacing_mobile":0,"ocean_menu_typo_spacing_unit":"","ocean_menu_link_color":"","ocean_menu_link_color_hover":"","ocean_menu_link_color_active":"","ocean_menu_link_background":"","ocean_menu_link_hover_background":"","ocean_menu_link_active_background":"","ocean_menu_social_links_bg":"","ocean_menu_social_hover_links_bg":"","ocean_menu_social_links_color":"","ocean_menu_social_hover_links_color":"","ocean_disable_title":"default","ocean_disable_heading":"default","ocean_post_title":"","ocean_post_subheading":"","ocean_post_title_style":"","ocean_post_title_background_color":"","ocean_post_title_background":0,"ocean_post_title_bg_image_position":"","ocean_post_title_bg_image_attachment":"","ocean_post_title_bg_image_repeat":"","ocean_post_title_bg_image_size":"","ocean_post_title_height":0,"ocean_post_title_bg_overlay":0.5,"ocean_post_title_bg_overlay_color":"","ocean_disable_breadcrumbs":"default","ocean_breadcrumbs_color":"","ocean_breadcrumbs_separator_color":"","ocean_breadcrumbs_links_color":"","ocean_breadcrumbs_links_hover_color":"","ocean_display_footer_widgets":"default","ocean_display_footer_bottom":"default","ocean_custom_footer_template":"","ocean_post_oembed":"","ocean_post_self_hosted_media":"","ocean_post_video_embed":"","ocean_link_format":"","ocean_link_format_target":"self","ocean_quote_format":"","ocean_quote_format_link":"post","ocean_gallery_link_images":"on","ocean_gallery_id":[],"footnotes":""},"categories":[276],"tags":[],"class_list":["post-1249","post","type-post","status-publish","format-standard","hentry","category-theses-2020-fr","entry"],"_links":{"self":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts\/1249","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/comments?post=1249"}],"version-history":[{"count":1,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts\/1249\/revisions"}],"predecessor-version":[{"id":1423,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts\/1249\/revisions\/1423"}],"wp:attachment":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/media?parent=1249"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/categories?post=1249"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/tags?post=1249"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}