From Lambda calculus to cybersecurity through program analysis

Preface......Page 7
 References......Page 8
Organization......Page 10
Contents......Page 11
Logic......Page 13
 1 Introduction......Page 14
 2 Cables and Types......Page 15
 3 Trains and Types......Page 20
 4 Conclusion......Page 26
 References......Page 27
 1 Introduction......Page 28
  1.1 Material Incompatibility and Negation......Page 30
  1.2 Negation as the Minimal Incompatible......Page 31
  1.3 Inferences Between Atomic Sentences......Page 32
  1.4 Wittgenstein's Vision of a Logic of Elementary Propositions......Page 33
 2 Mathematical Preliminaries......Page 34
  3.2 Semantics......Page 37
  4.1 Intra-atomic Inferences in Cathoristic Logic......Page 40
  4.2 Intra-atomic Inferences in First-Order Logic......Page 42
  5.1 Representing Facts in Cathoristic Logic......Page 44
  5.3 Using Tantum ! to Optimise Preconditions......Page 46
 6 Semantics and Decision Procedure......Page 47
  6.1 Semantic Characterisation of Elementary Equivalence......Page 48
  6.2 Quotienting Models......Page 50
  6.3 The Bounded Lattice of Models......Page 51
  6.4 Computing the Least Upper Bound of the Models that Satisfy a Formula......Page 52
  6.5 A Decision Procedure for cathoristic logic......Page 58
  6.6 Incompatibility Semantics......Page 59
 7 Inference Rules......Page 61
  7.3 Characteristic Formulae......Page 62
  7.5 Proofs of Lemmas 8, 9 and 10......Page 64
  8.1 Translating from Cathoristic to First-Order Logic......Page 69
  8.2 Compactness by Translation......Page 71
  9.1 Syntax and Semantics......Page 75
  9.2 Decision Procedure......Page 76
 10 Quantified Cathoristic Logic......Page 77
  11.1 Brandom's Incompatibility Semantics......Page 79
  11.2 Peregrin on Defining a Negation Operator......Page 80
  11.4 Linear Logic......Page 81
 12 Open Problems......Page 82
  12.2 Understanding the Expressive Strength of Cathoristic Logic......Page 83
  A.1  Pure Cathoristic Models......Page 87
  A.3  Non-determinism and Cathoristic Models......Page 88
  A.4  Semantic Characterisation of Elementary Equivalence......Page 90
  B.1  Proof of Lemma 5......Page 93
  B.3  Proof of Lemma 7......Page 94
 References......Page 95
 1 Introduction......Page 97
 2 A Probabilistic Typed -calculus......Page 98
  2.1 Probabilistic Types and Subtypes......Page 99
  2.2 Terms and Type Assignment......Page 101
 3 Probabilistic Reduction......Page 103
  3.1 Soundness......Page 106
  3.2 Normalization......Page 107
 4 Examples......Page 108
 5 Related Works......Page 110
 6 Future Work......Page 111
 References......Page 112
