Formal Methods in Computer-Aided Design 2023

μA RCHI FI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections

Simon Tollec∗ , Mihail Asavoae∗ , Damien Courouss´e§ , Karine Heydemann¶‡ and Mathieu Jan∗ ∗Universit´e Paris-Saclay, CEA, List, F-91120, Palaiseau, France – firstname.lastname@cea.fr §Univ. Grenoble Alpes, CEA, List, F-38000, Grenoble, France – firstname.lastname@cea.fr ¶Thales DIS, France – firstname.lastname@thalesgroup.com ‡Sorbonne Univ., CNRS, LIP6, F-75005, Paris, France

Abstract—This paper introduces μARCHIFI, an open-source software-level consequences [10], such as: immediate replay tool dedicated to the formal modeling and verification of of instructions that are alive in the prefetch buffer; execution microarchitecture-level fault injections and their effects on com- of instructions in incorrect order; and corruption of the next plex hardware/software systems. First, we address the problem of the system modeling, and our implementation is integrated into branch target. However, such effects, induced by faults in the the Yosys toolchain. Second, we introduce verification strategies processor microarchitecture, can only be leveraged in an attack to evaluate the fault effects for software-level security. We by specific software conditions, in particular the sequence demonstrated the practical use of μARCHIFI on RISC-V use of program instructions executed, such that the fault effects cases using state-of-the-art model-checking tools for hardware propagate until the attack target is reached. verification. Index Terms—Faulty transition system ; Bounded model check- Problem Statement. There is a need for modeling and ing ; SW/HW co-verification ; Security analysis methods to better understand fault effects while considering the software and the hardware together. Such I. INTRODUCTION techniques can help to highlight microarchitectural implemen- tation details impacting the system’s security. We need to Context. Fault Injection (FI) attacks aim at applying abnor- automatically build a model that encompasses both hardware mal execution conditions to an embedded system, such as high and software implementation details, and fault effects. Such a temperature or electromagnetic radiation. These disturbances model needs to be tractable by verification tools in order to induce computational errors in the system, leading to undesired leverage automated verification techniques. behaviors. From a security point of view, these FI attacks Proposal and contributions. We propose a complete work- can create vulnerabilities, such as the ability of an attacker flow for the formal analysis of a full system composed to retrieve sensitive data or to acquire execution privileges on of hardware and software components under fault injection. the platform. Consequently, there is a growing desire to study Faults are modeled at the microarchitectural level to accurately fault injections and better understand their effects to analyze analyze the impact of a fault injection at the hardware level and the system’s security or develop countermeasures. their effects at the software level. We leverage bounded model Different abstraction layers are involved in describing faults checking in order to reason about the impact of fault injections in a system [1]. Faults initially appear in the circuit, and on the system and their possible exploitation by an attacker. representing faults at this level permits to describe their This work is a follow-up of [10], and we bring improvements initial effect, e.g., bit-flip, bit-reset. The consequences of the in two directions. First, we formalize the model-checking fault then propagate in the microarchitecture, can be captured problem with a transition system including the attacker model. by sequential logic, and induce a different behavior at the We describe its implementation in an end-to-end formal anal- software level. An analysis at the hardware level, e.g., [2]– ysis workflow, named μARCHIFI, based on Yosys [12] and a [4], can show that a module is functionally incorrect due to the third-party model checker. μARCHIFI generates the system’s perturbation induced by fault injections. Such approaches are formal model from the RTL implementation of the hardware, sufficient for the robustness analysis of standalone components an input binary program, and the attacker model to analyze the such as cryptographic IPs, but usually, the exploitation of a system’s robustness under fault injection. The attacker model fault injection, in an attack, involves software. On the other supports various fault-injection models. Second, we discuss side, a pure software analysis, e.g., [5]–[7], struggles to model practical strategies to improve the efficiency of the workflow, many subtle behavioral effects induced by fault injection [8]. leveraging well-known optimization techniques from formal Recent research motivates the need to consider both the methods. We illustrate the use of μARCHIFI on several case hardware and the software in the same analysis [8]–[10]. Lau- studies and evaluate the impact of the proposed strategies. rent et al. show how faults on the forwarding mechanism per- μARCHIFI is open-source and will be publicly available on mit to retrieve a previously computed value and reintroduces the GitHub of Yosys1. it in one of the processor pipeline stages [11]. Tollec et al. show how faults on the prefetch buffer can result in various 1Currently available on https://zenodo.org/record/7958412

https://doi.org/10.34727/2023/isbn.978-3-85448-060-0 18     This article is licensed under a Creative
                                                            Commons Attribution 4.0 International License

      Paper outline. Section II introduces microarchitectural fault   instance. Uninitialized registers imply multiple initial states in
injection models and hardware transition systems. Section III         the system.
describes the faulty transition system we introduce to analyze        An input    x ∈ X is a vector x := ⟨i1,..., im⟩           composed
microarchitectural fault consequences at the software level.          with a valuation of the m input variables given to the system.
Section IV introduces our verification problem. The formal            Circuit outputs are not considered in the formalization as they
model is then automatically generated by the tool detailed in         are not useful for the rest of this work.
Section V. Section VI evaluates our approach in three case            The transition function    T       describes the valid transitions
studies. Section VII discusses our contributions wrt. related         from a state si and an input vector xi to the state si+1 at the
work, and Section VIII concludes.                                     next circuit clock cycle. The function T        is determined with
    II. BACKGROUND                                                    the combinational logic of the hardware design and can be
    decomposed in n register transition functions δr where each
    j δr to the

