Abstract
This thesis presents a general theory of system composition for possibilistic security properties. It is shown that possibilistic security properties can be viewed as a predicate over the traces that are consistent with a low level observation tlow. We provide a uniform framework for analyzing and comparing these properties. We demonstrate how to determine what security property a system satisfies given the security properties satisfied by its constituent components. Also, we show how to construct a system that satisfies a desired security property. This analysis yields a condition that can be used to determine how a property may emerge under composition. We examine the reasons for the failure of feedback composition and provide necessary and sufficient conditions for determining when feedback composition will fail for all properties based on Generalized Noninterference. Unwinding theorems are given for a large class of security properties.
Table Of Contents
Abstract .........................................................................................................................ii
Acknowledgments.........................................................................................................iii
Table Of Contents ........................................................................................................iv
List of Figures.............................................................................................................viii
List of Definitions .........................................................................................................ix
Glossary of Symbols ......................................................................................................x
1. INTRODUCTION AND OVERVIEW 1
1.1. INTRODUCTION 1
1.2. SECURITY PROPERTIES AND SYSTEMS 2
1.3. COMPOSABILITY 2
1.4. THIS THESIS 3
1.5. OVERVIEW 3
2. PREVIOUS WORK 5
2.1. INTRODUCTION 5
2.2. EVENT SYSTEMS 5
2.3. CONFIDENTIALITY MODELS 5
2.3.1. LATTICE APPROACHES TO SECURITY 6
2.3.2. FORMAL CRITERIA 6
2.3.3. POSSIBILISTIC SECURITY PROPERTIES 7
2.3.4. SUTHERLAND’S DEDUCIBILITY 7
2.4. COMPOSABILITY 8
2.4.1. HOOK-UP SECURITY 8
2.4.2. SAFETY AND LIVENESS 9
2.4.3. COMPOSING SPECIFICATIONS 9
2.4.4. SELECTIVE INTERLEAVING FUNCTIONS 10
2.5. BUNCH THEORY 11
2.6. UNWINDING THEOREMS 12
2.7. SUMMARY 13
3. COMPONENTS AND SYSTEMS 14
3.1. INTRODUCTION 14
3.2. TRACES 15
3.3. DISCRETE EVENT SYSTEMS 16
3.4. COMPOSITION 18
3.5. SUMMARY 24
4. SECURITY PROPERTIES 25
4.1. INTRODUCTION 25
4.2. PROPERTIES OF SECURE SYSTEMS 26
4.3. INFERENCE 27
4.3.1. THE PERFECT SECURITY PROPERTY 30
4.4. SECURITY PROPERTIES 33
4.4.1. NONINFERENCE 34
4.4.2. NONINTERFERENCE 35
4.4.2.1. Forward Correctability 36
4.4.3. NON-DEDUCIBLE OUTPUT SECURITY 36
4.4.4. SEPARABILITY 37
4.5. COMPARING SECURITY PROPERTIES 38
4.6. PSP SECURITY PROOFS 40
4.7. SECURITY PROPERTIES VS. SAFETY/LIVENESS PROPERTIES 42
4.8. CONCLUSIONS 43
5. COMPOSITION AND THE EMERGENCE OF SECURITY PROPERTIES 44
5.1. INTRODUCTION 44
5.2. CLASSIFICATION OF PROPERTIES 45
5.3. INTERCONNECTIONS OF COMPONENTS 46
5.3.1. CASCADE COMPOSITION 47
5.3.2. CONSEQUENCES OF INPUT TOTALITY 54
5.4. EMERGENT PROPERTIES 55
5.5. FEEDBACK COMPOSITION 58
5.5.1. LOW LEVEL PRECONDITIONS AND SYSTEM STATE 61
5.5.2. THEOREMS ON FEEDBACK COMPOSITION 62
5.5.3. WHY DUMMY COMPONENTS? 68
5.5.4. EMERGENT PROPERTIES IN THE PRESENCE OF FEEDBACK 69
5.5.5. WHY CERTAIN PROPERTIES COMPOSE 69
5.6. SUMMARY AND CONCLUSIONS 71
6. COMPARISON TO SELECTIVE INTERLEAVING FUNCTIONS 72
6.1. INTRODUCTION 72
6.2. COMPARISON OF EXPRESSABILITY 73
6.3. COMPARISON OF RESULTS 75
6.4. SUMMARY 76
7. IMPLEMENTATION ISSUES 77
7.1. INTRODUCTION 77
7.2. EVENT SYSTEM ACCEPTORS 78
7.3. SECURITY PROPERTIES 82
7.4. UNWINDING THEOREMS 83
7.5. UNWINDING THEOREM FOR GNI AND N-FORWARD CORRECTABILITY 84
7.5.1. FORWARD CORRECTABLE VERSUS NON-FORWARD CORRECTABLE GNI 85
7.5.2. UNWINDING THEOREMS 86
7.6. UNWINDING THEOREM FOR PSP 90
7.7. UNWINDING THEOREM FOR GENERALIZED NONINTERFERENCE. 91
7.8. CONCLUSIONS 91
8. SUMMARY AND CONCLUSIONS 92
8.1. SUMMARY 92
