Translating Common Security Assertions Across Processor Designs: A RISC-V Case Study

TL;DR

This paper presents a methodology for translating security assertions across different processor architectures, demonstrated on RISC-V, significantly reducing effort and validated against hardware Trojans.

Contribution

It introduces a novel approach for translating security assertions between processor designs, specifically applied to RISC-V, improving efficiency and effectiveness in security verification.

Findings

Nearly 100% success in assertion translation across modules

Validated assertions detect hardware Trojans effectively

Reduces time and cost compared to manual assertion development

Abstract

RISC-V is gaining popularity for its adaptability and cost-effectiveness in processor design. With the increasing adoption of RISC-V, the importance of implementing robust security verification has grown significantly. In the state of the art, various approaches have been developed to strengthen the security verification process. Among these methods, assertion-based security verification has proven to be a promising approach for ensuring that security features are effectively met. To this end, some approaches manually define security assertions for processor designs; however, these manual methods require significant time, cost, and human expertise. Consequently, recent approaches focus on translating pre-defined security assertions from one design to another. Nonetheless, these methods are not primarily centered on processor security, particularly RISC-V. Furthermore, many of these approaches have not been validated against real-world attacks, such as hardware Trojans. In this work, we introduce a methodology for translating security assertions across processors with different architectures, using RISC-V as a case study. Our approach reduces time and cost compared to developing security assertions manually from the outset. Our methodology was applied to five critical security modules with assertion translation achieving nearly 100% success across all modules. These results validate the efficacy of our approach and highlight its potential for enhancing security verification in modern processor designs. The effectiveness of the translated assertions was rigorously tested against hardware Trojans defined by large language models (LLMs), demonstrating their reliability in detecting security breaches.