This section introduces microarchitectural fault models, pro- register next state value is computed by applying j vides definitions on hardware transition systems modeling, and current state and the input vector. describes the Yosys framework that can translate a hardware s description to formal models. i+1 = T (si, xi) = ⟨δr1 (si, xi), . . . , δrn (si, xi)⟩ A. Microarchitectural Faults In hardware circuits, intermediate combinational results are often factorized to minimize the number of operations. Fault Injection (FI) attacks are a powerful threat against This optimization avoids duplicating identical operations to embedded systems that cover various physical injection means reduce hardware costs. We denote combinational functions like clock glitches, electromagnetic pulses, or laser fault these intermediate results. Consequently, the register transition injections. In [13], Brockmann et al. propose a unified fault functions δr can be expressed as a composition of these j injection model that describes fault effects in the microarchi- intermediate combinational functions. tecture. The authors represent the synchronous digital circuit C. Yosys Framework as a directed graph (V, E) composed of vertices V and edges E. Vertices V represent logic gates, state-holding elements, Yosys [12] is an open-source synthesis tool with a compiler- inputs, and outputs in the circuit, while edges E represent like infrastructure. Its frontend takes as input a design de- circuit wires connecting two vertices and carrying a digital scription using a hardware description language like Verilog. value. Each vertex representing a logic gate in the graph The Yosys intermediate language, called RTLIL, is a netlist is associated with a Boolean function describing the gate composed of gates and wires. The backend converts the RTLIL behavior. By definition, a fault occurs in the circuit when design into various outputs ranging from technological targets a given logic gate is not evaluated with its correct Boolean like FPGA or ASIC to formal languages. function. In particular, Yosys can transform a hardware design de- Microarchitectural faults in the graph are parametrized with scription into a hardware transition system. Supported for- the three following attributes: location, effect, and number. mal languages are AIGER, SMV, BTOR2 and SMT-LIB. The location lists the vertices v ∈ V targeted by the fault AIGER [15] describes hardware systems at the bit level using injection. The effect specifies the fault effect by associating a an and-inverter graph. The SMV language [16] is provided faulty Boolean function with the targeted vertices. Finally, the by the symbolic model checker NUXMV [17] and describes number describes the maximum number of vertices simulta- finite and infinite transition systems. NUXMV lifts the verifi- neously affected by a fault. cation from the bit level to the word level with data types like bit vectors or memories. BTOR2 [18] is a word-level B. Transition System for Sequential Hardware Circuits generalization of AIGER and provides word-level data types, We model sequential hardware circuit [14, §2.1.2] as a registers, and memories. Finally, the SMT-LIB language [19] transition system M = (S, S0, X, T ) where: is the standard specification to describe SMT problems and is broadly supported by SMT solvers. SMT-LIB can also • S is the set of circuit states, specify hardware transition systems using the quantifier-free • S0 ⊆ S is the set of initial states, bit-vector theory. Yosys can produce VCD waveform traces of • X is the set of circuit inputs, the successive hardware states from model-checker outputs. • T : S × X → S is the transition function of the circuit. Finally, Yosys has built-in options to simulate the design A system state s ∈ S corresponds to a valuation of state- and set the register’s initial values. These functionalities allow holding elements (e.g., microarchitectural registers, memories) a user to configure the initial state of the circuit before in the hardware design. Assuming there are n state-holding converting it into a hardware transition system M. elements, denoted as registers in the following, the state s can be seen as a vector of the n register values s := ⟨r1,..., rn⟩. III. FAULTY SYSTEM MODELING An initial state s0 ∈ S0 is a system state where each Hardware analysis often relies on equivalence-checking register rj,1≤j≤n is evaluated with its initial values. Initial techniques [4], [20] to capture faults that induce a different states can be determined according to register reset values, for circuit behavior compared to a reference model. But these

                                 102

methods can only classify fault effects at the circuit level
and cannot determine whether the faults have consequences on                                           e ∈ E              :                   δr (s) → δe (s)
                                                                                                                                j          r
the running software. To analyze the consequences of a fault                                           reset              : δ      (s) →   j
                                                                                                                               r     0x00
described at the microarchitectural level on the software, we                                          set                : δ   j
                                                                                                                               r (s) → 0xff
need to observe its propagation in the system. For this purpose,                                       flips              : δ   j
in the following, we perform model checking to capture the                                                                : δ  r (s) → ¬δ
successive system states between the fault injection and the                                           fliplsb                 rjj (s) → δrjr(s)j (s)⊕ 0x01
fault manifestation. This section defines a faulty transition                                              The number of fault injections  N restricts the possibilities

