Formal Modeling and Verification of Access-Control Policies

  • Hubert Toussaint

Thèse de l'étudiant: Doc typesDocteur en Sciences


The construction of secure software is a notoriously difficult task. The abstract security requirements have to be turned into functional requirements and then implemented. However, only few techniques allow to verify that the implemented elements fulfill the originally expressed requirements. The potential gap between the specification and the implementation gets even wider with iterative development schemes where code (and sometimes specification) is updated numerous times. In this document we propose a methodology aimed at facilitating the co-evolution of the security requirements and the implemented code. Focusing on the access-control perspective, we provide models and algorithms to specify the expected requirements and to extract the implemented access-control rules directly from the executable source code. Then we verify the conformance of the implemented features towards the specified requirements and, if inconsistencies are found, we provide potential corrective measures that can be applied directly into the source code.
la date de réponse21 sept. 2011
langue originaleAnglais
L'institution diplômante
  • Universite de Namur
SuperviseurPIERRE-YVES SCHOBBENS (Promoteur), Jean-Marie JACQUET (Président), Jean-Noel COLIN (Jury), Charles Morisset (Jury) & Yves Le Traon (Jury)

Contient cette citation