The presentation slides and video recording for the TLA+ Community Event 2020 are now available.
The TLA+ specification can be found here (or the raw .tla and .cfg files).
While side-channels have been formalised before, including confidentiality properties, most such models do not cover speculative instruction execution and the information leakage is derived only from data explicitly accessed by the victim program. The specification above proposes a formal model of cache speculation side-channel with the model checker providing a counterexample to the confidentiality property: a form of Spectre-v1.
In this model, the abstract machine consists of a privilege mode (low/high), registers, memory and cached state(true/false) together with a set of actions modifying such state.
The confidentiality property is equivalent to an attacker execution trace being deterministic of only its initial state, the output of the victim program) and instructions executed under a given observation function (view of the system state). In other words, the attacker does not observe anything other than what the victim explicitly provides in its output.
References:
- Lamport. Specifying Systems
- Subramanyan et al. A Formal Foundation for Secure Remote Execution of Enclaves
- Guarnieri et al. SPECTECTOR: Principled Detection of Speculative Information Flows