2026-04-29

Within the theory of model checking, one technique to combat the state space explosion is symmetry reduction. The general idea of symmetry reduction is quite straightforward: when generating the state space of a model, we ignore symmetric states. A key ingredient here is that we need to be able to identify which states are indeed symmetric.

We consider symmetry detection for Parametrised Boolean Equation Systems (PBESs). PBESs can be used to encode model checking problems, such as verifying first-order modal mu-calculus formulae on LPSs. For PBESs there exists a denotational semantics, but also an equivalent game semantics that is described in terms of parity games. The underlying state space of a PBES can be depicted as a parity game, on which symmetry reduction can be carried out.

We use the concept of control flow as a basis for identifying symmetries in a PBES. When statically analysing a PBES, one can deduce the values that certain parameters attain throughout the state space. Such parameters are called control flow parameters and can be thought of as "program counters" for the system at hand. We use this information as a basis for symmetry detection.

In this talk, we go over the relevant definitions for control flow for PBESs and show how we can base the search for symmetries on these concepts.

Memory safety bugs are pervasive in nearly all compiled programming languages. To mitigate this, modern languages such as Rust have been designed with a sophisticated ownership system that enforces memory safety. This system controls how variables are accessed and mutated, distinguishing between data that can be safely read and data that can be safely modified.

However, these guarantees are compromised when interacting with external libraries. While Rust’s Foreign Function Interface (FFI) can encode ownership constraints in its type signatures, there is no mechanism to ensure that external libraries—such as those written in C—respect these constraints. This mismatch can lead to discrepancies between Rust’s expectations and the actual behavior of foreign code, potentially resulting in undefined behavior and memory safety violations.

We propose two directions for detecting memory safety violations across language boundaries. Both approaches build on the insight that Rust’s type system makes implicit assumptions about external C code at the time of an FFI call. By turning these implicit type assumptions into explicit dynamic checks, we can detect when external code fails to satisfy Rust’s expectations. Early experiments show encouraging results in terms of both efficiency and effectiveness on existing benchmarks.

In the cyber threats landscape, Advanced Persistent Threats carry out attack campaigns—e.g. operations Dream Job, Wocao, and WannaCry—against which cybersecurity practitioners must defend. To prioritise which of these to defend against, experts must be equipped with the ability to evaluate the most threatening ones: they would strongly benefit from (a) an estimation of the likelihood values for each attack recorded in the wild, and (b) transparently operationalising these values to compare campaigns quantitatively.

In this talk, we present such a framework, that: (1) quantifies the likelihood of attack campaigns via data-driven procedures on the MITRE knowledge-base, (2) introduces a methodology for automatic modelling of MITRE intelligence data, that captures any attack campaign via template attack tree models, and (3) proposes an open-source tool to perform these comparisons based on the cATM logic. Finally, we quantify the likelihood of all MITRE Enterprise campaigns, and compare the likelihood of the Wocao and Dream Job MITRE campaigns—generated with our proposed approach—against manually-built attack tree models. We demonstrate how our methodology is substantially lighter in modelling effort, and capable of capturing all the quantitative relevant data.