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.