Les systèmes informatiques offrent une grande flexibilité aux usagers en leur permettant
l’accès, notamment par le biais de réseaux de télécommunication ou de l’Internet, à
un vaste éventail de services. Toutefois, certains de ces services sont soumis à de fortes
contraintes de sécurité, comme le télépaiement qui est au coeur du commerce électronique.
Ainsi, les fournisseurs et les utilisateurs expriment des besoins croissants, et antagonistes,
en sécurité. Répondre à ces deux besoins simultanément est un enjeu technologique transversal
à de nombreux domaines de l’informatique. L’objectif de ce travail est de développer
un mécanisme permettant de garantir la sécurité des systèmes, en s’appuyant sur
l’expérience établie dans le domaine de la sécurité et des méthodes formelles. Pour se
faire, nous définissons un nouveau cadre de vérification des propriétés de sécurité d’un
programme informatique par l’analyse des flots de données et de contrôle construits à
partir du code de ce dernier. L’idée principale consiste à définir un modèle pouvant abstraire
la trace d’événements et les dépendances de ressources engendrés au moment de
l’exécution du programme, et pouvant être soumis à des algorithmes de vérification de
modèle (model-checking) pour l’analyse de la sûreté du programme vis-à-vis d’une propriété.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2008/25710 |
| Date | 10 1900 |
| Creators | Chorfi, Redha |
| Contributors | Ktari, Béchir |
| Publisher | Université Laval |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | text/html, application/pdf |
| Rights | © Redha Chorfi, 2008 |
Page generated in 0.0991 seconds