Constellation, le dépôt institutionnel de l'Université du Québec à Chicoutimi

Résumé

Runtime Verification is the process of observing a sequence of events produced by a running software system and determining whether this sequence complies with a specified property expressed using a formal notation. It is commonly believed that a monitor possesses full access to the event trace. However, there are numerous scenarios where the monitor functions with a certain degree of uncertainty regarding the trace’s content. In this thesis, we define a logical framework where uncertainty is modeled by a stateful access control proxy that has the capacity to transform events into sets of possible events, resulting in what we refer to as a “multi-trace”. We also provide an algorithm to lift a classical monitor into a sound, loss-tolerant monitor. Both the proxy and the monitor are extensions of Mealy machines. Experiments conducted on various scenarios demonstrate that our approach can effectively account for various types of data degradation and access limitations. Furthermore, our approach provides a tighter verdict than existing works in some cases and preserves the scalable performance of the model. In other scenarios, it is crucial for the underlying system to adhere to specific security policies. In such cases, runtime enforcement can be employed to ensure the respect of a user-specified security policy by a program. This is achieved by providing a valid replacement for any misbehaving sequence of events that may occur during the program’s execution. However, depending on the capabilities of the enforcement mechanism, multiple possible replacement sequences may be available, and the current literature lacks guidance on how to choose the optimal one. Additionally, the current design of runtime monitors imposes a substantial burden on the designer, as the monitoring task is typically accomplished by a monolithic construct, often an automata-based model. This thesis addresses these issues by proposing a new modular model of enforcement monitors, where the tasks of altering the execution, ensuring compliance with the security policy, and selecting the optimal replacement are split into three separate modules. This modular approach simplifies the creation of runtime monitors. We implement this approach using the event stream processor BeepBeep, and a use case is presented to demonstrate its effectiveness. Experimental evaluation shows that our proposed framework can dynamically select appropriate enforcement actions at runtime, eliminating the need for manual definition of an enforcement monitor.

Au début des années 2000, on a constaté une augmentation significative de la complexité des systèmes logiciels, caractérisée par un nombre croissant de composants et d’interactions. Les méthodes traditionnelles de test et de vérification formelle se sont avérées insuffisantes pour garantir la précision et la sécurité de ces systèmes. De plus, il est devenu évident que des techniques d’analyse dynamique étaient nécessaires pour surveiller et analyser le comportement des logiciels en temps réel pendant leur exécution. Cela était crucial pour identifier et résoudre des actions imprévues ou malveillantes qui ne pouvaient pas être entièrement anticipées lors de la conception ou de l’analyse statique. En conséquence, le domaine de la vérification de l’exécution est apparu comme une discipline distincte en informatique. La vérification de l’exécution consiste à utiliser un système de surveillance pour observer le comportement d’un programme cible, en le traitant comme une séquence d’événements. L’objectif est de détecter les violations potentielles d’une politique de sécurité définie par l’utilisateur et de fournir un verdict vrai si la politique est respectée, ou un verdict faux si elle est enfreinte. Le domaine de la vérification de l’exécution englobe un large éventail de sujets et fait face à divers défis. Un problème particulier concerne la nature des événements surveillés. Il n’est pas toujours réaliste de supposer que tous les événements sont complets, précis et arrivent dans l’ordre attendu. Plusieurs facteurs peuvent affecter les événements, entraînant une incomplétude, une imprécision ou des interruptions dans leur séquence d’arrivée vers le moniteur. En conséquence, le moniteur peut faire face à des difficultés à analyser avec précision les événements, ce qui conduit à des verdicts non concluants. Pour résoudre ce problème, plusieurs solutions ont été proposées dans la littérature. Une approche consiste simplement à ignorer les événements imprécis et à les traiter comme s’ils ne s’étaient pas produits. Une autre solution consiste à construire des modèles probabilistes pour estimer la probabilité qu’un événement se soit produit et produire un verdict correspondant. De plus, une troisième solution consiste à remplacer les événements imprécis ou manquants par un ensemble de toutes les substitutions possibles, ce qui permet une analyse plus complète. La troisième solution peut potentiellement générer un ensemble de verdicts au lieu d’un seul verdict. L’innovation clé de cette thèse réside dans le développement d’une méthode pour représenter les événements incertains et générer les substitutions possibles correspondantes. Cette innovation s’étend au langage de spécification utilisé pour définir la politique de sécurité et construire un moniteur capable de traiter les ensembles de toutes les substitutions possibles pour un événement tout en minimisant le temps d’exécution et les surcharges. Dans cette thèse, nous établissons un cadre logique qui utilise un proxy de contrôle d’accès étatique pour modéliser l’incertitude. Ce proxy a la capacité de transformer les événements en ensembles d’événements possibles, ce qui aboutit à ce que nous appelons une "multi-trace". De plus, nous présentons un algorithme pour transformer un moniteur traditionnel en un moniteur fiable et tolérant aux pertes. Le proxy et le moniteur sont tous deux des extensions de machines de Mealy. À travers des expériences menées dans différents scénarios, nous démontrons l’efficacité de notre approche dans la gestion de différents types de dégradation des données et de limitations d’accès. La vérification de l’exécution est étroitement liée au concept de l’application à l’exécution (runtime enforcement), qui va encore plus loin en réagissant aux violations observées de manière à les corriger et à s’en remettre. Dans le processus d’application d’actions correctives à une séquence d’événements en entrée, plusieurs séquences correctes d’événements peuvent être générées. Cependant, la littérature existante ne propose pas suffisamment d’approches pour sélectionner la meilleure ou l’optimale séquence correcte. Cette thèse propose un pipeline d’application à l’exécution qui englobe l’altération de la séquence d’entrée par l’application des actions correctives nécessaires, garantissant la conformité à la politique de sécurité, et sélectionnant le remplacement optimal en fonction de critères spécifiques. Ces étapes sont divisées en trois modules distincts, offrant une approche modulaire qui simplifie le développement des moniteurs à l’exécution. Nous mettons en oeuvre cette approche à l’aide du processeur de flux d’événements BeepBeep et démontrons son efficacité à travers des cas d’utilisation. L’évaluation expérimentale démontre que le cadre proposé permet de choisir dynamiquement des actions correctives appropriées à l’exécution, éliminant ainsi la nécessité de définir manuellement un moniteur d’application.