ABSTRACT. The standard trick for proving hypersafety properties is to build a product program and reason about the multiple behaviours of multiple copies in the context of a single program. But there are many choices for the product program, and any choice is only as good as the runs you choose to include in it. Verification (especially the automated variety) may succeed or fail depending on this choice. This talk tells that story as a sequence of escalating challenges—from sequential to concurrent to recursive programs—on how an effective state space of product programs can be defined and algorithmically used for effective hypersafety verification.

ABSTRACT. Many important functional and security properties—including non-interference, determinism, and generalized non-interference (GNI)—are hyperproperties, i.e., properties relating multiple executions of a program. Existing separation logics allow one to reason about specific classes of hyperproperties, e.g., ∀∀-hyperproperties such as non-interference and ∃∃-properties such as non-determinism. However, they do not support quantifier alternation, which is for instance needed to express GNI. The only existing logic that can reason about such properties is Hyper Hoare Logic, but it does not support heap-manipulating programs and, thus, is not applicable to common imperative programs. This paper introduces Hyper Separation Logic (HSL), the first program logic that supports modular reasoning about hyperproperties with arbitrary quantifier alternation over programs that manipulate the heap. HSL generalizes Hyper Hoare Logic with a novel hyper separating conjunction that lifts the standard separating conjunction to sets of states, enabling a generalized frame rule for hyperproperties. We prove HSL sound in Isabelle/HOL and demonstrate its expressiveness for hyperproperties that lie beyond the reach of existing separation logics.

ABSTRACT. Heisenbugs—a pun on the name of Werner Heisenberg—are bugs that alter their behavior or disappear when attempts are made to find and analyze them. Such bugs occur in a range of contexts including elusive concurrency bugs as well as unintended system alterations during debugging, and can be caused by various sources of nondeterminism on different system levels. We frame Heisenbugs and their causes as two- safety hyperproperties, thus providing formal foundations for rigorously reasoning about causes of Heisenbugs, and making this challenging class of bugs amenable to an arsenal of existing tools and techniques.

ABSTRACT. Hyperproperties, properties that relate sets of execution traces rather than a single one, are needed to express information-flow security policies like noninterference, consistency criteria like linearizability, robustness in cyber-physical systems, and diagnosability, none of which can be captured by standard trace logics. Since HyperLTL and HyperCTL* equipped LTL and CTL* with explicit, simultaneous quantification over traces, the area has grown into a small zoo of logics, semantics, and verification techniques. In this talk I will take a chronological tour of that landscape, starting from the original synchronous hyperlogics and their automata-based and reduction-based model-checking algorithms, then follow two threads: time, including discrete and pointwise timed semantics (HyperMTL) and finite-trace semantics with past operators; and asynchrony, including traces that stutter or advance along independent contexts or trajectories (HyperLTL_S, HyperLTL_C, A-HLTL), undecidability in general but with decidable fragments, and recent attempts to unify these extensions into a single framework. I will also look at non-standard semantics, from multimodels to what these logics express when evaluated for a single trace model, where some asynchronous fragments turn out to characterize non-regular properties. From the algorithmic side, we move from automata constructions and self-composition reductions to bounded model checking via QBF and SAT, with an eye on the elusive loop conditions; and from static verification to gray-box runtime verification. I will close the talk by looking past finite-state systems, e.g. population protocols, with some thoughts on open problems.

ABSTRACT. There are two main contenders for a grand unified theory of computer security: hyperproperties in the formal methods community, and the Real–Ideal paradigm (e.g., Universal Composability) in the cryptography community. I describe how they meet in the Viaduct compiler, which transforms high-level sequential programs to distributed, concurrent cryptographic realizations. Even though the source and target systems have very different properties, the Viaduct compiler transformation preserves the security promises of the original source program, because it robustly preserves all hyperproperties. The proof of Robust Hyperproperty Preservation is achieved by building a series of Real–Ideal simulations that transitively connect the source to the final target. This work points to a deep connection between these two contending perspectives, and suggests that Real–Ideal simulations are a powerful tool for security specification and provable enforcement.

ABSTRACT. So far, the verification of reactive systems against temporal hyperproperties has been mostly studied from the perspective of model-checking for finite-state systems (e.g., hardware). However, there is still a lack of interactive and deductive techniques to prove temporal hyperproperties of infinite-state systems (e.g., software). This presentation aims to give an introduction to recent works based on \emph{cyclic deductive proof system} for verifying temporal hyperproperties with the help of an interactive proof assistant. In particular, we will present HyCo, a framework for the interactive verification of $\forall^*\exists^*$-safety properties embedded in the Rocq proof assistant.

ABSTRACT. Information flow security ensures that the secret data manipulated by a program does not influence its observable output. In concurrent programs, operations on secret data may influence the execution time of a thread and, thereby, the interleaving between threads; such internal timing channels may affect the observable outcome of a program even if an attacker does not observe execution times. Existing verification techniques attempt to prove that secret data does not influence the relative timing of threads. However, these techniques are often restrictive (forbidding branching on secrets) and make strong assumptions about the execution platform (ignoring caching and other common features that affect execution time). In this talk, we will give an overview of CommCSL, a verification technique for secure information flow in concurrent programs that lifts these restrictions and does not make any assumptions about timing behavior. We will explain its key idea, which is to prove that all mutating operations performed on shared data commute, such that different thread interleavings do not influence its final value. Subsequently, we will describe some limitations of CommCSL in its current form and outline ideas on how they can be addressed.

ABSTRACT. Some security properties of cryptographic protocols cannot be expressed as trace properties. This is typically the case for privacy-related properties such as anonymity, or unlinkability. They are generally expressed in terms of an adversary's inability to distinguish two distinct scenarios, while actively interacting with the protocol. In symbolic models (following the initial work of Dolev and Yao) such indistinguishability properties can be naturally modeled using process equivalences in extensions of the pi calculus such as the applied pi calculus. We will illustrate how process equivalences can be used to model privacy properties. We provide complexity results for the underlying verification problem (when the number of sessions is bounded) and we will describe the decision procedure underlying the DeepSec verification tool.

ABSTRACT. We introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic that can express a wide range of probabilistic hyperproperties, including probabilistic non-interference and perfect indistinguishability. DTL is based on the notion of measure disintegration from probability theory, which allows for conditioning probabilities on a finite or infinite sequence of events occurring during a program execution. We relate the new logic to existing concepts, such as distributional transformers for Markov decision processes, probabilistic au- tomata on infinite words, and existing probabilistic logics. While model checking Markov chains against full DTL is undecidable, we identify two decidable fragments that capture many hyperproperties of interest. The qualitative fragment is handled by an automata-theoretic procedure that extends the standard algorithm for HyperCTL∗ with reasoning about the bottom strongly connected components. The linear fragment admits a polynomial-time model-checking procedure based on linear algebraic techniques.

ABSTRACT. This work investigates the affine segment decomposition algorithm used in the Rocq-NN-Roll prover for neural network hyperproperties through the lens of monoidal categories. This perspective is designated for future integration into Rocq-NN-Roll to facilitate reasoning.