Sécurisation de code basée sur la combinaison de la vérification statique et dynamique : génération de moniteur à partir d'un automate de Rabin
Authors: | Chabot, Hugues |
Advisor: | Tawbi, Nadia |
Abstract: | Ce mémoire présente une nouvelle approche pour sécuriser du code potentiellement malicieux à l'aide d'un moniteur incorporé au code. Les premiers chapitres du mémoire introduisent les notions préliminaires à la présentation de l'approche. Plus précisément, les concepts fondamentaux de la vérification de modèle et du contrôle des systèmes à événements discrets. Le dernier chapitre présente les fondements théoriques de l'approche en généralisant les résultats de Ligatti, Bauer et Walker, et montre une classe de moniteurs qui est plus puissante lorsqu'on précise son contexte d'application. Cette observation mène à l'élaboration d'une approche consistant à instrumenter un programme, dans le but de le rendre sécuritaire, à partir d'un modèle du programme et d'une propriété de sécurité représentée par un automate de Rabin. |
Document Type: | Mémoire de maîtrise |
Issue Date: | 2009 |
Open Access Date: | 16 April 2018 |
Permalink: | http://hdl.handle.net/20.500.11794/20727 |
Grantor: | Université Laval |
Collection: | Thèses et mémoires |
All documents in CorpusUL are protected by Copyright Act of Canada.