# Verifying Timed Properties of Programs in IoT nodes using Parametric Time Petri Nets

Étienne André, Jean-Luc Béchennec, Sudipta Chattopadhyay, Sébastien

Faucou, Didier Lime, Dylan Marinho, Olivier H Roux, Jun Sun

► To cite this version:

Étienne André, Jean-Luc Béchennec, Sudipta Chattopadhyay, Sébastien Faucou, Didier Lime, et al. Verifying Timed Properties of Programs in IoT nodes using Parametric Time Petri Nets. SAC '25: 40th ACM/SIGAPP Symposium on Applied Computing, Mar 2025, Catania (IT), Italy. pp.1998-2006, 10.1145/3672608.3707861 . hal-05408909

HAL Id: hal-05408909

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

Submitted on 10 Dec 2025

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 Attribution 4.0 International License
Verifying Timed Properties of Programs in IoT nodes using
Parametric Time Petri Nets

Étienne André

Université Sorbonne Paris Nord,
CNRS, LIPN
Villetaneuse, France
Institut Universitaire de France (IUF)
Paris, France

Jean-Luc Béchennec

Nantes Université, École Centrale
Nantes, LS2N, CNRS UMR 6004
Nantes, France

Sudipta Chattopadhyay

Singapore University of Technology
and Design
Singapore

Sébastien Faucou

Nantes Université, École Centrale
Nantes, LS2N, CNRS UMR 6004
Nantes, France

Didier Lime

Nantes Université, École Centrale
Nantes, LS2N, CNRS UMR 6004
Nantes, France

Dylan Marinho

Université de Lorraine, CNRS, Inria,
LORIA
Nancy, France
Sorbonne Université, CNRS, LIP6
Paris, France

Olivier H. Roux

Nantes Université, École Centrale
Nantes, LS2N, CNRS UMR 6004
Nantes, France

Jun Sun

Singapore Management University
Singapore

Abstract

The analysis of timed properties of programs is a complex task,
as it is highly dependent on both the software and the hardware.
In this work, we propose a framework for modeling with timed
formal models the execution of programs, taking into account the
micro-architecture of the machine on which it executes.

We model both the program, at the instruction set architecture
level, and the hardware, including the processor micro-architecture,
using time Petri nets.

Our implementation uses the ARM Cortex-M instruction set
architecture and a hardware architecture representative of micro-
controllers used in IoT nodes.

The whole translation is fully automated and allows, starting
from binary code, to automatically produce the models usable by
the state-of-the-art time Petri net model checker ROMÉO.

In addition, and as a proof of concept, we show how we can
check, and enforce to some extent, opacity properties on programs,
leveraging the ability of ROMÉO to verify a parametric timed exten-
sion of the classical computation tree logic.

CCS Concepts

• Software and its engineering → Software verification; • Security and privacy → Logic and verification; • Theory of computation → Program verification.

Keywords

program verification, execution time, timing attacks, formal meth-
ods

ACM Reference Format:

