Fault injection attacks pose a significant threat to the security of embedded devices. While their effects are commonly modeled as instruction skips or data corruption, characterizing these faults requires programs that expose software-visible faulty behavior. However, many fault effects originate from microarchitectural elements, making them difficult to identify using existing approaches. On one hand, Register Transfer Level (RTL) analyses provide fine-grained insights but rely on abstract models that may not fully reflect the physical circuit. On the other hand, empirical characterization captures real faults but requires extensive experimentation and often reveals multiple fault models simultaneously, complicating precise identification. To address this gap, we propose an automated methodology that synthesizes characterization programs specifically designed to expose targeted microarchitectural fault models using a model-checking algorithm. Our methodology also assesses additional fault models revealed by these programs. Applied to two RISC-V processor cores, CV32E40P and Ibex, our methodology synthesizes programs that expose bit-flip faults for approximately 70% of microarchitectural signals, using two days of computation on 10 parallel cores. For 25% of the control signals in CV32E40P, we synthesize programs enabling the precise attribution of a bit-flip to a targeted signal. Such programs could facilitate the use of fault injection to deduce the placement of microarchitectural elements and help design more effective countermeasures. To the best of our knowledge, this work represents the first systematic methodology for building fault characterization programs, marking a significant step beyond empirical approaches.

The adoption of high-performance multi-core platforms in avionics and automotive systems introduces significant challenges in ensuring predictable execution, primarily due to shared resource interferences. Many existing approaches study interference from a single angle-for example, through hardware-level analysis or by monitoring software execution. However, no single abstraction level is sufficient on its own. Hardware behavior, program structure, and system configuration all interact, and a complete view is needed to understand where interferences come from and how to reduce them. In this paper, we present a methodology that brings together several tools that operate at different abstraction levels. At the lowest level, PHYLOG provides a formal model of the hardware and identifies possible interference channels using micro-architectural transactions. At the program level, machine learning analysis locates the exact parts of the code that are most sensitive to shared-resource contention. At the compilation level, MLIR-based transformations use this information to reshape memory access patterns and reduce pressure on shared resources. Finally, at the system level, Linux cgroups enforce static execution constraints to prevent highly interfering tasks from running together. The goal of our approach is to reduce memory interference and improve the system's predictability, thereby easing the certification process of multi-core systems in safety-critical domains.

Fault injection attacks are a serious threat to system security, enabling attackers to bypass protection mechanisms or access sensitive information. To evaluate the robustness of CPU-based systems against these attacks, it is essential to analyze the consequences of the fault propagation resulting from the complex interplay between the software and the processor. However, current formal methodologies combining hardware and software face scalability issues due to the monolithic approach used. To address this challenge, this work formalizes the k-fault-resistant partitioning notion to solve the fault propagation problem when assessing redundancy-based hardware countermeasures in a first step. Proven security guarantees can then reduce the remaining hardware attack surface when introducing the software in a second step. First, we validate our approach against previous work by reproducing known results on cryptographic circuits. In particular, we outperform state-of-the-art tools for evaluating AES under a three-fault-injection attack. Then, we apply our methodology to the OpenTitan secure element and formally prove the security of its CPU’s hardware countermeasure to single bit-flip injections. Besides that, we demonstrate that previously intractable problems, such as analyzing the robustness of OpenTitan running a secure boot process, can now be solved by a co-verification methodology that leverages a k-fault-resistant partitioning. We also report a potential exploitation of the register file vulnerability in two other software use cases. Finally, we provide a security fix for the register file, prove its robustness, and integrate it into the OpenTitan project.

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.

Static worst-case timing analyses compute safe timing bounds of applications running in real-time systems. These bounds are necessary to evaluate the strict timing constraints of real-time systems. Moreover, the inherent complexity of such systems demands that their timing analyses are able to cope with the large resulting state space. In this direction, a potential solution is to perform compositional timing analysis, where the system-level timing is obtained from component-level timings. Undesired timing phenomena, called timing anomalies, threaten the soundness of (compositional) timing analyses. In this work, we investigate how the industrial superscalar TriCore architecture is amenable for compositional timing analyses via a formal evaluation of amplification timing anomalies. Firstly, we adapt and extend a specialized abstraction, called canonical pipeline model, to capture the amplification effects in a formal model of the TriCore architecture. Then, we use model checking to efficiently detect amplification timing anomalies and report the associated complexity results. Finally, we aim for better precision as we design and implement counterexample-based methods so as to uncover patterns leading to such anomalies.

