Mads Dam

Hamed Nemati, Mads Dam

Shared-memory concurrency is notoriously difficult to reason about because each thread executes under interference from other threads. At the same time, many correctness arguments for classical algorithms are fundamentally epistemic: a thread enters a critical region only when, from its local view, it can rule out that another thread is concurrently in that region. We make such arguments explicit by introducing a past-time temporal epistemic logic interpreted over interleaving executions with perfect recall over local histories. Past-time operators support "since"-style reasoning, while epistemic modalities capture what a given thread can conclude from its own observation history. We give a semantics and a sound proof system, instantiate the logic to a simple shared-memory language with instrumented read/write observations, and illustrate the approach on Peterson's mutual exclusion algorithm: an epistemic condition established at the loop-exit step, combined with ownership-based stability obligations, yields global mutual exclusion. We additionally show how the logic embeds rely-guarantee reasoning as an epistemic stability-lifting principle, yielding a parallel-composition meta-theorem that matches the classical compatibility obligations.

Roberto Guanciale, Musard Balliu, Mads Dam

The recent Spectre attacks has demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive formal microarchitectural model capable of representing the forms of out-of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. In this paper we present such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically, we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of three existing countermeasures: constant time, Retpoline, and ARM's Speculative Store Bypass Safe (SSBS).

Musard Balliu, Mads Dam, Gurvan Le Guernic

Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways.