Workshop on formal methods for secure systems*

Reykjavik University, Room V102
23 May 2023

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).

Draft programme

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)

Abstracts of the talks, in order of presentation

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.