Intuitively, a counter-intuitive timing anomaly manifests when a locally faster execution becomes globally slower. While the presence of such timing anomalies threatens the soundness and/or scalability of timing analyses, tools to systematically detect them do not exist. The main reason lies in the absence of a definition of counter-intuitive timing anomalies that establishes relations between local and global timing effects. In this paper, we address these relations through an important concept, that of causality, which we further use to revise the formalization of counter-intuitive timing anomalies. We also propose a specialized instance of the notions to implement a detection procedure for out-of-order pipelines.

This paper introduces a formal workflow for modeling software/hardware systems in order to explore the effects of fault injections and evaluate the robustness to fault injection attacks. We illustrate this workflow on four versions of a PIN authentication code, embedding different software countermeasures. The code is symbolically evaluated on two implementations of the RISC-V CV32E40P core: the original implementation from the OpenHW group and an implementation that integrates protection of the pipeline control signals. On the original, unprotected core, our formal workflow exposes various vulnerabilities, including previously unknown ones, whereas, on the protected core, it confirms the effectiveness of the proposed countermeasures.

Safety-critical applications require well-defined and documented timing behavior. These requirements shape the design and implementation of a timing analyzer based on a formal Instruction-Set Architecture (ISA) semantics and formal micro-architecture models. In this paper we present the key elements of such a timing analyzer and how to systematically combine the formal components to address timing properties such as evaluating memory interferences. We also report preliminary experiments of memory interference analysis of multi-threaded applications in a multicore context.

Safety-critical systems rely on worst-case timing analysis under architecture considerations to ensure that their timing bounds could be guaranteed. Usually, such architecture models are constructed by hand, from processor manuals. However, with open hardware initiatives and high-level Hardware Description Languages (HDL), automation would and should be possible. In this paper, we present an approach for constructing pipeline datapath models from processor designs described in high-level HDLs. We propose a methodology based on the Chisel/FIRRTL Hardware Compiler Framework and we report preliminary results on several open-source RISC-V processors.

Static worst-case timing analysis is important in the context of safety-critical systems as it is one approach that could be used to validate the required timing bounds. In order to derive accurate bounds, the worst-case timing analysis is performed under (micro)-architecture consideration, consequently, these bounds are expressed in processor cycles. The required (micro)-architecture models are usually constructed by hand, from processor manuals and validated through testing. Recent advances in hardware design promote open hardware initiatives and high-level Hardware Description Languages (HDLs), revisiting the perspectives to automatically construct (micro)-architecture models for worst-case timing analysis. In this paper, we present an approach concerning the construction of pipeline datapath models from processor designs described in high-level HDLs. We propose a methodology based on the Chisel/FIRRTL Hardware Compiler Framework which we apply on several open-source RISC-V processors.

Correctness is an important concern during the development of real-time systems. In addition to the functional correctness, the timing behavior is often formally verified in order to ensure that correct results are delivered in-time for all possible execution conditions. The timing behavior of real-time software is thus often validated through a rigorous timing analysis that aims at determining the worst-case execution time.Timing anomalies present a major obstacle during the validation of timing properties on modern computer platforms. Out-of-order execution and concurrent accesses to shared resources may sometimes lead to – at first sight – surprising timing behavior. Several (semi-)formal definitions have been proposed in the literature in order to capture such situations. However, as we present in this work, none of the existing definitions appears to be precise enough to be systematically used for detecting timing anomalies in modern processors with out-of-order execution.

Real-time systems are subject to strong timing requirements, and thus rely on worst-case timing analyses to safely address them. Undesired timing phenomena, called timing anomalies, threaten the soundness of timing analyses. In this regard, we consider the following inauspicious partnership - a compositional timing analysis and amplification timing anomalies. Precisely, we investigate how the industrial, superscalar TriCore architecture is amenable for compositional timing analyses via a formal evaluation of amplification timing anomalies. We adapt and extend a specialized abstraction, called canonical pipeline model, to quantify the amplification effects in a model of a dual-pipelined TriCore, its asynchronous store buffer, data dependencies, and structural hazards. We use model checking to efficiently detect amplification timing anomalies and report the associated complexity results.