Étienne André, Jean-Luc Béchennec, Sudipta Chattopadhyay, Sébastien
Faucou, Didier Lime, Dylan Marinho, Olivier H. Roux, and Jun Sun. 2025.
Verifying Timed Properties of Programs in IoT nodes using Parametric Time
Petri Nets. In *The 40th ACM/SIGAPP Symposium on Applied Computing (SAC
'25), March 31-April 4, 2025, Catania, Italy*. ACM, New York, NY, USA, 9 pages.
https://doi.org/10.1145/3672608.3707861

# 1 Introduction

Context. Timing analysis of programs is a hard problem because their timed behavior is strongly impacted by the hardware on which they are run, most importantly by the micro-architecture (pipeline, memory hierarchy, etc.). Existing program analysis techniques abstract time away (e.g., safety analysis, flow analysis) or focus on specific and gross grain timing properties (schedulability, worst case execution time). They are thus unsuited for the verification of finer grain properties of programs, such as timed opacity that address timed side channel detection or mitigation [16, 31]. Such properties require reasoning on timed execution traces, i.e., sequences of timestamped instructions. For that, one then needs models of both the program and of the hardware that are precise enough paired with efficient analysis tools to explore their sets of behaviors.

Contributions. In this article, we study the problem of verifying
properties over timed execution traces of programs in the context

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

SAC '25, March 31-April 4, 2025, Catania, Italy

© 2025 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM ISBN 979-8-4007-0629-5/25/03

https://doi.org/10.1145/3672608.3707861
of the security of IoT nodes, which are small yet important building
blocks of emerging infrastructures such as smart cities, smart health,
industry 5.0, environmental, etc.

Our main contribution are as follows:

(1) A modular, automated approach to build formal models of both the binary code and the hardware, including their timing behaviors.

(2) An implementation targeting a realistic micro-architecture of a simple micro-controller capable of running a Cortex-M instruction set and producing time Petri nets models [26].

(3) An illustrative case-study showcasing the end-to-end approach for the verification of timed opacity properties on secure and insecure variants of a password checking program, and the parametric timed model-checking procedures, implemented in the state-of-the-art parametric timed model checker ROMÉO [24], both to measure execution times and to synthesize mitigations.

While time for programs can be seen as a discrete quantity (num-
ber of processor cycles) for most purposes, we have chosen to model
our systems with time Petri nets, for which time is dense, for two
main reasons: first we want to benefit from all features of a state-of-
the-art time model-checker like ROMÉO, including most importantly
for this work timing parameter synthesis, but also (for future work)
controller synthesis, and energy modeling, both possibly mixed
with parameters [20, 23]. Second, in the presence of timing uncer-
tainty, especially mixed with parallelism, dense time abstractions
may also be more efficient in certain cases.

1.1 Related work

Timed analysis of programs. The analysis of timed properties on binary code has been widely studied, most often in the context of the WCET problem [30]. This problem consists of computing an upper bound on the set of possible program execution times, independent of the initial state of the microarchitecture and the initial memory contents. To solve this problem, the scientific community has reused and improved program analysis techniques (flow, value and loop analysis), developed new techniques for microarchitectural analysis based on abstract interpretation [29], and for path analysis based on integer linear programming [22]. Combining these approaches yields solutions that are scalable even for complex programs and/or processors [8]. The cost of this scalability is the introduction of overapproximations during microarchitectural analysis (construction of inaccessible states) and/or resolution (exploration of infeasible paths). Apart from these overapproximations, these techniques are not designed to generate timed traces describing program execution at the instruction set level, which is required to explore more general timed properties.

For this, we must turn to techniques based on model checking [9, 11, 15]. By retaining in the model all elements that have an impact on the construction of the program execution trace, they allow accurate analysis (i.e., without over-approximating the model), at the cost of reduced scalability. In the context of the WCET problem, this accuracy allows to deal with the case of architectures with timing anomalies: exhaustive path exploration means that they are insensitive to such anomalies.

There are two types of approaches: those that use a timed formalism, and those that use a discrete formalism. In the first category, we can cite the work of Cassez and Béchennec [15], who propose on the one hand an automatic technique for constructing a program model from its binary code by exploiting program slicing, and on the other a model of the micro-architecture of the ARM920T processor. Both models are timed automata (TAs) [1], a formalism extending finite-state automata with real-time variables called clocks. By computing the product of these TAs, the model obtained is that of program execution on hardware, where the execution end date of each instruction results from the resolution of the modeled hardware mechanisms. These can be, for example, memory hierarchies, pipelines, or branch predictions. It is not necessary to model these mechanisms faithfully, as long as their impact on execution time is correct. A real-time model checker (UPPAAL in their work) can then be used to verify timed properties at the instruction set architecture level.

The second category includes a recent work by Binder et al. [11], who propose techniques for detecting timing anomalies in pipeline models. Here, program instructions are abstracted, the work focusing primarily on the evolution of the internal pipeline state as a function of events such as the duration of a memory access or the latency of an operation on a functional unit of the execution stage. At such a modeling level, timing emerges naturally by counting the (discrete) number of processor cycles.

Techniques in this second category use very low-level models that allows to focus on properties of the hardware architecture *per se*. This level of detail is not required to reason on timed program properties.

Thus, the approach and models we use here are in line with
the work of Cassez and Béchennec [15]. Since we are interested in
studying timed traces from relatively short sequences of code (as
opposed to complete programs), it is not necessary to implement
advanced program abstraction strategies. Having a non-abstract
model has also the advantage of being able to check properties
involving any element of the original program, and makes it easier
to interpret the traces generated by the model checker.

*Opacity in real-time formalisms.* The notion of opacity [13, 25], which we will consider as a proof of concept in Section 4, concerns information leaks from a system to an attacker; that is, it expresses the power of the attacker to deduce some secret information based on some publicly observable behaviors. Time particularly influences the deductive capabilities of the attacker.

The notion is extended to *timed* opacity in [14], where the at-
tacker can also observe time. The input model is timed automata. It
is proved in [14] that this version of timed opacity is undecidable
for TAs. This negative result leaves hope only if the definition or
the setting is changed, which was done in four main lines of work.

First, in [28], the input model is simplified to *real-time automata*, a restricted formalism compared to TAs. In this setting, (initial-state) opacity becomes decidable [28].

Second, subclasses of TAs are considered to retrieve decidability.
In [21], opacity is studied over a *discrete-time* setting, which allows
to retrieve decidability by reducing to finite-state automata. In [3, 4],
the focus is on one-clock timed automata (together with other
subclasses such as one-action TAs [4]).
Third, in [2], the authors consider a time-bounded notion of the
opacity of [14], where the attacker has to disclose the secret before
an upper bound, using a partial observability. This can be seen as a
secrecy with an expiration date. In addition, the analysis is carried
over a time-bounded horizon. The authors prove that this problem
is decidable for TAs.

Fourth, in [6, 7], an alternative definition to Cassez' opacity is
introduced by studying execution-time opacity: the attacker has
only access to the execution time of the system, as opposed to
Cassez' partial observations with some observable events (with
their timestamps). In that case, most problems become decidable
(see [5] for a survey).

## 1.2 Outline

We recall parametric time Petri nets in Section 2. We present our
translation from binary code to PTPNs in Section 3, including hard-
ware and software models. We show that our translation is able to
verify security properties on binary code in Section 4. We conclude
in Section 5.

## 2 High-level Parametric Time Petri Nets
(PTPNs)

Petri nets and their extensions offer a powerful formalism for mod-
eling concurrent systems. Time Petri nets [26] notably offer expres-
sive means to model timing constraints. Their parametric timed
extension [27] further enriches their expressiveness by offering the
possibility of modeling uncertainty.

High-level Petri nets. Petri nets can be divided into two cate-
gories: ordinary Petri nets and high-level Petri nets. High-level
Petri nets [18] have been proposed for manipulating different types
of expressions consisting of variables and written according to a
predefined syntax. In high-level nets, each token can contain com-
plex information which, for example, can describe the complete
state of a process or database and handle different expressions and
data structures.

Preconditions (guards) and postconditions (updates) on a set $V$ of variables are associated with transitions. The variables take values in a finite range (such as bounded integers), the guards are boolean expressions over $V$, and updates can be described as a sequence of imperative code expressed in a programming language.

A transition is enabled (it may fire) if there are enough tokens in its input places and if the guard is true. When a transition is fired, corresponding updates are performed, modifying the values of the variables.

Parametric Time Petri Nets. Time Petri nets [10, 26] (TPNs) extend Petri nets with time intervals associated with transitions, specifying firing delay ranges for the transitions. Parametric Time Petri Nets (TPPNs) [27] allow the use of parameters in the time intervals of transitions. The use of parameters for certain durations (e.g., delays, periods, execution times, etc.) enables early verification when durations are not yet fully specified or measured, and provides permissible values for these parameters so that the properties of interest are satisfied.

## 2.1 Definition and semantics

Let $\mathbb{N}$, $\mathbb{Q}$, $\mathbb{Q}_{\ge 0}$, and $\mathbb{R}_{\ge 0}$ denote the sets of natural, rational, non-negative rational, and non-negative real numbers, respectively. $B^A$ stands for the set of mappings from $A$ to $B$. If $A$ is finite and $|A| = n$, an element of $B^A$ is also a vector in $B^n$.

