Modélisation formelle d'architectures sécurisées dans une perspective positive à l'aide d'Event-B : propriétés, modèles, analyse et outillage
- Thierry, Loic (1998-.... ; docteur en informatique et télécommunications) (2025)
Thèse
- Numéro national de thèse
- 2025TLSEJ144
- Titre en français
- Modélisation formelle d'architectures sécurisées dans une perspective positive à l'aide d'Event-B : propriétés, modèles, analyse et outillage
- Titre en anglais
- Formal modeling of secure architecture within the positive perspective using Event-B: properties,model, analysis and tool support
- Directeur de recherche
- Hamid, Brahim (1975-.... ; enseignant-chercheur en informatique)
- Co-directeur de recherche
- Jaskolka, Jason (19..-....)
- Date de soutenance
- 2 décembre 2025
- Établissement de co-tutelle
- Carleton university
- École doctorale
- MITT : Mathématiques Informatique Télécommunications de Toulouse
- Unité de recherche
- Institut de Recherche en Informatique de Toulouse - IRIT
- Sujet
- Informatique
- Mots-clés en français
- Sécurité
- Objectifs
- Architecture
- Modèles
- Techniques formelles
- Mots-clés en anglais
- Security
- Objectives
- Architecture
- Models
- Formal techniques
- Résumé en français
-
Le développement des systèmes informatiques distribués et leur utilisation dans des domaines tels que l’Internet des Objets, le Big Data, etc., soulèvent de nombreuses questions quant aux outils disponibles pour modéliser la complexité de ces systèmes. Les méthodes de modélisation non formelles échouent à fournir un cadre rigoureux permettant de décrire et d’analyser ces systèmes. Dans cette thèse, nous proposons de définir une approche permettant de modéliser et d’analyser à la fois les aspects fonctionnels et non fonctionnels de ces systèmes à l’aide de techniques formelles.
Les objectifs de ce travail incluent :
(1) explorer l'utilisation des méthodes formelles basées sur la preuve pour la spécification et la vérification des propriétés structurelles et comportementales des systèmes à base de composants,
(2) décrire et valider des propriétés de sécurité dans des bibliothèques réutilisables,
(3) décrire et classifier les relations entre les propriétés de sécurité,
et (4) développer un ensemble d’outils.
Pour atteindre ces objectifs, nous cherchons à :
(a) décrire les concepts de haut niveau pour l’architecture système selon une approche composant-port-connecteur sous forme de métamodèle ;
(b) développer une interprétation Event-B de ce métamodèle en y ajoutant des caractéristiques de communication telles que le tamponage, le premier entré-premier sorti (FIFO) et la synchronicité ;
(c) étendre ce modèle formel pour représenter les propriétés de sécurité ;
et (d) créer une suite d’outils automatisés basée sur ce modèle formel, pouvant être intégrée dans un cycle de développement.
L’approche combine à la fois l’ingénierie dirigée par les modèles (IDM) et les techniques formelles afin de créer des méthodes et des outils pour la conception, la vérification et la validation des architectures systèmes complexes. Les méthodes et outils proposés s’intéressent non seulement aux exigences fonctionnelles, mais aussi aux exigences non fonctionnelles, en s’appuyant sur des bibliothèques réutilisables de propriétés de sécurité, utilisables dès la phase de conception. Pour valider notre travail, nous étudions un ensemble d’objectifs de sécurité représentatifs issus de la classification confidentialité, intégrité, disponibilité (CIA), ainsi qu’une étude de cas sur le protocole TLS (Transport Layer Security). - Résumé en anglais
-
The development of distributed computing systems and of their usage in domains such as the Internet of Things, Big Data, etc., raises numerous questions on the tools available to model the complexity of such systems. Non-formal modeling methods fail to create a rigorous way to describe and analyze these systems. In this thesis, we propose to find an approach to model and analyze both functional and non-functional aspects of these systems using formal techniques.
The objectives of this work include: (1) exploring the use of proof-based formal methods for the specification and verification of both structural and behavioral properties of component-based systems, (2) describing and validating security properties in reusable libraries, (3) describing and classifying the relationships between security properties, and (4) developing a set of supporting tools.
To achieve these objectives, we seek to:
(a) describe high-level concepts for system architecture in a component-port-connector fashion as a metamodel; (b) develop an Event-B interpretation of the metamodel adding communication characteristics such as buffering, first-in-first-out (FIFO), and synchronicity; (c) extend this formal model to represent security properties; and (d) create an automated tool suite using the formal model that can be integrated into a systems development lifecycle.
The approach leverages both model-driven engineering (MDE) and formal techniques to create methods and tools for designing, verifying, and validating complex system architectures. The methods and tools will not only focus on functional requirements, but also on non-functional requirements by creating reusable libraries of security properties that can be used during the design phase. To validate our work, we explore a set of representative security objectives extracted from the confidentiality, integrity, availability (CIA) classification and a case study on the Transport Layer Security (TLS) protocol. - Accès au document
- Accès libre
Citation bibliographique
Thierry, Loic (1998-.... ; docteur en informatique et télécommunications) (2025), Modélisation formelle d'architectures sécurisées dans une perspective positive à l'aide d'Event-B : propriétés, modèles, analyse et outillage [Thèse]