Note: Attendance is free, but please register using the Google form that you can find here by Wednesday, 17 May at 12:00 GMT, so that we can make appropriate plans for the coffee breaks. Attendees will have to pay for their lunches.
*The workshop is partly supported by the project "Open Problems in the Equational Logic of Processes" of the Icelandic Research Fund (no. 196050-051).
09:20-09:30 Welcome (Hans, Jacky and Luca)
09:30-10:00 Stephen D. Wolthusen (Royal Holloway and NTNU), TBA
10:00-10:15 Questions
10:15-10:30 Coffee break
10:30-11:00 Rosario Giustolisi (ITU Copenhagen), Modelling Human Threats in Socio-Technical Systems
[slides]
11:00-11:15 Questions
11:15-11:45 Roberto Guanciale (KTH), Validating models in the post-Spectre era
[slides]
11:45-12:00 Questions
12:00-13:00 Lunch
13:00-13:30 James Wright (NTNU), How Industrial Control Security Blows Up the State Space
[slides]
13:30-13:45 Questions
13:45-14:15 Musard Balliu (KTH), Everything old is new again: Principled exploration of code-reuse attacks in modern web applications
[slides]
14:15-14:30 Questions
14:30-15:00 Coffee break
15:00-15:30 Sebastian Mödersheim (DTU), Logic for Privacy in Security Protocols
[slides]
15:30-15:45 Questions
15:45-16:00 Break
16:00-16:45 Panel discussion: What should we start doing now to have secure computers within 5-10 years? (TBC)
09:30-10:00 Stephen D. Wolthusen (Royal Holloway and NTNU)
Title: TBA
Abstract: TBA
10:30-11:00 Rosario Giustolisi (ITU Copenhagen)
Title: Modelling Human Threats in Socio-Technical Systems
Abstract: Socio-Technical Sytems (STSs) combine the operations of technical systems with the choices and intervention of
humans, namely the users of the technical systems. They are increasingly common, and innumerable examples can be drawn
at present from the areas of home automation, automotive and IoT in general. While the possible security issues about the technical components are well known yet continuously
investigated, the focus of this work is on the various levels of threat that human actors may pose, potentially leading to
breaking the overall system’s security successfully. The approach is to formally model human threats systematically and to
formally verify whether they can break the security properties of a few running examples: two currently deployed Deposit-
Return Systems (DRSs) and a variant that we designed to strengthen them. DRSs may contribute to waste reduction by offering people some cash back upon return of empty bottles or cans into reverse vending machines. The two real-world DRSs are found to support security properties differently, and some relevant properties fail, yet our variant is verified to be a fix.
11:15-11:45 Roberto Guanciale (KTH)
Title: Validating models in the post-Spectre era
Abstract: Attacks like Spectre have demonstrated that the foundations used for verifying side-channel resilience are fundamentally wrong.
We present a methodology to validate observational models for modern computer architectures. This approach combines symbolic execution and
relational analysis to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel.
This approach has been evaluated by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture.
The results show that this approach can generate tests that invalidate the models due to hidden microarchitectural behavior, including new types of speculative leakage.
13:00-13:30 James Wright (NTNU)
Title: How Industrial Control Security Blows Up the State Space
Abstract: An exploration of how ICS protocol QoS properties and adversary abilities trivially explode the state space that needs to be searched by formal methods to find violations in security properties.
13:45-14:15 Musard Balliu (KTH)
Title: Everything old is new again: Principled exploration of code-reuse attacks in modern web applications
Abstract: The last decade has seen a proliferation of code-reuse attacks in the context of web applications. These attacks target vulnerabilities in which attacker-controlled data exploits legitimate code fragments within a web application’s codebase to execute a code chain that performs malicious computations, for example Remote Code Execution (RCE), on the attacker’s behalf. In this talk, we will discuss how large-scale static code analysis helps discovering vulnerabilities in high-profile applications. Specifically, we have designed and implemented multi-label static taint analysis to identify RCE vulnerabilities pertaining to insecure deserialisation and prototype pollution in .NET and Node.js applications, including Azure DevOps Server, NPM CLI, and Parse Server.
15:00-15:30 Sebastian Mödersheim (DTU)
Title: Logic for Privacy in Security Protocols
Abstract: (alpha,beta)-privacy is an approach to the verification of privacy
properties of security protocols. While the de-facto standard is to
express privacy as an observational equivalence of two processes,
(alpha,beta)-privacy goes a radically different way to formulate
privacy a reachability problem, where every state is characterized by
two formulae alpha and beta. Here, alpha formalizes all the
information that has been intentionally revealed so far, e.g. the
result of an election, and that the intruder is allowed to know. In
contrast, beta formalizes what the intruder actually has found out by
observing messages, performing tests on these messages, and
interacting with other agents. In fact, we assume that the intruder
knows the protocol and thus can perform a symbolic execution that can
be contrasted with the actual observations. A given state violates
alpha-beta privacy, if beta implies any privacy-relevant facts that do
not follow from alpha already. We give a brief overview of the methods
for a decision procedure to check if such a privacy-violating state is
reachable within a given number of steps.