An interval $I$ of $\mathbb{R}_{\ge 0}$ is a $\mathbb{Q}$-interval if its left endpoint $\bar{I}$ belongs to $\mathbb{Q}_{\ge 0}$ and its right endpoint $\bar{I}$ belongs to $\mathbb{Q}_{\ge 0} \cup \{\infty\}$. We denote by $\mathcal{I}(\mathbb{Q})$ the set of $\mathbb{Q}$-intervals of $\mathbb{R}_{\ge 0}$.

Moreover, for any $d \in \mathbb{R}_{\ge 0}$ and any $\mathbb{Q}$-interval $I$, we let $I \ominus d$ be the interval defined by $\{\theta - d \mid \theta \in I \wedge \theta - d \ge 0\}$. Note that this is again a $\mathbb{Q}$-interval.

Given a finite set $V$ of variables over $\mathcal{V}$, let $\mathcal{G}(V)$ denote the set of Boolean expressions over $V$. A variable valuation is a mapping $V \to \mathcal{V}$. An update is a function $(V \to \mathcal{V}) \to (V \to \mathcal{V})$. Let $\mathcal{U}(V, \mathcal{V})$ denote the set of updates over $V$.

Timing parameters allow to replace some of the bounds of the
transitions of a high-level time Petri net with symbolic constants
that have rational values. Formally, given a finite set $\mathcal{P}$ of param-
eters, a *parameter valuation* is a function $\eta : \mathcal{P} \to \mathbb{Q}_{\ge 0}$.

A linear constraint over the parameters is an expression $\sum_{i=1}^{|\mathcal{P}|} \alpha_i \times \lambda_i \sim b$, where $\forall 1 \le i \le |\mathcal{P}|$, $\lambda_i \in \mathcal{P}$, $\alpha_i, b \in \mathbb{Q}$ and $\sim \in \{=, <, >, \le, \ge\}$.

A parametric time interval is a function $J : \mathbb{Q}_{\ge 0}^{|\mathcal{P}|} \to \mathcal{I}(\mathbb{Q}_{\ge 0})$ that associates to each parameter valuation a $\mathbb{Q}$-interval. The set of parametric time intervals over $\mathcal{P}$ is denoted by $\mathcal{J}(\mathcal{P})$. As for numerical intervals, $J$ can be split into two functions $J$ and $\bar{J}$ that are respectively the minimum bound and the maximum bound. They can be both represented by a linear constraint over the parameters.

**Definition 2.1 (High-level Parametric Time Petri Net).** A High-level Parametric Time Petri Net (PTPN) is a tuple $\mathcal{N} = (P, T, \mathcal{P}, V, \text{pre}(\cdot), \text{post}(\cdot), \text{guard}, \text{update}, (m_0, \mu_0), J_s)$ where

* $P$ is a finite non-empty set of *places*,

* $T$ is a finite set of *transitions* such that $T \cap P = \emptyset$,

* $\mathcal{P}$ is a finite set of *parameters*,

* $V$ is a finite set of *variables* taking their value in the finite set $\mathcal{V}$ (such as bounded integers),

* $\text{pre} : T \to \mathbb{N}^P$ is the *backward incidence mapping*,

* $\text{post} : T \to \mathbb{N}^P$ is the *forward incidence mapping*,

* $\text{guard} : T \to \mathcal{G}(V)$ is the *guard function*,

* $\text{update} : T \to \mathcal{U}(V, \mathcal{V})$ is the *update function*,

* $(m_0, \mu_0) \in \mathbb{N}^P \times \mathbb{V}^V$ is the *initial values* $m_0$ of the marking and $\mu_0$ of the variables, and

* $J_s : T \to \mathcal{J}(\mathcal{P})$ is the (parametric) *static firing interval function*.

*Discrete behavior.* For a marking $m \in \mathbb{N}^P$, $m(p)$ represents the number of *tokens* in place *p*. A *discrete state* of a PTPN is a pair $(m, \mu)$, where *m* is a marking, and $\mu \in \mathbb{V}^V$ is a variable valuation.

A transition $t \in T$ is said to be *enabled* by a given marking $m \in \mathbb{N}^P$ and a valuation $\mu \in \mathbb{V}^V$ if $m \ge \text{pre}(t)$ and $\text{guard}(t)(\mu) = \text{true}$. We denote by $\text{en}(m, \mu)$ the set of transitions that are enabled by $(m, \mu)$: $\text{en}(m, \mu) = \{t \in T \mid m \ge \text{pre}(t) \text{ and } \text{guard}(t)(\mu) = \text{true}\}$.