system comprising the program, the hardware, and the attacker offered by the fault model (L, T , E ). An attacker can use at model. most N faulty transitions δre to compute the next system states. A. Bringing the Software and the Hardware Together The attacker’s goal φ is a reachability property defined on the transition system M. It represents a vulnerability that the The hardware processor design is modeled as a transition attacker wants to reach in order to create an exploit on the system M = (S, S0, X, T ), as introduced in Section II. The system by injecting faults. In the system’s normal operation, software program is the sequence of instructions to be executed such an exploit should not exist. In other words, ¬φ is a on the processor. The program is encoded in the initial state system’s invariant that the attacker wants to break. of a memory modeled simultaneously with the processor. Let us illustrate some practical instantiations of the attacker Accordingly, the initial state S0 of the system restricts the model we defined. Laser fault injections are accurate in space possible processor executions to the software program under and time and can be modeled with only one or two bit-flip. study. The input set X of the system does not represent the On the other hand, voltage or clock glitches are less accurate program as it is already encoded in the transition system. and can affect the whole design. We may model them with Instead, system inputs are used to model the fault injections multiple bit-set and bit-reset. applied during the processor operation. The attacker model and the faulty transition system are introduced in the following of C. Faulty Hardware Transition System this section. The faulty transition system MF = (S, S0, X, T ) results B. Attacker Model from the modification of the hardware and software transition We define an attacker model which specifies how the system M and the attacker model ((L, T , E ), N, φ). First, a attacker can perturb the system operation. This model re- new variable cnt ∈ [[0, N ]] is added in the system model to lies on the definition of microarchitectural faults introduced encode the maximum number of fault injections N . The cnt in Section II-A and extends this definition to describe the is incremented each time a faulty transition is applied and attacker’s capabilities on a hardware transition system. The cannot be targeted by the fault model, i.e., cnt ∈ L/ . Then, for attacker model comprises i) the attacker’s goal expressed as each targeted register rl in L, we add a new input xl to the a reachability property φ, ii) the number of faults N that the system to control the fault injection. The input xl determines attacker can inject into the system, and iii) the fault model. whether a fault is injected in register rl, and hence, if the value The fault model is parametrized by the triplet (L, T , E ) and of register rl in the next state should be computed using the describes the possible modifications that a fault may induce normal transition function δrₗ or the faulty transition δreₗ . on the system. • L is the set of possible locations of the fault, rl′ = δδreₗ (s) if xl = False • T is the timing range of the fault injection, rl (s) if xl = True • E is the set of possible effects of the fault. A possible extension of this faulty transition system is to The fault location L is a set that denotes the registers expose intermediate combinational functions often used in targeted by the fault injection, i.e., L ⊆ {r1,..., rn}. hardware circuits, as introduced in Section II. We can then ex- The timing range T ⊂ N of the fault is a set of non-negative tend our fault model and the resulting faulty transition system integers that specifies when the fault injection can occur in the to target these combinational functions with fault injection. system. For example, a fault can be injected in the transition This extension is not formalized here but is implemented in system between states si and si+1 if i ∈ T . the μARCHIFI tool. The fault effect E ⊂ {set, reset , flips, . . . } is a set of functions that modifies how a register is updated in the next IV. TRANSITION SYSTEM VERIFICATION state. For instance, a fault e ∈ E injected in register rj consists in replacing the transition function δr with the faulty This section introduces verification techniques on a faulty transition δe within the same domain, i.e., it produces the same output data type. A non-exhaustive list of possible effectsrʲ j transition system. In addition, we describe how the knowledge of the running software can be leveraged to refine the transition is given below for an 8-bit register: system verification.

                                                                      103

A. Verification Problem Statement                                        Algorithm 1: Bounded model checking (BMC) with
              In Section III, we model the system under attack as a      concretization
transition system MF    = (S, S0, X, T ). The set of initial states         Input: transition system M = (S, S₀, X, T ), reachability
S0 describes the possible software execution path to analyze,                     property φ, BMC bound k, concretization depth m,
and the inputs X       control the possibilities of the attacker to         Output:number of concretizations L
inject faults in the system. The verification problem is then a                    a path π if a φ is reachable, None otherwise

reachability property verification where an attacker wants to 1 Function BMC_Concretizing(M, φ, k, m, L) is find a sequence of states (s0, s1,..., sk) ∈ Sk+1 such that: // BMC() checks the reachability of φ up to • s0 is an initial state, i.e., s0 ∈ S0, the bound. M, φ, ϕ, i are global variables. 2 Function BMC(bound) is • transition between states si and si+1 is valid, i.e., it exists 3 while i < bound do an input xi ∈ X such that si+1 = T (si, xi), 4 if ϕ ∧ φ(si) is SAT then • the number of faults injected in the system does not 5 exit( π := (s₀, ..., si)) exceed the attacker capacity, i.e., cnt ≤ N and, 6 i ← i + 1 • φ(sk) is true. 7 end ϕ ← ϕ ∧ (si = T (si−1, xi−1)) // Unrolling 8 Such a path in the transition system allows an attacker to 9 end identify an instance of the fault model and a software execution trace that verifies the property φ. // Initial BMC verification up to step m Different strategies exist to iterate over the transition 10 ϕ ← S₀(s₀) ; i ← 0 model to verify the property. Unbounded verification tech- 11 BMC(m) // Concretization loop niques [21]–[24] prove the property in the general case, 12 ψ ← ϕ ; setPC ← ∅ ; iter ← 1 but the data dependency and the transient nature of faults 13 incomplete enum ← False make these techniques ill-suited [25] on the fault injection 14 while ψ is SAT do problem. Bounded verification techniques like Bounded Model 15 address ← get_model(ψ)(PC ) Checking (BMC) [26], [27] prove the property from an initial 16 setPC ← setPC ∪ address 17 ψ ← ψ ∧ (PC = address) state for a limited number of transitions, fixed a priori with 18 if iter = L then a bound. This bound is typically set according to the length 19 incomplete enum ← True; Break of execution trace of the analyzed software. In this work, we 20 end iter ← iter + 1 rely on bounded verification techniques to address the fault 21 verification problem. // Parallel BMC verifications for each The remainder of this section introduces software-related concretized path up to bound k 22 for address ∈ setPC do considerations for applying well-known optimization tech- 23 ϕ ← ϕ ∧ (P C = address) niques to speed up our BMC verification. 24 end BMC(k)// run BMC on ϕ (concretized paths) 25 B. Sandboxing Execution Paths 26 if incomplete enum then ϕ ← ϕ ∧ (P C / Sandboxing is a general technique that adds a global con- 27 ∈ setPC) straint on the model to reduce the problem’s state space. We 28 BMC(k) // run BMC on ϕ (remaining paths) apply sandboxing to restrict the Program Counter (PC) to a 29 end range of values that a simple static analysis can retrieve from the addresses in the binary, e.g., using objdump-like tool. The C. Concretizing Execution Paths verification framework then stops exploring software execution paths that do not satisfy this sandboxing constraint. Conse- BMC algorithms [27] typically unroll the transition system quently, the BMC procedure can also terminate faster when in a formula ϕ to check the reachability of a property φ. As the entire state space has been explored. However, adding such a result, solving the formula ϕ suffers from the increasing a global constraint on the model may lose the k-completeness number of variables and clauses. of the bounded verification procedure. This technique must We apply the general concretizing technique to split ϕ into therefore be used to explore possible vulnerabilities rather than sub-formulas encoding the different software execution paths. prove the system’s robustness. Like sandboxing, we rely on the PC to distinguish between While only one PC exists at the software level, several these different execution paths. However, a given PC value microarchitectural registers store its value in the processor de- can refer to several microarchitectural contexts if more than sign. The fetch stage PC speculates on the next addresses to be one execution path can reach this address at the same time. read from memory. Applying the sandboxing technique on this This aspect is discussed at the end of this section. register would thus require relaxing the sandboxing constraint. The concretization procedure is detailed in Algorithm 1. The execute stage PC misses unconditional branches that are After initializing the formula ϕ with an initial state s0 and resolved directly in the decode stage. We therefore implement performing BMC up to bound m (lines 10-11), a concretization sandboxing by constraining the PC of the decode stage of in- loop enumerates the possible values for the PC (lines 12-21). order processors, as presented later in Section VI. This loop successively asks an SMT solver to give models

    104

