# Modular and automatic formal verification of a RISC-V processor with security mechanisms

Cyprien Jules, Pierre Wilke, Guillaume Hiet

► To cite this version:

Cyprien Jules, Pierre Wilke, Guillaume Hiet. Modular and automatic formal verification of a RISC-V processor with security mechanisms. 2026. hal-05472602

HAL Id: hal-05472602

https://hal.science/hal-05472602v1

Preprint submitted on 22 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Modular and automatic formal verification of a RISC-V processor with security mechanisms

Cyprien Jules, Pierre Wilke, Guillaume Hiet

CentraleSupélec, Inria, CNRS, Univ. Rennes

France

firstname.lastname@centralesupelec.fr

## Abstract

The security of computer systems eventually relies on the security of the underlying hardware and on the security mechanisms that it offers. We extend a simple RISC-V processor written in the Kôika Hardware Description Language (HDL) with security mechanisms, and prove that these mechanisms are correct.

We do so by compiling Kôika circuits into a representation well-suited for automated theorem provers. We strive to make our proofs modular, i.e., function by function or rule by rule.

**Keywords** formal verification, hardware description languages, hardware security mechanisms.

## 1 Introduction

Critical systems require high confidence in all the system stack, from the software to the hardware. In particular, we are interested in formal verification of hardware security mechanisms. To that end, we are using the Kôika Hardware Description Language (HDL), embedded in the Rocq proof assistant.

In previous work, we extended a RISC-V processor [2] written in Kôika with a hardware shadow stack [1] to prevent attacks against control-flow integrity. More recently, we introduced trap (interrupts and exceptions) handling, privilege levels and an implementation of the PMP, a hardware mechanism to restrict access to physical memory [3].

In this paper, we report on our past, current and future proof methodology to prove properties over these hardware mechanisms.

## 2 Background

### 2.1 Kôika

Kôika [2] is a HDL embedded in the Rocq proof assistant. Unlike VHDL and Verilog, Kôika is a rule-based language, i.e. circuits are expressed as a set of rules that manipulate registers. The rules run in parallel, but appear to execute sequentially. This is known as the One-Rule-At-A-Time (ORAAT)

semantics. Rules are guarded – they might fail if some condition holds – and atomic – they either succeed entirely or have no effect at all.

### 2.2 RISC-V processor

The RISC-V processor [2] we study and extend is a 4-stage pipelined in-order, non speculative processor. Each stage of the pipeline (Fetch, Decode, Execute, Writeback) corresponds to a rule in the Kôika design, with extra rules to model external memory. We introduced a hardware shadow stack [1]: we keep a copy of return addresses on a separate, unreachable stack, so that attacks like buffer overflows that overwrite return addresses for Return-Oriented Programming are detected.

We introduced traps handling (interrupts and exceptions), privilege levels (Machine and User), and physical memory protection (PMP) [3].

### 2.3 Intermediate Representation for Reasoning

We reuse the translation from Baty et al. [1] from Kôika circuits to an intermediate representation for reasoning (IRR), which gives for each register *r*, the value of register *r* at the end of a clock cycle as an expression depending on the values of all registers at the beginning of the clock cycle. Formally, the expressions are of the following form:

$$v ::= \vec{b} | \{(field\_name := v)^*\} \\ e ::= v | x | r | \triangleright e | e \triangleright e | e?e : e | f(e)$$

where *v* is a constant value (i.e. a bitvector or a struct-like value), *x* is a variable identifier, *r* is a register identifier, $\triangleright$ and $\triangleright$ are various unary and binary operators, $e?e : e$ is the familiar ternary condition, and *f(e)* is an external call (modelling interaction with hardware modules defined outside the current Kôika module). These expressions allow to encode explicitly the conflict conditions. In the end, the result is a record *llr* ::= {V : N $\leftarrow$ e; R : reg $\rightarrow$ N}, where *R* is a mapping from registers to variable identifiers, and *V* is a mapping from variable identifiers to expressions.

This translation is proved correct, meaning that getting the final value of a register from this IRR, or from the semantics of Kôika circuits gives the same result.
# 3 Proof methodology

## 3.1 A full-Rocq approach

In [1], we transformed the Kôika circuit into an IRR, and devised custom tactics to transform the IRR into a simpler one, allowing to replace expressions with others, prune useless variables, etc. When the IRR was simple enough, we would finish the proof using standard Rocq tactics. Working directly in Rocq on the generated IRR has proven to be difficult for several reasons. First, the IRR obtained from the RISC-V processor description is a rather large Rocq object, which makes Rocq too slow to be usable in an interactive way. Second, the IRR contains variable numbers which (1) sometimes need to be referenced in the proof scripts, and (2) are subject to changes when the processor description is updated (which happens as soon as we implement new mechanisms). This makes the proofs very fragile and tedious to maintain.

