SPP 2253, Project: HaSPro - Verifiable Hardware Security for Out-of-Order Processors - Phase 2

Transient Execution Side Channels (TES), including Spectre and Meltdown, pose continual security risks to modern computer systems, despite mitigation efforts. These vulnerabilities, exacerbated by the security-performance trade-off, are the focus of the HaSPro project. It concentrates on out-of-order processors with speculation and Trusted Execution Environments (TEEs), key for improved system security. HaSPro Phase 1 utilized Unique Program Execution Checking (UPEC) for security analysis against TES in processors. A central objective of Phase 1 was to make UPEC scalable to advanced processor architectures. Phase 1 yielded a boost in scalability by a novel notion called microequivalence. We also explored side channels that compromise the constant-time programming paradigm and developed UPEC-DIT that can provide security guarantees for data-oblivious computing. With respect to TEEs, Phase 1 focused on identifying and mitigating vulnerabilities in prevalent TEE designs such as Intel SGX and AMD SEV, revealing a number of weaknesses including ciphertext leakage and data-dependent execution. The project led to the development of countermeasures for these vulnerabilities, including a proposed attestation protocol to secure memory layout and exploration of strategies to address the shortcomings of deterministic memory encryption. Phase 1 produced tools like Microwalk-CI, which identifies data-dependent runtime behavior in large code bases, and Cipherfix, which automates the identification and protection of sensitive memory writes vulnerable to ciphertext side-channels. HaSPro Phase 2 aims at developing new and highly efficient countermeasures against TES at different levels: hardware (HW), software (SW) and HW/SW interface. We investigate how HW-supported in-process isolation mechanisms can effectively counteract Spectre variants and whether these isolation barriers can be utilized by SW compartmentalization for automated and robust protection. We automate the separation of potential Spectre gadgets from sensitive data using compiler-based protection. At the HW level, we examine microarchitectural choices to support the proposed extensions to in-process isolation, leveraging formal methods to assure security guarantees. As an alternative to SW-based solutions, we also explore a fully HW-implemented architecture for secure speculation, using a secure-by-construction design methodology. In addition, we explore the combination of code compartmentalization with a partial probabilistic memory encryption engine to establish a new cost-latency tradeoff for TEE memory encryption, aiming for effective prevention of ciphertext side channels. All developed protection mechanisms will be analyzed for effectiveness and overheads and compared to existing countermeasures to evaluate the efficiency of the identified solutions, in order to provide better protection against the remaining attack surface on modern out-of-order processors.