DIKU Security Research Workshop 2019
Are you interested in the latest research in System-level Security and wish to learn more about the technical side?
DIKU will be hosting a day filled with technical talks about cutting-edge topics in security research. The workshop will feature leading researchers in Systems-level Security giving scientific talks. Topics will include hardware-assisted security, security for active storage, Security challenges for WebAssembly, DSL to generate memory-safe IoT code, and other topics. The target audience is anyone interested in technical aspects of security.
Join the workshop, become updated and get the change to interact with leading experts/researchers. Coffeebreaks and sandwiches are complementary. Participation is free but sign up is required - deadline for registration is Monday 5 August.
Find abstracts below the programme.
|09.00 - 09-15||Welcome by Mads Nielsen, Head of Department of Computer Science, University of Copenhagen|
|09.15 - 10.45||IoT
Alejandro Russo: DPella: A Programming Framework for Differential Privacy with Accuracy
Boris Düdder: Production Infrastructure and Cybersecurity: Potentials and risks in sensor applications
|10.45 - 11.00||Coffee break|
|11.00 - 12.30||WebAssembly
Conrad Watt: Constant-time WebAssembly
Ken Friis Larsen: WebAssembly in the Linux kernel
|12.30 - 13.15||Lunch|
|13.15 - 14.45||Hardware
Mads Dam: Hypervisor Verification
Michael Kirkedal Thomsen: Reversible Cryptography
|14.45 - 15.00||Coffee break|
|15.00 - 16.30||Security protocols and policies
David Basin: Security Protocols: Model Checking Standards
Thomas Hildebrandt: Security Policies, Processes and Workflows as Dynamic Condition Response (DCR) Graphs
More info about David Basin, Professor and Department Head, Department of Computer Science, ETH Zurich.
Security Protocols: Model Checking Standards
The design of security protocols is typically approached as an art, rather than a science, and often with disastrous consequences. But this need not be so! I have been working for ca. 20 years on foundations, methods, and tools, both for developing protocols that are correct by construction and for the post-hoc verification of existing designs. In this talk I will introduce my work in this area and describe my experience analyzing, improving, and contributing to different industry standards, both existing and upcoming.
More info about Alejandro Russo, Professor, Chalmers University of Technology.
DPella: A Programming Framework for Differential Privacy with Accuracy
Differential privacy offers a formal framework for reasoning about privacy and accuracy of computations on private data like those collected by IoT devices. It also offers a rich set of building blocks for constructing data analyses. When carefully calibrated, these analyses simultaneously guarantee privacy of the individuals contributing their data and accuracy of their results for inferring useful properties about the population. One important building block for differential privacy are composition theorems, which allow multiple differentially private data analyses to be composed together with a graceful degradation of the privacy and accuracy parameters. The compositional nature of differential privacy has motivated the design and implementation of several programming languages aimed at helping a data analyst in programming differentially private data analyses. However, most of the programming languages for differential privacy proposed so far provide support for reasoning about privacy but not for reasoning about accuracy of data analyses. To overcome this limitation, in this work we present DPella, a programming framework providing data analysts with support for reasoning about privacy, accuracy and their trade-offs. DPella is implemented as a domain specific language in the functional programming language Haskell. The distinguished feature of DPella is a novel component which statically tracks the accuracy of different data analyses. In order to make tighter accuracy estimations, this component leverages information-flow control techniques, in the form of taint analysis, for automatically inferring statistical independence of the different noise quantities added for guaranteeing privacy. We show the flexibility of our approach by implementing classical counting queries (e.g., CDFs) found in the literature and how DPella exposes the trade-offs between privacy and accuracy. Furthermore, we use DPella to analyze hierarchical counting queries (like those done by Census Bureaus), where accuracy have different constrains per level and data analysts should figure out the best manner to trade-off privacy to meet the accuracy requirements.
This talk is based on a joint work with Elisabet Lobo-Vesga, Marco Gaboardi, and Gilles Barthe.
More info about Ken Friis Larsen, Associate Professor, Department of Computer Science, University of Copenhagen.
WebAssembly in the Linux Kernel
More info about Thomas Hildebrandt, Professor, Department of Computer Science, University of Copenhagen.
Security Policies, Processes and Workflows as Dynamic Condition Response (DCR) Graphs
Most formal approaches to verification and enforcement of security policies goes through an initial step of formalisation from natural text to formal model, e.g. as a variant of temporal logic or automata. As in any translation, the meaning may change during the formalisation process, and it may be required to analyse the interplay between the policy and other processes, such as workflows, and subsequently revise the formalisation. The talk presents the Dynamic Condition Response (DCR) Graphs notation and tools from DCRSolutions.net for iterative formalisation of security policies and workflows, which have been developed through the last 10 years in joint research and innovation projects.
More info about Mads Dam, Professor, Kungliga Tekniska Högskolan.
More info about Boris Düdder, Assistant Professor, Department of Computer Science, University of Copenhagen
Production Infrastructure and Cybersecurity: Potentials and risks in sensor applications
Industrial production systems make the transition from digitally supported to (smart) digitally connected in the Industry 4.0 paradigm. The connection allows for automation and data exchange between production units and control following the four design principles of (1) interconnection, (2) information transparency, (3) technical assistance, and (4) decentralized decisions. The smart manufacturing builds on IT-based components, e.g., cyber-physical systems or IoT. Such a smart manufacturing system is embedded in supporting infrastructure as a smart factory. The talk will focus on the security challenges of the supporting infrastructure, especially on facilities.
More info about Michael Kirkedal Thomsen, Assistant Professor, Department of Computer Science, University of Copenhagen.
More info about Conrad Watt, PhD student, Cambridge University.
We present Constant-Time WebAssembly (CT-Wasm), a type-driven, strict extension to WebAssembly which facilitates the verifiably secure implementation of cryptographic algorithms. CT-Wasm’s type system ensures that code written in CT-Wasm is both information flow secure and resistant to timing side channel attacks; like base Wasm, these guarantees are verifiable in linear time. Building on an existing Wasm mechanization, we mechanize the full CT-Wasm specification, prove soundness of the extended type system, implement a verified type checker, and give several proofs of the language’s security properties.
Slides from presentations (still under update)
Participation is free (coffee breaks and sandwich included) - registration is required.
Registration deadline 5 August 2019.
Registration is closed, but please send an email to email@example.com if you wish to join the workshop (no later than Friday 9 August 2019 at 1:00 PM).