Overview

Ibex is a small 32-bit RISC-V CPU core that was previously known as zero-riscy. It is developed as an open-source SystemVerilog implementation and is maintained in the lowRISC/ibex GitHub repository. [C1]

Architecture

Ibex is characterized as a 32-bit RISC-V CPU core, implementing the RISC-V instruction set architecture. The primary implementation language of the repository is SystemVerilog. [C1] The core has been used in multiple academic verification and security research efforts as a representative small / embedded-class RISC-V implementation.

Role in the TestRIG ecosystem

Ibex is one of the RISC-V processor implementations adopted by the TestRIG randomized testing ecosystem. In the TestRIG comparison, Ibex (alongside Piccolo) is characterized as a simple 32-bit implementation, in contrast to other listed implementations such as RVBS, Flute, and Toooba. The TestRIG paper points to a CTSRD-CHERI fork of Ibex (https://github.com/CTSRD-CHERI/ibex) as the version used in that work, distinct from the mainline lowRISC/ibex repository. [C2]

TestRIG proposes a standardized communication interface so that verification engines, golden models, and hardware implementations can be interchanged. To participate in TestRIG, implementations are instrumented with RVFI-DII (RISC-V Formal Interface — Direct Instruction Injection), and are expected to be architecturally identical, expose an RVFI-DII interface, provide 8 MiB of memory at address 0x80000000, return access faults for other addresses, and support reset to a known state including zeroed registers and zeroed memory. [C2]

In practice, integrating Ibex with RVFI-DII requires modifying its pipeline stages, and one reported verification effort based on the RVFI-DII approach of [Joannou 2024] required more than 450 lines of code for the Ibex setup. [C3]

Leakage contract verification case study

The TCHES 2024 paper Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches uses the RISC-V Ibex core as its primary case study for end-to-end security verification of masked cryptographic software against gate-level hardware. The authors show that a power (leakage) contract can be written for Ibex without any modifications to the hardware design, and use that contract to prove end-to-end security between masked software and the gate-level hardware. The paper extends the leakage-contracts model to account for glitches and transitions, presents what it describes as the first end-to-end verification tool for transient leakage contracts, and allows contracts to be written in C. [C4]

Related entities

• RISC-V — Ibex is a CPU core that targets the RISC-V instruction set architecture.