34 citations · 71 across the 10 of their papers we have counts for
11 papers
VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL
Anna Lena Duque Antón, Johannes Müller, Philipp Schmitz +6
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-g…
A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators
Anna Lena Duque Antón, Johannes Müller, Lucas Deutschmann +3
The threat of hardware Trojans (HTs) in security-critical IPs like cryptographic accelerators poses severe security risks. The HT detection methods available today mostly rely on g…
Okapi: Efficiently Safeguarding Speculative Data Accesses in Sandboxed Environments
Philipp Schmitz, Tobias Jauch, Alex Wezel +6
This paper introduces Okapi, a new hardware/software cross-layer architecture designed to mitigate Transient Execution Side Channel attacks, including Spectre variants, in modern c…
MCU-Wide Timing Side Channels and Their Detection
Johannes Müller, Anna Lena Duque Antón, Lucas Deutschmann +8
Microarchitectural timing side channels have been thoroughly investigated as a security threat in hardware designs featuring shared buffers (e.g., caches) or parallelism between at…
A Scalable Formal Verification Methodology for Data-Oblivious Hardware
Lucas Deutschmann, Johannes Mueller, Mohammad Rahmani Fadiheh +2
The importance of preventing microarchitectural timing side channels in security-critical applications has surged in recent years. Constant-time programming has emerged as a best-p…
A Framework for Formal Verification of DRAM Controllers
Lukas Steiner, Chirag Sudarshan, Matthias Jung +2
The large number of recent JEDEC DRAM standard releases and their increasing feature set makes it difficult for designers to rapidly upgrade the memory controller IPs to each new s…
An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors
Mohammad Rahmani Fadiheh, Alex Wezel, Johannes Mueller +6
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 co…
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection
Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki +6
We present a novel approach to pre-silicon verification of processor designs. The purpose of pre-silicon verification is to find logic bugs in a design at an early stage and thus a…
Efficient Binary-Level Coverage Analysis
M. Ammar Ben Khadra, Dominik Stoffel, Wolfgang Kunz
Code coverage analysis plays an important role in the software testing process. More recently, the remarkable effectiveness of coverage feedback has triggered a broad interest in f…
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study
Eshan Singh, Keerthikumara Devarajegowda, Sebastian Simon +8
We present an industrial case study that demonstrates the practicality and effectiveness of Symbolic Quick Error Detection (Symbolic QED) in detecting logic design flaws (logic bug…
Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking
Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark Barrett +2
Recent discovery of security attacks in advanced processors, known as Spectre and Meltdown, has resulted in high public alertness about security of hardware. The root cause of thes…