-  Sandboxing
-  Concretization




    Fig. 1: μARCHIFI architecture and verification tool-chain.

of the system with different PC values. It stops when no set the initial state of the hardware right before the instruction more system model exists, i.e., ψ becomes unsatisfiable, or sequence to analyze formally. Then, the user needs to spec- after a given number of concretizations L (lines 18-19). A ify the attacker model comprising the goal φ, the maximal new BMC procedure is performed for each enumerated PC number of faults N , and the fault model (location, timing, value until bound k (lines 22-25). When the PC enumeration and fault effects). This model is automatically integrated into is incomplete, the remaining paths are encoded within a the system through the FaultRTLIL pass. The attacker’s single formula and checked together (lines 26-28). A program goal can also be specified into the hardware design using analysis can identify branches’ locations in the program and the SystemVerilog Assertion subset supported by Yosys. Fi- determine the optimal depth m the user should perform the nally, the μARCHIFI tool produces a transition system, as concretization. introduced in Section III-B, in SMT-LIB or BTOR2 format. D. Discussion The faulty transition system can be verified using external model-checking tools compatible with these input formats, like Both the sandboxing or the concretization techniques reduce AVR [25], PONO [28] or BTORMC [18]. the state space to explore by adding terms and clauses to When an external model checker finds a counterexample, as the formula encoding the problem. However, this general illustrated in the verification box in Fig. 1, a VCD file reports approach has some limitations. To speed up verification, a precisely where the fault is injected and when the attacker’s trade-off must be found between eliminating execution paths goal is reached. However, understanding the propagation of and the number of additional state variables that increase faults and their consequences requires human expertise, but the complexity of the formula to check. For example, we this task can be facilitated by external tools that perform might want to add constraints ensuring that injected faults differential traces comparison against a reference model. lead to a different system behavior than the fault-free reference Additional global constraints for the sandboxing technique model. This technique allows to focus on analyzing effective can be specified to the model checker or can be directly faults while ineffective ones are ignored. However, it requires included in the input Verilog design parsed by Yosys. The capturing the complete microarchitectural state twice, leading concretization technique requires an external model checker to to an excessively complex system encoding formula. The enumerate possible execution paths and is thus not integrated verification times thus increase. into the μARCHIFI tool. V. TOOL IMPLEMENTATION B. μARCHIFI Architecture This section introduces the μARCHIFI tool we developed to Fig. 1, in the modeling box, illustrates the integration generate a formal transition system from a hardware descrip- of the μARCHIFI tool with the Yosys framework. Yosys tion, a program, and an attacker model. First, we detail how a can parse and translate a hardware specification into formal user can use the tool, then we give its implementation details. languages, allowing us to focus on the automated integration A. μARCHIFI Usage of an attacker model into the system. We work on the RTLIL intermediate representation of Yosys to get the best μARCHIFI, illustrated in Fig. 1, takes as input a processor expressivity and exhaustiveness to specify the fault model. hardware description in Verilog, a binary software program, Besides, as the Yosys RTLIL translation preserves all signal and an attacker model comprising the fault model. First, and register names from the Verilog processor design, the user the user can simulate the execution of the target program, can accurately select fault locations based on name pattern compiled for the corresponding ISA, on the hardware design to matching, cell type, or cell-width filtering. In addition, the

105

                                       TABLE I: Use Cases description and expected verification result.
                          Hardware Design                 Software Program                             Attacker Model                                  BMC Results
                   Name     Logic Gates  Flip-Flops   Name            gcc Flag  Attacker goal φ       Location                    Timing  Effect   N   k    Reachability
    Use Case I     CV32E40P     2842   179            VerifyPIN V7       Og   Bypass authentication   Flip-Flops in Control path  60:75  Symbolic  1   75   φ reachable
    Use Case II    Secure Ibex  4422   211            VerifyPIN V1       Os   Bypass authentication   Flip-Flops in Lockstep        *    Symbolic  5   46  φ unreachable
    Use Case III   Ibex         1983   114            KeySchedule (AES)  Os   Set expanded key to 0   Combinational in EX Stage     *     Reset    2   38  φ unreachable

preservation of names facilitates the generation of compre-                     Use Case I, we target VerifyPIN v7 with the most software
hensive counterexamples.                                                        countermeasures. It implements hardened booleans, constant

