Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau (RPTU)

The Chair of Electronic Design Automation at RPTU in Kaiserslautern has a long background in formal verification of hardware designs.With the emergence of microarchitectural vulnerabilities, such as Spectre and Meltdown, we extended our research to not only cover functional correctness of designs but also to detect security vulnerabilities on a pre-silicon basis.

In 2024, we developed VeriCHERI, a novel verification methodology that exhaustively detects security breaches in CHERI designs. VeriCHERI stands out by not requiring any ISA specification, instead focusing on well-established global security objectives of confidentiality and integrity. By introducing symbolic capability models, VeriCHERI ensures broad applicability to industry-grade RTL designs.