Cadre algébrique pour le renforcement de politique de sécurité sur des systèmes concurrents par réécriture automatique de programmes

La société moderne est de plus en plus dépendante de l'informatique dont le rôle est devenu tellement vital au point que tout dysfonctionnement peut engendrer des pertes considérables voire des conséquences irréversibles telles que la perte de vies humaines. Pour minimiser les dégâts, plusieurs techniques et outils ont été mis en place au cours des dernières années. Leur objectif est de faire en sorte que nos systèmes informatiques fonctionnent <<~tout le temps~>>, et ce, tout en produisant les résultats escomptés. La duplication du matériel et les tests de logiciels sont parmi les techniques les plus utilisées. Cependant, sans méthodes formelles, rien n'est garanti et des problèmes peuvent surgir à tout moment. En contrepartie, l'utilisation de méthodes formelles n'est pas à la portée de tout le monde y compris les programmeurs chevronnés et la tâche reste subtile et complexe même pour les spécialistes. Quelques lignes de code nécessitent parfois des centaines de lignes de preuve difficiles à lire et à comprendre. Malgré tout, leur utilisation n'est plus un luxe, mais plutôt nécessaire afin d'éviter les dégâts engendrés par les mauvais fonctionnements de nos systèmes critiques. Le principal objectif de notre recherche est de développer un cadre formel et automatique pour le renforcement de politique de sécurité sur des systèmes concurrents. Plus précisément, l'idée consiste à ajouter dans un programme des tests à des endroits soigneusement calculés pour qu'une politique de sécurité soit respectée. La nouvelle version du programme préserve toutes les traces de la version originale respectant la politique de sécurité et bloque les traces qui ne peuvent plus respecter la politique de sécurité même si elles sont complétées par certains suffixes. Les principaux résultats ayant contribué à l'atteinte de cet objectif sont : 1. La définition d'une algèbre de processus [symbol] offrant un cadre purement algébrique pour le renforcement de politique de sécurité sur des systèmes concurrents. Plus précisément, nous avons défini un nouvel opérateur qui permet de renforcer, d'une manière intuitive, une politique de sécurité sur un système concurrent. 2. La définition d'une logique, dénotée par [symbol], inspirée des expressions régulières étendues. En effet, [symbol] est une logique linéaire qui exprime la classe de langage régulier, mais avec la possibilité d'exprimer des propriétés infinies. 3. La définition d'une algèbre [symbol] basée sur l'algèbre [symbol]. [symbol] définit un nouvel opérateur de renforcement qui tient compte de l'introduction de la logique. 4. Le développement d'une technique d'optimisation qui, pour une certaine classe de propriétés de sécurité, permet de réduire le nombre de tests insérés dans le programme renforcé.One of the important goals of the software development process is proving that the produced systems always meet their requirements. However, establishing this goal is not only subtle and complex, but also requires high qualified persons. In addition, this operation is mostly omitted due to its high cost and the system is tested while trying to reduce the risk of errors as much as possible. The cost is, nevertheless, paid when this operation is required in order to avoid catastrophic consequences and major errors. In these cases, tools like theorem prover and those used for automatic generation of software are helpful to significantly reduce the cost of proof. Our aim is that this tool proves to be powerful and simple enough to generate benefits even to small companies and individuals with scarce budgets and limited theoretical skills . Many promising formal frameworks for automatic enforcement of security policies in programs have been proposed during the last years. Their goal is to ensure that a program respects a given security policy which generally specifies acceptable executions of the program and can be expressed in terms of access control problems, information flow, availability of resources, confidentiality, etc. The literature records various techniques for enforcing security policies belonging to mainly two principal classes: static approaches including typing theory, Proof Carrying Code, and dynamic approaches including reference monitors, Java stack inspection. Static analysis aims at enforcing properties before program execution. In dynamic analysis, however, the enforcement takes place at runtime by intercepting critical events during the program execution and halting the latter whenever an action is attempting to violate the property being enforced. Recently, several researchers have explored rewriting techniques in order to gather advantages of both static and dynamic methods. The idea consists in modifying a program statically, so that the produced version respects the requested requirements. The rewritten program is generated from the original one by adding, when necessary, some tests at some critical points to obtain the desired behaviors. This thesis aims to propose an algebraic and automatic approach that could generate from a given program, and a security policy, a new version of this program that respects the requested security policy. More precisely, we define an operator [symbol] that takes as input a process [symbol] and a security policy [symbol] and generates [symbol], a new process that respects the following conditions: [symbol] "satisfies" the security policy [symbol]. [symbol], behaviours of [symbol] are also behaviours of [symbol]. [symbol], all good behaviours of [symbol] are also behaviours [symbol]. The main results of our research are the following~: 1. The definition of a process algebra [symbol] offering an algebraic framework for the enforcement of security policies on concurrent systems. 2. The definition of a logic, denoted by [symbol], inspired from Kleene algebras and regular expressions. Basically, it allows to specify properties that can be checked on a trace-based model and properties related to infinite behavior (e.g. a server should not send the password of users). The choice of this logic is motivated by its syntax that is close to the one chosen for processes. In fact, this similarity is helpful to simplify the definition of our formal monitor. 3. The development of an optimization technique which, for a certain class of security properties, reduces the number of tests added in the target