Making distributed computation secure by construction


Download Making distributed computation secure by construction


Preview text

MAKING DISTRIBUTED COMPUTATION SECURE BY CONSTRUCTION
A Dissertation Presented to the Faculty of the Graduate School
of Cornell University in Partial Fulfillment of the Requirements for the Degree of
Doctor of Philosophy
by Lantian Zheng January 2007

c 2007 Lantian Zheng ALL RIGHTS RESERVED

MAKING DISTRIBUTED COMPUTATION SECURE BY CONSTRUCTION Lantian Zheng, Ph.D.
Cornell University 2007
This thesis introduces new techniques to build distributed applications that are secure by construction, satisfying strong, end-to-end policies for confidentiality, integrity and availability. The new techniques are designed to solve the problem of how to specify, analyze and enforce end-to-end availability policies in distributed settings, without jeopardizing the enforcement of confidentiality and integrity policies. This thesis also presents a correctness proof for these techniques.

BIOGRAPHICAL SKETCH Lantian Zheng is a graduate student at the Computer Science Department of Cornell University. Lantian received his B.S. degree from Peking University and his M.S. degree from Cornell University.
iii

To my parents iv

ACKNOWLEDGEMENTS I have many people to thank for helping me complete this thesis. First and foremost is my advisor, Andrew Myers. I have learned a great deal from Andrew over the years. Without his guidance this thesis could not have been written.
I also owe a large debt to the other members of my thesis committee: Fred Schneider and Levent Orman. They provided invaluable advice in a timely fashion. I particularly want to thank Fred for his insightful feedback on drafts of this work.
I wish to express warm thanks to Steve Zdancewic, Nate Nystrom and Stephen Chong, who were my collaborators on the Jif/split project. Many of the ideas in this thesis were born out of the project.
Thanks go to Michael Clarkson for his feedback on early drafts of this thesis. Over the years, I have benefited from technical discussions with Andrei Sabelfeld, Lorenzo Alvisi, Heiko Mantel, Greg Morrisett, Wei Wei, Yong Yao, Jed Liu, Michael George, Krishnaprasad Vikram and Xin Qi. I would also like to thank Lidong Zhou for introducing me to the idea of quorum system.
I wish to thank my parents for all of their support during my never-ending education. And thanks to Yuan for providing much-needed distractions.
v

TABLE OF CONTENTS

1 Introduction

1

1.1 Security by construction . . . . . . . . . . . . . . . . . . . . . . . . . 3

1.1.1 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

1.1.2 Secure program partitioning and replication . . . . . . . . . . . 6

1.1.3 What is new . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

1.2 Enforcing availability policies . . . . . . . . . . . . . . . . . . . . . . 8

1.3 Proving correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

1.4 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

1.5 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

2 Universal decentralized label model

13

2.1 Security properties, labels and policies . . . . . . . . . . . . . . . . . . 13

2.2 Dependency analysis and noninterference . . . . . . . . . . . . . . . . 15

2.3 Universal decentralized label model . . . . . . . . . . . . . . . . . . . 18

2.3.1 Owned labels . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

2.3.2 Decentralized labels . . . . . . . . . . . . . . . . . . . . . . . 21

2.3.3 Comparing labels . . . . . . . . . . . . . . . . . . . . . . . . . 22

2.3.4 Information security labels . . . . . . . . . . . . . . . . . . . . 24

2.4 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

2.5 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

3 The Aimp language

30

3.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

3.2 Operational semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

3.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

3.4 Type system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

3.5 Security by type checking . . . . . . . . . . . . . . . . . . . . . . . . . 39

3.5.1 Noninterference properties . . . . . . . . . . . . . . . . . . . . 39

3.5.2 The Aimp* language . . . . . . . . . . . . . . . . . . . . . . . 44

3.5.3 Noninterference proof . . . . . . . . . . . . . . . . . . . . . . 57

3.6 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

4 Secure distributed computation

62

4.1 System model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

4.2 Reactors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

4.2.1 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

4.3 Dynamic label checking . . . . . . . . . . . . . . . . . . . . . . . . . 68

4.4 Replication and message synthesis . . . . . . . . . . . . . . . . . . . . 72

4.4.1 Analyzing security assurances of message synthesizers . . . . . 73

4.4.2 Label threshold synthesizer . . . . . . . . . . . . . . . . . . . . 76

4.5 Using quorum systems . . . . . . . . . . . . . . . . . . . . . . . . . . 78

vi

4.5.1 Tracking timestamps . . . . . . . . . . . . . . . . . . . . . . . 79 4.5.2 Quorum read . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 4.5.3 Quorum write . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 4.6 Multi-level timestamps . . . . . . . . . . . . . . . . . . . . . . . . . . 82 4.7 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 4.8 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

