Speculative execution avoids pipeline stalls by predicting intermediate results and by speculatively executing instructions based on such predictions. When a prediction turns out to be incorrect, the processor squashes the speculative instructions, thereby rolling back their effect on the architectural state. Speculative instructions, however, leave footprints in microarchitectural components (e.g., caches) that persist even after speculative execution terminates. Modern processors have different speculation mechanisms (branch predictors, memory disambiguators, etc.) that are used to speculate over different kinds of instructions: conditional branching [8], indirect jumps [8], store and load operations [6], and return instructions [9]. As shown by Spectre [8], attackers can exploit the side effect of these instructions to leak information about speculatively accessed data. Countermeasures against speculative leaks are typically developed as secure compiler passes. These passes have one concrete attacker model in mind, that is, an attacker that observes certain specific events during the execution of the program e.g., memory effects via store and load observations. Thus, a secure compiler is secure w.r.t a concrete attacker. For example, the SLH countermeasure [2] is used against Spectre v1; there, the attacker is able to observe speculative execution of branch instructions. However, three concerns arise in this setting. First, when the developer of the secure compiler pass does not consider other kinds of speculation (or, different attackers observing different kinds of speculation) new speculative leaks arise, as in the case of the work of Daniel et al. [3]. Second, new speculative execution attacks are still found to this day [1, 10], so we need to make sure that countermeasures have no speculative leaks even with respect to new attacks. Third, some secure compiler passes turn out to be secure even with regards to a stronger attacker, namely one that is observing more speculative leaks. In this paper, we want to identify when compilers can be secure even for stronger attacker models and we devise a formal framework for establishing exactly the kind of well-formedness conditions that lead to these kind of security guarantees. We focus on countermeasures against Spectre attacks, though we think our definitions scale to a more general setting too, but we leave this investigation to future work.