Showing 1–8 of 8 results for author: Oleksenko, O

AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures

Authors: Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, Gururaj Saileshwar

Abstract: In recent years, several hardware-based countermeasures proposed to mitigate Spectre attacks have been shown to be insecure. To enable the development of effective secure speculation countermeasures, we need easy-to-use tools that can automatically test their security guarantees early-on in the design phase to facilitate rapid prototyping. This paper develops AMuLeT, the first tool capable of test… ▽ More In recent years, several hardware-based countermeasures proposed to mitigate Spectre attacks have been shown to be insecure. To enable the development of effective secure speculation countermeasures, we need easy-to-use tools that can automatically test their security guarantees early-on in the design phase to facilitate rapid prototyping. This paper develops AMuLeT, the first tool capable of testing secure speculation countermeasures for speculative leakage early in their design phase in simulators. Our key idea is to leverage model-based relational testing tools that can detect speculative leaks in commercial CPUs, and apply them to micro-architectural simulators to test secure speculation defenses. We identify and overcome several challenges, including designing an expressive yet realistic attacker observer model in a simulator, overcoming the slow simulation speed, and searching the vast micro-architectural state space for potential vulnerabilities. AMuLeT speeds up test throughput by more than 10x compared to a naive design and uses techniques to amplify vulnerabilities to uncover them within a limited test budget. Using AMuLeT, we launch for the first time, a systematic, large-scale testing campaign of four secure speculation countermeasures from 2018 to 2024--InvisiSpec, CleanupSpec, STT, and SpecLFB--and uncover 3 known and 6 unknown bugs and vulnerabilities, within 3 hours of testing. We also show for the first time that the open-source implementation of SpecLFB is insecure. △ Less

Submitted 28 February, 2025; originally announced March 2025.

Comments: To be published in Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'25)

Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing

Authors: Oleksii Oleksenko, Marco Guarnieri, Boris Köpf, Mark Silberstein

Abstract: Attacks like Spectre abuse speculative execution, one of the key performance optimizations of modern CPUs. Recently, several testing tools have emerged to automatically detect speculative leaks in commercial (black-box) CPUs. However, the testing process is still slow, which has hindered in-depth testing campaigns, and so far prevented the discovery of new classes of leakage. In this paper, we i… ▽ More Attacks like Spectre abuse speculative execution, one of the key performance optimizations of modern CPUs. Recently, several testing tools have emerged to automatically detect speculative leaks in commercial (black-box) CPUs. However, the testing process is still slow, which has hindered in-depth testing campaigns, and so far prevented the discovery of new classes of leakage. In this paper, we identify the root causes of the performance limitations in existing approaches, and propose techniques to overcome these limitations. With these techniques, we improve the testing speed over the state-of-the-art by up to two orders of magnitude. These improvements enable us to run a testing campaign of unprecedented depth on Intel and AMD CPUs. As a highlight, we discover two types of previously unknown speculative leaks (affecting string comparison and division) that have escaped previous manual and automatic analyses. △ Less

Submitted 18 January, 2023; originally announced January 2023.

Comments: To appear in IEEE S&P 2023

Revizor: Testing Black-box CPUs against Speculation Contracts

Authors: Oleksii Oleksenko, Christof Fetzer, Boris Köpf, Mark Silberstein

Abstract: Speculative vulnerabilities such as Spectre and Meltdown expose speculative execution state that can be exploited to leak information across security domains via side-channels. Such vulnerabilities often stay undetected for a long time as we lack the tools for systematic testing of CPUs to find them. In this paper, we propose an approach to automatically detect microarchitectural information lea… ▽ More Speculative vulnerabilities such as Spectre and Meltdown expose speculative execution state that can be exploited to leak information across security domains via side-channels. Such vulnerabilities often stay undetected for a long time as we lack the tools for systematic testing of CPUs to find them. In this paper, we propose an approach to automatically detect microarchitectural information leakage in commercial black-box CPUs. We build on speculation contracts, which we employ to specify the permitted side effects of program execution on the CPU's microarchitectural state. We propose a Model-based Relational Testing (MRT) technique to empirically assess the CPU compliance with these specifications. We implement MRT in a testing framework called Revizor, and showcase its effectiveness on real Intel x86 CPUs. Revizor automatically detects violations of a rich set of contracts, or indicates their absence. A highlight of our findings is that Revizor managed to automatically surface Spectre, MDS, and LVI, as well as several previously unknown variants. △ Less