5 The DSR language

88

5.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88

5.2 Operational semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 90

5.3 Type system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96

5.3.1 Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

5.3.2 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98

5.3.3 Subject reduction . . . . . . . . . . . . . . . . . . . . . . . . . 101

5.3.4 Preventing races . . . . . . . . . . . . . . . . . . . . . . . . . 105

5.4 Noninterference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107

5.4.1 ζ-Consistency . . . . . . . . . . . . . . . . . . . . . . . . . . . 109

5.4.2 The DSR* language . . . . . . . . . . . . . . . . . . . . . . . 113

5.4.3 Noninterference proof . . . . . . . . . . . . . . . . . . . . . . 124

5.5 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129

6 Security by construction

130

6.1 Splitter . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130

6.1.1 Statement labels . . . . . . . . . . . . . . . . . . . . . . . . . 131

6.1.2 Secure distribution schemes . . . . . . . . . . . . . . . . . . . 133

6.2 Aimp/DSR translator . . . . . . . . . . . . . . . . . . . . . . . . . . . 135

6.2.1 Remote memory accesses . . . . . . . . . . . . . . . . . . . . 135

6.2.2 Translation rules . . . . . . . . . . . . . . . . . . . . . . . . . 136

6.3 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142

6.4 Typing preservation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144

6.5 Semantics preservation . . . . . . . . . . . . . . . . . . . . . . . . . . 147

6.6 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160

7 Conclusions

162

Bibliography

164

vii

LIST OF FIGURES 1.1 Distributed implementations of the bidding application . . . . . . . . . 4 1.2 Bidding program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Security by construction . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.4 Trustworthiness by construction . . . . . . . . . . . . . . . . . . . . . 10 3.1 Operational semantics for Aimp . . . . . . . . . . . . . . . . . . . . . 32 3.2 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.3 Bidding example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.4 Typing rules for Aimp . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.5 The operational semantics of Aimp* . . . . . . . . . . . . . . . . . . . 46 4.1 System model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 4.2 A distributed program . . . . . . . . . . . . . . . . . . . . . . . . . . 68 4.3 Linear entry creation . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 4.4 Replication example . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 4.5 Quorum replication and timestamps . . . . . . . . . . . . . . . . . . . 84 5.1 Syntax of the DSR language . . . . . . . . . . . . . . . . . . . . . . . 89 5.2 Operational semantics of DSR with respect to Γ and P . . . . . . . . . 91 5.3 Subtyping rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 5.4 Typing rules of DSR . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 5.5 ζ-Equivalence relation . . . . . . . . . . . . . . . . . . . . . . . . . . 108 5.6 The operational semantics of DSR* . . . . . . . . . . . . . . . . . . . 116 5.7 Typing rules of DSR* . . . . . . . . . . . . . . . . . . . . . . . . . . 120 6.1 Rules for inferring statement labels . . . . . . . . . . . . . . . . . . . 132 6.2 Aimp/DSR Translation rules . . . . . . . . . . . . . . . . . . . . . . . 137 6.3 The target DSR code of the bidding example . . . . . . . . . . . . . . 143
viii

Chapter 1 Introduction
Distributed computing systems are ubiquitous, yet it is currently difficult to make strong statements about the security provided by a distributed system as a whole, especially if some of the participants in a distributed computation do not trust other participants or the computing software and hardware they provide. Distributed systems serving mutually distrusting principals include clinical and financial information systems, business-tobusiness transactions, and joint military information systems.
This thesis proposes a unified approach (within a common framework of program analysis and transformation) to building distributed programs that enforce end-to-end confidentiality, integrity and availability policies, in a system with untrusted hosts.
Informally, an end-to-end confidentiality policy of data d specifies who can learn about d; an end-to-end integrity policy of d specifies who can affect d; an end-to-end availability policy of d specifies who can make d unavailable (d is available if the issuer of an authorized access request to d will eventually get the value of d). These policies regulate the behaviors of the whole system and can be viewed as an application of the end-to-end principle [74] to specifying security policies.
End-to-end confidentiality and integrity policies are also known as information flow policies, since they impose restrictions on how information is propagated throughout the system. Dynamic information flow control mechanisms, including mandatory access control (MAC) [9, 19], use run-time checks to ensure that information does not flow to a place protected by a weaker confidentiality policy or a stronger integrity policy. Although widely used in practice, those dynamic mechanisms suffer from high run-time overheads and covert exception channels associated with run-time security checks. Further, these dynamic mechanisms abort the programs that fail a run-time check, making it difficult to enforce availability policies. Denning [18] showed how to use static pro-
1

Preparing to load PDF file. please wait...

0 of 0
100%
Making distributed computation secure by construction