Firing an enabled transition $t$ from $(m, \mu)$ leads to the new marking $m' = m - \text{pre}(t) + \text{post}(t)$ and the new valuation $\mu' = \text{update}(t)(\mu)$. We denote by newen$(m, \mu), t$ the set of transitions that are newly enabled by the firing of $t$ from $(m, t)$:
newen((m, μ), t) = {t' ∈ en(m - pre(t) + post(t), update(t)(μ)) | t' /∈ en(m - pre(t), μ) or t = t'

Semantics. Instantiating every static interval $J_s$ of a PTPN $\mathcal{N}$ by a parameter valuation $\eta$ leads to a (high-level) TPN without parameters.

A state of the net $\mathcal{N}$ is a tuple $(m, \mu, I, \eta)$ in $\mathbb{N}^P \times \mathbb{V}^V \times \mathcal{I}(\mathbb{R}_{\ge 0})^T \times \mathbb{Q}_{\ge 0}^{\text{Par}}$, where: $(m, \mu)$ is a discrete state (i.e., $m$ is a marking and $\mu$ is a variable valuation), $\mathcal{I}$ is the interval function and associates a *time interval* to each transition enabled by $m$ and $\eta$ is a parameter valuation for the state.

*Definition 2.2 (Semantics of a PTPN).* The semantics of a PTPN is a timed transition system $(Q, Q_0, \rightarrow)$ where:

* $Q \subseteq \mathbb{N}^P \times \mathbb{V}^V \times \mathcal{I}(\mathbb{R}_{\ge 0})^T \times \mathbb{Q}_{\ge 0}^{\text{Par}}$

* $Q_0 = \{(m_0, \mu_0, I_0, \eta) \mid \eta \in \mathbb{Q}_{\ge 0}^{\text{Par}}, \forall t \in T, \eta(I_s(t)) \neq \emptyset\}$ where $\forall t \in \text{en}(m_0), I_0(t) = I_s(t)$

* $\rightarrow$ consists of two types of transitions:

- discrete transitions: $(m, \mu, I, \eta) \xrightarrow{t \in T} (m', \mu', I', \eta)$ iff

* $m \ge \text{pre}(t), m' = m - \text{pre}(t) + \text{post}(t)$ and $\eta(I(t)) = 0$,

* $\text{guard}(t)(\mu) = \text{true}$ and $\mu' = \text{update}(t)(\mu)$, and

* $\forall t' \in \text{en}(m')$

* $I'(t') = I_s(t')$ if $t' \in \text{newen}(m, t)$,

* $I'(t') = I(t')$ otherwise;

- time transitions: $(m, \mu, I, \eta) \xrightarrow{d \in \mathbb{R}_{\ge 0}} (m, \mu, I \ominus d, \eta)$, iff $\forall t \in \text{en}(m), (I \ominus d)(t) \ge 0$.

## 2.2 Decidability and implementation

A Petri net is said to be *bounded* when there exists some constant $k$ such that no place of the net ever contains more than $k$ tokens. Since the variables of $V$ take their value in a finite set such as bounded integers, the reachability problem for bounded High-level Time Petri Net is decidable [17].

Parametric timed models have a great expressiveness, but this comes at the price of the undecidability of most interesting problems and, in particular, the existence (and then the synthesis) of values for the parameters such that some discrete configuration is reachable. Fortunately, by considering bounded integer parameters, this problem becomes decidable [19] and then will be decidable for bounded PTPNs. In practice, model-checking for bounded PTPNs is proposed in the Roméo tool [24] allowing the synthesis of the constraints between parameters that describe the set of valuations that satisfy properties such as reachability or properties expressed in the parametric TCTL logic [12]. In the PTPNs handled by Roméo, the guards are boolean expressions over the set of declared variables, and updates are expressed using a syntax similar to the C language (including function calls).

## 2.3 A simple example

Consider the PTPN in Fig. 1 where guards and updates are respectively in blue and purple, where $v$ is a variable with a value in bounded integers, e.g., in $[0, 100]$. Transition $t_0$ has a guard $v \ge 3$ and is therefore only enabled if $v \ge 3$. On the other hand, this transition has no update, so its firing does not modify the value of $v$. Transition $t_1$ has no guard, but its firing decrements the value of

<figure><img src="image_2.png" /><figcaption>Figure 1: A PTPN with an integer variable $v$ (initialized to 4) and a timing parameter $\lambda$</figcaption></figure>

$v$ by 2. Hence the firing of $t_1$ makes the guard of $t_0$ false, and thus disables it.

The firing interval of $t_1$ is $[5, 7]$, which means that $t_1$ must remain enabled for at least 5 time units before firing, and must fire before 7 time units. The firing interval of $t_0$ is parameterized by $\lambda$, which is its maximum limit.

If we want every execution to reach a state with a token in $p_1$, which is written as $AF(p_1 == 1)$ with the tool Roméo, the firing of $t_0$ must occur before the firing of $t_1$. By checking this property with Roméo, the tool synthesizes that the property is true iff $2 \le \lambda < 5$ (i.e., $2 \le \lambda \le 4$ by considering that the parameter is integer-valued).

# 3 From binary code execution to PTPNs

## 3.1 Model overview and principles

Executing a program requires both a representation of the program in a machine language and a machine that implements that language. To model the execution of a binary program, we propose a two-part model: hardware and software. Our model is given in the form of a time Petri net.

**Hardware.** The hardware part consists of a model of the processor architecture and a model of the instruction set architecture (ISA). For the former, to limit architectural complexity, a model of a relatively simple architecture is implemented. It is similar to the ARMv6m architecture with a 2-stage pipeline: Fetch and Execute. The time in terms of number of cycles is expressed by firing intervals on the model’s transitions. This model includes:

* A unique memory space for instructions and data;

* A bus between the processor and memory;

* A direct-mapped instruction cache with 16 lines of 32 bytes;

* No data cache;

* The execution pipeline of the processor.

Of course, this model abstracts from many aspects of a real processor. For example, the cache does not contain actual instructions, but only information about their presence. Fig. 2 shows the processor pipeline model.

For the latter (the ISA part), the selected processor is an ARM Cortex-M core. The state of the model includes the content of the processor registers and of the memory. The model also includes an update function for each instruction of the program that encode its semantics. Fig. 3 shows the model of 3 instructions.

**Software.** The software part captures the ARM Cortex-M binary-level representation of the program as a TPN which synchronizes
<figure><img src="image_3.png" /><figcaption>Figure 2: Processor pipeline model. Token in $p_1$ means the pipeline can fetch a new instruction. `doFetch`, `isHit` and `accessCount` are variables used to synchronize the pipeline model with the program model. From $p_2$, instruction fetch can lead to an instruction cache hit (`ICacheHit` transition that takes 1 cycle) or a miss according to `isHit` variable. A token in $p_4$ means the bus is available and if so the miss is processed (`ICacheMiss` transition). A cache line refill takes 10 cycles. Once fetched (token in $p_5$), an instruction enters the Execute stage. Memory access instructions (`accessCount>0`) take the `DWaitBus`, `Mem` and `EndMem` path (4 cycles per memory access) while other instructions (`accessCount==0`) take the `Exe` and `EndExe` path (1 cycle) provided the Execute stage is free (token in $p_6$). When an instruction starts its execution, a token is put back in $p_1$ to allow a fetch of a new instruction in parallel to the execution of the current one.</figcaption></figure>

```c
int inst80b0(core_t &core, mem_t &mem) { // 80b0: ldr.w
    r3, [r7, #4]
    core regs.r[3] = memRead(mem, core regs.r[7] + 4);
    return cacheAccess(core ICache, 32944);
}

int inst80b2(core_t &core, mem_t &mem) { // 80b2: cmp
    r3, #0
    uint64_t op1 = core regs.r[3];
    uint64_t op2 = 0;
    uint64_t val = op1 - op2;
    updateSR(core regs, val, op1, -op2);
    return cacheAccess(core ICache, 32946);
}

int inst80b4(core_t &core, mem_t &mem) { // 80b4: bne.n
    809e
    return cacheAccess(core ICache, 32948);
}
```

<caption>Figure 3: Instruction model. For each instruction of a program, a function is generated in the C-like language supported by ROMÉO [24]. In the first part, the content of the registers and of the memory is updated according to the semantics of the instruction. In the second part, the state of the instruction cache is updated. The return value indicates whether the instruction was present in the cache or not.</caption>

with the pipeline model. It is structurally identical to the control

flow graph of the program. Firing a transition corresponds to executing an instruction. A transition includes a guard which synchronizes with the pipeline Fetch stage via the `doFetch` variable, and an update which includes functional execution of the instruction and assignment of the `accessCount` and `isHit` variables.

Conditional branches have two transitions from the upstream place to the downstream places corresponding to the branch taken and the branch not taken outcomes. The transition to the place corresponding to the branch target instruction carries the guard with the branch condition, while the transition to the place corresponding to the instruction in sequence carries the complementary guard. Fig. 4 shows the model of a part of a program.

**Synchronization between the hardware and the software model.**
The hardware model is given in figure 2 and a part of a software model is given in figure 4. These two models are synchronized thanks to three variables: `doFetch`, `isHit`, and `accessCount`.

In the initial state `doFetch` has the value 0. This allows `Fetch` transition of the hardware model to be fired, which in turns sets back `doFetch` to 1. By doing so, the transition corresponding to the current instruction in the software model can be fired, which sets `doFetch` back to 0. When the function associated with the instruction is executed, it sets variable `isHit`. It is used in the hardware model to compute the latency of the instruction in the first stage of the execution pipeline: in case of a cache miss, the memory bus must be locked and a memory access has to be performed to populate the corresponding cache line. Lastly, when the transition associated
with the current instruction is fired in the software model, it also sets `accessCount`. This variable is used in the hardware model, more specifically in the second stage of the pipeline, to detect if an instruction is accessing data memory or not, and in the former case how many accesses have to be done.

<figure><img src="image_4.png" /><figcaption>Figure 4: Program model. Each place is labeled with the address where the instruction is located in memory. All transition firing intervals are [0, 0], as time progress is determined by the pipeline model and memory accesses. Each transition is synchronized with the pipeline model via the `doFetch` variable, and the instruction itself is executed via a function call (a function is generated for each instruction in the program) which returns whether or not the instruction was present in the cache (`isHit` variable). The number of memory accesses is also assigned. On conditional branch transitions, the branch condition is combined with `doFetch` to enable one of the two downstream transitions.</figcaption></figure>

## 3.2 Translation from ELF binary to model

In the following, we describe a method to translate the binary file of a program into a TPN. Our translator determines the entry point and then decodes the instructions from this entry point. The user must enter the address of the instruction where they wish to end the program. The constants stored in the program are extracted.<fnref n="1" />

Branch targets are computed and our translator reconstructs the control flow graph. In the process, function calls are inlined. There is one limitation here: it is currently not possible to translate a program using indirect branches or unbounded recursive calls. The constants stored in the `.rodata` segment are also extracted and a function for initializing the memory with these constants is generated.

For each instruction appearing in the program, our translator generates a function named with the instruction address. The control flow graph is then traversed and the TPN is generated: each place is named with the instruction address, and transitions are updated with the instruction function call. Two files are generated: one file containing the PN and one file containing the instruction functions and the memory constant initialization function.

Our translation (written in C++ and python) is fully automated, from the C source code all the way to the PTPN model readable by ROMÉO, including the hardware and software models. The source code and installation instructions are available online in an open source manner, at https://github.com/DylanMarinho/codeToPN/.

# 4 A case-study: verifying a security property

We now show how we can use the previous translation into (high-level) parametric TPNs, together with the tool ROMÉO [24], to check opacity properties on binary programs. We use the opacity notion based on execution times [5, 7], where the attacker attempts to deduce private information based only on an observation of the execution time. More precisely, a system is opaque whenever the attacker cannot deduce any secret (e.g., a variable valuation, a visited state...) by only observing the execution time.

The performance figures we give were obtained on an Intel Core i7 2.8GHz processor with 16 GiB of RAM.

## 4.1 Methodology

In order to measure the execution time of a given program, we first add a Petri net place $p_{end}$ corresponding to the address after the last instruction, which is detected automatically by our toolchain.

We can then obtain the execution time of the program by the parametric CTL query $E(p_{end} == 0)U_{[a,a]}(p_{end} > 0)$, where $a$ is a parameter. This property means: "there exists a path on which $p_{end}$ is marked at date $a$ and is never marked before that". The property holds for all values of $a$ that correspond to the duration of an execution from start to end of the program.

We cannot have loops in the model in which $p_{end}$ would be marked twice or more, but the given property also forbids any delay after $p_{end}$ is eventually marked, contrary to, say, the simpler $EF_{[a,a]}(p_{end} > 0)$ property, which only specifies that $p_{end}$ is eventually marked at date $a$. The latter property thus also works if we add a transition consuming the token in $p_{end}$ with time interval $[0, 0]$—which is another way to prevent delay in $p_{end}$.

## 4.2 Application to C programs

*First case study.* We now consider the classical secure password check C program in Fig. 5, compiled for ARMv6m and executing on the architecture described in Section 3.1. Note that due to constraints of the cross-compiler (GCC) we also had to provide an implementation of the standard `memcpy` function, as shown in Fig. 6.

<footnote n="1">¹ARM compilers store 32-bit constants in the `.text` segment after the return of the function that uses them.</footnote>
```c
int main() {
    int i;
    int length = 10; // length of the strings

    char ca[11] = "choudoufou";
    char cb[11] = "cheese";

    int result = 1; // true

    for (i = 0; i < length; i++) {
        result &= (ca[i] == cb[i]);
    }

    return result;
}
```

<caption>Figure 5: A secure password checking program</caption>

```c
#include < stddef.h>

void *memcpy(char *b, int c, size_t len) {
    while (len > 0) {
        *b++ = c;
        len --;
    }
}
```

<caption>Figure 6: memcpy implementation</caption>

```c
int main() {
    int i;
    int length = 10; // length of the strings

    char ca[11] = "choudoufou";
    char cb[11] = "cheese";

    for (i = 0; i < length; i++) {
        if (ca[i] != cb[i]) {
            return 0; // false
        }
    }

    return 1; // true
}
```

<caption>Figure 7: An insecure password checking program</caption>

The secret in this example and the following is that the correct password was given.

Using the query above in ROMÉO, we find in less than 1 s that the execution time, which is constant for all inputs of a given length, is 876, and thus we cannot deduce the secret from observing the execution time.

**Second case study.** Consider now the insecure program given in Fig. 7. For the given input, we can find, again in less than 1 s, the execution time of 446 as before while, for the input matching the secret, the execution time is 758.

As expected, in the binary code, a forward conditional jump is generated for the `if` statement. In the Petri net model, this corresponds to two transitions from the same place as seen in Fig. 8, one for when the branch is taken (`i8050_T`) and one for when it is not (`i8050 NT`).

The guards for each of those transitions make them mutually exclusive but if we remove them, we obtain a non-deterministic Petri net modeling all the possible behaviors regarding whether the branch is taken or not. If we now query ROMÉO for the execution time we obtain in about 1 s, a set of all the possible execution times for all possible inputs (of the given length): `{362, 404, 446, 488, 530, 572, 614, 656, 698, 740, 758}`. Notice that the execution time corresponding to the secret is indeed in that set and is the biggest value as expected. To exclude this case corresponding to the secret, we can generate a token in an additional place $p_{NT}$ each time the “branch not taken” transition is fired, and ask in the parametric query that this place is also not empty. This indeed removes the 758 secret value from the set, and the performance is not impacted.

Consequently we can conclude that this insecure system does not have good opacity properties: the set of execution times when going through the secret and the set of execution times when not going through the secret are disjoint, so no execution time is opaque in the sense of [7], i.e., contained in the intersection of both sets. This formally confirms that this program is insecure w.r.t. timing attacks based on a measure of the execution time.

We can also automatically compute the intersection of those two sets of execution time, using the observer depicted in Fig. 9, and verifying property $EF_{[a,a]}(p_{end} > 0 \&& d_{\neg s} > 0 \&& p_{NT} > 0)$, assuming $p_{end}$ has the emptying $[0, 0]$ transition discussed above.

The idea is to go through the program once ($p_{end} > 0$), without going through the secret ($p_{NT} == 0$), and measuring the execution time as parameter $a$ as above. Since we have immediate $([0, 0])$ emptying transitions in both $d_s$ and $p_{end}$, those two places will be marked simultaneously only after exactly $p$ time units, so if transition “reset” is enabled, $p$ is now constrained to belong to the set of execution times of runs going through the secret.

Transition “reset” can then fire exactly at that time and immediately execute user-defined function `reinit()`, which we have written to reset the discrete state (including places other than the observer, models of the memory and cache, etc.) of the net exactly in its initial state. Transition “reset” also puts a token in $c_{\neg s}$. As before, since we have immediate $([0, 0])$ emptying transitions in both $d_{\neg s}$ and $p_{end}$, those two places will be marked simultaneously, only after exactly another $p$ time units.

In addition, the property asks that, on this second run through the net, we do not go through the secret ($p_{NT} > 0$).

Finally, the set of values for $p$ returned by the query is exactly the execution times that are common to the first and second runs of the net, i.e., that are opaque for the secret in the sense of [7].

This observer is generic, provided we can express the fact that we go through the secret or not using the discrete state of the net.

**Third case study.** Let us finally consider a slightly more subtle insecure program, given in Fig. 10. At high-level, the program is semantically equivalent to the one in Fig. 5, but we have created an additional branch in the binary and we will use the previous methodology to analyze the execution times: we find an execution time of 876 time units for the run going through the secret and set `{816, 822, 828, 834, 840, 846, 852, 858, 864, 870}` for the non-deterministic executions not going through the secret. The query takes about 5 s to get the latter set, and about 8 s to get the time for
<figure><img src="image_5.png" /><figcaption>Figure 8: “If” test in the binary code of the insecure program</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Figure 9: Observer for execution time set intersection</figcaption></figure>

```c
int main() {
    int i;
    int length = 10; // length of the strings

    char ca[11] = "choudoufou";
    char cb[11] = "cheese";

    int result = 1; // true

    for (i = 0; i < length; i++) {
        if (ca[i] == cb[i])
        {
            result &= 1;
        } else {
            result &= 0;
        }
    }

    return result;
}
```

<caption>Figure 10: Another insecure password checking program</caption>

the secret, or also about 8 s to get the set of all execution times at once. Again the two sets are distinct but we will try to patch this. To that effect, we add a transition with time interval $[b, b]$, with $b$ a parameter, at the end of the “branch taken” path, which here corresponds to the two characters being different. And now we synthesize the whole constraint describing the execution time of the non-deterministic program (going through the secret or not). We obtain, in about 145 s (and 1.5 GiB of used RAM), omitting part of the constraint to keep it readable:

$$ 
\begin{array}{l}
b \ge 4 \\
a \ge 816 \\
10 \times b - a = -776
\end{array}
$$

$$ 
\begin{array}{l}
b \ge 4 \\
a \ge 822 \\
9 \times b - a = -786
\end{array}
$$

$$ 
\begin{array}{l}
b \ge 4 \\
a \ge 864 \\
2 \times b - a = -856
\end{array}
$$

$$ 
\begin{array}{l}
b \ge 4 \\
a \ge 870 \\
b - a = -866
\end{array}
$$

$$ 
\begin{array}{l}
b \in [0, 4] \\
a \in [816, 816]
\end{array}
$$

$$ 
\begin{array}{l}
\text{or } \dots \text{ or } \\
b \in [0, 4] \\
a \in [864, 864]
\end{array}
\quad \text{or} \quad 
\begin{array}{l}
b \in [0, 4] \\
a \in [870, 870]
\end{array}
\quad \text{or} \quad 
\begin{array}{l}
b \ge 0 \\
a \in [876, 876]
\end{array}
$$

The last clause corresponds to the execution time of the secret: it is independent of $b$ because it never goes through the branch we have delayed. The previous few clauses show that the execution times are unchanged if $b \in [0, 4]$. This is because the instruction just before the delay is a memory access and it incurs a latency of 4 cycles in any case, as can be seen in transition “Mem” in Fig. 2.

Finally, from the first clauses, by substituting $a$ with the execution time of the secret (876), we see that we can make all those times equal with $b = 10$. Note however that, because the first 4 time units are in any case spent to wait for the end of the memory access, this tells us we would actually need to delay the branch by $10 - 4 = 6$ time units (cycles).

We thus modify the program accordingly by adding 6 nop instructions (doing nothing) at the end of the branch<fnref n="2" /> and by computing all the possible execution times as before, we see that they indeed reduce to a single possibility: 886.

Note that this is a bit lucky because in general, adding those nop instructions could incur new cache misses, and not necessarily in the same way for all branches. This is indeed the case here, as 886 corresponds to an additional cache miss compared to the previous time of 876. But here, this new cache miss happens for both branches, which in general might not be the case.

We could then iterate the procedure by adding a new delay on the relevant branch and so on.

## 5 Conclusion

We have presented an end-to-end approach on binary code timing analysis, subject to micro-architectural constraints, which allows for the verification of fine-grained timed properties such as timed opacity and similar security properties. Our approach includes the production of timed formal models of both the program and the hardware architecture, using the formalism of time Petri nets. We show through an illustrative case-study how parameter synthesis for this formalism can be leveraged both to detect security issues and to help design mitigation measures.

*Future work.* Further work includes modeling and analysis of programs on multicore architectures, as well as modeling more complex attacks such as fault-injection, cache side-channels (flush and reload, prime and probe), or energy-based attacks.

Proving the correctness of the translation (e.g., using a theorem prover) would be of interest.

<footnote n="2">²We use the asm statement to add this in the C code.</footnote>
Acknowledgments

This work is partially supported by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015 / 2019 ANR NRF 0092) and by ANR BisoUS (ANR-22-CE48-0012).

