The performance and reliability of Cyber-Physical Systems are increasingly aided through the use of digital twins, which mirror the static and dynamic behaviour of a Cyber-Physical System (CPS) in software. Digital twins enable the development of self-adaptive CPSs which reconfigure their behaviour in response to novel environments. It is crucial that these self-adaptations are formally verified at runtime, to avoid expensive re-certification of the reconfigured CPS. In this talk, I discuss formally verified self-adaptation in a digital twinning system, by constructing a non-deterministic model which captures the uncertainties in the system behaviour after a self-adaptation. We use Signal Temporal Logic to specify the safety requirements the system must satisfy after reconfiguration and employ formal methods based on verified monitoring over Flow* flowpipes to check these properties at runtime. This gives us a framework to predictively detect and mitigate unsafe self-adaptations before they can lead to unsafe states in the physical system.

Informally, obfuscation aims to compile programmes into unintelligible ones while preserving functionality. As a first approximation, this can be seen as trying to convert a programme to a “black-box representation”, which cannot be used for anything beyond obtaining its input/output behaviour. Learning, on the other hand, aims to generate the representation of a function given oracle access to it. In this talk, we will investigate new links between the two fields.

No specialised knowledge of cryptography or computational complexity is required, and the talk is aimed at a general TCS audience. For completeness however, we provide below a more technical description of our results.

Most recent works on cryptographic obfuscation focus on the high-end regime of obfuscating general circuits while guaranteeing computational indistinguishability between functionally equivalent circuits. Motivated by the goals of simplicity and efficiency, we initiate a systematic study of “low-end” obfuscation, focusing on simpler representation models and information-theoretic notions of security. We obtain the following results. 1) Positive results via “white-box” learning. We present a general technique for obtaining perfect indistinguishability obfuscation from exact learning algorithms that are given restricted access to the representation of the input function. We demonstrate the usefulness of this approach by obtaining simple obfuscation for decision trees and multilinear read-k arithmetic formulas. 2) Negative results via PAC learning. A proper obfuscation scheme obfuscates programs from a class C by programs from the same class. Assuming the existence of one-way functions, we show that there is no proper indistinguishability obfuscation scheme for k-CNF formulas for any constant k ≥ 3; in fact, even obfuscating 3-CNF by k-CNF is impossible. This result applies even to computationally secure obfuscation, and makes an unexpected use of PAC learning in the context of negative results for obfuscation. 3) Separations. We study the relations between different information-theoretic notions of indistinguishability obfuscation, giving cryptographic evidence for separations between them.

This is joint work with Elette Boyle, Yuval Ishai, Robert Robere, and Gal Yehuda, which was presented at ITCS 2023.

We analyze the two-point motions of iterated function systems on the unit interval generated by expanding and contracting affine maps, where the expansion and contraction rates are determined by a pair $(M,N)$ of integers.

This dynamics depends on the Lyapunov exponent.

For a negative Lyapunov exponent we establish synchronization, meaning convergence of orbits with different initial points. For a vanishing Lyapunov exponent we establish intermittency, where orbits are close for a set of iterates of full density, but are intermittently apart. For a positive Lyapunov exponent we show the existence of an absolutely continuous stationary measure for the two-point dynamics and discuss its consequences.

For nonnegative Lyapunov exponent and pairs $(M,N)$ that are multiplicatively dependent integers, we provide explicit expressions for absolutely continuous stationary measures of the two-point dynamics. These stationary measures are infinite $\sigma$-finite measures in the case of zero Lyapunov exponent.

This is joint work with Charlene Kalle.

ML modules are offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, and more recent extensions (abstract signatures, module aliases) lack a complete formalization. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a significant subset of OCaml modules, including both applicative and generative functors and the proposed feature of transparent ascription. By exploring the translations both to and from Fω, we provide a complete description of the signature avoidance issue, as well as insights on the limitations and benefits of the path-based approach of OCaml type-sharing.

Machine learning (ML) software is increasingly being employed in high stakes or sensitive applications. This poses important safety, privacy, and non-discrimination challenges. As a consequence, research in ML verification rapidly gained popularity and demand for interpretable ML models is more and more pronounced. Interpretability and verification are typically seen as orthogonal concerns. Research in ML interpretability is mainly carried out in the ML community, while research in ML verification is mostly carried out in the formal methods community, without much communication and exchanges between these research areas. In this talk, we advocate for closing this gap by presenting our recent and ongoing work on interpretability-aware verification of ML software. On the one hand, we show how verification can aid interpretability by providing a new feature importance measure for support vector machines. On the other hand, we discuss how interpretability can guide verification by proposing a new saliency-guided robustness verification problem for deep neural networks. We conclude with plans and perspectives on future work.

I will give a gentle introduction to higher-dimensional automata (HDAs) and their language theory. HDAs have been introduced some 30 years ago as a model for non-interleaving concurrency which generalizes, for example, Petri nets while retaining some automata-theoretic intuition. They have been studied mostly for their operational and geometric aspects and are one of the original motivations for directed algebraic topology. In a series of papers we have recently started to work on the language theory of HDAs: we have introduced languages of HDAs as weak sets of interval pomsets with interfaces and shown that HDAs satisfy Kleene and Myhill-Nerode type theorems. The picture which emerges is that, even though things can sometimes get hairy in proofs, HDAs have a rather pleasant language theory, a fact which should be useful in the theory of non-interleaving concurrency and its applications. Joint work with Christian Johansen, Georg Struth, and Krzysztof Ziemiański

The problem of solving parity games, or equivalently model-checking for mu-calculus, is known to be both in NP and co-NP: hence, it is widely believed that they are not NP-complete (nor coNP-complete). Yet, for 30 years, we failed to find a polynomial-time algorithm solving them, despite active research on the topic.

The first quasi-polynomial algorithm was found in 2017. Soon after, McNaughton-Zielonka algorithm (an exponential-time recursive algorithm, which is arguably one of the simplest algorithm for solving parity games, and the most effective in practice) was tweaked, first by Parys and then by Lehtinen, Schewe and Wojtczak, to run in quasipolynomial time. In some sense, these algorithms forces McNaughton-Zielonka algorithm to skip enough recursive calls as to run in quasipolynomial time, but not too much so that the output remains correct. We introduce a meta-algorithm that solves parity games, parametrized by trees, which will precisely guide the recursive call made by the algorithm, and show that the output is correct when the trees satisfy some combinatorial property called universality, introduced by Fijalkow and co-authors. McNaughton-Zielonka algorithm and variations can all three be seen as an instantiation of this meta-algorithm on particular classes of universal trees.

I will also emphasize and reformulate these ideas in the slightly more general context of nested fixpoints over finite lattices, and show that these algorithms can be turned into symbolic algorithm that only uses logarithmic symbolic space. The talk is mainly based on a joint work with Marcin Jurdziński and K. S. Thejaswini. The results were proven independently by André Arnold, Damian Niwiński and Paweł Parys, for nested fixpoints.