Our work extends the Yosys tool by proposing a iteration, loop counter check, inline PIN comparison, and FaultRTLIL translation pass, illustrated in Fig. 1, that takes duplication of critical tests. VerifyPIN V7 is compiled with the the attacker’s model (L, T , E ), N, φ in input and integrates it optimization flag Og to prevent the compiler from removing into the system. This integration is achieved in several steps. the countermeasure. The program runs in constant time, in 69 First, a new RTLIL register is created to encode the maximum clock cycles. number of fault injections N the attacker can inject into the Hardware. We execute the program on the 32-bit, in-order, system. Then, a clock is added to control the timing range 4-stage pipeline CV32E40P RISC-V core from the OpenHW of the fault injection T . Finally, additional logic functions are group [30]. The version under study does not provide any inserted into the intermediate representation for each location security countermeasures. l ∈ L potentially targeted by a fault injection, modeling Attacker Model. In this system, the attacker aims to bypass the possible fault effects E . The targeted elements are then the secure authentication mechanism without triggering the replaced by an if-then-else structure controlled by a fault software countermeasures. selector. Fault selectors are exposed as system inputs and φI := (authenticated ∧ ¬software alert) indicate whether the fault should be injected or not. The maximum counter value N and the clock for fault injection The VerifyPIN V7 program implements the authentication timing T , introduced previously, are used to constrain the fault process in two steps. First, a constant-time loop sets a Boolean selectors. to True if a difference is detected between the two PINs. VI. EVALUATION Second, a comparison is performed to test the Boolean value and allow the authentication. We evaluate the robustness of the This section illustrates the use of μARCHIFI in three case second comparison block against a single fault injected on the studies, applies the verification strategies introduced in Sec- sequential logic of the processor control path. The considered tion IV, and discusses the tool’s limitations. The μARCHIFI fault model targets 102 registers among 179 in the processor. implementation, the case studies, and the experimental results Use Case I is summarized in Table I. are publicly available2. Verification Results. Table II compares verification per- All verifications have been executed on an 11th Gen Intel(R) formance between three model checkers with and without Core(TM) i7-1185G7 CPU platform. Every program presented faults. Performing the verification without fault ensures that in this section is compiled with the RISC-V toolchain for the attacker goal φ does not hold outside of an attack. The the RV32IMC architecture (gcc version 10.2.0). For each analysis results in Table I highlight that the attacker can bypass verification, the BMC bound k is fixed according to the longest the authentication by injecting a single fault. Counterexamples program execution trace plus a 10-percent increment to capture provided by the model checkers permit the user to find the possible modifications in the control flow. exact location of the fault that leads to the vulnerability φI. A. Use Case I: Robust Software All solvers found the same fault model on this use case, but we can observe that PONO is faster to solve the model-checking Use Case I illustrates the possibility for a user to analyze problem. the robustness of a secure program running on a processor. B. Use Case II: Robust Hardware Software. We consider a memcmp-like authentication mech- anism from the FISSC benchmark suite [29]. This collection Use Case II details how a user can determine whether a provides eight versions of the VerifyPIN program embed- fault injected into a secure processor can induce a vulnera- ding software countermeasures against fault injections. The ble behavior on the software without being detected by the VerifyPIN program compares two 3-digit3 PIN codes stored hardware countermeasure. in memory: a user and a secret PIN. The user can authen- Software. We consider VerifyPIN V1, the baseline version ticate when the two codes are identical. In the following, of the VerifyPIN collection, without any countermeasure. As in PIN values are symbolic, but we assume that the user PIN Use Case I, the same constraint is applied to user- and secret- and the secret PIN are different in each of their digits. In PIN, which are still symbolic. VerifyPIN V1 is compiled with the optimization flag Os. 2https://doi.org/10.5281/zenodo.7958412 Hardware. The Ibex [31] is a parametrizable open-source 3VerifyPIN uses 4-digit PINs in its original version. 32-bit, in-order processor. We analyze the small version of the

                                                                                106

core [32] in its secure configuration. The Secure Ibex imple-          TABLE II: Use-cases verification time with three model checkers.
ments protections against physical attacks like the redundancy-                               Without Fault               With Faults
based Lockstep mechanism that instantiates the core twice                              PONO  YOSYS-BMC     BTORMC   PONO  YOSYS-BMC               BTORMC
and compares the outputs. The duplicated core is called the             Use Case I     12.6s   11.1s        1.5s    107s               249s        273s
Shadow Core and an alert signal is triggered if an attack has           Use Case II    20.7s   10.6s        3.5s    250s               373s      timeout
been detected during the operation of the processor.                    Use Case III    0.3s    2.4s        0.1s    313s              1945s       3427s

