Abstract FR:

Le but de cette thèse est de réussir à créer un environnement de conception et de réalisation d'un modèle de sécurité global d'un système d'informations. Après une première analyse des différents paradigmes mis en évidence sur différents systèmes informatiques (systèmes d'exploitation, S. G. B. D. , carte à microprocesseur), il est apparu que tous présentaient certaines faiblesses. D'une part le manque de capacité d'expression du système qui ne prend en compte que quelques opérations de base. La plupart du temps, ce manque impose la présence d'un super-utilisateur qui peut corriger le schéma selon les circonstances. D'autre part, l'éclatement du schéma selon les différentes entités à protéger ne permet pas une complète et facilement malléable description et a fortiori la preuve du schéma. Pour répondre à tous ces commentaires, nous avons pensé à une manière de résoudre ces problèmes. Nous avons construit un langage qui pourrait permettre à un utilisateur de décrire un schéma de sécurité dans le cas particulier d'un système d'exploitation. Nous nous efforcerons à ce propos d'obtenir un schéma de fine granularité en insistant fortement sur la possibilité de résoudre une partie de la conception de ce schéma par respect de règles d'intégrité. Nous avons mis en place un outil afin de tester et de valider ce langage sur un exemple se référant à un système d'exploitation d'une carte à microprocesseur que nous décrirons. L'adéquation du travail dans le milieu restreint de la carte à microprocesseur sera alors traité.