| CSF 2019 Workshops | Monday, June 24 |
| 08:00 - 18:00 | Registration Desk |
| CSF 2019: Day 1 | Tuesday, June 25 |
| 08:30 - 09:00 | Breakfast |
| 09:00 - 9:15 | Opening Remarks |
| Invited Talk I (Session Chair: Limin Jia) | |
| 09:15 - 10:30 | Legal Theorems of Privacy (Slides) Kobbi Nissim, Georgetown University |
| 10:30 - 11:00 | Break |
| Session 1: Information Flow (Session Chair: Alejandro Russo) | |
| 11:00 - 11:30 | Optimising Faceted
Secure Multi-Execution (Slides) M. Algehed, A. Russo, C. Flanagan |
| 11:30 - 12:00 | Canonical
Representations of k-Safety-Hyperproperties (Slides) B. Finkbeiner, L. Haas, H. Torfah |
| 12:00 - 12:30 | Timing Leaks and Coarse-Grained Clocks (Slides) P. Vasilikos, F. Nielson, H. Nielson, B. Köpf |
| 12:30 - 14:30 | Lunch |
| Session 2: Security Protocols I (Session Chair: Joshua Guttman) | |
| 14:30 - 15:00 | Decidability of a
Sound Set of Inference Rules for Computational
Indistinguishability (Slides) A. Koutsos |
| 15:00 - 15:30 | How To Wrap It Up - A Formally Verified Proposal for
the use of Authenticated Wrapping in PKCS#11 (Slides) A. Dax, S. Tangermann, R. Künnemann, M. Backes |
| 15:30 - 16:00 | Prime, Order Please! Revisiting Small Subgroup and
Invalid Curve Attacks on Protocols using Diffie-Hellman
(Distinguished paper) (Slides) C. Cremers, D. Jackson |
| 16:00 - 16:30 | Break/Poster |
| Short Talks (Session Chair: Cas Cremers) | |
| 16:30 - 18:00 | 5-Minute Poster/Research Talks |
| 18:00 - 20:00 | Reception |
| CSF 2019: Day 2 | Wednesday, June 26 |
| 08:30 - 09:00 | Breakfast |
| Session 3: Blockchain (Session Chair: Mayank Varia) | |
| 09:00 - 09:30 | Re-thinking Untraceability in the CryptoNote-Style
Blockchain (Video) J. Yu, M. Au, P. Esteves-Verissimo |
| 09:30 - 10:00 | Time-dependent Decision-making and Decentralization in
Proof-of-Work Cryptocurrencies (Slides) (PPS) Y. Zolotavkin, J. Garcia, J. Liu |
| 10:00 - 10:30 | Analysis of Deterministic Longest-Chain Protocols E. Shi |
| 10:30 - 11:00 | Break |
| Session 4: Computer-Aided Crypto (Session Chair: Véronique Cortier) | |
| 11:00 - 11:30 | Symbolic Methods in Computational Cryptography Proofs G. Barthe, B. Grégoire, C. Jacomme, S. Kremer, P. Strub |
| 11:30 - 12:00 | Formalizing Constructive Cryptography using CryptHOL A. Lochbihler, S. Sefidgar, D. Basin, U. Maurer |
| 12:00 - 12:30 | EasyUC: Using EasyCrypt to Mechanize Proofs of
Universally Composable Security (Slides) R. Canetti, A. Stoughton, M. Varia |
| 12:30 - 14:30 | Lunch |
| Invited Talk II (Session Chair: Andrei Sabelfeld) | |
| 14:30 - 15:30 | Adversarial Machine Learning (AML):
Research Trends and Directions (Slides) Somesh Jha, University of Wisconsin-Madison |
| 15:30 - 16:00 | Break/Poster |
| Session 5: Formal Methods and Verification — Attacker Model (Session Chair: Cas Cremers) | |
| 16:00 - 16:30 | On the Meaning and Purpose of Attack Trees H. Mantel, C. Probst |
| 16:30 - 17:00 | Efficient Attack-Defense Tree Analysis using Pareto Attribute Domains B. Fila, W. Wideł |
| 17:00 - 17:30 | Games for Security under Adaptive Adversaries T. Antonopoulos, T. Terauchi |
| 17:30 - 18:00 | Business Meeting (Chair: Andrei Sabelfeld) |
| CSF 2019: Day 3 | Thursday, June 27 |
| 08:30 - 09:00 | Breakfast |
| Session 6: Formal Methods and Verification — Secure Compilation (Session Chair: Catuscia Palamidessi) | |
| 09:00 - 09:30 | Information-Flow Preservation in Compiler
Optimisations (Slides) A. Dang, F. Besson, T. Jensen |
| 09:30 - 10:00 | Temporal Safety for Stack Allocated Memory on
Capability Machines (Slides) S. Tsampas, D. Devriese, F. Piessens |
| 10:00 - 10:30 | Journey Beyond Full Abstraction: Exploring Robust
Property Preservation for Secure Compilation
(Distinguished paper) (Slides) (PPT) C. Abate, R. Blanco, D. Garg, C. Hritcu, M. Patrignani, J. Thibault |
| 10:30 - 11:00 | Break |
| Session 7: Hardware-based security (Session Chair: Musard Balliu) | |
| 11:00 - 11:30 | Using Information Flow to Design an ISA that Controls
Timing Channels (Slides) D. Zagieboylo, G. Suh, A. Myers |
| 11:30 - 12:00 | A Formal Approach to Secure Speculation K. Cheang, C. Rasmussen, S. Seshia, P. Subramanyan |
| 12:00 - 12:30 | Information Flow Control for Distributed Trusted
Execution Environments (Slides) A. Gollamudi, S. Chong, O. Arden |
| 12:30 - 14:30 | Lunch |
| Invited Talk III (Session Chair: Stéphanie Delaune) | |
| 14:30 - 15:30 | WIM: An Expressive Formal Model of the
Web Infrastructure (Slides) Ralf Küsters, University of Stuttgart |
| 15:30 - 16:00 | Break/Poster |
| Session 8: Language-based Security (Session Chair: David Naumann) | |
| 16:00 - 16:30 | Securing Cross-App Interactions in IoT Platforms (Slides) M. Balliu, M. Merro, M. Pasqua |
| 16:30 - 17:00 | Static Enforcement of Security in Runtime Systems (Slides) M. Pedersen, A. Askarov |
| 17:00 - 17:30 | Beyond Labels: Permissiveness for Dynamic Information
Flow Enforcement (Slides) E. Kozyri, F. Schneider, A. Bedford, J. Desharnais, N. Tawbi |
| 18:00 - 21:30 | Boat Cruise |
| CSF 2019: Day 4 | Friday, June 28 |
| 08:30 - 09:00 | Breakfast |
| Session 9: Security Protocols II (Session Chair: Bruno Blanchet) | |
| 09:00 - 09:30 | BeleniosVS: Secrecy and Verifiability Against a Corrupted Voting Device V. Cortier, A. Filipiak, J. Lallemand |
| 09:30 - 10:30 | Resource-Bounded Intruders in Denial of Service
Attacks (Slides) A. Urquiza, M. AlTurki, M. Kanovich, T. Kirigin, V. Nigam, A. Scedrov, C. Talcott |
| 10:00 - 10:30 | Automated Verification of Accountability in Security
Protocols (Distinguished paper) (Slides) R. Künnemann, I. Esiyok, M. Backes |
| 10:30 - 11:00 | Break |
| Session 10: Quantitative Information Flow (Session Chair: Stephen Chong) | |
| 11:00 - 11:30 | Quantifying information Flow in Interactive Systems D. Mestel |
| 11:30 - 12:00 | Deterministic Channel Design for Minimum Leakage
(Slides) A. Américo, M. Khouzani, P. Malacaria |
| 12:00 - 12:30 | Comparing Systems: Max-Case Refinement Orders and
Application to Differential Privacy (Slides) K. Chatzikokolakis, N. Fernandes, C. Palamidessi |
| 12:30 | Concluding Remarks |
Legal Theorems of Privacy
Kobbi Nissim, Georgetown University, USA
There are significant gaps between legal and technical thinking around data privacy. Technical standards such as differential privacy and k-anonymity are described using mathematical language whereas legal standards often resort to concepts such as de-identification and anonymization which they do not define mathematically. As a result, arguments about the adequacy of technical privacy measures for satisfying legal privacy often lack rigor, and their conclusions are uncertain. The uncertainty is exacerbated by a litany of successful privacy attacks on privacy measures thought to meet legal expectations but then shown to fall short of doing so.
We ask whether it is possible to introduce mathematical rigor into such analyses, so as to make formal claims and prove “legal theorems” that technical privacy measures meet legal expectations. For that, we explore some of the gaps between these two very different approaches, and present initial strategies towards bridging these gaps considering examples from US and EU law.
Adversarial Machine Learning (AML): Research Trends and Directions
Somesh Jha, University of Wisconsin-Madison, USA
In this talk, we will discuss what happens to Machine Learning (ML) algorithms in the presence of an adversary. This field is called adversarial machine learning (AML), and in recent years the interest in this topic has exploded. We will systematically cover state-of-the art in AML and discuss various attacks (e.g. data poisoning, test-time attacks, and model stealing) and corresponding defenses. We will then explore "technical gaps" in the current state of the art in AML, which will lead to a discussion of open problems. We will also discuss lack of formal definitions and semantics in AML.
WIM: An Expressive Formal Model of the Web Infrastructure
Ralf Küsters, University of Stuttgart, Germany
The World Wide Web is a complex infrastructure with a rich set of security requirements and entities, such as DNS servers, web servers, and web browsers, interacting using diverse technologies. As illustrated by numerous attacks, rigorous analysis of the web infrastructure and web applications is indispensable.
In the last five years, we have therefore developed what we call the Web Infrastructure Model (WIM) in order to be able to formally analyze the security of web standards and applications. The WIM is a Dolev-Yao-style model which aims to precisely capture the web infrastructure, with its various standards, on an appropriate level of abstraction. It is the most comprehensive model of the web to date. We have used the WIM in the past few years to analyze various widespread web Single Sign-On (SSO) standards, including OAuth 2.0 and OpenID Connect, finding various new and partly severe attacks. We also proposed fixes and proved, for the first time, that the fixed standards are secure under appropriate assumptions. We have been in close contact with standardization organizations and actively support improving and fixing the standards.
In this talk, we present the WIM and discuss some of the case studies we carried out.
The talk is based on joint work with Daniel Fett and Guido Schmitz,
published at S&P 2014, ESORICS 2015, CCS 2015, CCS 2016, and CSF
2017.
| Title | Authors |
|---|---|
| Deciding Trace Equivalence for Protocols with Asymmetric Operations | Véronique Cortier, Stéphanie Delaune and Vaishnavi Sundararajan |
| Flowstate: A Language for Fault Tolerant Decentralized Computation | Priyanka Mondal and Owen Arden |
| A Symbolic Framework for Analyzing Distance Bounding Protocols | Alexandre Debant, Stephanie Delaune and Cyrille Wiedling |
| Improving Rider Safety Using QR Code & Fingerprint Biometrics | Raghu Avula and Cliff Zou |
| A Structured Semantic Domain for Smart Contracts | Sören Bleikertz, Andreas Lochbihler, Ognjen Mari, Simon Meier, Matthias Schmalz and Ratko G. Veprek |
| Principled Detection of Speculative Information Flows | Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke and Andrés Sánchez |
| New Axiomatization of Information Leakage Based on Core-Concavity | Arthur Américo, Mhr. Khouzani and Pasquale Malacaria |
| Trollthrottle — Raising the Cost of Astroturfing | Ilkan Esiyok, Lucjan Hanzlik, Robert Kuennemann, Lena M. Budde and Michael Backes |
| Application of the Expectation-Maximization Framework to Privacy | Ehab Elsalamouny and Catuscia Palamidessi |