Formal Processor Modeling for Analyzing Safety and Security Properties on RISC-V case studies
Mathieu Jan (CEA List), October 14th, 2022, Métivier Room
The emergence of open hardware initiatives, for instance based on the RISC-V ISA, exposes more easily the exact behavior of hardware designs. They can then be analyzed and combined with application-level semantics to formally verify complex safety and security properties at system level, in particular by integrating non-functional characteristics such as timing. This is the goal of the LEAF approach which currently focuses, on one hand, on timing predictability evaluations required by safety-critical systems, and on the other hand on assessments of fault-injection attacks over secured embedded systems. In this talk, we first briefly present an overview of LEAF and our various modeling requirements. Then, we review recent results over several RISC-V case studies for: 1) the introduction of causality in a code-specific approach to (better) detect (counter-intuitive) timing anomalies within out-of-order pipelines (published at RTCSA 2022) , 2) the automatic construction of pipeline datapaths from Chisel-based processor (to appear at MEMOCODE 2022) and finally 3) fault-injection assessment over different versions of the CV32E40P processor from the OpenHW Group (to appear at FDTC 2022).
