Ce mémoire traite en premier lieu des avantages et des
désavantages des différentes approches visant à assurer la sûreté
et la sécurité des logiciels. En second lieu, il présente une
nouvelle approche pour combiner l'analyse statique et l'analyse
dynamique afin de produire une architecture de sécurité plus
puissante.
Les premiers chapitres du mémoire comportent une revue analytique
des différentes approches statiques, dynamiques et hybrides qui
peuvent être utilisées afin de sécuriser le code potentiellement
malicieux. L'exposé identifie alors les avantages et les
inconvénients de chaque approche ainsi que le champ des politiques
de sécurité dans lesquels on peut l'appliquer. Le dernier
chapitre traite de la possibilité de combiner l'analyse statique
et l'analyse dynamique par une nouvelle approche hybride. Cette
approche consiste à instrumenter le code seulement là où c'est
nécessaire pour assurer satisfaire une politique de sécurité
définie par l'usager et exprimée en un ensemble de propriétés
exprimées μ-calcul modal. Cette instrumentation est guidée par
une analyse statique effectuée à priori et basée sur un système de
type à effets. Les effets représentent les accès aux ressources
protégées du système. / The purpose of this thesis is twofold. In the first place it presents a comparative
study of the advantages and drawbacks of several approaches to insure software safety
and security. It then focuses more particularly on combining static analyses and dynamic
monitoring in order to produce a more powerful security architecture.
The first chapters of the thesis present an analytical review of the various static,
dynamic and hybrid approaches that can be used to secure a potentially malicious
code. The advantages and drawbacks of each approach are thereby analyzed and the
field of security properties that can be enforced by using it are identified. The thesis
then focuses on the possibility of combining static and dynamic analysis through a
new hybrid approach. This approach consists in a code instrumentation, that only
alters those parts of a program where it is necessary to do so to insure the respect of
a user-defined security policy expressed in a set of modal μ-calculus properties. this
instrumentation is guided by a static analysis based on a type and effect system. The
effects represent the accesses made to pretested system ressources.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2005/23250 |
| Date | 12 1900 |
| Creators | Khoury, Raphaël |
| Contributors | Tawbi, Nadia |
| 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 | © Raphaël Khoury, 2005 |
Page generated in 0.0025 seconds