Un moniteur de référence sûr d'une base de données

摘要

La conception d'un logiciel chargé du contrôle d'accès d'un système doit s'effectuer selon des règles strictes, afin de prévenir la présence de failles dans le code qui sera élaboré. L'atelier Focal est un environnement permettant d'écrire, au sein d'un même cadre de travail, des spécifications formelles et du code en démontrant qu'il respecte ces spécifications. Nous avons utilisé cet outil pour formaliser une politique de contrôle d'accès, celle de Bell et La Padula, et l'implanter dans MySQL, un système de gestion de base de données. Cette implantation, fondée sur l'interprétation des requêtes SQL en termes d'accès, prend la forme d'un moniteur de référence qui filtre les requêtes, et rejette celles qui violent la politique de sécurité.%Designing a software in charge of the access control of a system must be carried out according to strict rules in order to avoid faults within this system. The Focal workshop is a programming environment making it possible to write, within the same working context, formal specifications and code with proof that it respects these specifications. We used this tool to formalise a policy of access control, the one of Bell and La Padula, and to implement it in MySQL, a database management system. This implementation, based on the translation of SQL requests in terms of Bell et La Padula requests, is done using an external reference monitor which filters the requests and rejects those which violate the security policy.