Les services Web permettent la communication de systèmes hétérogènes sur le Web. Ces facilités font que ces services sont particulièrement adaptés au déploiement dans le cloud. Les efforts de formalisation et de vérification permettent d’améliorer la confiance dans les services Web, néanmoins des problèmes tels que la haute disponibilité et la sécurité ne sont pas entièrement pris en compte. Par ailleurs, les services Web déployés dans une infrastructure cloud héritent des vulnérabilités de cette dernière. En raison de cette limitation, ils peuvent être incapables d’exécuter parfaitement leurs tâches. Dans cette thèse, nous pensons qu’une bonne tolérance nécessite un monitoring constant et des mécanismes de réaction fiables. Nous avons donc proposé une nouvelle méthodologie de monitoring tenant compte des risques auxquels peuvent être confrontés nos services. Pour mettre en oeuvre cette méthodologie, nous avons d’abord développé une méthode de tolérance aux attaques qui s’appuie sur la diversification au niveau modèle. On définit un modèle du système puis on dérive des variantes fonctionnellement équivalents qui remplaceront ce dernier en cas d’attaque. Pour ne pas dériver manuellement les variants et pour augmenter le niveau de diversification nous avons proposé une deuxième méthode complémentaire. Cette dernière consiste toujours à avoir des variants de nos services; mais contrairement à la première méthode, nous proposons un modèle unique avec des implantations différentes tant au niveau des interfaces, du langage qu’au niveau des exécutables. Par ailleurs, pour détecter les attaques internes, nous avons proposé un mécanisme de détection et de réaction basé sur la reflexivité. Lorsque le programme tourne, nous l’analysons pour détecter les exécutions malveillantes. Comme contremesure, on génère de nouvelles implantations en utilisant la reflexivité. Pour finir, nous avons étendu notre environnement formel et outillé de services Web en y incorporant de manière cohérente tous ces mécanismes. L’idée est de pouvoir combiner ces différentes méthodes afin de tirer profit des avantages de chacune d’elle. Nous avons validé toute cette approche par des expériences réalistes. / Web services allow the communication of heterogeneous systems on the Web. These facilities make them particularly suitable for deploying in the cloud. Although research on formalization and verification has improved trust in Web services, issues such as high availability and security are not fully addressed. In addition, Web services deployed in cloud infrastructures inherit their vulnerabilities. Because of this limitation, they may be unable to perform their tasks perfectly. In this thesis, we claim that a good tolerance requires attack detection and continuous monitoring on the one hand; and reliable reaction mechanisms on the other hand. We therefore proposed a new formal monitoring methodology that takes into account the risks that our services may face. To implement this methodology, we first developed an approach of attack tolerance that leverages model-level diversity. We define a model of the system and derive more robust functionally equivalent variants that can replace the first one in case of attack. To avoid manually deriving the variants and to increase the level of diversity, we proposed a second complementary approach. The latter always consists in having different variants of our services; but unlike the first, we have a single model and the implementations differ at the language, source code and binaries levels. Moreover, to ensure detection of insider attacks, we investigated a new detection and reaction mechanism based on software reflection. While the program is running, we analyze the methods to detect malicious executions. When these malicious activities are detected, using reflection again, new efficient implementations are generated as countermeasure. Finally, we extended a formal Web service testing framework by incorporating all these complementary mechanisms in order to take advantage of the benefits of each of them. We validated our approach with realistic experiments.

Les technologies de communication et les services web sont devenus disponibles dans notre vie numérique, les réseaux informatiques continuent de croître et de nouveaux protocoles de communication sont constamment définis et développés. Par la suite, la standardisation et la normalisation des protocoles sont dispensables pour permettre aux différents systèmes de dialoguer. Bien que ces normes peuvent être formellement vérifiés, les développeurs peuvent produire des erreurs conduisant à des implémentations défectueuses. C'est la raison pour laquelle leur mise en œuvre doit être strictement examinée. Cependant, la plupart des approches de tests actuels exigent une stimulation de l’exécution dans le cadre des tests (IUT). Si le système ne peut être consulté ou interrompu, l'IUT ne sera pas en mesure d'être testé. En outre, la plupart des travaux existants sont basées sur des modèles formels et très peu de travaux s'intéressent à la formalisation des exigences de performance. Pour résoudre ces problèmes, nous avons proposé une approche de test basé sur la logique "Horn" afin de tester passivement la conformité et la performance des protocoles. Dans notre approche, les exigences peuvent être formalisées avec précision. Ces exigences formelles sont également testées par des millions de messages collectés à partir des communicants réels. Les résultats satisfaisants des expériences effectuées ont prouvé le bon fonctionnement et l'efficacité de notre approche. Aussi pour satisfaire les besoins croissants de tests distribués en temps réel, nous avons également proposé un cadre de tests distribués et un cadre de tests en ligne et nous avons mis en œuvre notre plateforme dans un environnement réel à petite échelle avec succès / While today’s communications are essential and a huge set of services is available online, computer networks continue to grow and novel communication protocols are continuously being defined and developed. De facto, protocol standards are required to allow different systems to interwork. Though these standards can be formally verified, the developers may produce some errors leading to faulty implementations. That is the reason why their implementations must be strictly tested. However, most current testing approaches require a stimulation of the implementation under tests (IUT). If the system cannot be accessed or interrupted, the IUT will not be able to be tested. Besides, most of the existing works are based on formal models and quite few works study formalizing performance requirements. To solve these issues, we proposed a novel logic-based testing approach to test the protocol conformance and performance passively. In our approach, conformance and performance requirements can be accurately formalized using the Horn-Logic based syntax and semantics. These formalized requirements are also tested through millions of messages collected from real communicating environments. The satisfying results returned from the experiments proved the functionality and efficiency of our approach. Also for satisfying the increasing needs in real-time distributed testing, we also proposed a distributed testing framework and an online testing framework, and performed the frameworks in a real small scale environment. The preliminary results are obtained with success. And also, applying our approach under billions of messages and optimizing the algorithm will be our future works