Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Non Interference on Symbolic Transition System

De
35 pages
Niveau: Supérieur, Master
Uppsala University Non-Interference on Symbolic Transition System Jeremy Dubreil Superviser : Ivan Christoff Master project hosted at INRIA Rennes in the team VerTeCs. 1

  • interference checking

  • framework used

  • without any illegal

  • property given

  • between users

  • system calls invisible

  • system

  • model transformation


Voir plus Voir moins
Uppsala University
Non-Interference on Symbolic Transition System
Jeremy Dubreil
Superviser : Ivan Christoff
Master project hosted at INRIA Rennes in the team VerTeCs.
1
Contents
1 Security Policies 6 1.1 MLS, Multi Layer Secure models . . . . . . . . . . . . . . . . 6 1.1.1 The Bell and La Padula Model . . . . . . . . . . . . . 7 1.1.2 The Biba integrity model . . . . . . . . . . . . . . . . . 8 1.1.3 The HRU model . . . . . . . . . . . . . . . . . . . . . 9 1.2 Non-Interference model . . . . . . . . . . . . . . . . . . . . . . 9 2 Modeling framework 11 2.1 The LTS model . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.2 The STS model . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3 Semantics of an STS . . . . . . . . . . . . . . . . . . . . . . . 14 3 Notion of Non-Interference 16 3.1 Some introductory examples . . . . . . . . . . . . . . . . . . . 16 3.2 Definition of Non-Interference . . . . . . . . . . . . . . . . . . 20 3.2.1 general definition . . . . . . . . . . . . . . . . . . . . . 20 3.2.2 Interference and diagnosis . . . . . . . . . . . . . . . . 20 4 Model transformations 22 4.1 Composition of two STS . . . . . . . . . . . . . . . . . . . . . 22 4.2 Product of twoST S 23. . . . . . . . . . . . . . . . . . . . . . . 4.3ε-closure of anST S 24. . . . . . . . . . . . . . .. . . . . . . . . 4.4 Determination of an STS . . . . . . . . . . . . . . . . . . . . . 25 5 Checking Non-Interference 28 5.1 Case of finite automata . . . . . . . . . . . . . . . . . . . . . . 28 5.2 Extention of non-interference to the STS model . . . . . . . . 31
2
. . .
. . .
An example of LTS . . . . . . . . .
. . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
5.1
4.1 4.2
3.1 3.2 3.3
2.1
List of Figures
. .
. .
. .
. .
Calculating theε-closure of a STS . Basic step for calculatingdet(M) .
Example of calculation ofχψ(M)
.
.
. .
. .
. .
. .
. .
. .
. .
. .
. . .
. . .
. . .
. . .
. .
An example of interference . . . . . Unsafe coffee machine . . . . . . . Non-interfering coffee machine . . .
. .
. .
. . .
. . .
. . .
. . .
. . .
. . .
. . .
. . .
3
25 27
31
.
.
.
.
17 18 19
12
.
.
.
.
.
.
.
.
.
.
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin