Formal Processor Modeling for Analyzing Safety and Security Properties
Abstract
Thanks to the emergence of open hardware initiatives, the exact behavior of the hardware design can be analyzed and combined with program representations to verify system-level safety and security properties. However, such formal verifications require the design of appropriate abstract models to scale with the complexity of the analyzed computational systems. In this paper, we compare the different needs when designing abstract processor models for the evaluation of timing predictability, a safety property, and for security assessments when considering fault injections. We also report how the process of building these abstract processor models could be automated.
Origin : Files produced by the author(s)