Here you can find a list of publications attributed to the COVERT project
Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities
37th IEEE Computer Security Foundations Symposium (CSF 2024)
Authors: Brijesh Dongol, Matt Griffin, Andrei Popescu, Jamie Wright
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.
Full paper
Rely-Guarantee Is Coinductive: A Proof-Centered Investigation of Inductively Approximated Coinduction
To appear in the 35th European Symposium on Programming (ESOP 2026)
Authors: John Derrick, Chelsea Edmonds, Andrei Popescu, Jamie Wright
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.
Paper will be uploaded soon.
Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities -- Extended Version
To appear in the Journal of Automated Reasoning
Authors: John Derrick, Chelsea Edmonds, Brijesh Dongol, Matt Griffin, Andrei Popescu, Jamie Wright
This is a considerable extension of the conference paper. It includes proof sketches, Isabelle formalization details, and extensive examples.
Paper draft