Non Interference on Symbolic Transition System

Ivan Christoff

Description

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

Sujets

• Uppsala University
• Christoff
• System
• Model transformation

Informations

• Publié par: profil-mupheg-2012
• Nombre de lectures: 31
• Langue: English

Extrait

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

.

.

.

.

.

.

.

.

.

.