Spectre and Meltdown attacks and their variants exploit hardware performance optimization features to cause security breaches. Secret information is accessed and leaked through covert or side channels. New attack variants keep appearing and we do not have a systematic way to capture the critical characteristics of these attacks and evaluate why they succeed or fail.In this paper, we provide a new attack-graph model for reasoning about speculative execution attacks. We model attacks as ordered dependency graphs, and prove that a race condition between two nodes can occur if there is a missing dependency edge between them. We define a new concept, “security dependency”, between a resource access and its prior authorization operation. We show that a missing security dependency is equivalent to a race condition between authorization and access, which is a root cause of speculative execution attacks. We show detailed examples of how our attack graph models the Spectre and Meltdown attacks, and is generalizable to all the attack variants published so far. This attack model is also very useful for identifying new attacks and for generalizing defense strategies. We identify several defense strategies with different performance-security tradeoffs. We show that the defenses proposed so far all fit under one of our defense strategies. We also explain how attack graphs can be constructed and point to this as promising future work for tool designers
more »
« less
SoK: Practical Foundations for Software Spectre Defenses
Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about microarchitectural details such as speculative execution. In order to aid developers with these attacks in a principled way, the research community has sought formal foundations for speculative execution upon which to rebuild provable security guarantees.This paper systematizes the community’s current knowledge about software verification and mitigation for Spectre. We study state-of-the-art software defenses, both with and without associated formal models, and use a cohesive framework to compare the security properties each defense provides. We explore a wide variety of tradeoffs in the expressiveness of formal frameworks, the complexity of defense tools, and the resulting security guarantees. As a result of our analysis, we suggest practical choices for developers of analysis and mitigation tools, and we identify several open problems in this area to guide future work on grounded software defenses.
more »
« less
- Award ID(s):
- 2120696
- NSF-PAR ID:
- 10384762
- Editor(s):
- Holz, Thorsten; Ristenpart, Thomas
- Date Published:
- Journal Name:
- 2022 IEEE Symposium on Security and Privacy (SP)
- Page Range / eLocation ID:
- 666 to 680
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Speculative execution attacks leverage the speculative and out-of-order execution features in modern computer processors to access secret data or execute code that should not be executed. Secret information can then be leaked through a covert channel. While software patches can be installed for mitigation on existing hardware, these solutions can incur big performance overhead. Hardware mitigation is being studied extensively by the computer architecture community. It has the benefit of preserving software compatibility and the potential for much smaller performance overhead than software solutions. This paper presents a systematization of the hardware defenses against speculative execution attacks that have been proposed. We show that speculative execution attacks consist of 6 critical attack steps. We propose defense strategies, each of which prevents a critical attack step from happening, thus preventing the attack from succeeding. We then summarize 20 hardware defenses and overhead-reducing features that have been proposed. We show that each defense proposed can be classified under one of our defense strategies, which also explains why it can thwart the attack from succeeding. We discuss the scope of the defenses, their performance overhead, and the security-performance trade-offs that can be made.more » « less
-
Speculative execution attacks like Spectre and Meltdown exploit hardware performance optimization features to illegally access a secret and then leak the secret to an unauthorized recipient. Many variants of speculative execution attacks (also called transient execution attacks) have been proposed in the last few years, and new ones are constantly being discovered. While software mitigations for some attacks have been proposed, they often cause very significant performance degradation. Hardware solutions are also being proposed actively by the research community, especially as these are attacks on hardware microarchitecture. In this talk, we identify the critical steps in a speculative attack, and the root cause of successful attacks. We define the concept of "security dependencies", which should be implemented to prevent data leaks and other security breaches. We propose a taxonomy of defense strategies and show how proposed hardware defenses fall under each defense strategy. We discuss security-performance tradeoffs, which can decrease the performance overhead while still preventing security breaches. We suggest design principles for future security-aware microarchitecture.more » « less
-
more » « less
Abstract Transient execution attacks such as Spectre and Meltdown exploit speculative execution in modern microprocessors to leak information via cache side‐channels. Software solutions to defend against many transient execution attacks employ the
lfence serialising instruction, which does not allow instructions that come after thelfence to execute out‐of‐order with respect to instructions that come before thelfence . However, errors and Trojans in the hardware implementation oflfence can be exploited to compromise the software mitigations that uselfence . The aforementioned security gap has not been identified and addressed previously. The authors provide a formal method solution that addresses the verification oflfence hardware implementation. The authors also show how hardware Trojans can be designed to circumventlfence and demonstrate that their verification approach will flag such Trojans as well. The authors have demonstrated the efficacy of our approach using RSD, which is an open source RISC‐V based superscalar out‐of‐order processor. -
Speculative execution is an essential performance enhancing technique in modern processors, but it has been shown to be insecure. In this paper, we propose SpectreGuard, a novel defense mechanism against Spectre attacks. In our approach, sensitive memory blocks (e.g., secret keys) are marked using simple OS/library API, which are then selectively protected by hardware from Spectre attacks via low-cost micro-architecture extension. This technique allows microprocessors to maintain high performance, while restoring the control to software developers to make security and performance trade-offs.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/SP46214.2022.9833707
