Show simple document record

dc.contributor.advisorFrappier, Marcfr
dc.contributor.advisorLaleau, Réginefr
dc.contributor.advisorGervais, Frédéricfr
dc.contributor.authorMilhau, Jérémyfr
dc.date.accessioned2014-05-16T16:04:30Z
dc.date.available2014-05-16T16:04:30Z
dc.date.created2011fr
dc.date.issued2011fr
dc.identifier.isbn9780494833285fr
dc.identifier.urihttp://savoirs.usherbrooke.ca/handle/11143/5165
dc.description.abstractSecurity is a key aspect in information systems (IS) development. One cannot build a bank IS without security in mind. In medical IS, security is one of the most important features of the software. Access control is one of many security aspects of an IS. It defines permitted or forbidden execution of system's actions by an user. Between the conception of an access control policy and its effective deployment on an IS, several steps can introduce unacceptable errors. Using formal methods may be an answer to reduce errors during the modeling of access control policies. Using the process algebra EB[superscript 3], one can formally model IS. Its extension, EB[superscript 3]SEC, was created in order to model access control policies. The ASTD notation combines Harel's Statecharts and EB[superscript 3] operators into a graphical and formal notation that can be used in order to model IS. However, both methods lack tools allowing a designer to prove or verify security properties in order to validate an access control policy. Furthermore, the implementation of an access control policy must correspond to its abstract specification. This thesis defines translation rules from EB[superscript 3] to ASTD, from ASTD to Event-B and from ASTD to B. It also introduces a formal architecture expressed using the B notation in order to enforce a policy over an IS. This modeling of access control policies in B can be used in order to prove properties, thanks to the B prover, but also to verify properties using ProB, a model checker for B. Finally, a refinement strategy for the access control policy into an implementation is proposed. B refinements are proved, this ensures that the implementation corresponds to the initial model of the access control policy.fr
dc.language.isofrefr
dc.publisherUniversité de Sherbrookefr
dc.rights© Jérémy Milhaufr
dc.subjectEB[indice supérieur 3]fr
dc.subjectASTDfr
dc.subjectEvent-Bfr
dc.subjectBfr
dc.subjectContrôle d'accèsfr
dc.subjectSystème d'informationfr
dc.titleUn processus formel d'intégration de politiques de contrôle d'accès dans les systèmes d'informationfr
dc.typeThèsefr
tme.degree.disciplineInformatiquefr
tme.degree.grantorFaculté des sciencesfr
tme.degree.grantotherUniversité Paris-Estfr
tme.degree.levelDoctoratfr
tme.degree.namePh.D.fr


Files in this document

Thumbnail

This document appears in the following Collection(s)

Show simple document record