Vérification et configuration automatiques de pare-feux par Model Checking et synthèse de contrôleur

Les pare-feux jouent un rôle crucial dans le renforcement de la politique de sécurité d'un réseau. Cependant, leur configuration, qui nécessite souvent l'intervention humaine, est une source majeure de failles de sécurité. Par conséquent, des solutions automatisées sont nécessaires afin de détecter les incohérences de configuration des pare-feux. Dans ce mémoire, nous proposons des approches d'aide à la configuration des pare-feux, basées sur des techniques formelles comme le model checking et la synthèse de contrôleur. La première approche permet de vérifier par model checking la cohérence des pare-feux vis-a-vis d'un objectif de sécurité et de détecter, le cas échéant, les incohérences. Elle permet notamment de vérifier l'incohérence de croisement de chemins (i.e. si un paquet est rejeté par l'un des pare-feux en direction de sa destination, il ne pourra pas l'atteindre en empruntant un autre chemin). Nous étendons cette approche, en utilisant SMC-UPPAAL, afin d'étudier les performances du réseau en fonction des paramètres de qualité de service tels que le délai d'acheminement des paquets, le délai d'attente et le taux de perte. Cette extension permet, entre autres, de calculer la probabilité qu'un paquet passant par un nœud malicieux soit accepté, la probabilité qu'un nœud tombe en panne, les taux d'acceptation et de rejet de paquets. En outre, nous proposons une approche formelle permettant de configurer formellement les pare-feux privés sur un réseau, conformément à un objectif de sécurité donné, en utilisant la technique de synthèse de contrôleur implémentée par l'outil UPPAAL-TIGA. Par ailleurs, pour atténuer le problème d'explosion combinatoire inhérent au model checking et la synthèse de contrôleur, les approches proposées ici sont basées sur des abstractions. Des études expérimentales sont conduites pour démontrer la performance de ces abstractions.

Abstract

Firewalls play a crucial role in the enforcement of network security policies. However, their configuration, which often requires human intervention, is a major source of security vulnerabilities. Therefore, automated solutions are needed in order to detect firewall configuration inconsistencies. In this master thesis, we propose support approaches of firewall configuration based on formal techniques such as model checking and controller synthesis. The first approach is used to check the firewalls consistency by model checking with respect to a security objective and to detect firewall configuration incoherencies such as cross path incoherence (i.e. if a packet is rejected by a firewall towards its destination, it cannot reach it by taking a different path). We extend this approach, using SMC UPPAAL to study the network performance according to QoS parameters such as end-to-end time routing, latency and loss rate. This extension allows, inter alia, the computation of the probability to accept a packet passing through a malicious node, the probability that a node fails and packets acceptance or rejection rates. In addition, we propose another approach to formally configure private firewalls on a network, according to a given security policy, using the controller synthesis technique implemented in the UPPAAL TIGA tool. Furthermore, to alleviate the problem of combinatorial explosion inherent in model checking and controller synthesis, the approaches proposed here are based on abstractions. Experimental studies were conducted to demonstrate the performance of these abstractions.