Attacker Model. In this second use case, the attacker still TABLE III: Verification time improvement with the sandboxing aims to bypass the secure authentication mechanism without technique wrt. the baseline verification time with faults in Table II. triggering the hardware countermeasures. PC Sandboxing PONO YOSYS-BMC BTORMC φII := (authenticated ∧ ¬hardware alert ) Use Case I 0x1c4 ≤ PC ≤ 0x234 110s ( +2.8%) 242s ( -2.8%) 205s (-24.9%) Use Case II 0x84 ≤ PC ≤ 0x114 206s (-17.6%) 297s (-20.4%) timeout The considered attacker model cannot inject more than five Use Case III 0x40 ≤ PC ≤ 0xc0 107s (-65.8%) 1454s (-25.2%) 1659s (-52.0%) faults into the system. Fault Locations are limited to the sequential logic in the Shadow core since we do not want TABLE IV: Verification time improvement with the concretization to inject the same fault in both cores. technique wrt. the baseline verification time with faults from Table II. Verification Results. Table I reports that an attacker cannot Concretization bypass the secure authentication with the considered fault Concretized step Baseline Parallelized Accumulated model. This use case leverages the fact that the Secure Ibex Use Case I 62 (Status comparison) 249s 189s (-24.1%) 509s (+104%) implements hardware countermeasures. On the one hand, Use Case II 31 (PIN comparison) 373s 304s (-18.5%) 891s (+139%) assuming that the hardware alert cannot be triggered makes Use Case III 23 (No branch instruction) 1945s 1504s (-22.7%) 2955s ( +51%) sense as the attacker wants to bypass the authentication without being detected. On the other hand, it helps the solver D. Influences of Verification Strategies simplify the formula during the verification. Table II reports verification performance. BTORMC fails to solve the problem, Sandboxing Execution Paths. For each use case introduced and we stop the verification after 2 hours. before, we determine the range of possible values for the program counter (PC) by dumping addresses from the binary C. Use Case III: Cryptographic Software file. Here, the possible addresses are contiguous, and we add a Use Case III details how a user can apply the tool to global constraint on the system to force the PC to stay in this software implementations of cryptographic algorithms. set of values. Table III illustrates that the sandboxing strategy Software. Tiny AES [33] is a small software implementation results in an improvement of the performances up to 65%, of the encryption algorithm. The key schedule function of and these additional constraints do not prevent model checkers the AES program expands the key into several separate keys from retrieving the vulnerability highlighted in Use Case I for each round of AES. We focus here on a round of the Such improvements are due to two factors. First, some fault key schedule function from the 128-bit AES. The program is effects are not analyzed if they lead to PC values out of compiled with the optimization flag Os. the memory range considered. Secondly, the verification may Hardware. We run the key schedule function on the baseline end before the bound k if all execution paths in the system version of the small Ibex core without any countermeasure. exit from the considered address range. We also observe that Attacker Model. The attacker wants to set to zero a byte improvements vary between the different solvers even if PONO in the penultimate round key. An attacker can then use the remains more efficient on the use cases analyzed. observation of such an effect to perform differential fault Concretizing Execution Paths. We apply the concretization analysis [34], [35]. Fault consequences are observed at the strategy for each use case with an enumeration bound L = 3 end of the key schedule function to limit the analysis to a to split the bounded verification procedure into L + 1 sub- small sequence of instruction. verifications (c.f., Algorithm 1). We arbitrarily set L = 3 as it φIII := (9 th Round keybyte = 0) provides the best performance in these practical use cases. A higher value of L increases the accumulated verification time To attempt to reach the property φIII, we allow an attacker without improving the parallelized time. to inject up to two word-reset faults anywhere in the execute Table IV reports the concretization steps, the baseline verifi- stage of the Ibex. cation time from Table II, and the concretization performance. Verification Results. As reported in Table I, an attacker can- We show each experiment’s wall-clock time and accumulated not reach his goal with the considered fault model. Additional verification time since we can parallelize the executions. Per- verification not described here shows that a more powerful formance is given for the YOSYS-BMC since other evaluated attacker reaches his goal with four fault injections instead of model checkers do not permit to retrieve the SMT formula two. We can also note that the verification of φIII on the AES encoding the unrolled system. program without fault is faster than both Use Case I and II On Use Case I, we concretize the execution at the first because the AES key is fixed for while the two 3-digit PINs branching instruction targeted by fault injection. It corresponds are symbolic for the VerifyPIN program. to the PIN-status comparison to allow authentication (step 62).

107

This results in an improvement of the verification time by 24%. address the binary or the Instruction Set Architecture level On Use Case II, we apply concretization during a PIN-digit and propose methodologies to analyze the robustness of the comparison and enumerate PC values associated to different software programs. SAMVA [40] assesses a binary program execution paths. However, few performance improvements are against multiple instruction-skip attacks with static analysis. observed, especially regarding the accumulated verification The proposed method by Ducousso et al. [7] permits scaling on time. We believe this is due to the hardware countermeasure large programs like bootloader with up to 10 fault injections. that already prevents executing different paths due to the faults. However, these works do not consider the execution platform, No branching instruction exists on Use Case III. However, and the generic fault models used are sometimes inadequate many execution paths are possible due to fault injections. to model microarchitectural implementation details. Concretization is applied at step 23, at half of the verification Furthermore, commercial tools offer all the building blocks time. This results in a 22.7% verification time improvement. required for such a fault injection analysis, but their closed In conclusion, concretization often improves the verification nature prevents users from integrating them into the same time thanks to the parallelization of the executions. However, verification framework. SystemVerilog Assertion (SVA), sup- these verification times remain higher than the one obtained ported by tools such as Synopsys VC Formal or Siemens when using the PONO model checker (Table II). QuestaVerify, could define the attacker’s goal, but is not VII. RELATED WORK suitable for fault modeling. On the other hand, tools such as Cadence JasperGold offer support for fault injection but do Similar works propose modeling and verification method- not consider software. In short, none of these tools address the ologies to study fault injection effects. Classical verification verification of software and hardware against fault injection. methods like simulation are used [3], [6], [36], [37], but they Finally, apart from fault injection, some works [41], [42] are often not exhaustive, and it is often difficult to highlight tackle the problem of hardware-software co-verification using corner cases, like the Prefetch Buffer introduced in Section I. BMC verification. Schmidt et al. [42] propose to separate the For instance, VERFI [3] needs to set a fixed input test vector control path and the computation in the modeling to cope with to evaluate cryptographic implementation robustness to faults. system complexity. However, this compositional approach is In the following, we will discuss papers that propose a formal undermined when the underlying hardware is corrupted by framework to analyze fault effects on the system. fault injection since data and control are then both impacted. First, some works analyze fault effects on hardware imple- VIII. C mentation [2], [4], [20]. Formal techniques were first dedicated ONCLUSION to analyzing cryptographic circuits with equivalence checking. In this paper, we propose a faulty transition system to AutoFAULT tool [2] can parse and transform a small block model the hardware implementation of a processor and the cipher written in VHDL into a SAT formula to determine if software program conjointly. This modeling allows to formally a fault can induce a wrong ciphertext. The FIVER tool [4] analyze and study the propagation of faults in the microarchi- translates Verilog netlists to Binary Decision Diagram to tecture and their consequences on the system behavior. The compare a fault-free circuit with a faulty copy to determine μARCHIFI tool automatically implements this model, from the fault effects. FIVER symbolically checks every possible the hardware design description at the RTL level, in Verilog, input and classifies fault effects according to the expected a binary program, and a specification of the attacker model. reference behavior. Faults are classified as effective, ineffective, μARCHIFI allows to specify a large variety of microarchitec- or detected, depending on whether they induce a different tural fault models with high expressiveness. We illustrate the behavior and if the countermeasure (if any) detects them. use of μARCHIFI on three use cases encompassing complete SYNFI [20] can parse technological netlists to prove the microarchitectural designs of RISC-V processors representa- equivalence between golden and faulty circuits to detect if tive of the embedded market and binary programs of hundreds the synthesis step removes countermeasures. However, SYNFI of machine instructions. We discuss possible strategies to does not handle sequential verification since the design to improve the verification performance. At this stage, the user analyze is unrolled to perform equivalence checking, and thus, of μARCHIFI must find a sweet spot between the size of the tool cannot analyze software. In comparison, μARCHIFI the hardware design, the size of the analyzed program, and does not support advanced technological netlists, but we still the complexity of the fault model. Future work will focus on support any Verilog or SystemVerilog design by plugging combining several verification strategies leveraging software, our translation pass into the Yosys tool. In addition, we such as sandboxing and concretization techniques, but also take advantage of a simplified word-level netlist to bridge robust hardware embedding countermeasures to analyze fault the gap with the software and facilitate the analysis of the injections on a larger scale. transitional system. We also keep the sequential logic instead of unrolling and flattening the whole design to use model- checking verification techniques. On the other hand, some additional works model and study faults at the software level and analyze fault effects on the control flow [5], [7], [38]–[40]. These approaches

108

      REFERENCES                                                              [25]  A. Goel and K. Sakallah, “AVR: Abstractly Verifying Reachability,”
                                                                                    in     Tools and Algorithms for the Construction and Analysis of Systems,

[1] B. Yuce, P. Schaumont, and M. Witteman, “Fault Attacks on Secure Em- A. Biere and D. Parker, Eds., 2020. bedded Software: Threats, Design and Evaluation,” Journal of Hardware [26] E. Clarke, A. Biere, R. Raimi, and Y. Zhu, “Bounded Model Checking and Systems Security, Jun. 2018. Using Satisfiability Solving,” Formal Methods in System Design, 2001. [2] J. Burchard, M. Gay, A.-S. M. Ekossono, J. Hor´aˇcek, B. Becker, [27] E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Eds., Handbook T. Schubert, M. Kreuzer, and I. Polian, “AutoFault: Towards Automatic of Model Checking. Springer International Publishing, 2018. Construction of Algebraic Fault Attacks,” in 2017 Workshop on Fault [28] M. Mann, A. Irfan, F. Lonsing, Y. Yang, H. Zhang, K. Brown, A. Gupta, Diagnosis and Tolerance in Cryptography (FDTC), 2017. and C. Barrett, “Pono: A Flexible and Extensible SMT-Based Model [3] V. Arribas, F. Wegener, A. Moradi, and S. Nikova, “Cryptographic Checker,” in Computer Aided Verification, 2021, pp. 461–474. Fault Diagnosis using VerFI,” in 2020 IEEE International Symposium [29] L. Dureuil, G. Petiot, M.-L. Potet, T.-H. Le, A. Crohen, and P. de on Hardware Oriented Security and Trust (HOST), Dec. 2020. Choudens, “FISSC: A Fault Injection and Simulation Secure Collection,” [4] J. Richter-Brockmann, A. Rezaei Shahmirzadi, P. Sasdrich, A. Moradi, in Computer Safety, Reliability, and Security, 2016. and T. G¨uneysu, “FIVER – Robust Verification of Countermeasures [30] OpenHW group, “OpenHW Group CV32E40P User Manual,” https:// against Fault Injections,” IACR Transactions on Cryptographic Hard- cv32e40p.readthedocs.io/en/latest/. ware and Embedded Systems, Aug. 2021. [31] LowRISC, “Ibex: An embedded 32 bit RISC-V CPU core,” https: [5] M.-L. Potet, L. Mounier, M. Puys, and L. Dureuil, “Lazart: A Symbolic //ibex-core.readthedocs.io/en/latest/. Approach for Evaluation the Robustness of Secured Codes against [32] “Ibex RISC-V Core github repository,” https://github.com/lowRISC/ Control Flow Injections,” in Verification and Validation 2014 IEEE ibex#configuration. Seventh International Conference on Software Testing, Mar. 2014. [33] kokke, “Tiny AES,” https://github.com/kokke/tiny-AES-c, 2019. [6] M. Hoffmann, F. Schellenberg, and C. Paar, “ARMORY: Fully Auto- [34] J. Takahashi, T. Fukunaga, and K. Yamakoshi, “DFA Mechanism on the mated and Exhaustive Fault Simulation on ARM-M Binaries,” IEEE AES Key Schedule,” in Workshop on Fault Diagnosis and Tolerance in Transactions on Information Forensics and Security, vol. 16, 2021. Cryptography (FDTC 2007). Vienna, Austria: IEEE, Sep. 2007. [7] S. Ducousso, S. Bardin, and M.-L. Potet, “Adversarial Reachability [35] S. S. Ali and D. Mukhopadhyay, “A Differential Fault Analysis on AES for Program-level Security Analysis,” in 32nd European Symposium on Key Schedule Using Single Fault,” in 2011 Workshop on Fault Diagnosis Programming (ESOP), 2023, pp. 59–89. and Tolerance in Cryptography, Sep. 2011. [8] J. Laurent, C. Deleuze, F. Pebay-Peyroula, and V. Beroulle, “Bridging [36] J. Grycel and P. Schaumont, “SimpliFI: Hardware Simulation of Em- the Gap between RTL and Software Fault Injection,” ACM Journal on bedded Software Fault Attacks,” Cryptography, vol. 5, no. 2, Jun. 2021. Emerging Technologies in Computing Systems, vol. 17, no. 3, May 2021. [37] T. Given-Wilson, N. Jafri, and A. Legay, “Combined software and [9] B. Yuce, N. F. Ghalaty, H. Santapuri, C. Deshpande, C. Patrick, and hardware fault injection vulnerability detection,” Innovations in Systems P. Schaumont, “Software Fault Resistance is Futile: Effective Single- [38] and Software Engineering, vol. 16, no. 2, Jun. 2020. Glitch Attacks,” in 2016 Workshop on Fault Diagnosis and Tolerance K. Pattabiraman, N. Nakka, Z. Kalbarczyk, and R. Iyer, “SymPLFIED: in Cryptography (FDTC), Aug. 2016. Symbolic program-level fault injection and error detection framework,” [10] S. Tollec, M. Asavoae, D. Courouss´e, K. Heydemann, and M. Jan, “Ex- in 2008 IEEE International Conference on Dependable Systems and ploration of Fault Effects on Formal RISC-V Microarchitecture Models,” [39] Networks With FTCS and DCC (DSN), Jun. 2008. in 2022 Workshop on Fault Detection and Tolerance in Cryptography J.-B. Br´ejon, K. Heydemann, E. Encrenaz, Q. Meunier, and S.-T. Vu, (FDTC), Sep. 2022. “Fault attack vulnerability assessment of binary code,” in Proceedings [11] J. Laurent, V. Beroulle, C. Deleuze, and F. Pebay-Peyroula, “Fault of the Sixth Workshop on Cryptography and Security in Computing Injection on Hidden Registers in a RISC-V Rocket Processor and [40] Systems. Valencia Spain: ACM, Jan. 2019. Software Countermeasures,” in 2019 Design, Automation & Test in A. Gicquel, D. Hardy, K. Heydemann, and E. Rohou, “SAMVA: Static Europe Conference & Exhibition (DATE), 2019. Analysis for Multi-fault Attack Paths Determination,” in Constructive [12] C. X. Wolf, “Yosys open synthesis suite,” [41] Side-Channel Analysis and Secure Design (COSADE), 2023, pp. 3–22. https://github.com/YosysHQ/yosys, 2016. D. Groβe, U. K¨uhne, and R. Drechsler, “HW/SW co-verification of [13] J. Richter-Brockmann, P. Sasdrich, and T. Guneysu, “Revisiting Fault embedded systems using bounded model checking,” in Proceedings Adversary Models – Hardware Faults in Theory and Practice,” IEEE of the 16th ACM Great Lakes Symposium on VLSI - GLSVLSI ’06. Transactions on Computers, 2022. [42] Philadelphia, PA, USA: ACM Press, 2006. [14] C. Baier and J.-P. Katoen, Principles of Model Checking. MIT Press, B. Schmidt, C. Villarraga, T. Fehmel, J. Bormann, M. Wedler, Apr. 2008. M. Nguyen, D. Stoffel, and W. Kunz, “A New Formal Verification [15] A. Biere, K. Heljanko, and S. Wieringa, “AIGER 1.9 and beyond,” 2011. Approach for Hardware-dependent Embedded System Software,” IPSJ Transactions on System LSI Design Methodology, pp. 135–145, 2013. [16] A. Irfan, A. Cimatti, A. Griggio, M. Roveri, and R. Sebastiani, “Ver- ilog2SMV: A Tool for Word-level Verification,” in Proceedings of the 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016. [17] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta, “The nuXmv Symbolic Model Checker,” in Computer Aided Verification, 2014. [18] A. Niemetz, M. Preiner, C. Wolf, and A. Biere, “Btor2 , BtorMC and Boolector 3.0,” in Computer Aided Verification, 2018. [19] C. Barrett, P. Fontaine, and A. Stump, “The SMT-LIB Standard,” 2010. [20] P. Nasahl, M. Osorio, P. Vogel, M. Schaffner, T. Trippel, D. Rizzo, and S. Mangard, “SYNFI: Pre-Silicon Fault Analysis of an Open-Source Secure Element,” May 2022. [21] M. Sheeran, S. Singh, and G. St˚almarck, “Checking Safety Properties Using Induction and a SAT-Solver,” in Formal Methods in Computer- Aided Design, 2000, pp. 127–144. [22] K. L. McMillan, “Interpolation and SAT-Based Model Checking,” in Computer Aided Verification, vol. 2725. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003. [23] A. R. Bradley, “SAT-Based Model Checking without Unrolling,” in Verification, Model Checking, and Abstract Interpretation, 2011. [24] N. Een, A. Mishchenko, and R. Brayton, “Efficient implementation of property directed reachability,” in 2011 Formal Methods in Computer- Aided Design (FMCAD), Oct. 2011.

  109