Principles of Security and Trust : 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6{u2013}11, 2019, Proceedings

This open access book constitutes the proceedings of the 8th International Conference on Principles of Security and Trust, POST 2019, which took place in Prague, Czech Republic, in April 2019, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2019. The 10 papers presented in this volume were carefully reviewed and selected from 27 submissions. They deal with theoretical and foundational aspects of security and trust, including on new theoretical results, practical applications of existing foundational ideas, and innovative approaches stimulated by pressing practical problems. ETAPS Foreword 6 Preface 8 Organization 9 Contents 10 Foundations for Parallel Information Flow Control Runtime Systems 11 1 Introduction 11 2 Internal Manifestation of External Attacks 14 2.1 Overview of the Concurrent LIO Information Flow Control System 14 2.2 External Timing Attacks to Runtime Systems 15 2.3 Internalizing External Timing Attacks 16 3 Secure, Parallel Runtime System 17 4 Hierarchical Calculus 18 4.1 Core Scheduler 21 4.2 Resource Reclamation and Observations 24 4.3 Parallel Scheduler 26 5 Security Guarantees 28 5.1 Erasure Function 28 5.2 Timing-Sensitive Non-interference 30 6 Limitations 31 7 Related Work 33 8 Conclusion 34 References 34 A Formal Analysis of Timing Channel Security via Bucketing 39 1 Introduction 39 2 Security Against Adaptive Side-Channel Attacks 41 2.1 Insufficiency of Bucketing 44 3 Sufficient Conditions for Security Against Adaptive Side-Channel Attacks 45 3.1 Secret-Restricted Side-Channel Refinement Condition 45 3.2 Low-Input Side-Channel Non-Interference Condition 48 3.3 Combining Bucketing and Constant-Time Implementation Compositionally 52 4 Related Work 57 5 Conclusion and Future Work 57 References 58 A Dependently Typed Library for Static Information-Flow Control in Idris 61 1 Introduction 61 1.1 Assumptions and Threat Model 63 2 The DepSec Library 64 3 Case Study: Conference Manager System 67 4 Policy-Parameterized Functions 69 5 Declassification 71 5.1 The what Dimension 71 5.2 The who and when Dimensions 74 6 Soundness 76 7 Related Work 78 8 Conclusion and Future Work 80 References 81 Achieving Safety Incrementally with Checked C 86 1 Introduction 86 2 Overview of Checked C 88 3 Formalism: CORECHKC 90 3.1 Syntax 90 3.2 Semantics 92 3.3 Typing 94 4 Checked Code Cannot Be Blamed 97 4.1 Progress and Preservation 97 4.2 Blame 98 5 Porting Assistance 99 5.1 Constraint Logic and Solving 99 5.2 Algorithm 100 5.3 Resolving Conflicts 101 5.4 Experimental Evaluation 103 6 Related Work 104 7 Conclusions and Future Work 105 References 106 Wys: A DSL for Verified Secure Multi-party Computations 109 1 Introduction 109 2 Verifying and Deploying Wys Programs 111 2.1 Secure Computations with assec 112 2.2 Optimizing median with aspar 112 2.3 Embedding a Type System for Wys in F 113 2.4 Correctness and Security Verification 116 2.5 Deploying Wys Programs 118 3 Formalizing and Implementing Wys 119 3.1 Syntax 119 3.2 Single-Threaded Semantics 120 3.3 Distributed Semantics 121 3.4 Metatheory 122 3.5 Implementation 123 4 Applications 124 5 Related Work 127 6 Conclusions 129 References 129 Generalised Differential Privacy for Text Document Processing 133 1 Introduction 133 2 Documents, Topic Classification and Earth Moving 135 2.1 Word Embeddings 136 3 Differential Privacy and the Earth Mover's Metric 138 3.1 Application to Text Documents 141 3.2 Properties of Earth Mover's Privacy 141 4 Earth Mover's Privacy for Bags of Vectors in Rn 143 4.1 Earth Mover's Privacy in BRn 146 4.2 Utility Bounds 146 5 Text Document Privacy 147 6 Experimental Results 149 7 Related Work 152 8 Conclusions 154 References 154 Symbolic Verification of Distance Bounding Protocols 159 1 Introduction 159 2 Background 161 2.1 Distance Bounding Protocols 161 2.2 Attacks on Distance Bounding Protocols 162 2.3 Symbolic Security Analysis 163 3 A Security Model Dealing with Time and Location 163 3.1 Term Algebra 163 3.2 Timing Constraints 164 3.3 Process Algebra 165 4 Modelling Using Horn Clauses 168 4.1 Preliminaries 169 4.2 Seed Statements 170 4.3 Soundness and Completeness 172 5 Saturation 173 5.1 Saturation Procedure 173 5.2 Completeness 175 6 Algorithm 177 6.1 Description 177 6.2 Termination Issues 178 6.3 Correctness of Our Algorithm 179 7 Implementation and Case Studies 180 7.1 Integration in Akiss 180 7.2 Case Studies 180 8 Conclusion 181 References 182 On the Formalisation of -Protocols and Commitment Schemes 185 1 Introduction 185 2 Formalisation Overview 187 2.1 Outline of Formalisation 187 2.2 Instantiating the Abstract Frameworks 188 2.3 Asymptotic Security 188 3 CryptHOL and Isabelle Background 189 3.1 Isabelle Notation 189 3.2 CryptHOL 189 4 Formalising -Protocols 191 4.1 Definition of -protocols 191 5 Formalising the Schnorr -Protocol 193 5.1 The Schnorr -protocol 193 6 Formalising Commitment Schemes 196 6.1 Properties of Commitment Schemes 197 7 The Pedersen Commitment Scheme 198 7.1 Formal Proofs for the Pedersen Protocol 199 8 Using -Protocols to Construct Commitment Schemes 200 8.1 Asymptotic Case 201 9 Conclusions 202 10 Related Work 203 10.1 Comparison with EasyCrypt 204 References 205 Orchestrating Layered Attestations 207 1 Introduction 207 2 Examples of Layered Attestations 210 3 Phrases 212 4 Events 214 5 Partial Order Semantics 216 6 Small-Step Semantics 218 7 Proof Summary 221 8 Related Work 224 9 Conclusion and Ongoing Work 226 A Annotated Terms 227 B Coq Cross Reference 228 References 229 Verifying Liquidity of Bitcoin Contracts 232 1 Introduction 232 2 Overview 234 2.1 BitML in a Nutshell 234 2.2 BitML Semantics 236 2.3 Liquidity 238 2.4 Verifying Liquidity 239 3 Liquidity 240 4 A Finite-State Semantics of BitML 245 5 Verifying Liquidity 250 6 Conclusions 251 A Appendix 252 References 255 Author Index 258 This volume is a self-contained introduction to interactive proof in high- order logic (HOL), using the proof assistant Isabelle 2002. Compared with existing Isabelle documentation, it provides a direct route into higher-order logic, which most people prefer these days. It bypasses ?rst-order logic and minimizes discussion of meta-theory. It is written for potential users rather than for our colleagues in the research world. Another departure from previous documentation is that we describe Markus Wenzel’s proof script notation instead of ML tactic scripts. The l- ter make it easier to introduce new tactics on the ?y, but hardly anybody does that. Wenzel’s dedicated syntax is elegant, replacing for example eight simpli?cation tactics with a single method, namely simp, with associated - tions. The book has three parts. – The ?rst part, Elementary Techniques, shows how to model functional programs in higher-order logic. Early examples involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion. – The second part, Logic and Sets, presents a collection of lower-level tactics that you can use to apply rules selectively. It also describes I- belle/HOL’s treatment of sets, functions, and relations and explains how to de?ne sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages. Front Matter ....Pages i-xi Foundations for Parallel Information Flow Control Runtime Systems (Marco Vassena, Gary Soeller, Peter Amidon, Matthew Chan, John Renner, Deian Stefan)....Pages 1-28 A Formal Analysis of Timing Channel Security via Bucketing (Tachio Terauchi, Timos Antonopoulos)....Pages 29-50 A Dependently Typed Library for Static Information-Flow Control in Idris (Simon Gregersen, Søren Eller Thomsen, Aslan Askarov)....Pages 51-75 Achieving Safety Incrementally with Checked C (Andrew Ruef, Leonidas Lampropoulos, Ian Sweet, David Tarditi, Michael Hicks)....Pages 76-98 \(\textsc {Wys}^\star \): A DSL for Verified Secure Multi-party Computations (Aseem Rastogi, Nikhil Swamy, Michael Hicks)....Pages 99-122 Generalised Differential Privacy for Text Document Processing (Natasha Fernandes, Mark Dras, Annabelle McIver)....Pages 123-148 Symbolic Verification of Distance Bounding Protocols (Alexandre Debant, Stéphanie Delaune)....Pages 149-174 On the Formalisation of \(\varSigma \)-Protocols and Commitment Schemes (David Butler, David Aspinall, Adrià Gascón)....Pages 175-196 Orchestrating Layered Attestations (John D. Ramsdell, Paul D. Rowe, Perry Alexander, Sarah C. Helble, Peter Loscocco, J. Aaron Pendergrass et al.)....Pages 197-221 Verifying Liquidity of Bitcoin Contracts (Massimo Bartoletti, Roberto Zunino)....Pages 222-247 Back Matter ....Pages 249-249 The four-volume set LNCS 11244, 11245, 11246, and 11247 constitutes the refereed proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018, held in Limassol, Cyprus, in October/November 2018. The papers presented were carefully reviewed and selected for inclusion in the proceedings. Each volume focusses on an individual topic with topical section headings within the volume: Part I, Modeling: Towards a unified view of modeling and programming; X-by-construction, STRESS 2018. Part II, Verification: A broader view on verification: from static to runtime and back; evaluating tools for software verification; statistical model checking; RERS 2018; doctoral symposium. Part III, Distributed Systems: rigorous engineering of collective adaptive systems; verification and validation of distributed systems; and cyber-physical systems engineering. Part IV, Industrial Practice: runtime verification from the theory to the industry practice; formal methods in industrial practice - bridging the gap; reliable smart contracts: state-of-the-art, applications, challenges and future directions; and industrial day. This textbook-like tutorial is a self-contained introduction to interactive proof, specification, and verification in higher-order logic, using the proof assistant Isabelle 2002. In contrast to existing Isabelle documentation, this book provides a direct route into higher-order logic by bypassing first-order logic and minimizing discussion of meta-theory. Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for higher-order logic; this theorem prover is well suited as a specification and verification system