Submitted 8 February, 2022; v1 submitted 14 May, 2021; originally announced May 2021.

Comments: Published in Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'22)

T-Lease: A Trusted Lease Primitive for Distributed Systems

Authors: Bohdan Trach, Rasha Faqeh, Oleksii Oleksenko, Wojciech Ozga, Pramod Bhatotia, Christof Fetzer

Abstract: A lease is an important primitive for building distributed protocols, and it is ubiquitously employed in distributed systems. However, the scope of the classic lease abstraction is restricted to the trusted computing infrastructure. Unfortunately, this important primitive cannot be employed in the untrusted computing infrastructure because the trusted execution environments (TEEs) do not provide a… ▽ More A lease is an important primitive for building distributed protocols, and it is ubiquitously employed in distributed systems. However, the scope of the classic lease abstraction is restricted to the trusted computing infrastructure. Unfortunately, this important primitive cannot be employed in the untrusted computing infrastructure because the trusted execution environments (TEEs) do not provide a trusted time source. In the untrusted environment, an adversary can easily manipulate the system clock to violate the correctness properties of lease-based systems. We tackle this problem by introducing trusted lease -- a lease that maintains its correctness properties even in the presence of a clock-manipulating attacker. To achieve these properties, we follow a "trust but verify" approach for an untrusted timer, and transform it into a trusted timing primitive by leveraging two hardware-assisted ISA extensions (Intel TSX and SGX) available in commodity CPUs. We provide a design and implementation of trusted lease in a system called T-Lease -- the first trusted lease system that achieves high security, performance, and precision. For the application developers, T-Lease exposes an easy-to-use generic APIs that facilitate its usage to build a wide range of distributed protocols. △ Less

Submitted 16 January, 2021; originally announced January 2021.

SpecFuzz: Bringing Spectre-type vulnerabilities to the surface

Authors: Oleksii Oleksenko, Bohdan Trach, Mark Silberstein, Christof Fetzer

Abstract: SpecFuzz is the first tool that enables dynamic testing for speculative execution vulnerabilities (e.g., Spectre). The key is a novel concept of speculation exposure: The program is instrumented to simulate speculative execution in software by forcefully executing the code paths that could be triggered due to mispredictions, thereby making the speculative memory accesses visible to integrity check… ▽ More SpecFuzz is the first tool that enables dynamic testing for speculative execution vulnerabilities (e.g., Spectre). The key is a novel concept of speculation exposure: The program is instrumented to simulate speculative execution in software by forcefully executing the code paths that could be triggered due to mispredictions, thereby making the speculative memory accesses visible to integrity checkers (e.g., AddressSanitizer). Combined with the conventional fuzzing techniques, speculation exposure enables more precise identification of potential vulnerabilities compared to state-of-the-art static analyzers. Our prototype for detecting Spectre V1 vulnerabilities successfully identifies all known variations of Spectre V1 and decreases the mitigation overheads across the evaluated applications, reducing the amount of instrumented branches by up to 77% given a sufficient test coverage. △ Less

Submitted 10 March, 2020; v1 submitted 24 May, 2019; originally announced May 2019.

Comments: To appear in USENIX Security Symposium (2020)

You Shall Not Bypass: Employing data dependencies to prevent Bounds Check Bypass

Authors: Oleksii Oleksenko, Bohdan Trach, Tobias Reiher, Mark Silberstein, Christof Fetzer

Abstract: A recent discovery of a new class of microarchitectural attacks called Spectre picked up the attention of the security community as these attacks can circumvent many traditional mechanisms of defense. One of the attacks---Bounds Check Bypass---can neither be efficiently solved on system nor architectural levels and requires changes in the application itself. So far, the proposed mitigations involv… ▽ More A recent discovery of a new class of microarchitectural attacks called Spectre picked up the attention of the security community as these attacks can circumvent many traditional mechanisms of defense. One of the attacks---Bounds Check Bypass---can neither be efficiently solved on system nor architectural levels and requires changes in the application itself. So far, the proposed mitigations involved serialization, which reduces the usage of CPU resources and causes high overheads. In this report, we explore methods of delaying the vulnerable instructions without complete serialization. We discuss several ways of achieving it and compare them with Speculative Load Hardening, an existing solution based on a similar idea. The solutions of this type cause 60% overhead across Phoenix benchmark suite, which compares favorably to the full serialization causing 440% slowdown. △ Less

