Durant ces dernières décennies, nous avons assisté à une automatisation massive de la
société selon toutes ses sphères. Malheureusement, cette révolution technologique n’a pas eu
que des bienfaits. En effet, une nouvelle génération de criminels en a profité, afin d’occasionner
davantage d’activités illégales. De ce fait, afin de protéger les systèmes informatiques, il
est devenu plus que primordial de définir rigoureusement des politiques de sécurité ainsi que
de mettre en oeuvre des mécanismes efficaces capables de les appliquer. L’objectif majeur
d’un mécanisme de sécurité consiste souvent à contrôler des logiciels, afin de les contraindre
à “bien” se comporter. Cependant, la plupart des mécanismes de sécurité procèdent par des
méthodes ad hoc qui sont loin d’être efficaces. En outre, ils sont peu fiables, puisqu’il n’y
a aucune preuve sur leur capacité à faire respecter les politiques de sécurité. De là apparaît
la nécessité de concevoir des mécanismes de sécurité alternatifs qui résolvent le problème
de l’application de la sécurité d’une manière formelle, correcte et précise. Dans ce contexte,
notre thèse cible principalement la caractérisation formelle de l’application effective des politiques
de sécurité via des mécanismes basés sur la réécriture de programmes. On entend par
application effective, le fait d’éliminer tous les “mauvais” comportements d’un programme,
tout en conservant tous les “bons” comportements qu’il engendre, et ce, sans compromettre
la sémantique du programme à sécuriser. Nous avons opté pour la réécriture de programmes,
vu sa grande puissance par rapport aux autres mécanismes de sécurité qui sont soit laxistes
soit très restrictifs. Les principaux résultats qui ont été réalisés, afin d’atteindre les objectifs
ciblés par cette thèse sont les suivants :
– Caractérisation formelle de l’application des propriétés de sûreté par la réécriture de
programmes. Il s’agit d’appliquer les propriétés de sûreté qui constituent la classe de
propriétés de sécurité la plus communément appliquée par les mécanismes de sécurité.
– Caractérisation formelle de l’application de n’importe quelle propriété de sécurité par
la réécriture de programmes. Cette contribution montre comment la réécriture de programmes
permet l’application de politiques de sécurité qu’aucune autre classe de mécanismes
de sécurité ne peut appliquer.
– Caractérisation alternative de l’application de la sécurité par une approche algébrique.
Cette contribution propose un formalisme algébrique afin de réduire l’écart
entre la spécification et l’implantation des mécanismes de sécurité basés-réécriture. / During the last decades, we have witnessed a massive automation of the society at all
levels. Unfortunately, this technological revolution came with its burden of disadvantages.
Indeed, a new generation of criminals emerged and is benefitting from continuous progress of
information technologies to cause more illegal activities. Thus, to protect computer systems,
it has become very crucial to rigorously define security policies and provide the effective mechanisms
required to enforce them. Usually, the main objective of a security mechanism is to
control the executions of a software and ensure that it will never violate the enforced security
policy. However, the majority of security mechanisms are based on ad hoc methods and thus,
are not effective. In addition, they are unreliable, since there is no evidence on their ability
to enforce security policies. Therefore, there is a need to develop novel security mechanisms
that allow enforcing security policies in a formal, correct, and accurate way. In this context,
our thesis targets the formal characterization of effective security policies enforcement that is
based on programs rewriting. We mean by “effective” enforcement preventing all the “bad”
behaviors of a program while keeping all its "good" behaviors. In addition, effective enforcement
should not compromise the semantics of controlled programs. We have chosen for
rewriting programs, because it has a great power compared to other security mechanisms that
are either permissive or too restrictive. Themain contributions of this thesis are the following :
– Formal characterization of security enforcement of safety properties through program
rewriting. Safety properties represent the main class of properties usually enforced by
security mechanisms.
– Formal characterization of any security property using program rewriting. This contribution
shows how program rewriting allows the enforcement of security policies that
no other class of security mechanisms can enforce.
– Algebraic approach as an alternative formal characterization of program rewriting
based security enforcement. In this contribution, we investigate an algebraic formal
model in order to reduce the gap between the specification and the implementation of
program rewriting based security mechansisms.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2011/28026 |
| Date | 03 1900 |
| Creators | Ould-Slimane, Hakima |
| Contributors | Mejri, Mohamed, Adi, Kamel |
| 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 | application/pdf |
| Rights | © Hakima Ould-Slimane, 2011 |
Page generated in 0.0024 seconds