Description de propriétés de sécurité pour un processus de validation/vérification
Résumé
The work presented in this report deals with the validation of access control dened through security policies. We are interested in the validation by means of test generation based on a security model, written in B. We use the Meca tool, which takes as input a functional model and a description of the security policy, both expressed as B models. Meca generates a security kernel, that is in charge of intercepting the access of the subjects to the objects, and restricts the behaviors to those that satisfy the security requirements. We present a complete case study, led on an electronic purse case study, using a discretionary access control policy.
Les travaux présentés dans ce rapport s'articulent autour de la validation du contrôle d'accès déni par des politiques de sécurité. Nous nous intéressons à la validation par génération de tests à partir d'un modèle de sécurité écrit en B et décrivant les fonctionnalités de l'application. Nous utilisons l'outil Meca, qui prend en entrée un modèle fonctionnel et une description d'une politique de sécurité sous la forme de machines abstraites B, et qui génère un noyau de sécurité pour le modèle fonctionnel. Ce noyau de sécurité est en charge d'intercepter tous les accès des sujets aux objets, et restreint les comportements à ceux satisfaisant les exigences de sécurité. Nous présentons une étude de cas complète, sur une application de type porte-monnaie électronique, agrémentée d'une politique de sécurité discrétionnaire.