Submitted 10 October, 2018; v1 submitted 22 May, 2018; originally announced May 2018.

Intel MPX Explained: An Empirical Study of Intel MPX and Software-based Bounds Checking Approaches

Authors: Oleksii Oleksenko, Dmitrii Kuvaiskii, Pramod Bhatotia, Pascal Felber, Christof Fetzer

Abstract: Memory-safety violations are a prevalent cause of both reliability and security vulnerabilities in systems software written in unsafe languages like C/C++. Unfortunately, all the existing software-based solutions to this problem exhibit high performance overheads preventing them from wide adoption in production runs. To address this issue, Intel recently released a new ISA extension - Memory Prote… ▽ More Memory-safety violations are a prevalent cause of both reliability and security vulnerabilities in systems software written in unsafe languages like C/C++. Unfortunately, all the existing software-based solutions to this problem exhibit high performance overheads preventing them from wide adoption in production runs. To address this issue, Intel recently released a new ISA extension - Memory Protection Extensions (Intel MPX), a hardware-assisted full-stack solution to protect against memory safety violations. In this work, we perform an exhaustive study of the Intel MPX architecture to understand its advantages and caveats. We base our study along three dimensions: (a) performance overheads, (b) security guarantees, and (c) usability issues. To put our results in perspective, we compare Intel MPX with three prominent software-based approaches: (1) trip-wire - AddressSanitizer, (2) object-based - SAFECode, and (3) pointer-based - SoftBound. Our main conclusion is that Intel MPX is a promising technique that is not yet practical for widespread adoption. Intel MPX's performance overheads are still high (roughly 50% on average), and the supporting infrastructure has bugs which may cause compilation or runtime errors. Moreover, we showcase the design limitations of Intel MPX: it cannot detect temporal errors, may have false positives and false negatives in multithreaded code, and its restrictions on memory layout require substantial code changes for some programs. △ Less

Submitted 16 June, 2017; v1 submitted 2 February, 2017; originally announced February 2017.

Elzar: Triple Modular Redundancy using Intel Advanced Vector Extensions (technical report)

Authors: Dmitrii Kuvaiskii, Oleksii Oleksenko, Pramod Bhatotia, Pascal Felber, Christof Fetzer

Abstract: Instruction-Level Redundancy (ILR) is a well-known approach to tolerate transient CPU faults. It replicates instructions in a program and inserts periodic checks to detect and correct CPU faults using majority voting, which essentially requires three copies of each instruction and leads to high performance overheads. As SIMD technology can operate simultaneously on several copies of the data, it a… ▽ More Instruction-Level Redundancy (ILR) is a well-known approach to tolerate transient CPU faults. It replicates instructions in a program and inserts periodic checks to detect and correct CPU faults using majority voting, which essentially requires three copies of each instruction and leads to high performance overheads. As SIMD technology can operate simultaneously on several copies of the data, it appears to be a good candidate for decreasing these overheads. To verify this hypothesis, we propose Elzar, a compiler framework that transforms unmodified multithreaded applications to support triple modular redundancy using Intel AVX extensions for vectorization. Our experience with several benchmark suites and real-world case-studies yields mixed results: while SIMD may be beneficial for some workloads, e.g., CPU-intensive ones with many floating-point operations, it exhibits higher overhead than ILR in many applications we tested. We study the sources of overheads and discuss possible improvements to Intel AVX that would lead to better performance. △ Less

Submitted 24 August, 2016; v1 submitted 2 April, 2016; originally announced April 2016.

Comments: Short version of this report appeared in the 46th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN'2016) under the title "ELZAR: Triple Modular Redundancy using Intel Advanced Vector Extensions (practical experience report)"