Security Policy Enforcement Through Refinement Process

Abstract : In the area of networks, a common method to enforce a security policy expressed in a high-level language is based on an ad-hoc and manual rewriting process. We argue that it is possible to build a formal link between concrete and abstract terms, which can be dynamically computed from the environment data. In order to progressively introduce configuration data and then simplify the proof obligations, we use the B refinement process. We present a case study modeling a network monitor. This program, described by refinement following the layers of the TCP/IP suite protocol, has to warn for all observed events which do not respect the security policy. To design this model, we use the event-B method because it is suitable for modeling network concepts. This work has been done within the framework of the POTESTAT project, based on the research of network testing methods from a high-level security policy.
Type de document :
Communication dans un congrès
Jacques Julliand and Olga Kouchnarenko. B 2007, 2007, besançon, France. Springer-Verlag, 4355, pp.216--231, 2007, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00384182
Contributeur : Nicolas Stouls <>
Soumis le : jeudi 8 avril 2010 - 09:32:02
Dernière modification le : jeudi 11 janvier 2018 - 06:20:26
Document(s) archivé(s) le : mardi 14 septembre 2010 - 17:05:06

Fichiers

b07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00384182, version 1
  • ARXIV : 1004.1460

Collections

IMAG | UGA

Citation

Nicolas Stouls, Marie-Laure Potet. Security Policy Enforcement Through Refinement Process. Jacques Julliand and Olga Kouchnarenko. B 2007, 2007, besançon, France. Springer-Verlag, 4355, pp.216--231, 2007, Lecture Notes in Computer Science. 〈inria-00384182〉

Partager

Métriques

Consultations de la notice

164

Téléchargements de fichiers

250