μARCHIFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections
2023 Formal Methods in Computer-Aided Design (FMCAD)(2023)
摘要
This paper introduces μARCHiFI, an open-source tool dedicated to the formal modeling and verification of microarchitecture-level fault injections and their effects on complex hardware/software systems. First, we address the problem of the system modeling, and our implementation is integrated into the Yosys toolchain. Second, we introduce verification strategies to evaluate the fault effects for software-level security. We demonstrated the practical use of μARCHiFI on RISC-V use cases using state-of-the-art model-checking tools for hardware verification.
更多查看译文
关键词
Faulty transition system,Bounded model checking,SW/HW co-verification,Security
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要