Towards Trustworthy RISC-V Designs: Formal Verification of the MFENCE Instruction

被引:0
作者
Ponugoti, Kushal K. [1 ]
Karlapalem, Nikhila [1 ]
机构
[1] North Dakota State Univ, Dept Elect & Comp Engn, Fargo, ND 58105 USA
来源
4TH INTERDISCIPLINARY CONFERENCE ON ELECTRICS AND COMPUTER, INTCEC 2024 | 2024年
关键词
Formal Verification; Hardware Security; Memory Barriers; MFENCE; RISC-V;
D O I
10.1109/INTCEC61833.2024.10603157
中图分类号
TP39 [计算机的应用];
学科分类号
081203 ; 0835 ;
摘要
Memory barriers play a crucial role in maintaining the consistency of shared data in parallel and multithreaded programming. The mfence instruction is a key component in addressing memory inconsistencies and preventing certain microarchitectural data sampling attacks. Specifically, mfence ensures the completion of certain memory operations in a specific order, preventing the reordering of memory operations across the barrier. Despite its significance, potential security vulnerabilities in the hardware implementation of mfence could be exploited by attackers, compromising its defense mechanism. This paper introduces a formal method for verifying the hardware implementation of mfence, aiming to identify and address potential bugs and trojans. The methodology is designed to detect areas where trojans could be crafted to circumvent the protective features of mfence. The efficacy of this approach is demonstrated using the RSD, an open-source RISC-V-based superscalar Out-of-Order processor.
引用
收藏
页数:6
相关论文
共 13 条
  • [1] Constant-Time Foundations for the New Spectre Era
    Cauligi, Sunjay
    Disselkoen, Craig
    Gleissenthall, Klaus, V
    Tullsen, Dean
    Stefan, Deian
    Rezk, Tamara
    Barthe, Gilles
    [J]. PROCEEDINGS OF THE 41ST ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '20), 2020, : 913 - 926
  • [2] A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-Order Processors
    Fadiheh, Mohammad Rahmani
    Mueller, Johannes
    Brinkmann, Raik
    Mitra, Subhasish
    Stoffel, Dominik
    Kunz, Wolfgang
    [J]. PROCEEDINGS OF THE 2020 57TH ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2020,
  • [3] MFence: Defending Against Memory Access Interference in a Disaggregated Cloud Memory Platform
    Lee, Jinhoon
    Jung, Yeonwoo
    Lee, Suyeon
    Jamil, Safdar
    Park, Sungyong
    Koh, Kwangwon
    Kim, Hongyeon
    Kim, Kangho
    Kim, Youngjae
    [J]. 38TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, SAC 2023, 2023, : 1309 - 1317
  • [4] An Open Source FPGA-Optimized Out-of-Order RISC-V Soft Processor
    Mashimo, Susumu
    Fujita, Akifumi
    Matsuo, Reoma
    Akaki, Seiya
    Fukuda, Akifumi
    Koizumi, Toru
    Kadomoto, Junichiro
    Irie, Hidetsugu
    Goshima, Masahiro
    Inoue, Koji
    Shioya, Ryota
    [J]. 2019 INTERNATIONAL CONFERENCE ON FIELD-PROGRAMMABLE TECHNOLOGY (ICFPT 2019), 2019, : 63 - 71
  • [5] FPTree: A Hybrid SCM-DRAM Persistent and Concurrent B-Tree for Storage Class Memory
    Oukid, Ismail
    Lasperas, Johan
    Nica, Anisoara
    Willhalm, Thomas
    Lehner, Wolfgang
    [J]. SIGMOD'16: PROCEEDINGS OF THE 2016 INTERNATIONAL CONFERENCE ON MANAGEMENT OF DATA, 2016, : 371 - 386
  • [6] Verification of serialising instructions for security against transient execution attacks
    Ponugoti, Kushal K.
    Srinivasan, Sudarshan K.
    Mathure, Nimish
    [J]. IET COMPUTERS AND DIGITAL TECHNIQUES, 2023, 17 (3-4) : 127 - 140
  • [7] Illegal Trojan design and detection in asynchronous NULL Convention Logic and Sleep Convention Logic circuits
    Ponugoti, Kushal K.
    Srinivasan, Sudarshan K.
    Smith, Scott C.
    Mathure, Nimish
    [J]. IET COMPUTERS AND DIGITAL TECHNIQUES, 2022, 16 (5-6) : 172 - 182
  • [8] Formal Verification Approach to Detect Always-On Denial of Service Trojans in Pipelined Circuits
    Ponugoti, Kushal K.
    Srinivasan, Sudarshan K.
    Mathure, Nimish
    [J]. 2021 28TH IEEE INTERNATIONAL CONFERENCE ON ELECTRONICS, CIRCUITS, AND SYSTEMS (IEEE ICECS 2021), 2021,
  • [9] Hardware Trojan Design and Detection in Asynchronous NCL Circuits
    Ponugoti, Kushal K.
    Srinivasan, Sudarshan K.
    Smith, Scott C.
    [J]. 2020 27TH IEEE INTERNATIONAL CONFERENCE ON ELECTRONICS, CIRCUITS AND SYSTEMS (ICECS), 2020,
  • [10] SpecTaint: Speculative Taint Analysis for Discovering Spectre Gadgets
    Qi, Zhenxiao
    Feng, Qian
    Cheng, Yueqiang
    Yan, Mengjia
    Li, Peng
    Yin, Heng
    Wei, Tao
    [J]. 28TH ANNUAL NETWORK AND DISTRIBUTED SYSTEM SECURITY SYMPOSIUM (NDSS 2021), 2021,