References

[1] Rajeev Alur and David L. Dill. 1994. A theory of timed automata. *TCS* 126, 2 (April 1994), 183–235. https://doi.org/10.1016/0304-3975(94)90010-8

[2] Ikhlass Ammar, Yamen El Touati, Moez Yeddes, and John Mullins. 2021. Bounded opacity for timed systems. *Journal of Information Security and Applications* 61 (Sept. 2021), 1–13. https://doi.org/10.1016/j.jisa.2021.102926

[3] Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan, and Ichiro Hasuo. 2024. The Opacity of Timed Automata. In *FM* (Milano, Italy) (*LNCS*, Vol. 14933), André Platzer, Kristin-Yvonne Rozier, Matteo Pradella, and Matteo Rossi (Eds.). Springer, 620–637. https://doi.org/10.1007/978-3-031-71162-6_32

[4] Étienne André, Sarah Dépernet, and Engel Lefauchex. 2024. The Bright Side of Timed Opacity. In *ICFEM* (Hiroshima, Japan) (*LNCS*, Vol. 15394), Kazuhiro Ogata, Meng Sun, and Dominique Méry (Eds.). Springer, 51–69. https://doi.org/10.1007/978-981-96-0617-7_4

[5] Étienne André, Engel Lefauchex, Didier Lime, Dylan Marinho, and Jun Sun. 2023. Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata. In *TiCSA* (Paris, France) (*Electronic Proceedings in Theoretical Computer Science*, Vol. 392), Maurice H. ter Beek and Clemens Dubslaff (Eds.). 1–26. https://doi.org/10.4204/EPTCS.392.1 Invited paper.

