Vérification formelle des propriétés de sécurité des logiciels

Simple item page
dc.contributor.advisorAhmed-Nacer, Mohamed
dc.contributor.authorMohand Oussaïd, Linda
dc.date.accessioned2013-11-25T15:06:52Z
dc.date.available2013-11-25T15:06:52Z
dc.date.issued2006
dc.description.abstractCette thèse présente une démarche de vérification formelle des propriétés de sécurité des logiciels. En effet, après étude des approches possibles : preuve formelle et model checking, nous avons identifié le model checking comme étant l'approche la plus adéquate pour notre problématique. Ainsi, la démarche proposée est fondée sur une combinaison de la technique de model checking et des mécanismes : d'annotation et d'abstraction basés sur l'interprétation abstraite. Pour procéder au model checking, nous avons commencé par exprimer les propriétés de sécurité (confidentialité, intégrité, disponibilité) dans une logique temporelle appropriée. Ensuite, nous avons spécifié les systèmes auxquels pouvait s'appliquer notre démarche à savoir : les systèmes dont l'évolution peut être assimilée à un programme impératif réduit aux structures de contrôle de base. Moyennant deux étapes : la première qui enrichit le code source par des informations relatives à la propriété à vérifier et la deuxième qui débarrasse le code source enrichi des informations superflues à la vérification de la propriété de sécurité, nous avons transformé le code source d'un programme impératif en un programme abstrait qui exhibe les instructions concernées par les propriétés à vérifier tout en faisant abstraction du reste. L'annotation aussi bien que l'abstraction ont été développées par interprétation abstraite autour d'une correspondance de Galois qui assure que le programme abstrait correspond au programme initial. Cette démarche a été illustrée par un exemple qui consiste en un gestionnaire de transactions bancaires simplifié.fr_FR
dc.identifier.urihttp://dl.cerist.dz/handle/CERIST/368
dc.publisherInstitut National de Formation en Informatique (INI)fr_FR
dc.relation.ispartofMémoires de Magister
dc.relation.placeOued Smar, El Harrach - Alger
dc.specialityInformatique : Systèmes d'Informationfr_FR
dc.structureSûreté de Fonctionnement dans le Développement des Logicielsfr_FR
dc.subjectSystèmes informatiques : Mesures de sûretéfr_FR
dc.subjectVérification formellefr_FR
dc.subjectModel checkingfr_FR
dc.subjectPropriétés de sécuritéfr_FR
dc.subjectInterprétation abstraitefr_FR
dc.titleVérification formelle des propriétés de sécurité des logicielsfr_FR
dc.typeThesis
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Vérification formelle des propriétés de sécurité des logiciels.pdf
Size:
647.29 KB
Format:
Adobe Portable Document Format
Description:
Download
Collections
Magister theses