## 3.2 A SMT-backed approach

To make proofs more maintainable, we leverage an SMT solver to do the heavy lifting for us. We focus in particular on proofs over one clock cycle, i.e. properties relating the values of registers before and after a clock cycle. We will then use standard Rocq tools (e.g. induction) to conduct whole proofs.

In order to discharge our proofs to a SMT solver, we first need to encode the IRR into a SMT formula over the theories of bitvectors and uninterpreted functions. Conveniently, the solver we use (Z3) supports struct-like types, which we map Kôika structures directly to. All operations on bitvectors in Kôika are straightforwardly mapped to corresponding operations on SMT bitvectors. External functions are mapped to uninterpreted functions.

Now, we encode the property *P* we want to prove as an IRR expression *e*<sub>*P*</sub>, and assert the negation of this expression in our SMT problem. This way, if the property *P* is valid (true for any initial values of the registers), then ¬*e*<sub>*P*</sub> is necessarily false, and the problem will be unsatisfiable. We will therefore interpret an unsat result from the SMT solver as a proof of our property *P*, and a sat result as a counter-example which we can use to debug our processor (or fix the statement of the property).

This SMT-backed methodology allows us for faster developing- proving-fixing iterations, and to introduce more mechanisms in the processor, without manually reworking the proofs of the earlier mechanisms each time a new mechanisms is added or modified. However, the reasoning is still done over the whole processor.

# 4 Making the proofs modular

Even though most of the proof effort is discharged to a SMT solver, there is still some incentive for making the proofs modular, i.e. reasoning not about the whole circuit, but rather

about individual rules or even about Kôika functions. First, rule-based HDLs divide circuits into rules exactly for the purpose of being able to reason about rules individually. This allows for smaller proofs, and for easier understanding of counterexamples. Second, function-wise reasoning helps establishing a refinement/simulation relation between the circuit and a specification. The ideas in this section are currently under development and are not finalized yet.

**Rule-level modularity.** It can therefore be studied in isolation. Say we have a list of rules *r*<sub>1</sub>, ..., *r*<sub>*n*</sub>, and we want to prove that some property *P* is an invariant of the system. It is sufficient to prove that the initial state satisfies *P*, and that each rule *r*<sub>*i*</sub> taken in isolation preserves that invariant. We can re-use the methodology from Section 3.2 and prove that our invariant holds for each rule.

**Function-level modularity.** Kôika features external functions, to model interaction with external modules, but also internal functions, used to encapsulate reusable blocks of code. In order to reuse our SMT methodology to reason about an individual function *f*, we need to extend it in two ways: (1) introduce variables for each of the arguments of function *f*, (2) introduce a variable for the return value of function *f*. We can then prove a property *P* of *f* in a similar fashion as how we currently prove properties of a complete circuit. Then, we can leverage this property in further proofs by replacing function calls to *f* with an uninterpreted function, together with an assertion that *P* holds for each call to *f*.

# 5 Further work and Conclusion

With the improvements proposed in Section 4, our proofs will be more modular, and we will be able to tackle more challenging goals, e.g. proving that our RISC-V processor indeed implements the Instruction Set Architecture. We are also interested in proving security properties at the hardware/software interface, i.e. properties that require the cooperation of hardware mechanisms and OS management.

# Acknowledgments

This work is supported by the Défi Inria CocoRISCo.

# References

[1] Matthieu Baty, Pierre Wilke, Guillaume Hiet, Arnaud Fontaine, and Alix Trieu. 2023. A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity. In *36th IEEE Computer Security Foundations Symposium, CSF 2023, Dubrovnik, Croatia, July 10-14, 2023*. IEEE, 372–387. https://doi.org/10.1109/CSF57540.2023.00029

[2] Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, and Arvind. 2020. The essence of Bluespec: a core language for rule-based hardware design. In *Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020*. Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 243–257. https://doi.org/10.1145/3385412.3385965
[3] Cyprien Jules, Pierre Wilke, Guillaume Hiet, and Gabriel Desfrène. 2025. heRVé: towards a formally verified RISC-V processor with security mechanisms (Work in Progress). In *Hardware-Supported Security Software 2025, co-located with ESORICS, HS3 2025, Toulouse, France, September 25, 2025*.