[6] Étienne André, Engel Lefauchex, and Dylan Marinho. 2023. Expiring opacity problems in parametric timed automata. In *ICECCS* (Toulouse, France), Yamine Ait-Ameur and Ferhat Khendek (Eds.). 89–98. https://doi.org/10.1109/ICECCS59891.2023.00020

[7] Étienne André, Didier Lime, Dylan Marinho, and Jun Sun. 2022. Guaranteeing timed opacity using parametric timed model checking. *ACM Transactions on Software Engineering and Methodology* 31, 4 (Oct. 2022), 1–36. https://doi.org/10.1145/3502851

[8] Zhenyu Bai, Hugues Cassé, Thomas Carle, and Christine Rochange. 2023. Computing Execution Times With Execution Decision Diagrams in the Presence of Out-of-Order Resources. *IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems* 42, 11 (2023), 3665–3678. https://doi.org/10.1109/TCAD.2023.3258752

[9] Martin Becker, Ravindra Metta, R. Venkatesh, and Samarjit Chakraborty. 2019. Scalable and precise estimation and debugging of the worst-case execution time for analysis-friendly processors: a comeback of model checking. *STTT* 21, 5 (2019), 515–543. https://doi.org/10.1007/S10009-018-0497-2

[10] Bernard Berthomieu and Michel Diaz. 1991. Modeling and Verification of Time Dependent Systems Using Time Petri Nets. *TSE* 17, 3 (1991), 259–273. https://doi.org/10.1109/32.75415

