arXiv subjects

Alex Wezel

Publications and source records attributed to Alex Wezel.

3 recordsLinked to original sources

arXiv2024

VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL

Protecting data in memory from attackers continues to be a concern in computing systems. CHERI is a promising approach to achieve such protection, by providing and enforcing fine-grained memory protection directly in the hardware. Creating trust for the entire system stack, however, requires a gap-free verification of CHERI's hardware-based protection mechanisms. Existing verification methods for CHERI target the abstract ISA model rather than the underlying hardware implementation. Fully ensuring the CHERI security guarantees for a concrete RTL implementation is a challenge in previous flows and demands high manual efforts. This paper presents VeriCHERI, a novel approach to security verification. It is conceptionally different from previous works in that it does not require any ISA specification. Instead of checking compliance with a golden ISA model, we check against well-established global security objectives of confidentiality and integrity. Fully covering these objectives, VeriCHERI uses as few as four unbounded properties to exhaustively prove or disprove any vulnerability. We demonstrate the effectiveness and scalability of VeriCHERI on a RISC-V based processor implementing a CHERI variant.

cs.CR↗

arXiv2023

Okapi: Efficiently Safeguarding Speculative Data Accesses in Sandboxed Environments

This paper introduces Okapi, a new hardware/software cross-layer architecture designed to mitigate Transient Execution Side Channel attacks, including Spectre variants, in modern computing systems. Okapi provides a hardware basis for secure speculation in sandboxed environments and can replace expensive speculation barriers in software. At its core, it allows for speculative data accesses to a memory page only after the page has been accessed non-speculatively by the current trust domain. The granularity of the trust domains can be controlled in software to achieve different security and performance trade-offs. For environments with less stringent security needs, the features can be deactivated to remove all performance overhead. Without relying on any software modification, the Okapi hardware features provide full protection against TES breakout attacks, e.g., by Spectre-PHT or Spectre-BTB, at a thread-level granularity. This incurs an average performance overhead of only 3.17% for the SPEC CPU2017 benchmark suite. Okapi introduces the OkapiReset instruction for additional software-level security support. This instruction allows for fine-grained sandboxing with any custom size, resulting in 2.34% performance overhead in our WebAssembly runtime experiment. On top, Okapi provides the possibility to eliminate poisoning attacks. For the highest level of security, the OkapiLoad instruction prevents confidential data from being added to the trust domain after a sequential access, thereby enforcing weak speculative non-interference. In addition, we present a hardware extension that limits the exploitable code space for Spectre gadgets to well-defined sections of the program. Therefore, by ensuring the absence of gadgets in these sections, developers can tailor their software towards achieving beneficial trade-offs between the size of a trust domain and performance.

cs.CR↗

arXiv2021

An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors

Hardware (HW) security issues have been emerging at an alarming rate in recent years. Transient execution attacks, in particular, pose a genuine threat to the security of modern computing systems. Despite recent advances, understanding the intricate implications of microarchitectural design decisions on processor security remains a great challenge and has caused a number of update cycles in the past. number of update cycles in the past. This papers addresses the need for a new approach to HW sign-off verification which guarantees the security of processors at the Register Transfer Level (RTL). To this end, we introduce a formal definition of security with respect to transient execution attacks, formulated as a HW property. We present a formal proof methodology based on Unique Program Execution Checking (UPEC) which can be used to systematically detect all vulnerabilities to transient execution attacks in RTL designs. UPEC does not exploit any a priori knowledge on known attacks and can therefore detect also vulnerabilities based on new, so far unknown, types of channels. This is demonstrated by two new attack scenarios discovered in our experiments with UPEC. UPEC scales to a wide range of HW designs, including in-order processors (RocketChip), pipelines with out-of-order writeback (Ariane), and processors with deep out-of-order speculative execution (BOOM). To the best of our knowledge, UPEC is the first RTL verification technique that exhaustively covers transient execution side channels in processors of realistic complexity.

cs.CR↗