Network Functions Virtualization (NFV) is transforming the way enterprises deploy, maintain, and evolve their network services. With NFV, enterprises can deploy various network functions such as routers, firewalls, and load balancers as software instances running on commercial off-the-shelf servers. By adopting this new approach, enterprises are increasingly outsourcing their network services to the cloud, ultimately reaping the rewards of cloud computing, which include high availability, lower costs, and theoretically infinite resources.However, many enterprises are reluctant to embrace this new approach, due to a lack of trust in the cloud. Such reluctance stems from the opacity of the cloud, the risk of dishonest behavior by the cloud provider, and the risk of attacks from inside or outside. As a result, enterprises considering outsourcing their network services to the cloud are sorely lacking in assurances that their network services will meet their specifications. Violations of network service specifications are highly detrimental to the business success and image of enterprises, as these violations compromise their security, quality of service, and resiliency objectives. Thus, outsourcing network services to the cloud requires first and foremost establishing trust between enterprises and the cloud.In this thesis, we argue that a systematic verification of network services remains the key to addressing the lack of enterprises’ trust in the cloud. Verification involves confronting the network service state to detect network service anomalies or to assess the compliance of the network service state with its specification. Thus, with verification mechanisms, enterprises can anticipate and detect specification violations, a.k.a. network service anomalies, remediate them, and claim compensation from cloud-NFV providers.This thesis proposes several contributions in the context of verification of outsourced network services to the cloud. First, we present a taxonomy of network service anomalies that can occur in NFV environments. Along with this taxonomy, we analyze the negative impacts of network service anomalies on critical service attributes such as confidentiality, integrity, and performance. As a second contribution, we introduce VeriNeS, a verification system that observes the behavior of the NFV Orchestrator to detect network service anomalies. By intercepting configuration commands issued by the NFV Orchestrator, VeriNeS builds a global state of all network services instead of a single state per network service. With this approach, VeriNeS overcomes cardinal limitations of the NFV architecture that include the lack of details to correlate the state of network services with their respective owners. VeriNeS integrates with the NFV architecture without the need to modify existing components and responds to verification requests in an acceptable time frame for real-world deployment scenarios., La Virtualisation des Fonctions Réseau (NFV) transforme la façon dont les entreprises déploient, maintiennent et font évoluer leurs services réseau. Avec la NFV, les entreprises peuvent déployer diverses fonctions réseau telles que les routeurs, les pare-feux, les équilibreurs de charges sous forme d’instances logicielles s’exécutant dans des serveurs standards bon marché. En adoptant cette nouvelle approche, les entreprises externalisent de plus en plus leurs services réseau vers le cloud, pour récolter finalement les fruits du cloud computing qui incluent la haute disponibilité, la réduction des couts et des ressources théoriquement infinies.Cependant, de nombreuses entreprises hésitent à emboiter cette nouvelle approche, à cause du manque de confiance envers le cloud. Une telle réticence s’explique par l’opacité du cloud, le risque de comportement malhonnête du fournisseur cloud, et le risque d’attaques de l’intérieur ou de l’extérieur. Ainsi, les entreprises qui envisagent d’externaliser leurs services réseau vers le cloud manquent cruellement de garanties quant à la conformité de leurs services réseau par rapport à leurs spécifications. Les violations de spécifications de service réseau nuisent grandement à la réussite commerciale et à l’image des entreprises, car ces violations compromettent leurs objectifs de sécurité, de qualité de service et de résilience. Ainsi, l’externalisation des services réseau vers le cloud nécessite avant tout d’établir la confiance entre les entreprises et le cloud.Dans cette thèse, nous soutenons que la vérification systématique de service réseau reste la clé pour combler le manque de confiance des entreprises envers le cloud. La vérification consiste à confronter l’état du service réseau pour détecter des anomalies de service réseau ou pour évaluer la conformité de l’état du service réseau par rapport à sa spécification. Ainsi, avec des mécanismes de vérification, les entreprises peuvent anticiper et détecter les violations de spécifications, alias anomalies de services réseau, y remédier et réclamer des compensations auprès des fournisseurs de cloud-NFV.Cette thèse propose plusieurs contributions dans le contexte de la vérification de services réseau externalisés vers le cloud. D’abord, nous présentons une taxonomie des anomalies de service réseau qui peuvent survenir dans les environnements NFV. Parallèlement à cette taxonomie, nous analysons les impacts négatifs des anomalies de service réseau sur des attributs de service critiques tels que la confidentialité, l’intégrité, et la performance. Comme seconde contribution, nous introduisons VeriNeS, un système de vérification qui observe le comportement de l’Orchestrateur NFV, afin de détecter des anomalies de service réseau. En interceptant les commandes configurations émises par l’Orchestrateur NFV, VeriNeS construit un état global de tous les services réseau au lieu d’un état par service réseau. Avec cette approche, VeriNeS surmonte des limites cardinales de l’architecture NFV qui incluent le manque de détails pour corréler l’état des services réseau avec leurs propriétaires respectifs. VeriNeS s’intègre à l’architecture NFV sans besoin de modifier les composants existants et répond aux requêtes de vérification en un temps acceptable pour des scénarios réels de déploiement.