Biblio
The SPECTRE family of speculative execution attacks has required a rethinking of formal methods for security. Approaches based on operational speculative semantics have made initial inroads towards finding vulnerable code and validating defenses. However, with each new attack grows the amount of microarchitectural detail that has to be integrated into the underlying semantics. We propose an alternative, lightweight and axiomatic approach to specifying speculative semantics that relies on insights from memory models for concurrency. We use the CAT modeling language for memory consistency to specify execution models that capture speculative control flow, store-to-load forwarding, predictive store forwarding, and memory ordering machine clears. We present a bounded model checking framework parameterized by our speculative CAT models and evaluate its implementation against the state of the art. Due to the axiomatic approach, our models can be rapidly extended to allow our framework to detect new types of attacks and validate defenses against them.
ISSN: 2375-1207
Since 2018, a broad class of microarchitectural attacks called transient execution attacks (e.g., Spectre and Meltdown) have been disclosed. By abusing speculative execution mechanisms in modern CPUs, these attacks enable adversaries to leak secrets across security boundaries. A transient execution attack typically evolves through multiple stages, termed the attack chain. We find that current transient execution attacks usually rely on static attack chains, resulting in that any blockage in an attack chain may cause the failure of the entire attack. In this paper, we propose a novel defense-aware framework, called TEADS, for synthesizing transient execution attacks dynamically. The main idea of TEADS is that: each attacking stage in a transient execution attack chain can be implemented in several ways, and the implementations used in different attacking stages can be combined together under certain constraints. By constructing an attacking graph representing combination relationships between the implementations and testing available paths in the attacking graph dynamically, we can finally synthesize transient execution attacks which can bypass the imposed defense techniques. Our contributions include: (1) proposing an automated defense-aware framework for synthesizing transient execution attacks, even though possible combinations of defense strategies are enabled; (2) presenting an attacking graph extension algorithm to detect potential attack chains dynamically; (3) implementing TEADS and testing it on several modern CPUs with different protection settings. Experimental results show that TEADS can bypass the defenses equipped, improving the adaptability and durability of transient execution attacks.
The impact of microarchitectural attacks in Personal Computers (PCs) can be further adapted to and observed in internetworked All Programmable System-on-Chip (AP SoC) platforms. This effort involves the access control or execution of Intellectual Property cores in the FPGA of an AP SoC Victim internetworked with an AP SoC Attacker via Internet Protocol (IP). Three conceptions of attacks were implemented: buffer overflow attack at the stack, return-oriented programming attack, and command-injection-based attack for dynamic reconfiguration in the FPGA. Indeed, a specific preventive countermeasure for each attack is proposed. The functionality of the countermeasures mainly comprises adapted words addition (stack protection) for the first and second attacks and multiple encryption for the third attack. In conclusion, the recommended countermeasures are realizable to counteract the implemented attacks.
Microarchitectural Side-Channel Attacks (SCAs) have emerged recently to compromise the security of computer systems by exploiting the existing processors' hardware vulnerabilities. In order to detect such attacks, prior studies have proposed the deployment of low-level features captured from built-in Hardware Performance Counter (HPC) registers in modern microprocessors to implement accurate Machine Learning (ML)-based SCAs detectors. Though effective, such attack detection techniques have mainly focused on binary classification models offering limited insights on identifying the type of attacks. In addition, while existing SCAs detectors required prior knowledge of attacks applications to detect the pattern of side-channel attacks using a variety of microarchitectural features, detecting unknown (zero-day) SCAs at run-time using the available HPCs remains a major challenge. In response, in this work we first identify the most important HPC features for SCA detection using an effective feature reduction method. Next, we propose Phased-Guard, a two-level machine learning-based framework to accurately detect and classify both known and unknown attacks at run-time using the most prominent low-level features. In the first level (SCA Detection), Phased-Guard using a binary classification model detects the existence of SCAs on the target system by determining the critical scenarios including system under attack and system under no attack. In the second level (SCA Identification) to further enhance the security against side-channel attacks, Phased-Guard deploys a multiclass classification model to identify the type of SCA applications. The experimental results indicate that Phased-Guard by monitoring only the victim applications' microarchitectural HPCs data, achieves up to 98 % attack detection accuracy and 99.5% SCA identification accuracy significantly outperforming the state-of-the-art solutions by up to 82 % in zero-day attack detection at the cost of only 4% performance overhead for monitoring.
Modern processors use branch prediction and speculative execution to maximize performance. For example, if the destination of a branch depends on a memory value that is in the process of being read, CPUs will try to guess the destination and attempt to execute ahead. When the memory value finally arrives, the CPU either discards or commits the speculative computation. Speculative logic is unfaithful in how it executes, can access the victim's memory and registers, and can perform operations with measurable side effects. Spectre attacks involve inducing a victim to speculatively perform operations that would not occur during correct program execution and which leak the victim's confidential information via a side channel to the adversary. This paper describes practical attacks that combine methodology from side channel attacks, fault attacks, and return-oriented programming that can read arbitrary memory from the victim's process. More broadly, the paper shows that speculative execution implementations violate the security assumptions underpinning numerous software security mechanisms, including operating system process separation, containerization, just-in-time (JIT) compilation, and countermeasures to cache timing and side-channel attacks. These attacks represent a serious threat to actual systems since vulnerable speculative execution capabilities are found in microprocessors from Intel, AMD, and ARM that are used in billions of devices. While makeshift processor-specific countermeasures are possible in some cases, sound solutions will require fixes to processor designs as well as updates to instruction set architectures (ISAs) to give hardware architects and software developers a common understanding as to what computation state CPU implementations are (and are not) permitted to leak.
This paper presents a multilayer protection approach to guard programs against Return-Oriented Programming (ROP) attacks. Upper layers validate most of a program's control flow at a low computational cost; thus, not compromising runtime. Lower layers provide strong enforcement guarantees to handle more suspicious flows; thus, enhancing security. Our multilayer system combines techniques already described in the literature with verifications that we introduce in this paper. We argue that modern versions of x86 processors already provide the microarchitectural units necessary to implement our technique. We demonstrate the effectiveness of our multilayer protection on a extensive suite of benchmarks, which includes: SPEC CPU2006; the three most popular web browsers; 209 benchmarks distributed with LLVM and four well-known systems shown to be vulnerable to ROP exploits. Our experiments indicate that we can protect programs with almost no overhead in practice, allying the good performance of lightweight security techniques with the high dependability of heavyweight approaches.