Programme de Doctorat en informatique

Département d’informatique et de génie logiciel

Faculté des sciences et de génie

Présentation orale de la proposition de projet de recherche

(IFT-8003)

de

Gildas Syla Déo Kouko

Le jeudi 20 juin 2024 à 13h30

Local 3904, Pavillon Adrien Pouliot

Contrôle du flux d’information et de la sûreté
de fonctionnement en Internet des objets

Membres du jury

Josée Desharnais, Ph.D. (Directrice de recherche)

Département d’informatique et de génie logiciel

Nadia Tawbi, Ph.D. (Co-directrice)

Département d’informatique et de génie logiciel

Djedjiga Mouheb, Ph.D. (Examinatrice)

Département d’informatique et de génie logiciel

Talal Halabi, Ph.D. (Examinateur)

Département d’informatique et de génie logiciel

Résumé

Définis au sens large comme l’Internet des objets (IdO), les applications et objets intelligents relient le monde physique au monde numérique. Malgré leur bienfait dans la société moderne, ils reposent malheureusement souvent sur des protocoles propriétaires, mal documentés avec des formats et sémantiques de communication parfois inconnus. Les interactions entre les objets et les applications sont souvent les véritables causes de fuites de données et de violations de propriétés de sûreté, de confidentialité et de sécurité. La maîtrise du comportement autonome de ces dispositifs intelligents face aux évènements et actions de leur environnement est très importante. C’est la clé pour une meilleure compréhension de leur interopérabilité et connectivité et pour découvrir automatiquement des conflits entre les attentes définies par les utilisateurs.  Pour contrôler ces comportements imprévisibles dans un écosystème IdO, tant à la conception chez les fournisseurs qu’à l’usage chez les utilisateurs, nous axons l’objectif général de notre thèse sur le contrôle des flux d’information par évaluation de modèle. Nous proposons un modèle basé sur une abstraction du fonctionnement des objets et des applications pour représenter les interactions dans un réseau IdO. Cette abstraction est le résultat d’une analyse du flux d’information effectuée, à priori, pour tous les objets analysés ainsi que pour toutes les applications les contrôlant. Le système de transitions construit à partir de ces abstractions nous permet de transformer le problème de contrôle du flux de d’information en un problème de vérification de propriétés d’atteignabilité et de sûreté de fonctionnement que nous exprimons avec un nouveau langage formel (logique et sémantique). Nous illustrons notre approche avec un exemple particulier (fictif) de réseau relativement complexe d’objets intelligents. Étant donné que nous avons un vérificateur existant, il faut au préalable adapter le langage et le modèle à ce vérificateur. Les résultats de modélisation montrent que l’architecture IdO adoptée peut résoudre à la fois des tâches simples et complexes et mieux refléter la nature des interactions indépendamment de toutes hétérogénéités fonctionnelle et technique.

Abstract

Broadly defined as the Internet of Things (IoT), smart objects and applications link the physical world to the digital one. Despite their benefits in modern society, they are unfortunately often based on owner protocols, poorly documented protocols with sometimes unknown communication formats and semantics. Interactions between objects and applications are often the real cause of data leakage and violations of safety, confidentiality and security properties. Mastering the autonomous behavior of these intelligent devices in the face of events and actions in their environment is extremely important. This is the key to a better understanding of their interoperability and connectivity and to automatic discovery of conflicts between properties defined by users.  To control these unpredictable behaviors in an IoT ecosystem, both at the design stage for suppliers and at the usage stage for users, we focus the overall goal of our thesis on controlling information flows through model checking. We propose a model based on an abstraction of the functioning of objects and applications to represent interactions in an IoT network. The abstraction is a result of information flow analysis. This analysis is performed a priori on all the codes of the objects under study and all the applications controlling them. The system of transitions built from these abstractions enables us to transform the information flow control problem into a problem of verifying reachability and dependability properties, which we express with a new formal language (logic and semantics). We illustrate our approach with a particular (fictitious) example of a relatively complex network of intelligent objects. Since we have an existing model checker, we need to adapt first the language and the model to the model checker. The modeling results show that the adopted IoT architecture can solve both simple and complex tasks, and better reflect the nature of interactions independently of any functional and technical heterogeneities.

Note : La présentation sera donnée en français, mais une partie sera en anglais.

Bienvenue à tous !