A technical paper titled “A Scalable Formal Verification Methodology for Data-Oblivious Hardware” was published by researchers at RPTU Kaiserslautern-Landau and Stanford University.
“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-practice technique for preventing the leakage of secret information through timing. It is based on the assumption that the timing of certain basic machine instructions is independent of their respective input data. However, whether or not an instruction satisfies this data-independent timing criterion varies between individual processor microarchitectures. In this paper, we propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. The proposed methodology is based on an inductive property that enables scalability even to complex out-of-order cores. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. In addition, the paper discusses several techniques that can be used to make the verification process easier and faster. We demonstrate the feasibility of the proposed methodology through case studies on several open-source designs. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core. In addition to several hardware accelerators and in-order processors, our experiments also include RISC-V BOOM, a complex out-of-order processor, highlighting the scalability of the approach.”
Find the technical paper here. Published August 2023 (preprint).
Deutschmann, Lucas, Johannes Mueller, Mohammad Rahmani Fadiheh, Dominik Stoffel, and Wolfgang Kunz. “A Scalable Formal Verification Methodology for Data-Oblivious Hardware.” arXiv preprint arXiv:2308.07757 (2023).
Related Reading
How Secure Are RISC-V Chips?
Open source by itself doesn’t guarantee security. It still comes down to the fundamentals of design.
New Concepts Required For Security Verification
Why it’s so difficult to ensure that hardware works correctly and is capable of detecting vulnerabilities that may show up in the field.
Power/Performance Costs Of Securing Systems
Security requires significant overhead, but it is no longer an option to ignore it. Cybercriminals will continue to exploit weak components.
Leave a Reply