[11] Benjamin Binder, Mihai Asavoea, Florian Brandner, Belgacem Ben Hedia, and Mathieu Jan. 2022. Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture. *STTT* 24, 3 (2022), 415–440. https://doi.org/10.1007/S10009-022-00655-1

[12] Véronique Bruyère and Jean-François Raskin. 2007. Real-Time Model-Checking: Parameters everywhere. *LMCS* 3, 1:7 (2007), 1–30. https://doi.org/10.2168/LMCS-3(1:7)2007

[13] Jeremy W. Bryans, Maciej Koutny, Laurent Mazaré, and Peter Y. A. Ryan. 2008. Opacity generalised to transition systems. *International Journal of Information Security* 7, 6 (2008), 421–435. https://doi.org/10.1007/s10207-008-0058-x

[14] Franck Cassez. 2009. The Dark Side of Timed Opacity. In *ISA* (Seoul, Korea) (*LNCS*, Vol. 5576), Jong Hyuk Park, Hsiao-Hwa Chen, Mohammed Atiquzzaman, Changhoon Lee, Tai-Hoon Kim, and Sang-Soo Yeo (Eds.). Springer, 21–30. https://doi.org/10.1007/978-3-642-02617-1_3

[15] Franck Cassez and Jean-Luc Béchennec. 2013. Timing Analysis of Binary Programs with UPPAAL. In *ACSD* (Barcelona, Spain), Josep Carmona, Mihai T. Lazarescu, and Marta Pietkiewicz-Koutny (Eds.). *IEEE Computer Society*, 41–50. https://doi.org/10.1109/ACSD.2013.7

