Publications

Certified Infinite Descent Criteria in Isabelle/HOL

17th International Conference on Interactive Theorem Proving

Infinite Descent is the global trace condition that underpins the soundness of cyclic reasoning and, in program analysis, the size change termination principle. Many (semi-)decision procedures for Infinite Descent are known, based on criteria ranging from automata-based constructions and relation-based characterizations, to effective (but incomplete) heuristics. Although these criteria are well studied on paper and implemented in tools, a unified, machine-checked account that relates them to the (abstract) Infinite Descent property has been missing. We present an Isabelle/HOL mechanization of this landscape. We develop a reusable, locale-based framework of sloped graphs that defines Infinite Descent at an abstract level, independently of any concrete graph encoding. Within this framework we formalize standard complete criteria and prove their equivalence to the locale-level InfiniteDescent predicate. We also formalize tool-facing sufficient criteria, prove their soundness, and certify incompleteness where appropriate via verified counterexamples. Along the way we contribute reusable Isabelle lemmas for omega-regular reasoning over streams and for Buchi-automata constructions needed by the inclusion proofs.

Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle/HOL

Journal Of Automated Reasoning

Meltdown and Spectre are vulnerabilities known as transient execution vulnerabilities, where an attacker exploits speculative execution (a semantic optimization present in most modern processors) to break confidentiality. We introduce relative security, ageneral notion of information-flow security that models this type of vulnerability by contrasting the leaks that are possible in a “vanilla” semantics with those possible in a different semantics, often obtained from the vanilla semantics via some optimizations. We describe incremental proof methods, in the style of Goguen and Meseguer’s unwinding, both for proving and for disproving relative security, and deploy these to formally establish the relative (in)security of some standard Spectre examples. Both the abstract results and the case studies have been mechanized in the Isabelle/HOL theorem prover. This paper is an extension of an earlier conference paper that provides significantly more detail on the Isabelle formalization and the unwinding proof process.

Rely-Guarantee Is Coinductive: A Proof-Centered Investigation of Inductively Approximated Coinduction

35th European Symposium on Programming (ESOP 2026)

We make the case that the foundation for Rely-Guarantee reasoning can be fruitfully delivered by a coinductive semantics. Using insight from an Isabelle formalization, via a proof analysis we show that the coinductive semantics tends to simplify the proof development; in particular it enables more direct proofs for the soundness of the Rely-Guarantee rules. The comparison between inductive and coinductive proofs also suggests inductive counterparts of coinductive “up-to” enhancements. On the way, we fill a gap in the literature, by showing that three previously defined inductive semantics for Rely-Guarantee are equivalent. Underlying our transformation of an inductive into a coinductive semantics is the notion of inductively approximating a coinductive predicate—which, deployed in the opposite direction (from coinduction to induction), is a standard technical tool for approximating process algebra bisimilarities. On the spectrum between the abstract fixpoint theorems and concrete instances, we formalize effective format-based criteria that enable sound approximation.

Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities

37th IEEE Computer Security Foundations Symposium (CSF 2024)

Meltdown and Spectre are vulnerabilities known as transient execution vulnerabilities, where an attacker exploits speculative execution (a semantic optimization present in most modern processors) to break confidentiality. We introduce relative security, a general notion of information-flow security that models this type of vulnerability by contrasting the leaks that are possible in a “vanilla” semantics with those possible in a different semantics, often obtained from the vanilla semantics via some optimizations. We describe incremental proof methods, in the style of Goguen and Meseguer's unwinding, both for proving and for disproving relative security, and deploy these to formally establish the relative (in)security of some standard Spectre examples. Both the abstract results and the case studies have been mechanized in the Isabelle/HOL theorem prover.

A formalized programming language with speculative execution

In Isabelle Workshop 2024, associated with ITP 2024

Archive Of Formal Proofs (AFP 2024)

We present the formalization of a programming language whose operational semantics allows for the speculative execution of its statements. This type of semantics is relevant for discussing transient execution security vulnerabilities such as Spectre and Meltdown. An instantiation of Relative Security to this language is provided along with proofs of security and insecurity of selected programs from the Spectre benchmark.

Relative Security

Archive Of Formal Proofs (AFP 2024)

This entry formalizes the notion of relative security presented in the CSF 2024 paper “Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities” by Brijesh Dongol, Matt Griffin, Andrei Popescu and Jamie Wright. It defines two versions of relative security: a finitary one (restricted to finite traces), and an infinitary one (working with both finite and infinite traces). It introduces unwinding methods for verifying relative security in both the finitary and infinitary versions, and proves their soundness. The proof of soudness in the infinitary case is a substantial application of Isabelle’s corecursion and coinduction infrastructure.

Secret-Directed Unwinding

Archive Of Formal Proofs (AFP 2024)

This entry formalizes the secret-directed unwinding disproof method for relative security. The method was presented in the CSF 2024 paper "Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities". Secret-directed unwinding can be used to prove the existence of transient execution vulnerabilities. The main characteristics of secret-directed unwinding are that (1) it is used to disprove rather than prove security and (2) it proceeds in a manner that is "directed" by given sequences of secrets. The second characteristic is shared with the unwinding method for bounded- deducibility security.

More Operations on Lazy Lists

Archive Of Formal Proofs (AFP 2024)

We formalize some operations and reasoning infrastructure on lazy (coinductive) lists. The operations include: building a lazy list from a function on naturals and an extended natural indicating the intended domain, take-until and drop-until (which are variations of take-while and drop-while), splitting a lazy list into a lazy list of lists with cut points being those elements that satisfy a predicate, and filtermap. The reasoning infrastructure includes: a variation of the corecursion combinator, multi-step (list-based) coinduction for lazy-list equality, and a criterion for the filtermapped equality of two lazy lists.