Design and verification of a cryptographic security architecture

Cover......Page 1
Overview and Goals......Page 8
Organisation and Features......Page 9
Acknowledgements......Page 11
Contents......Page 14
1.1 Introduction......Page 20
1.2 An Introduction to Software Architecture......Page 21
1.2.1 The Pipe-and-Filter Model......Page 22
1.2.2 The Object-Oriented Model......Page 23
1.2.3 The Event-Based Model......Page 24
1.2.5 The Repository Model......Page 25
1.2.7 The Forwarder-Receiver Model......Page 26
1.3 Architecture Design Goals......Page 27
1.4 The Object Model......Page 28
1.4.1 User   Object Interaction......Page 29
1.4.2 Action Objects......Page 31
1.4.3 Data Containers......Page 32
1.4.4 Key and Certificate Containers......Page 33
1.4.6 The Overall Architectural and Object Model......Page 34
1.5 Object Internals......Page 36
1.5.1 Object Internal Details......Page 37
1.5.2 Data Formats......Page 39
1.6 Interobject Communications......Page 40
1.6.1 Message Routing......Page 42
1.6.2 Message Routing Implementation......Page 44
1.6.3 Alternative Routing Strategies......Page 45
1.7 The Message Dispatcher......Page 46
1.7.1 Asynchronous versus Synchronous Message Dispatching......Page 49
1.8 Object Reuse......Page 50
1.8.1 Object Dependencies......Page 53
1.9 Object Management Message Flow......Page 54
1.10 Other Kernel Mechanisms......Page 56
1.10.2 Threads......Page 57
1.11 References......Page 58
2.1 Security Features of the Architecture......Page 64
2.1.1 Security Architecture Design Goals......Page 65
2.2.1 Access Control......Page 66
2.2.3 Security Policies and Models......Page 68
2.2.4 Security Models after Bell–LaPadula......Page 70
2.2.5 Security Kernels and the Separation Kernel......Page 73
2.2.6 The Generalised TCB......Page 76
2.2.7 Implementation Complexity Issues......Page 78
2.3 The cryptlib Security Kernel......Page 80
2.3.1 Extended Security Policies and Models......Page 82
2.3.2 Controls Enforced by the Kernel......Page 84
2.4 The Object Life Cycle......Page 85
2.4.1 Object Creation and Destruction......Page 87
2.5 Object Access Control......Page 89
2.5.1 Object Security Implementation......Page 91
2.5.2 External and Internal Object Access......Page 93
2.6 Object Usage Control......Page 94
2.6.1 Permission Inheritance......Page 95
2.6.2 The Security Controls as an Expert System......Page 96
2.6.3 Other Object Controls......Page 97
2.7 Protecting Objects Outside the Architecture......Page 98
2.7.1 Key Export Security Features......Page 100
2.8 Object Attribute security......Page 101
2.9 References......Page 102
3.1.1 Rule-based Policy Enforcement......Page 112
3.1.2 The DTOS/Flask Approach......Page 113
3.1.3 Object-based Access Control......Page 115
3.1.4 Meta-Objects for Access Control......Page 117
3.1.5 Access Control via Message Filter Rules......Page 118
3.2 Filter Rule Structure......Page 120
3.2.1 Filter Rules......Page 121
3.3 Attribute ACL Structure......Page 125
3.3.1 Attribute ACLs......Page 127
3.4 Mechanism ACL Structure......Page 131
3.4.1 Mechanism ACLs......Page 132
3.5.1 Pre-dispatch Filters......Page 136
3.5.2 Post-dispatch Filters......Page 138
3.6 Customising the Rule-Based Policy......Page 139
3.7 Miscellaneous Implementation Issues......Page 141
3.9 References......Page 142
4.2 Formal Security Verification......Page 146
4.2.1 Formal Security Model Verification......Page 149
4.3.1 Problems with Tools and Scalability......Page 150
4.3.2 Formal Methods as a Swiss Army Chainsaw......Page 152
4.3.3 What Happens when the Chainsaw Sticks......Page 154
4.3.4 What is being Verified/Proven?......Page 157
4.3.5 Credibility of Formal Methods......Page 161
4.3.6 Where Formal Methods are Cost-Effective......Page 163
4.3.7 Whither Formal Methods?......Page 164
4.4 Problems with other Software Engineering Methods......Page 165
4.4.1 Assessing the Effectiveness of Software Engineering Techniques......Page 168
4.5 Alternative Approaches......Page 171
4.5.1 Extreme Programming......Page 172
4.6 References......Page 173
5.1 An Analytical Approach to Verification Methods......Page 186
5.1.1 Peer Review as an Evaluation Mechanism......Page 187
5.1.3 Selecting an Appropriate Specification Method......Page 189
5.1.4 A Unified Specification......Page 192
5.1.5 Enabling Verification All the way Down......Page 193
5.2 Making the Specification and Implementation Comprehensible......Page 194
5.2.1 Program Cognition......Page 195
5.2.2 How Programmers Understand Code......Page 196
5.2.3 Code Layout to Aid Comprehension......Page 199
5.2.4 Code Creation and Bugs......Page 201
5.2.5 Avoiding Specification/Implementation Bugs......Page 202
5.3 Verification All the Way Down......Page 203
5.3.1 Programming with Assertions......Page 205
5.3.2 Specification using Assertions......Page 207
5.3.3 Specification Languages......Page 208
5.3.4 English-like Specification Languages......Page 209
5.3.5 Spec......Page 211
5.3.6 Larch......Page 212
5.3.7 ADL......Page 213
5.3.8 Other Approaches......Page 216
5.4.1 Verification of the Kernel Filter Rules......Page 218
5.4.2 Specification-Based Testing......Page 219
5.4.3 Verification with ADL......Page 221
5.5 Conclusion......Page 222
5.6 References......Page 223
6.1 Introduction......Page 234
6.2 Requirements and Limitations of the Generator......Page 237
6.3 Existing Generator Designs and Problems......Page 240
6.3.1 The Applied Cryptography Generator......Page 242
6.3.2 The ANSI X9.17 Generator......Page 243
6.3.3 The PGP 2.x Generator......Page 244
6.3.4 The PGP 5.x Generator......Page 246
6.3.5 The /dev/random Generator......Page 247
6.3.6 The Skip Generator......Page 249
6.3.7 The ssh Generator......Page 250
6.3.8 The SSLeay/OpenSSL Generator......Page 251
6.3.9 The CryptoAPI Generator......Page 254
6.3.10 The Capstone/Fortezza Generator......Page 255
6.3.11 The Intel Generator......Page 257
6.4.1 The Mixing Function......Page 258
6.4.2 Protection of Pool Output......Page 259
6.4.5 Nonce Generation......Page 261
6.4.6 Generator Continuous Tests......Page 262
6.4.7 Generator Verification......Page 263
6.4.8 System-specific Pitfalls......Page 264
6.4.9 A Taxonomy of Generators......Page 267
6.5.1 Problems with User-Supplied Entropy......Page 268
6.5.2 Entropy Polling Strategy......Page 269
6.5.4 Macintosh and OS/2 Polling......Page 270
6.5.6 Win32 Polling......Page 271
6.5.7 Unix Polling......Page 272
6.6 Randomness-Polling Results......Page 275
6.6.1 Data Compression as an Entropy Estimation Tool......Page 276
6.6.2 Win16/Windows 95/98/ME Polling Results......Page 278
6.6.3 Windows NT/2000/XP Polling Results......Page 279
6.7 Extensions to the Basic Polling Model......Page 280
6.8 Protecting the Randomness Pool......Page 282
6.9 Conclusion......Page 285
6.10 References......Page 286
7.1 Problems with Crypto on End-User Systems......Page 294
7.1.1 The Root of the Problem......Page 296
7.1.2 Solving the Problem......Page 298
7.1.3 Coprocessor Design Issues......Page 299
7.2.1 Coprocessor Hardware......Page 302
7.2.2 Coprocessor Firmware......Page 304
7.2.3 Firmware Setup......Page 305
7.3 Crypto Functionality Implementation......Page 306
7.3.2 Communications Hardware......Page 308
7.3.3 Communications Software......Page 309
7.3.4 Coprocessor Session Control......Page 310
7.3.5 Open versus Closed-Source Coprocessors......Page 312
7.4.1 Controlling Coprocessor Actions......Page 313
7.4.2 Trusted I/O Path......Page 314
7.4.3 Physically Isolated Crypto......Page 315
7.4.4 Coprocessors in Hostile Environments......Page 316
7.6 References......Page 318
8.1.1 Separation Kernel Enforcing Filter Rules......Page 324
8.1.3 Use of Specification-based Testing......Page 325
8.1.5 Practical Design......Page 326
8.2 Future Research......Page 327
9 Glossary......Page 328
Index......Page 336