Multi-core architectures pose many challenges in real-time systems, which arise from contention between concurrent accesses to shared memory. Among the available memory arbitration policies, time-division multiplexing (TDM) ensures a predictable behavior by bounding access latencies and guaranteeing bandwidth to tasks independently from the other tasks. To do so, TDM guarantees exclusive access to the shared memory in a fixed time window. TDM, however, provides a low resource utilization as it is non-work-conserving . Besides, it is very inefficient for resources having highly variable latencies, such as sharing the access to a DRAM memory. The constant length of a TDM slot is, hence, highly pessimistic and causes an underutilization of the memory. To address these limitations, we present dynamic arbitration schemes that are based on TDM. However, instead of arbitrating at the level of TDM slots, our approach operates at the granularity of clock cycles by exploiting slack time accumulated from preceding requests. This allows the arbiter to reorder memory requests, exploit the actual access latencies of requests, and thus improve memory utilization. We demonstrate that our policies are analyzable as they preserve the guarantees of TDM in the worst case, while our experiments show an improved memory utilization. We furthermore present and evaluate an efficient hardware implementation for a variant of our arbitration strategy.

Timing analysis of safety-critical systems derives timing bounds of applications, or software (SW), executed on dedicated platforms, or hardware (HW). The ensemble HW–SW features, from a timing perspective, two different types of computation – a SW-specific, instruction-driven timing progression and a HW-specific, cycle-driven one. The two timings are unified under a concept of timing model , which is crucial to establish a sound and precise worst-case timing reasoning. In this paper, we propose an investigation on how to systematically derive and formally prove such timing models. Our approach is exemplified on a simple, accumulator-based processor called Lipsi.

Computer architectures used in safety-critical domains are subjected to worst-case execution time analysis. The presence of performance-driven microarchitectures may trigger undesired timing phenomena, called timing anomalies, and complicate the timing analysis. This paper investigates pipelines specifically designed to simplify the worst-case execution time analysis (also called predictable pipelines). We propose formal and executable models of four research-oriented pipelines and one industrial pipeline to validate some of their claims related to their timing behavior. We indeed validate, via bounded model checking, the absence of a type of timing anomalies called amplification timing anomalies, or its potential presence by identifying prerequisite to situations where they can occur.

The interactions among concurrent tasks pose a challenge in the design of real-time multi-core systems, where blocking delays that tasks may experience while accessing shared memory have to be taken into consideration. Various memory arbitration schemes have been devised that address these issues, by providing trade-offs between predictability, average-case performance, and analyzability. Time-Division Multiplexing (TDM) is a well-known arbitration scheme due to its simplicity and analyzability. However, it suffers from low resource utilization due to its non-work-conserving nature. We proposed in our recent work dynamic schemes based on TDM, showing work-conserving behavior in practice, while retaining the guarantees of TDM. These approaches have only been evaluated in a restricted setting. Their applicability in a preemptive setting appears problematic, since they may induce long memory blocking times depending on execution history. These blocking delays may induce significant jitter and consequently increase the tasks' response times. This work explores means to manage and, finally, bound these blocking delays. Three different schemes are explored and compared with regard to their analyzability, impact on response-time analysis, implementation complexity, and runtime behavior. Experiments show that the various approaches behave virtually identically at runtime. This allows to retain the approach combining low implementation complexity with analyzability.

We discuss ongoing work towards a meta-language, execution model, and compiler tool chain that promotes determinism and grants first-class citizenship to the timing aspects of computation.

The design of tailored hardware has proven a successful strategy to reduce the timing analysis overhead for (hard) real-time systems. The stack cache is an example of such a design that was shown to provide good average-case performance, while remaining easy to analyze. So far, however, the analysis of the stack cache was limited to individual tasks, ignoring aspects related to multitasking. A major drawback of the original stack cache design is that, due to its simplicity, it cannot hold the data of multiple tasks at the same time. Consequently, the entire cache content needs to be saved and restored when a task is preempted. We propose (a) an analysis exploiting the simplicity of the stack cache to bound the overhead induced by task preemption, (b) preemption mechanisms for the stack cache exploiting the previous analysis and, finally, (c) an extension of the design that allows to (partially) hide the overhead by virtualizing stack caches.