Program Analysis......Page 114
 1 Introduction......Page 115
 2 Expression Language and Its Collecting Semantics......Page 117
 3 Abstract Interpretation and Galois Connections......Page 120
  4.1 Recursively Defined Lattices......Page 122
  4.2 Defining the Galois Connection......Page 123
  4.3 Example: Integer Lists......Page 126
  5.1 k-Limited Trees......Page 128
  5.2 Modular Typed Regular Tree Expressions......Page 129
 6 Implementation......Page 133
 7 Related Work......Page 134
 8 Conclusion......Page 135
 A  Proofs......Page 136
 References......Page 140
 1 Introduction......Page 142
 2 Related Work......Page 143
 3 The Top-Down Solver......Page 144
  3.1 Abstract Semantics, Systems of Equations and Their Lower Monotonization......Page 145
  3.2 Generic Local Solving, Variable Dependencies and Computation Trees......Page 146
 4 Invariants......Page 151
 5 Practical Incremental Analysis......Page 152
 6 Experimental Evaluation......Page 154
 References......Page 156
 1 Introduction......Page 159
  2.1 Syntax of EFSMs......Page 163
  2.2 Slicing EFSMs......Page 164
  2.3 Semantics of EFSMs......Page 165
 3 Slicing an EFSM: What Does Correctness Mean?......Page 168
  3.1 Event Sequences......Page 169
  3.2 Relevant Variables......Page 170
  3.3 Completeness......Page 171
  3.4 Soundness......Page 172
 4 Slicing an EFSM: How to Get Correctness?......Page 173
  4.2 Next Observable......Page 174
  4.4 Strong Commitment Closure......Page 175
 5 Computing Least Slices......Page 176
  5.1 Computing Least WCC-Satisfying Slices......Page 178
  5.2 Computing Least SCC-Closed Slices......Page 180
  6.1 Preliminary Definitions......Page 183
  6.3 Definitions for EFSMs with Arbitrary Number of Exit States......Page 184
  6.4 Examples of Slicing Wrt Various Definitions......Page 185
  6.5 Simple Quantitative Comparison of Various Approaches......Page 187
 7 Empirical Evaluation......Page 189
  7.1 Implementation and Tool......Page 190
  7.2 Metrics......Page 191
  7.3 Results Concerning RQ1: Typical Slices Using WCC or SCC......Page 192
  7.4 Results Concerning RQ2(a): Comparing WCC to Previous Control Dependences......Page 194
  7.5 Results Concerning RQ2(b): Comparing SCC to Previous Control Dependences......Page 196
 8 Conclusion......Page 197
  A.1  General Results......Page 198
  A.2  Proving Completeness......Page 199
  A.3  Proving Soundness......Page 200
 B  Proofs of Correctness for Algorithms Computing Least Slices......Page 202
 References......Page 205
Security......Page 208
 1 Introduction......Page 209
 2 Syntax......Page 210
 3 Semantics......Page 213
 4 The Information Flow Landscape......Page 216
 5 Information Flow Type System......Page 218
 References......Page 222
 1 Introduction......Page 224
 2 Background......Page 226
 3 Kill Chain Model......Page 227
 4 Experimental Approach......Page 229
  4.1 Experimental Configuration......Page 230
  4.4 Initial Knowledge Levels......Page 231
  4.6 Intelligence Recall Decay......Page 232
  5.1 Payoff for Threat Intelligence......Page 233
  5.2 Attacker Determination......Page 234
  5.3 Initial Knowledge Levels......Page 235
  5.4 Effectiveness of Learning......Page 236
 6 Discussion......Page 237
 References......Page 239
 1 Introduction......Page 241
 2 Motivating Example......Page 243
 3 Overview of IoT-LySa......Page 248
 4 Control Flow Analysis......Page 251
 5 Conclusions......Page 257
 References......Page 262
 1 Purpose and Aims......Page 264
 2 Verifiable Local Differential Privacy......Page 268
 3 Dependency Analysis: The Need for Disjunction......Page 269
 4 The Abstract Domain of Privacy Regions......Page 271
 References......Page 273
Optimizing Investments in Cyber Hygiene for Protecting Healthcare Users......Page 276
 1 Introduction......Page 277
  2.1 Cyber Hygiene in Healthcare......Page 278
  2.2 Optimal Selection of Cybersecurity Controls......Page 280
  3.1 System Model......Page 281
  3.2 Game-Theoretic Model for Selection of Safeguards Levels......Page 282
  3.3 CSG Solutions......Page 285
  3.4 Optimality Analysis......Page 286
  3.6 Investment in Nash Safeguards Plans......Page 288
  4.1 Use Case......Page 291
  4.2 Comparison with Alternative Defense Strategies......Page 293
  4.3 Analysis of the Investment Problem......Page 296
 5 Conclusions......Page 297
 References......Page 298
Author Index......Page 300