11.07.2023
Formal Hardware/Software Modeling for Timing Properties: from Safety to Security
Short abstract
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 the system level. In this talk, we first present an overview of the LEAF approach for verifying such timing-related properties. Then, we focus on the required formal model tailored to a specific property: the detection of Timing Anomalies (TA) within pipelines of processors. A TA is a counterintuitive timing behavior that can threaten Worst-Case Execution Time (WCET) analyses. We also report ongoing work to generate such pipeline formal models from RISC-V processors described in Chisel/FIRRTL. Finally, we conclude on current extensions to apply the LEAF approach to safety properties.
Bio
Dr. Mathieu Jan obtained his engineering diploma in 2003 and got a Ph.D. in 2006 on data management for grid architectures from Univ. of Rennes 1 in an INRIA laboratory. He joined CEA LIST in 2007 as a full-time researcher. Since then, his main research interests are embedded systems and real-time systems. Senior expert at CEA LIST since 2014, he obtained a "Habilitation à Diriger des Recherches" (HDR) in 2016, and is a CEA Research Director since 2021. He spent the whole year 2019 as visiting scholar at the University of California, Berkeley (UCB) in the group of Prof. Edward Lee. Since 2020, Mathieu focuses on the hardware/software formal verification of embedded systems and is the Ph.D. director of several Ph.D. students in this area.
Photo: Private
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 the system level. In this talk, we first present an overview of the LEAF approach for verifying such timing-related properties. Then, we focus on the required formal model tailored to a specific property: the detection of Timing Anomalies (TA) within pipelines of processors. A TA is a counterintuitive timing behavior that can threaten Worst-Case Execution Time (WCET) analyses. We also report ongoing work to generate such pipeline formal models from RISC-V processors described in Chisel/FIRRTL. Finally, we conclude on current extensions to apply the LEAF approach to safety properties.
Bio
Dr. Mathieu Jan obtained his engineering diploma in 2003 and got a Ph.D. in 2006 on data management for grid architectures from Univ. of Rennes 1 in an INRIA laboratory. He joined CEA LIST in 2007 as a full-time researcher. Since then, his main research interests are embedded systems and real-time systems. Senior expert at CEA LIST since 2014, he obtained a "Habilitation à Diriger des Recherches" (HDR) in 2016, and is a CEA Research Director since 2021. He spent the whole year 2019 as visiting scholar at the University of California, Berkeley (UCB) in the group of Prof. Edward Lee. Since 2020, Mathieu focuses on the hardware/software formal verification of embedded systems and is the Ph.D. director of several Ph.D. students in this area.
Photo: Private