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

Files in this item:
SizeFormat 
26107.pdf839.18 kBAdobe PDFView/Open
All documents in CorpusUL are protected by Copyright Act of Canada.