[16] Shengjian Guo, Meng Wu, and Chao Wang. 2018. Adversarial symbolic execution for detecting concurrency-related cache timing leaks. In *ESEC/SIGSOFT FSE* (Lake Buena Vista, FL, USA), Gary T. Leavens, Alessandro Garcia, and Corina S. Pasareanu (Eds.). ACM, 377–388. https://doi.org/10.1145/3236024.3236028

[17] Imane Haur, Jean-Luc Béchennec, and Olivier H. Roux. 2023. Model-Checking of Concurrent Real-Time Software Using High-Level Colored Time Petri Nets with Stopwatches. *Cybernetics and Systems* (2023), 1–31. https://doi.org/10.1080/01969722.2023.2247261

[18] Lom Hillah, Fabrice Kordon, Laure Petrucci-Dauchy, and Nicolas Trèves. 2006. PN Standardisation: A Survey. In *FORTE* (Paris, France) (*LNCS*, Vol. 4229), Elie Najm, Jean-François Pradat-Peyre, and Véronique Donzeau-Gouge (Eds.). Springer, 307–322. https://doi.org/10.1007/11888116_23

[19] Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. 2015. Integer Parameter Synthesis for Real-Time Systems. *TSE* 41, 5 (2015), 445–461. https://doi.org/10.1109/TSE.2014.2357445

[20] Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. 2022. Control of Real-time Systems with Integer Parameters. *IEEE Trans. Automat. Control* 67, 1 (2022), 75–88. https://doi.org/10.1109/TAC.2020.3046578

[21] Julian Klein, Paul Kogel, and Sabine Glesner. 2024. Verifying Opacity of Discrete-Timed Automata. In *FormaliSE* (Lisbon, Portugal), Nico Plat, Stefania Gnesi, Carlo A. Furia, and Antónia Lopes (Eds.). ACM, 55–65. https://doi.org/10.1145/3644033.3644376

[22] Yau-Tsun Steven Li and Sharad Malik. 1997. Performance analysis of embedded software using implicit path enumeration. *IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems* 16, 12 (1997), 1477–1487. https://doi.org/10.1109/43.664229

[23] Didier Lime, Olivier H. Roux, and Charlotte Seidner. 2021. Cost Problems for Parametric Time Petri Nets. *FI* 183, 1-2 (2021), 97–123. https://doi.org/10.3233/FI-2021-2083

[24] Didier Lime, Olivier H. Roux, Charlotte Seidner, and Louis-Marie Traonouez. 2009. Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In *TACAS* (York, United Kingdom) (*LNCS*, Vol. 5505), Stefanowalewski and Anna Philippou (Eds.). Springer, 54–57. https://doi.org/10.1007/978-3-642-00768-2_6

[25] Laurent Mazaré. 2004. Using unification for opacity properties. In *WITS* (Barcelona, Spain), Peter Ryan (Ed.). 165–176.

[26] Philip Meir Merlin. 1974. *A study of the recoverability of computing systems*. Ph. D. Dissertation. University of California, Irvine, CA, USA.

[27] Louis-Marie Traonouez, Didier Lime, and Olivier H. Roux. 2009. Parametric Model-Checking of Stopwatch Petri Nets. *Journal of Universal Computer Science* 15, 17 (2009), 3273–3304. https://doi.org/10.3217/jucs-015-17-3273

[28] Lingtai Wang, Naijun Zhan, and Jie An. 2018. The Opacity of Real-Time Automata. *IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems* 37, 11 (2018), 2845–2856. https://doi.org/10.1109/TCAD.2018.2857363

[29] Reinhard Wilhelm, Sebastian Altmeyer, Claire Burguière, Daniel Grund, Jörg Herter, Jan Reineke, Björn Wachter, and Stephan Wilhelm. 2010. Static Timing Analysis for Hard Real-Time Systems (*LNCS*, Vol. 5944), Gilles Barthe and Manuel V. Hermenegildo (Eds.). Springer, 3–22. https://doi.org/10.1007/978-3-642-11319-2_3

[30] Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David B. Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter P. Puschner, Jan Staschulat, and Per Stenström. 2008. The worst-case execution-time problem – Overview of methods and survey of tools. *ACM Transactions in Embedded Computing Systems* 7, 3 (2008), 36:1–36:53. https://doi.org/10.1145/1347375.1347389

[31] Meng Wu, Shengjian Guo, Patrick Schaumont, and Chao Wang. 2018. Eliminating timing side-channel leaks using program repair. In *ISSTA* (Amsterdam, The Netherlands), Frank Tip and Eric Bodden (Eds.). ACM, 15–26. https://doi.org/10.1145/3213846.3213851