Non Interference on Symbolic Transition System

pages

English

Documents

Écrit par
Ivan Christoff

Publié par
profil-mupheg-2012

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

profil-mupheg-2012

Nombre de lectures

Langue

English

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

Publié par

profil-mupheg-2012

Nombre de lectures

Langue

English

Uppsala University

Non-Interference on Symbolic Transition System

Jeremy Dubreil

Superviser : Ivan Christoﬀ

Master project hosted at INRIA Rennes in the team VerTeCs.

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 Deﬁnition of Non-Interference . . . . . . . . . . . . . . . . . . 20 3.2.1 general deﬁnition . . . . . . . . . . . . . . . . . . . . . 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 ﬁnite automata . . . . . . . . . . . . . . . . . . . . . . 28 5.2 Extention of non-interference to the STS model . . . . . . . . 31

. . .

An example of LTS . . . . . . . . .

. . .