pta short=PTA, long=parametric timed automaton, short-plural=s, long-plural-
form=parametric timed automata, cite=AHV93, extra=4, tag=models lupta
short=L/U-PTA, long=lower/upper parametric timed automaton, short-plural=s,
long-plural-form=lower/upper parametric timed automata, short-indefinite=an,
long-indefinite=a, cite=HRSV02, extra=6, tag=models upta short=U-PTA,
long=upper-bound parametric timed automaton, short-plural=s, long-plural-
form=upper-bound parametric timed automata, short-indefinite=a, long-
indefinite=an, cite=BlT09, tag=models ta short=TA, long=timed automaton,
short-plural=s, long-plural-form=timed automata, cite=AD94, extra=1,
tag=models ppta short=(P)TA, long=(possibly parametric) *ta, short-plural=s,
long-plural-form=(possibly parametric) *ta, ipta short=IPTA, long=IMITATOR
*pta, short-plural=s, long-plural-form=IMITATOR *pta, cite=Andre21,
extra=LABEL:sec:library:pta, tag=models tga short=TGA, long=timed game
automaton, short-plural=s, long-plural-form=timed game automata, cite=MPS95,
tag=models pga short=PGA, long=parametric timed game automaton, short-
plural=s, long-plural-form=parametric timed game automata, cite=JLR19,
tag=models probTA short=PrTA, long=probabilistic timed automaton, short-
plural=s, long-plural-form=probabilistic timed automata, cite=Beauquier03,
tag=models lts short=LTS, long=labeled transition system, short-plural=s,
long-plural-form=labeled transition systems, short-indefinite=an, long-
indefinite=a, cite=Keller76, extra=LABEL:def:LTS, tag=models dfa short=DFA,
long=deterministic finite-state automaton, short-plural=s, long-plural-
form=deterministric finite-state automata, extra=LABEL:def:DFA, tag=models tts
short=TTS, long=timed transition system, short-plural=s, long-plural-
form=timed transition systems, cite=HMP91, extra=LABEL:def:TTS, tag=models era
short=ERA, long=event-recording automaton, short-plural=s, long-plural-
form=event-recording automata, cite=AFH99, tag=models rta short=RTA,
long=real-time automaton, short-plural=s, long-plural-form=real-time automata,
tag=models pn short=PN, long=Petri net, short-plural=s, long-plural-form=Petri
nets, cite=Pet62, tag=models ha short=HA, long=hybrid automaton, short-
plural=s, long-plural-form=hybrid automata, cite=Henzinger96, tag=models mra
short=MRA, long=multi-rate automaton, short-plural=s, long-plural-form=multi-
rate automata, cite=ACHHHNOSY95, tag=models pzg short=PZG, long=parametric
zone graph, extra=LABEL:def:PTA:symbolic, tag=misc opacity short=ET-opacity,
long=execution-time opacity, tag=notion, extra=7, post=opaque opaque short=ET-
opaque, long=execution-time opaque, tag=notion, post=opacity tempopacity
short=exp-*opacity, long=expiring *opacity, tag=notion, extra=11,
post=tempopaque tempopaque short=exp-*opaque, long=expiring *opaque,
tag=notion, post=tempopacity

# Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed
Automata††thanks: 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).

Étienne André Université Sorbonne Paris Nord, LIPN, CNRS UMR 7030
F-93430 Villetaneuse, FranceUniversité de Lorraine, CNRS, Inria, LORIA
F-54000 Nancy, FranceNantes Université, École Centrale Nantes, CNRS, LS2N, UMR
6004
F-44000 Nantes, FranceUniversité de Lorraine, CNRS, Inria, LORIA
F-54000 Nancy, FranceSchool of Computing and Information Systems
Singapore Management University Engel Lefaucheux Université de Lorraine, CNRS,
Inria, LORIA
F-54000 Nancy, FranceNantes Université, École Centrale Nantes, CNRS, LS2N, UMR
6004
F-44000 Nantes, FranceUniversité de Lorraine, CNRS, Inria, LORIA
F-54000 Nancy, FranceSchool of Computing and Information Systems
Singapore Management University Didier Lime Nantes Université, École Centrale
Nantes, CNRS, LS2N, UMR 6004
F-44000 Nantes, FranceUniversité de Lorraine, CNRS, Inria, LORIA
F-54000 Nancy, FranceSchool of Computing and Information Systems
Singapore Management University Dylan Marinho Université de Lorraine, CNRS,
Inria, LORIA
F-54000 Nancy, FranceSchool of Computing and Information Systems
Singapore Management University Jun Sun School of Computing and Information
Systems
Singapore Management University

###### Abstract

Timing information leakage occurs whenever an attacker successfully deduces
confidential internal information by observing some timed information such as
events with timestamps. Timed automata are an extension of finite-state
automata with a set of clocks evolving linearly and that can be tested or
reset, making this formalism able to reason on systems involving concurrency
and timing constraints. In this paper, we summarize a recent line of works
using timed automata as the input formalism, in which we assume that the
attacker has access (only) to the system execution time. First, we address the
following execution-time opacity problem: given a timed system modeled by a
timed automaton, given a secret location and a final location, synthesize the
execution times from the initial location to the final location for which one
cannot deduce whether the secret location was visited. This means that for any
such execution time, the system is opaque: either the final location is not
reachable, or it is reachable with that execution time for both a run visiting
and a run not visiting the secret location. We also address the full
execution-time opacity problem, asking whether the system is opaque for all
execution times; we also study a weak counterpart. Second, we add timing
parameters, which are a way to configure a system: we identify a subclass of
parametric timed automata with some decidability results. In addition, we
devise a semi-algorithm for synthesizing timing parameter valuations
guaranteeing that the resulting system is opaque. Third, we report on problems
when the secret has itself an expiration date, thus defining expiring
execution-time opacity problems. We finally show that our method can also
apply to program analysis with configurable internal timings.

##  1 Introduction

Complex timed systems often combine hard real-time constraints with
concurrency. Information leakage, notably through side channels (see, e.g.,
[24, 32]), can have dramatic consequences on the security of such systems.
Among harmful information leaks, the _timing information leakage_ (see, e.g.,
[23, 26, 39, 34, 36]) is the ability for an attacker to deduce internal
information depending on observable timing information. In this paper, we
focus on timing leakage through the total execution time, i.e., when a system
works as an almost black-box and the ability of the attacker is limited to
know the model and observe the total execution time. We consider here the
formalism of ta, which is a popular extension of finite-state automata with
clocks measuring time, i.e., variables evolving linearly at the same rate.
Such clocks can be tested against integer constants in locations
(“invariants”) or along transitions (“guards”), and can be reset to $0$ when
taking transitions.

##### Context and related works

Franck Cassez proposed in [20] a first definition of _timed_ opacity for ta:
the system is opaque if an attacker can never deduce whether some sequence of
actions (possibly with timestamps) was performed, by only observing a given
set of observable actions together with their timestamp. It is then proved in
[20] that it is undecidable whether a ta is opaque, even for the restricted
class of event-recording automata [3] (a subclass of ta). This notably relates
to the undecidability of timed language inclusion for ta [2]. Security
problems for ta are surveyed in [14].

The aforementioned negative result leaves hope only if the definition or the
setting is changed, which was done in three main lines of works. The different
studied options were to reduce the expressiveness of the formalism [37, 38],
to constrain the system to evolve in a time-bounded setting [5] or to consider
a weaker attacker, who has access only to the _execution time_ [10, 9], rather
than to all observable actions with their timestamps. We present here a
summary of our recent works in this latter setting [10, 9].

##### Contributions

In the setting of ta, we denote by _execution time_ the time from the system
start to the time a given (final) location is entered. Therefore, given a
secret location, a ta is opaque for an execution time $d$ if there exist at
least two runs of duration $d$ from the initial location to a final location:
one visiting the secret location, and another one _not_ visiting the secret
location. In other words, if an attacker measures such an execution time from
the initial location to the target location $\mathrm{\mathrm{\ell}_{f}}$, then
this attacker is not able to deduce whether the system visited
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$. Deciding whether at least one such
$d$ exists can be seen as an _existential_ version of opacity (called
$\exists$-*opacity).

Then, a ta is _fully *opaque_ if it is opaque _for all execution times_ : that
is, for each possible execution time $d$, either the final location is
unreachable, or the final location is reachable for at least two runs, one
visiting the secret location, and another one not visiting it. We define a
_weak_ version of opacity by only requiring that runs visiting the secret
location on the way to the final location have a counterpart of the same
duration not visiting the secret location on the way to the final location,
but not necessarily the opposite: the ta is _weakly opaque_ if for each run
visiting the secret location, there exists a run not visiting it with the same
duration; the dual does not necessarily hold.

We also consider an _expiring version_ of opacity, where the secret is subject
to an expiration date $\Delta$. That is, we consider that an attack is
successful only when the attacker can decide that the secret location was
visited less than $\Delta$ time units before the system completion.
Conversely, if the attacker exhibits an execution time $d$ for which it is
certain that the secret location was visited, but this location was visited
strictly more than $\Delta$ time units prior to the system completion, then
this attack is useless, and can be seen as a failed attack. The system is
therefore _fully expiring opaque_ if the set of execution times for which the
private location was visited within $\Delta$ time units prior to system
completion (referred as “secret times”) is exactly equal to the set of
execution times for which the private location was either not visited or
visited more than $\Delta$ time units prior to system completion (referred as
“non-secret times”). Moreover, it is _weakly expiring opaque_ when the
inclusion of the secret times into the non-secret ones is verified—and not
necessarily the dual.

Finally, we study the aforementioned problems for a _parametric_ extension of
ta, i.e., pta, where integer constants compared to clocks can be made
(rational-valued) timing parameters, i.e., unknown constants. Interesting
problems include emptiness problems, i.e., the emptiness of the parameter
valuations set such that (expiring) opacity holds, and synthesis, i.e., the
synthesis of all parameter valuations such that (expiring) opacity holds.

##### About this manuscript

This manuscript mainly summarizes results from two recent works, providing
unified notations and concept names for the sake of consistency:

  1. 1.

defining and studying opacity problems [10] in ta (Section 3) and pta (Section
4); these notions from [10] are presented differently (including the problem
names) in this paper for sake of consistency; and

  2. 2.

defining and studying tempopacity problems [9] in both ta and pta (Section 5).

In addition, we prove a few original results on weak *opacity (that were not
addressed in [10] because we had not yet defined the concept of weak *opacity
when writing [10]) and on tempopacity. These original results are Propositions
2, 4, 5, 6 and 9.

In Tables 1 and 2, we summarize the decidability results recalled in this
paper for opacity and tempopacity. We denote a problem with a green check if
it is decidable, with a red cross if it is undecidable, and with a yellow
question mark if it is open (or not considered in the aforementioned papers
[10, 9]). We emphasize using a bold font the original results of this paper.
The p-emptiness (resp. p-synthesis) problem asks for the synthesis (resp. for
the non-existence) of a parameter valuation for which opacity is enforced. The
$\Delta$-p-synthesis (resp. emptiness) problem asks for the synthesis (resp.
for the non-existence) of a parameter valuation and an expiring bound $\Delta$
for which the tempopacity is enforced. L/U-PTA denote the lower-bound/upper-
bound parametric timed automata [28] subclass of pta. These notions will be
formally defined in the paper.

Table 1: Summary of the results for opacity [10] |  $\exists$-*opaque |  weakly *opaque |  fully *opaque
---|---|---|---
Decision |  ta |  $\surd$(Proposition 2) |  $\surd$(Proposition 4) |  $\surd$(Proposition 3)
p-emptiness |  lupta |  $\surd$(Theorem 2) |  $\times$(Theorem 6) |  $\times$(Theorem 4)
pta |  $\times$(Theorem 1) |  $\times$(Theorem 5) |  $\times$(Theorem 3)
p-synthesis |  lupta |  $\times$(Proposition 5) |  $\times$(Corollary 5) |  $\times$(Corollary 3)
pta |  $\times$(Corollary 1) |  $\times$(Corollary 4) |  $\times$(Corollary 2)
Table 2: Summary of the results for tempopacity [9] |  $\exists$-*tempopaque |  weakly *tempopaque |  fully *tempopaque
---|---|---|---
Decision |  ta |  $\surd$(Theorem 9) |  $\surd$(Theorem 8) |  $\surd$(Theorem 8)
$\Delta$-emptiness | TA |  $?$ |  $\surd$(Corollary 6) |  $\surd$(Theorem 11)
$\Delta$-computation |  $?$ |  $\surd$(Theorem 10) |  $?$
$\Delta$-p-emptiness | L/U-PTA |  $?$ |  $\times$(Theorem 12) |  $\times$(Theorem 12)
PTA |  $?$ |  $\times$(Theorem 13) |  $\times$(Theorem 13)
$\Delta$-p-synthesis | L/U-PTA |  $?$ |  $\times$(Corollary 7) |  $\times$(Theorem 12)
PTA |  $?$ |  $\times$(Corollary 8) |  $\times$(Corollary 8)

##### Outline

Section 2 recalls the necessary preliminaries, notably (parametric) timed
automata. Section 3 defines and reviews execution-time opacity problems in
timed automata. Section 4 defines and reviews execution-time opacity problems
in timed automata. Section 5 defines and reviews _expiring_ execution-time
opacity problems in (parametric) timed automata. Section 6 briefly reports on
our existing implementation of some of the problems using the parametric timed
model checker IMITATOR [7]. Section 7 concludes the paper and reports on
perspectives.

##  2 Preliminaries

We denote by $\mathbb{N},\mathbb{Z},\mathbb{Q}_{\geq 0},\mathbb{R}_{\geq 0}$
the sets of non-negative integers, integers, non-negative rationals and non-
negative reals, respectively.

###  2.1 Clocks, parameters and constraints

_Clocks_ are real-valued variables that all evolve over time at the same rate.
Throughout this paper, we assume a set
$\mathbb{X}=\\{\mathit{\mathit{x}_{1}},\dots,\mathit{\mathit{x}_{H}}\\}$ of
_clocks_. A _clock valuation_ is a function
$\mu:\mathbb{X}\rightarrow\mathbb{R}_{\geq 0}$, assigning a non-negative value
to each clock. We write $\vec{0}$ for the clock valuation assigning $0$ to all
clocks. Given a constant $d\in\mathbb{R}_{\geq 0}$, $\mu+d$ denotes the
valuation s.t. $(\mu+d)(\mathit{x})=\mu(\mathit{x})+d$, for all
$\mathit{x}\in\mathbb{X}$.

A _(timing) parameter_ is an unknown rational-valued constant of a model.
Throughout this paper, we assume a set
$\mathbb{P}=\\{{{p}_{1}},\dots,{{p}_{M}}\\}$ of _parameters_. A _parameter
valuation_ $v$ is a function $v:\mathbb{P}\rightarrow\mathbb{Q}_{\geq 0}$.

As often, we choose _real_ -valued clocks and _rational_ -valued parameters,
because irrational constants render reachability undecidable in ta [31] (see
[6] for a survey on the impact of these domains in (P)TAs).

We assume ${\bowtie}\in\\{<,\leq,=,\geq,>\\}$. A constraint $C$ is a
conjunction of inequalities over $\mathbb{X}\cup\mathbb{P}$ of the form
$\mathit{x}\bowtie\sum_{1\leq i\leq M}\alpha_{i}{{p}_{i}}+d$, with
${{p}_{i}}\in\mathbb{P}$, and $\alpha_{i},d\in\mathbb{Z}$. Given $C$, we write
$\mu\models v(C)$ if the expression obtained by replacing each $\mathit{x}$
with $\mu(\mathit{x})$ and each ${p}$ with $v({p})$ in $C$ evaluates to true.

###  2.2 Timed automata

A ta is a finite-state automaton extended with a finite set of real-valued
clocks. We also add to the standard definition of ta a special private
location, which will be used to define our subsequent opacity concepts.

######  Definition 1 (*ta [2]).

A ta $\mathcal{A}$ is a tuple
$\mathcal{A}=\left(\Sigma,L,\mathrm{\mathrm{\ell}_{0}},\mathrm{\mathrm{\ell}_{\mathit{priv}}},\mathrm{\mathrm{\ell}_{f}},\mathbb{X},I,E\right)$,
where:

  1. 1.

$\Sigma$ is a finite set of actions,

  2. 2.

$L$ is a finite set of locations,

  3. 3.

$\mathrm{\mathrm{\ell}_{0}}\in L$ is the initial location,

  4. 4.

$\mathrm{\mathrm{\ell}_{\mathit{priv}}}\in L$ is a special private location,

  5. 5.

$\mathrm{\mathrm{\ell}_{f}}\in L$ is the final location,

  6. 6.

$\mathbb{X}$ is a finite set of clocks,

  7. 7.

$I$ is the invariant, assigning to every $\mathrm{\ell}\in L$ a constraint
$I(\mathrm{\ell})$ over $\mathbb{X}$ (called _invariant_),

  8. 8.

$E$ is a finite set of edges
$e=(\mathrm{\ell},g,\mathit{a},R,\mathrm{\ell}^{\prime})$ where
$\mathrm{\ell},\mathrm{\ell}^{\prime}\in L$ are the source and target
locations, $\mathit{a}\in\Sigma$, $R\subseteq\mathbb{X}$ is a set of clocks to
be reset, and $g$ is a constraint over $\mathbb{X}$ (called _guard_).

$\mathrm{\mathrm{\ell}_{0}}$$\mathrm{\mathrm{\ell}_{2}}$$\mathrm{\mathrm{\ell}_{1}}$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq
3$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq
2$${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}{\mathit{a}}}$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\geq
1$${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}{\mathit{c}}}$${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}{\mathit{b}}}$
Figure 1: A *ta example

######  Example 1.

In Fig. 1, we give an example of a ta with three locations
$\mathrm{\mathrm{\ell}_{0}}$, $\mathrm{\mathrm{\ell}_{1}}$ and
$\mathrm{\mathrm{\ell}_{2}}$, three edges, three actions
$\left\\{a,b,c\right\\}$, and one clock $\mathit{x}$.
$\mathrm{\mathrm{\ell}_{0}}$ is the initial location,
$\mathrm{\mathrm{\ell}_{2}}$ is the private location, while
$\mathrm{\mathrm{\ell}_{1}}$ is the final location.
$\mathrm{\mathrm{\ell}_{0}}$ has an invariant
${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq
3$ and the edge from $\mathrm{\mathrm{\ell}_{0}}$ to
$\mathrm{\mathrm{\ell}_{2}}$ has a guard
${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\geq
1$.

##### Concrete semantics of timed automata

We recall the concrete semantics of a ta using a tts.

######  Definition 2 (Semantics of a *ta).

Given a ta
$\mathcal{A}=\left(\Sigma,L,\mathrm{\mathrm{\ell}_{0}},\mathrm{\mathrm{\ell}_{\mathit{priv}}},\mathrm{\mathrm{\ell}_{f}},\mathbb{X},I,E\right)$,
the semantics of $\mathcal{A}$ is given by the tts
$\mathfrak{T}_{\mathcal{A}}=\left(\mathfrak{S},\mathfrak{s}_{0},\Sigma\cup\mathbb{R}_{\geq
0},{\rightarrow}\right)$, with

  1. 1.

$\mathfrak{S}=\\{(\mathrm{\ell},\mu)\in L\times\mathbb{R}_{\geq
0}^{H}\mid\mu\models I(\mathrm{\ell}){v}\\}$,

  2. 2.

$\mathfrak{s}_{0}=(\mathrm{\mathrm{\ell}_{0}},\vec{0})$,

  3. 3.

${\rightarrow}$ consists of the discrete and (continuous) delay transition
relations:

    1. (a)

discrete transitions: $(\mathrm{\ell},\mu)\stackrel{{\scriptstyle
e}}{{\mapsto}}(\mathrm{\ell}^{\prime},\mu^{\prime})$, if
$(\mathrm{\ell},\mu),(\mathrm{\ell}^{\prime},\mu^{\prime})\in\mathfrak{S}$,
and there exists $e=(\mathrm{\ell},g,\mathit{a},R,\mathrm{\ell}^{\prime})\in
E$, such that $\mu^{\prime}=[\mu]_{R}$, and $\mu\models v(g$).

    2. (b)

delay transitions: $(\mathrm{\ell},\mu)\stackrel{{\scriptstyle
d}}{{\mapsto}}(\mathrm{\ell},\mu+d)$, with $d\in\mathbb{R}_{\geq 0}$, if
$\forall d^{\prime}\in[0,d],(\mathrm{\ell},\mu+d^{\prime})\in\mathfrak{S}$.

Moreover we write
$(\mathrm{\ell},\mu)\stackrel{{\scriptstyle(d,e)}}{{\longrightarrow}}(\mathrm{\ell}^{\prime},\mu^{\prime})$
for a combination of a delay and discrete transition if
$\exists\mu^{\prime\prime}:(\mathrm{\ell},\mu)\stackrel{{\scriptstyle
d}}{{\mapsto}}(\mathrm{\ell},\mu^{\prime\prime})\stackrel{{\scriptstyle
e}}{{\mapsto}}(\mathrm{\ell}^{\prime},\mu^{\prime})$.

Given a TA $\mathcal{A}$ with concrete semantics
$\left(\mathfrak{S},\mathfrak{s}_{0},\Sigma\cup\mathbb{R}_{\geq
0},{\rightarrow}\right)$, we refer to the states of $\mathfrak{S}$ as the
_concrete states_ of $\mathcal{A}$. A _run_ of $\mathcal{A}$ is an alternating
sequence of concrete states of $\mathcal{A}$ and pairs of edges and delays
starting from the initial state $\mathfrak{s}_{0}$ of the form
$(\mathrm{\mathrm{\ell}_{0}},\mu_{0}),(d_{0},e_{0}),(\mathrm{\mathrm{\ell}_{1}},\mu_{1}),\cdots$
with $i=0,1,\dots$, $e_{i}\in E$, $d_{i}\in\mathbb{R}_{\geq 0}$ and
$(\mathrm{\mathrm{\ell}_{i}},\mu_{i})\stackrel{{\scriptstyle(d_{i},e_{i})}}{{\longrightarrow}}(\mathrm{\mathrm{\ell}_{i+1}},\mu_{i+1})$.

######  Definition 3 (Duration of a run).

Given a finite run
$\rho:(\mathrm{\mathrm{\ell}_{0}},\mu_{0}),(d_{0},e_{0}),(\mathrm{\mathrm{\ell}_{1}},\mu_{1}),\cdots,(d_{i-1},e_{i-1}),(\mathrm{\mathrm{\ell}_{n}},\mu_{n})$,
the _duration_ of $\rho$ is $\mathit{dur}(\rho)=\sum_{0\leq i\leq n-1}d_{i}$.
We also say that $\mathrm{\mathrm{\ell}_{n}}$ is reachable in time
$\mathit{dur}(\rho)$.

######  Example 2.

Consider again the ta $\mathcal{A}$ in Fig. 1. Consider the following run
$\rho$ of $\mathcal{A}$:
$(\mathrm{\mathrm{\ell}_{0}},\mathit{x}=0),(1.4,a),(\mathrm{\mathrm{\ell}_{2}},\mathit{x}=1.4),(0.4,b),(\mathrm{\mathrm{\ell}_{1}},\mathit{x}=1.8)$
Note that we write “$\mathit{x}=1.4$” instead of “$\mu$ such that
$\mu(\mathit{x})=1.4$”. We have $\mathit{dur}(\rho)=1.4+0.4=1.8$.

###  2.3 Parametric timed automata

A pta is a ta extended with a finite set of timing parameters allowing to
model unknown constants.

######  Definition 4 (*pta [4]).

A pta $\mathcal{P}$ is a tuple
$\mathcal{P}=\left(\Sigma,L,\mathrm{\mathrm{\ell}_{0}},\mathrm{\mathrm{\ell}_{\mathit{priv}}},\mathrm{\mathrm{\ell}_{f}},\mathbb{X},\mathbb{P},I,E\right)$,
where:

  1. 1.

$\Sigma$ is a finite set of actions;

  2. 2.

$L$ is a finite set of locations;

  3. 3.

$\mathrm{\mathrm{\ell}_{0}}\in L$ is the initial location;

  4. 4.

$\mathrm{\mathrm{\ell}_{\mathit{priv}}}\in L$ is a special private location,

  5. 5.

$\mathrm{\mathrm{\ell}_{f}}\in L$ is the final location;

  6. 6.

$\mathbb{X}$ is a finite set of clocks;

  7. 7.

$\mathbb{P}$ is a finite set of parameters;

  8. 8.

$I$ is the invariant, assigning to every $\mathrm{\ell}\in L$ a constraint
$I(\mathrm{\ell})$ over $\mathbb{X}\cup\mathbb{P}$ (called _invariant_);

  9. 9.

$E$ is a finite set of edges
$e=(\mathrm{\ell},g,\mathit{a},R,\mathrm{\ell}^{\prime})$ where
$\mathrm{\ell},\mathrm{\ell}^{\prime}\in L$ are the source and target
locations, $\mathit{a}\in\Sigma$, $R\subseteq\mathbb{X}$ is a set of clocks to
be reset, and $g$ is a constraint over $\mathbb{X}\cup\mathbb{P}$ (called
_guard_).

$\mathrm{\mathrm{\ell}_{0}}$$\mathrm{\mathrm{\ell}_{2}}$$\mathrm{\mathrm{\ell}_{1}}$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq
3$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{p}_{2}}}}$${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}{\mathit{a}}}$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\geq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{p}_{1}}}}$${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}{\mathit{c}}}$${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}{\mathit{b}}}$
Figure 2: A *pta example

######  Example 3.

In Fig. 2, we give an example of a pta with three locations
$\mathrm{\mathrm{\ell}_{0}}$, $\mathrm{\mathrm{\ell}_{1}}$ and
$\mathrm{\mathrm{\ell}_{2}}$, three edges, three actions
$\left\\{a,b,c\right\\}$, one clock $\mathit{x}$ and two parameters
$\left\\{{{p}_{1}},{{p}_{2}}\right\\}$. $\mathrm{\mathrm{\ell}_{0}}$ is the
initial location, $\mathrm{\mathrm{\ell}_{2}}$ is the private location, while
$\mathrm{\mathrm{\ell}_{1}}$ is the final location.
$\mathrm{\mathrm{\ell}_{0}}$ has an invariant
${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq
3$ and the edge from $\mathrm{\mathrm{\ell}_{0}}$ to
$\mathrm{\mathrm{\ell}_{2}}$ has a guard
${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\geq{{p}_{1}}$.

######  Definition 5 (Valuation of a *pta).

Given a parameter valuation $v$, we denote by $v(\mathcal{P})$ the non-
parametric structure where all occurrences of a parameter ${{p}_{i}}$ have
been replaced by $v({{p}_{i}})$.

######  Remark 1.

We have a direct correspondence between the valuation of a pta and the
definition of a ta given in Definition 1. ta were originally defined with
integer constants in [2] (as done in Definition 1), while our definition of
pta allows _rational_ -valued constants. By assuming a rescaling of the
constants (i.e., by multiplying all constants in a ta by the least common
multiple of their denominators), we obtain an equivalent (integer-valued) ta,
as defined in Definition 1. So we assume in the following that
$v(\mathcal{P})$ is a ta.

######  Example 4.

Consider again the pta in Fig. 2 and let $v$ be such that $v({{p}_{1}})=1$ and
$v({{p}_{2}})=2$. Then $v(\mathcal{P})$ is the ta depicted in Fig. 1.

#####  *lupta

While most decision problems are undecidable for the general class of pta (see
[6] for a survey), lupta is the most well-known subclass of pta with some
decidability results: for example, reachability-emptiness (“the emptiness of
the valuations set for which a given location is reachable”), which is
undecidable for pta [4], becomes decidable for lupta [28]. Various other
results were studied for this subclass (e.g., [18, 29, 13]).

######  Definition 6 (*lupta [28]).

lupta is a pta where the set of parameters is partitioned into lower-bound
parameters and upper-bound parameters, where each upper-bound (resp. lower-
bound) parameter ${{p}_{i}}$ must be such that, for every guard or invariant
constraint $\mathit{x}\bowtie\sum_{1\leq i\leq M}\alpha_{i}{{p}_{i}}+d$, we
have:

  * •

${\bowtie}\in\left\\{\leq,<\right\\}$ implies $\alpha_{i}\geq 0$ (resp.
$\alpha_{i}\leq 0$), and

  * •

${\bowtie}\in\left\\{\geq,>\right\\}$ implies $\alpha_{i}\leq 0$ (resp.
$\alpha_{i}\geq 0$).

######  Example 5.

The pta in Fig. 2 is lupta with $\left\\{{{p}_{1}}\right\\}$ as lower-bound
parameter set, and $\left\\{{{p}_{2}}\right\\}$ as upper-bound parameter set.

##  3 Execution-time opacity problems in timed automata

Throughout this paper, the attacker model is as follows: the attacker knows
the ta modeling the system, and can only observe the execution time between
the start of the system and the time it reaches the final location. The
attacker cannot observe actions, nor the values of the clocks, nor whether
some locations are visited. Its goal will be to deduce from its observations
whether the private location was visited.

###  3.1 Defining the execution times

Let us first introduce two key concepts necessary to define our notion of
execution-time opacity.

Given a ta $\mathcal{A}$ and a run $\rho$, we say that
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ is _visited on the way to
$\mathrm{\mathrm{\ell}_{f}}$ in $\rho$_ if $\rho$ is of the form

$(\mathrm{\mathrm{\ell}_{0}},\mu_{0}),(d_{0},e_{0}),(\mathrm{\mathrm{\ell}_{1}},\mu_{1}),\cdots,(\mathrm{\mathrm{\ell}_{m}},\mu_{m}),(d_{m},e_{m}),\cdots(\mathrm{\mathrm{\ell}_{n}},\mu_{n})$

for some $m,n\in\mathbb{N}$ such that
$\mathrm{\mathrm{\ell}_{m}}=\mathrm{\mathrm{\ell}_{\mathit{priv}}}$,
$\mathrm{\mathrm{\ell}_{n}}=\mathrm{\mathrm{\ell}_{f}}$ and $\forall 0\leq
i\leq n-1,\mathrm{\mathrm{\ell}_{i}}\neq\mathrm{\mathrm{\ell}_{f}}$. We denote
by $\mathit{Visit}^{\mathit{priv}}(\mathcal{A})$ the set of those runs, and
refer to them as _private_ runs. We denote by
$\mathit{DVisit}^{\mathit{priv}}(\mathcal{A})$ the set of all the durations of
these runs.

Conversely, we say that $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ is _avoided
on the way to $\mathrm{\mathrm{\ell}_{f}}$ in $\rho$_ if $\rho$ is of the form

$(\mathrm{\mathrm{\ell}_{0}},\mu_{0}),(d_{0},e_{0}),(\mathrm{\mathrm{\ell}_{1}},\mu_{1}),\cdots,(\mathrm{\mathrm{\ell}_{n}},\mu_{n})$

with $\mathrm{\mathrm{\ell}_{n}}=\mathrm{\mathrm{\ell}_{f}}$ and $\forall
0\leq
i<n,\mathrm{\mathrm{\ell}_{i}}\notin\left\\{\mathrm{\mathrm{\ell}_{\mathit{priv}}},\mathrm{\mathrm{\ell}_{f}}\right\\}$.
We denote the set of those runs by
$\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A})$, referring to them as
_public_ runs, and by
$D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A})$ the set of all the
durations of these public runs.

Therefore, $\mathit{DVisit}^{\mathit{priv}}(\mathcal{A})$ (resp.
$D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A})$) is the set of all
the durations of the runs for which $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$
is visited (resp. avoided) on the way to $\mathrm{\mathrm{\ell}_{f}}$.

These concepts can be seen as the set of execution times from the initial
location $\mathrm{\mathrm{\ell}_{0}}$ to the final location
$\mathrm{\mathrm{\ell}_{f}}$ while visiting (resp. not visiting) a private
location $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$. Observe that, from the
definition of the duration of a run (Definition 3), this “execution time” does
not include the time spent in $\mathrm{\mathrm{\ell}_{f}}$.

######  Example 6.

Consider again the ta in Fig. 1. We have
$\mathit{DVisit}^{\mathit{priv}}(\mathcal{A})=[1,2]$ and
$D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A})=[0,3]$.

###  3.2 Defining execution-time opacity

We now introduce formally the concept of “opacity for a set of durations (or
execution times) $D$”: a system is _opaque for execution times $D$_ whenever,
for any duration in $D$, it is not possible to deduce whether the system
visited $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ or not. In other words, if an
attacker measures an execution time within $D$ from the initial location to
the target location $\mathrm{\mathrm{\ell}_{f}}$, then this attacker is not
able to deduce whether the system visited
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$.

######  Definition 7 (*opacity for $D$).

Given a ta $\mathcal{A}$ and a set of execution times $D$, we say that
$\mathcal{A}$ is _*opaque for execution times $D$_ if
$D\subseteq(\mathit{DVisit}^{\mathit{priv}}(\mathcal{A})\cap
D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A}))$.

In the following, we will be interested in the existence of such an execution
time. We say that a ta is $\exists$-*opaque if it is opaque for a non-empty
set of execution times.

######  Definition 8 ($\exists$-*opacity).

A ta $\mathcal{A}$ is _$\exists$ -*opaque_ if
$(\mathit{DVisit}^{\mathit{priv}}(\mathcal{A})\cap
D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A}))\neq\emptyset$.

If one does not have the ability to tune the system (i.e., change internal
delays, or add some Thread.sleep() statements in a program), one may be first
interested in knowing whether the system is opaque for all execution times. In
other words, if a system is _fully *opaque_ , for any possible measured
execution time, an attacker is not able to deduce whether
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ was visited or not.

######  Definition 9 (full *opacity).

A ta $\mathcal{A}$ is _fully *opaque_ if
$\mathit{DVisit}^{\mathit{priv}}(\mathcal{A})=D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A})$.

That is, a system is fully *opaque if, for any execution time ${d}$, a run of
duration ${d}$ reaches $\mathrm{\mathrm{\ell}_{f}}$ after visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ iff another run of duration ${d}$
reaches $\mathrm{\mathrm{\ell}_{f}}$ without visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$.

######  Remark 2.

This definition is symmetric: a system is not fully *opaque iff an attacker
can deduce $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ or
$\neg\mathrm{\mathrm{\ell}_{\mathit{priv}}}$. For instance, if there is no run
to $\mathrm{\mathrm{\ell}_{f}}$ visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$, but still a run to
$\mathrm{\mathrm{\ell}_{f}}$ (not visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$), a system is not fully *opaque
w.r.t. Definition 9.

We finally define weak *opacity, not considered in [10], but defined in the
specific context of expiring opacity [9]. We therefore reintroduce this
definition in the “normal” opacity setting considered in this section, in the
following:

######  Definition 10 (weak *opacity).

A ta $\mathcal{A}$ is _weakly *opaque_ if
$\mathit{DVisit}^{\mathit{priv}}(\mathcal{A})\subseteq
D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A})$.

That is, a ta is weakly *opaque whenever, for any run reaching the final
location after visiting the private location, there exists another run of the
same duration reaching the final location but not visiting the private
location; but the converse does not necessarily hold.

######  Remark 3.

Our notion of weak *opacity may still leak some information: on the one hand,
if a run indeed visits the private location, there exists an equivalent run
not visiting it, and therefore the system is opaque; _but_ on the other hand,
there may exist execution times for which the attacker can deduce that the
private location was _not_ visited. This remains acceptable in some cases, and
this motivates us to define a weak version of opacity. Also note that the
“initial-state opacity” for real-time automata considered in [37] can also be
seen as _weak_ in the sense that their language inclusion is also
unidirectional.

######  Example 7.

Consider again the pta $\mathcal{P}$ in Fig. 2 and let $v$ such that
$v({{p}_{1}})=1$ while $v({{p}_{2}})=2$ (i.e., the ta in Fig. 1). Recall that
$\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}))=[1,2]$ and
$D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}))=[0,3]$. Hence, it
holds that $\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}))\subseteq
D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}))$ and therefore
$v(\mathcal{P})$ is weakly *opaque. However,
$\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}))\neq
D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}))$ and therefore
$v(\mathcal{P})$ is not fully *opaque.

Now consider again the pta $\mathcal{P}$ in Fig. 2 and let $v^{\prime}$ such
that $v^{\prime}({{p}_{1}})=0$ while $v^{\prime}({{p}_{2}})=3$. This time,
$\mathit{DVisit}^{\mathit{priv}}(v^{\prime}(\mathcal{P}))=D\overline{\mathit{Visit}}^{\mathit{priv}}(v^{\prime}(\mathcal{P}))=[0,3]$
and therefore $v^{\prime}(\mathcal{P})$ is fully *opaque.

###  3.3 Decision and computation problems

####  3.3.1 Computation problem for opacity

We can now define the *opacity t-computation problem, which consists in
computing the possible execution times ensuring opacity.

*opacity t-computation problem:
Input: A ta $\mathcal{A}$ Problem: Compute the execution times $D$ such that
$\mathcal{A}$ is opaque for $D$.

Let us illustrate that this computation problem is certainly not easy. For the
ta $\mathcal{A}$ in Fig. 3, the execution times $D$ for which $\mathcal{A}$ is
opaque is exactly $\mathbb{N}$; that is, only integer times ensure opacity (as
the system can only leave $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ and hence
enter $\mathrm{\mathrm{\ell}_{f}}$ at an integer time), while non-integer
times violate opacity.

$\mathrm{\mathrm{\ell}_{0}}$$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$$\mathrm{\mathrm{\ell}_{f}}$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=0$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=1$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leftarrow
0$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=0$
Figure 3: *ta for which the set of execution times ensuring opacity is
$\mathbb{N}$

####  3.3.2 Decision problems

We define the three following decision problems:

$\exists$-*opacity decision problem:
Input: A ta $\mathcal{A}$ Problem: Is $\mathcal{A}$ $\exists$-*opaque?

Full *opacity decision problem:
Input: A ta $\mathcal{A}$ Problem: Is $\mathcal{A}$ fully *opaque?

Weak *opacity decision problem:
Input: A ta $\mathcal{A}$ Problem: Is $\mathcal{A}$ weakly *opaque?

###  3.4 Answering the *opacity t-computation problem

######  Proposition 1 (Solvability of the *opacity t-computation problem [10,
Proposition 5.2]).

The *opacity t-computation problem is solvable for ta.

This positive result can be put in perspective with the negative result of
[20] that proves that it is undecidable whether a ta (and even the more
restricted subclass of era) is opaque, in a sense that the attacker can deduce
some actions, by looking at observable actions together with their timing. The
difference in our setting is that only the global time is observable, which
can be seen as a single action, occurring once only at the end of the
computation. In other words, our attacker is less powerful than the attacker
in [20].

###  3.5 Checking for $\exists$-*opacity

The following result was not strictly speaking proved in [10], and we provide
here an original proof for it.

######  Proposition 2 (Decidability of the $\exists$-*opacity decision
problem).

The $\exists$-*opacity decision problem is decidable in 5EXPTIME for ta.

###### Proof.

Let $\mathcal{A}$ be a ta. Suppose we add a Boolean variable ${\mathit{priv}}$
to $\mathcal{A}$ which is initially false and set to true on every edge going
into the location $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$. This Boolean
variable (not strictly part of the ta syntax) can also be simulated by adding
a copy of $\mathcal{A}$ instead, and jumping to that copy on edges going into
location $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$.

Then the $\exists$-*opacity decision problem amounts to checking the following
parametric TCTL formula [19], with ${p}$ a parameter:

$\exists{p}\big{(}\exists\Diamond_{={p}}(\mathrm{\mathrm{\ell}_{f}}\wedge{\mathit{priv}})\wedge\exists\Diamond_{={p}}(\mathrm{\mathrm{\ell}_{f}}\wedge\neg{\mathit{priv}})\big{)}$

From [19], this can be checked in 5EXPTIME, since the size of the ta it is
checked on is at most twice that of $\mathcal{A}$, and the size of the formula
is constant w.r.t. the size of $\mathcal{A}$. ∎

###  3.6 Checking for full *opacity

The following result matches [10, Proposition 5.3] but we provide an original
proof, also fixing a complexity issue in [10, Proposition 5.3].

######  Proposition 3 (Decidability of the full *opacity decision problem).

The full *opacity decision problem is decidable in 5EXPTIME for ta.

###### Proof.

As before, we can write a parametric TCTL formula for this problem, with ${p}$
a parameter:

$\forall{p}\big{(}\exists\Diamond_{={p}}(\mathrm{\mathrm{\ell}_{f}}\wedge{\mathit{priv}})\Leftrightarrow\exists\Diamond_{={p}}(\mathrm{\mathrm{\ell}_{f}}\wedge\neg{\mathit{priv}})\big{)}$

This formula can be checked in 5EXPTIME [19]. ∎

###  3.7 Checking for weak *opacity

The _weak_ notion of opacity had not been defined in [10]. Nevertheless, the
proof of Proposition 3 can be adapted in a very straightforward manner to
prove its weak counterpart as follows:

######  Proposition 4 (Decidability of the weak *opacity decision problem).

The weak *opacity decision problem is decidable in 5EXPTIME for ta.

###### Proof.

Let $\mathcal{A}$ be a ta. As before, we can write a parametric TCTL formula
for this problem, with ${p}$ a parameter:

$\forall{p}\big{(}\exists\Diamond_{={p}}(\mathrm{\mathrm{\ell}_{f}}\wedge{\mathit{priv}})\Rightarrow\exists\Diamond_{={p}}(\mathrm{\mathrm{\ell}_{f}}\wedge\neg{\mathit{priv}})\big{)}$

This formula can be checked in 5EXPTIME [19]. ∎

##  4 Execution-time opacity problems in parametric timed automata

We now extend opacity problems to parametric timed automata. We first address
the parametric problems related to $\exists$-*opacity in Section 4.1. The
decision problems associated to full *opacity and weak *opacity will then be
considered in Sections 4.2 and 4.3 respectively.

Following the usual concepts for parametric timed automata, we consider both
_emptiness_ and _synthesis_ problems. An emptiness problem aims at _deciding_
whether the set of parameter valuations for which a given property holds in
the valuated ta is empty, while a synthesis problem aims at _synthesizing_ the
set of parameter valuations for which a given property holds in the valuated
ta.

###  4.1 $\exists$-*opacity

####  4.1.1 Problems

##### Emptiness problem for $\exists$-*opacity

Let us consider the following decision problem, i.e., the problem of checking
the _emptiness_ of the set of parameter valuations guaranteeing
$\exists$-*opacity.

$\exists$-*opacity p-emptiness problem:
Input: A pta $\mathcal{P}$ Problem: Decide the emptiness of the set of
parameter valuations $v$ such that $v(\mathcal{P})$ is $\exists$-*opaque.

The negation of the $\exists$-*opacity p-emptiness problem consists in
deciding whether there exists at least one parameter valuation for which
$v(\mathcal{P})$ is $\exists$-*opaque.

##### Synthesis problem for $\exists$-*opacity

The synthesis counterpart allows for a higher-level problem by also
synthesizing the internal timings guaranteeing $\exists$-*opacity.

$\exists$-*opacity p-synthesis problem:
Input: A pta $\mathcal{P}$ Problem: Synthesize the set $V$ of parameter
valuations such that $v(\mathcal{P})$ is $\exists$-*opaque, for all $v\in V$.

####  4.1.2 Undecidability in general

With the rule of thumb that all non-trivial decision problems are undecidable
for general pta [6], the following result is not surprising, and follows from
the undecidability of reachability-emptiness for pta [4].

######  Theorem 1 (Undecidability of the $\exists$-*opacity p-emptiness
problem [10, Theorem 6.1]).

The $\exists$-*opacity p-emptiness problem is undecidable for general pta.

Since the emptiness problem is undecidable, the synthesis problem is
immediately unsolvable as well.

######  Corollary 1.

The $\exists$-*opacity p-synthesis problem is unsolvable for general pta.

Nevertheless, in [10] we proposed a procedure solving this problem. While this
procedure is not guaranteed to terminate, its result is correct when
termination can be achieved. See [10, Section 8] for details.

####  4.1.3 The subclass of lupta

##### Decidability

We now show that the $\exists$-*opacity p-emptiness problem is decidable for
lupta. Despite early positive results for lupta [28, 18], more recent results
(notably [29, 12, 13]) mostly proved undecidable properties of lupta, and
therefore this positive result is welcome.

######  Theorem 2 (Decidability of the $\exists$-*opacity p-emptiness problem
[10, Theorem 6.2]).

The $\exists$-*opacity p-emptiness problem is decidable for lupta.

##### Intractability of synthesis for *lupta

Even though the $\exists$-*opacity p-emptiness problem is decidable for lupta
(Theorem 2), the _synthesis_ of the parameter valuations remains intractable
in general, as shown in the following Proposition 5. By intractable we mean
more precisely that the solution, if it can be computed, cannot (in general,
i.e., for some sufficiently complex solutions) be represented using any
formalism for which the emptiness of the intersection with equality
constraints is decidable. That is, a formalism in which it is decidable to
decide “the emptiness of the valuation set of the computed solution
intersected with an equality test between variables” cannot be used to
represent the solution. For example, let us question whether we could
represent the solution of the $\exists$-*opacity p-synthesis problem for lupta
using the formalism of a _finite union of polyhedra_ : testing whether a
finite union of polyhedra intersected with “equality constraints” (typically
${{p}_{1}}={{p}_{2}}$) is empty or not _is_ decidable. The Parma polyhedra
library [15] can typically compute the answer to this question. Therefore,
from the following Proposition 5, finite unions of polyhedra cannot be used to
represent the solution of the $\exists$-*opacity p-synthesis problem for
lupta. As finite unions of polyhedra are a very common formalism (not to say
the _de facto_ standard) to represent the solutions of various timing
parameters synthesis problems, the synthesis is then considered to be
infeasible in practice, or _intractable_ (following the vocabulary used in
[29, Theorem 2]).

######  Proposition 5 (Intractability of the $\exists$-*opacity p-synthesis
problem [10, Proposition 6.4]).

In case a solution to the $\exists$-*opacity p-synthesis problem for lupta can
be computed, this solution may be not representable using any formalism for
which the emptiness of the intersection with equality constraints is
decidable.

###  4.2 Parametric full *opacity

We address here the following decision problem, which asks about the emptiness
of the parameter valuation set guaranteeing full *opacity. We also define the
full *opacity p-synthesis problem, this time _synthesizing_ the timing
parameters guaranteeing full *opacity.

####  4.2.1 Problem definitions

Full *opacity p-emptiness problem:
Input: A pta $\mathcal{P}$ Problem: Decide the emptiness of the set of
parameter valuations $v$ such that $v(\mathcal{P})$ is fully *opaque.

Equivalently, we are interested in deciding whether there exists at least one
parameter valuation for which $v(\mathcal{P})$ is fully *opaque.

We also define the _full *opacity p-synthesis problem_ , aiming at
synthesizing (ideally the entire set of) parameter valuations $v$ for which
$v(\mathcal{P})$ is fully *opaque.

Full *opacity p-synthesis problem:
Input: A pta $\mathcal{P}$ Problem: Synthesize the set $V$ of parameter
valuations such that $v(\mathcal{P})$ is fully *opaque, for all $v\in V$.

####  4.2.2 Undecidability for general PTAs

Considering that Theorem 1 shows the undecidability of the $\exists$-*opacity
p-emptiness problem, the undecidability of the full *opacity p-emptiness
problem is not surprising, but does not follow immediately.

######  Theorem 3 (Undecidability of the full *opacity p-emptiness problem
[10, Theorem 7.2]).

The full *opacity p-emptiness problem is undecidable for general pta.

The proof relies on a reduction from the problem of reachability-emptiness in
constant time, a result proved itself undecidable in the same paper [10, Lemma
7.1].

Since the emptiness problem is undecidable, the synthesis problem is
immediately unsolvable as well.

######  Corollary 2.

The full *opacity p-synthesis problem is unsolvable for pta.

####  4.2.3 Undecidability for *lupta

$\mathrm{\mathrm{\ell}_{0}}$$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$$\mathrm{\mathrm{\ell}_{f}}$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{p}}}$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq
1$ Figure 4: No monotonicity for full *opacity in *lupta

Let us now study the full *opacity p-emptiness problem for lupta. While it is
well-known that lupta enjoy a monotonicity for reachability properties
(“enlarging an upper-bound parameter or decreasing a lower-bound parameter
preserves reachability”) [28], we can show in the following example that this
is not the case for full *opacity.

######  Example 8.

Consider the pta in Fig. 4. First assume $v$ such that $v({p})=0.5$. Then,
$v(\mathcal{P})$ is not fully *opaque: indeed, $\mathrm{\mathrm{\ell}_{f}}$
can be reached in $1$ time unit by visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$, but not without visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$.

Second, assume $v^{\prime}$ such that $v^{\prime}({p})=1$. Then,
$v^{\prime}(\mathcal{P})$ is fully *opaque: indeed,
$\mathrm{\mathrm{\ell}_{f}}$ can be reached for any duration in $[0,1]$ by
runs both visiting and not visiting $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$.

Finally, let us enlarge ${p}$ further, and assume $v^{\prime\prime}$ such that
$v^{\prime\prime}({p})=2$. Then, $v^{\prime\prime}(\mathcal{P})$ becomes again
not fully *opaque: indeed, $\mathrm{\mathrm{\ell}_{f}}$ can be reached in $2$
time units without visiting $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$, but
cannot be reached in $2$ time units by visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$.

As a side note, remark that this pta is actually upta, that is, monotonicity
for this problem does not even hold for upta.

In fact, we show that, while the $\exists$-*opacity p-emptiness problem is
decidable for lupta (Theorem 2), the full *opacity p-emptiness problem becomes
undecidable for this same class. This confirms (after previous works in [18,
29, 12, 13]) that lupta stand at the frontier between decidability and
undecidability.

######  Theorem 4 (Undecidability of the full *opacity p-emptiness problem for
*lupta [10, Theorem 7.4]).

The full *opacity p-emptiness problem is undecidable for lupta.

Since the emptiness problem is undecidable, the synthesis problem is
immediately unsolvable as well.

######  Corollary 3.

The full *opacity p-synthesis problem is unsolvable for lupta.

######  Remark 4.

Since L/U-PTAs are a subclass of PTAs (put it differently: “any L/U-PTA is a
PTA”), the negative results proved for L/U-PTAs (Theorems 4 and 3) immediately
imply those previously shown for general PTAs (Theorems 3 and 2). However, in
[10], a smaller number of clocks and parameters is needed to prove the
aforementioned negative results for general PTAs, which justifies the two
versions of the proofs in [10].

###  4.3 Parametric weak *opacity

####  4.3.1 Problem definitions

Weak *opacity p-emptiness problem:
Input: A pta $\mathcal{P}$ Problem: Decide the emptiness of the set of
parameter valuations $v$ such that $v(\mathcal{P})$ is weakly *opaque.

Weak *opacity p-synthesis problem:
Input: A pta $\mathcal{P}$ Problem: Synthesize the parameter valuations $v$
such that $v(\mathcal{P})$ is weakly *opaque.

####  4.3.2 Undecidability for general PTAs

We provide below an original result in the context of _weak_ opacity, but
partially inspired by the construction used in the proof of Theorem 3.

######  Theorem 5 (Undecidability of the weak *opacity p-emptiness problem).

The weak *opacity p-emptiness problem is undecidable for general pta.

$\mathrm{\mathrm{\ell}_{0}}$$\mathrm{\mathrm{\ell}_{f}}$$\mathcal{P}$$\mathrm{\mathrm{\ell}_{0}}^{\prime}$$\mathrm{\mathrm{\ell}_{\mathit{pub}}}$$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$$\mathrm{\mathrm{\ell}_{f}}^{\prime}$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=0$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=1$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=1$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=0$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=1$
Figure 5: Reduction from reachability-emptiness for the proof of Theorem 5

###### Proof.

We reduce from the reachability-emptiness problem in bounded time, which is
undecidable from [11, Theorem 3.12]. (This is different from the proof of [10,
Theorem 7.2], which reduces from the reachability-emptiness problem in
_constant_ time, which is undecidable according to [10, Lemma 7.1].)

Consider an arbitrary PTA $\mathcal{P}$, with initial location
$\mathrm{\mathrm{\ell}_{0}}$ and a final location
$\mathrm{\mathrm{\ell}_{f}}$. We add the following locations and transitions
in $\mathcal{P}$ to obtain a PTA $\mathcal{P}^{\prime}$, as in Fig. 5:  (i) a
new initial location $\mathrm{\mathrm{\ell}_{0}}^{\prime}$, with outgoing
transitions in 0-time (due to their guard $\mathit{x}=0$, where $\mathit{x}$
is a new clock not belonging to $\mathcal{P}$, and never reset in
$\mathcal{P}^{\prime}$) to $\mathrm{\mathrm{\ell}_{0}}$ and to a new location
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$,  (ii) a new location
$\mathrm{\mathrm{\ell}_{\mathit{pub}}}$ with an incoming transition from
$\mathrm{\mathrm{\ell}_{f}}$ guarded by $\mathit{x}=1$, and  (iii) a new final
location $\mathrm{\mathrm{\ell}_{f}}^{\prime}$ with incoming transitions from
$\mathrm{\mathrm{\ell}_{\mathit{pub}}}$ and
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ both guarded by $\mathit{x}=1$.

First, note that, due to the guarded transitions,
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$ is reachable for any parameter valuation
via runs visiting $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$, (only) for an
execution time equal to $1$. That is, for all $v$,
$\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\left\\{1\right\\}$.

We now show that there exists a valuation $v$ such that
$v(\mathcal{P}^{\prime})$ is weakly *opaque (with
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ as private location, and
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$ as final location) iff there exists a
valuation $v$ such that $\mathrm{\mathrm{\ell}_{f}}$ is reachable in
$v(\mathcal{P})$ for an execution time $\leq 1$.

  * $\Leftarrow$

Assume there exists some valuation $v$ such that $\mathrm{\mathrm{\ell}_{f}}$
is reachable from $\mathrm{\mathrm{\ell}_{0}}$ in $\mathcal{P}$ for an
execution time $\leq 1$. Then, due to our construction,
$\mathrm{\mathrm{\ell}_{\mathit{pub}}}$ is visited on the way to
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$ in $v(\mathcal{P}^{\prime})$ (only) for
the execution time $1$. Therefore,
$D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\left\\{1\right\\}=\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))$
and then $v(\mathcal{P}^{\prime})$ is weakly *opaque (and also fully *opaque,
which plays no role here).

  * $\Rightarrow$

Conversely, if $\mathrm{\mathrm{\ell}_{f}}$ is not reachable from
$\mathrm{\mathrm{\ell}_{0}}$ in $\mathcal{P}$ for any valuation for an
execution time $\leq 1$, then no run reaches
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$ in time 1 without visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$, for any valuation of
$\mathcal{P}^{\prime}$. Therefore, for any valuation $v$,
$\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\left\\{1\right\\}\not\subseteq
D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\emptyset$.
Therefore, there is no valuation $v$ such that $v(\mathcal{P}^{\prime})$ is
weakly *opaque.

Therefore, there exists a valuation $v$ such that $v(\mathcal{P}^{\prime})$ is
weakly *opaque iff there exists a valuation $v$ such that
$\mathrm{\mathrm{\ell}_{f}}$ is reachable in $v(\mathcal{P})$ for an execution
time $\leq 1$—which is undecidable from [11, Theorem 3.12]. This concludes the
proof. ∎

Since the emptiness problem is undecidable, the synthesis problem is
immediately unsolvable as well.

######  Corollary 4.

The weak *opacity p-synthesis problem is unsolvable for general pta.

####  4.3.3 Undecidability for *lupta

We provide below another original result in the context of _weak_ opacity,
this time for lupta, largely inspired by the proof of Theorem 4, even though
our construction needed to be changed.

######  Theorem 6 (Undecidability of the weak *opacity p-emptiness problem for
lupta).

The weak *opacity p-emptiness problem is undecidable for lupta.

$\mathrm{\mathrm{\ell}_{0}}$$\mathcal{P}$$\mathrm{\mathrm{\ell}_{f}}$$\mathrm{\mathrm{\ell}_{0}}^{\prime}$$\mathrm{\ell}_{1}$$\mathrm{\ell}_{2}$$\mathrm{\ell}_{3}$$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$$\mathrm{\ell}_{4}$$\mathrm{\mathrm{\ell}_{f}}^{\prime}$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=2$${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{1}}^{l}}}}\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{1}}^{u}}}})$${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{2}}^{l}}}}\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{2}}^{u}}}})$${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{2}}^{l}}}}\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{2}}^{u}}}})$${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{1}}^{l}}}}\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{1}}^{u}}}})$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=1$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathbb{X}}}\setminus\\{{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\\}\leftarrow
0$$\bigvee_{i}({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{i}}^{l}}}}<{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}{{{{p}_{i}}^{u}}}})$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}>2$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leftarrow
0$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=2$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}\leftarrow
0$${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}{\mathit{x}}}=0$

Figure 6: Undecidability of full *opacity p-emptiness problem for *lupta

###### Proof.

Let us recall from [11, Theorem 3.12] that the reachability-emptiness problem
is undecidable over bounded time for pta with (at least) 3 clocks and 2
parameters. Assume a pta $\mathcal{P}$ with 3 clocks and 2 parameters, say
${{p}_{1}}$ and ${{p}_{2}}$, and a final location
$\mathrm{\mathrm{\ell}_{f}}$. Take $1$ as a time bound. From [11, Theorem
3.12], it is undecidable whether there exists a parameter valuation for which
$\mathrm{\mathrm{\ell}_{f}}$ is reachable in $\mathcal{P}$ in time $\leq 1$.

The idea of our proof is that, as in [29, 10], we “split” each of the two
parameters used in $\mathcal{P}$ into a lower-bound parameter
(${{{p}_{1}}^{l}}$ and ${{{p}_{2}}^{l}}$) and an upper-bound parameter
(${{{p}_{1}}^{u}}$ and ${{{p}_{2}}^{u}}$). Each constraint of the form
$\mathit{x}<{{p}_{i}}$ (resp. $\mathit{x}\leq{{p}_{i}}$) is replaced with
$\mathit{x}<{{{p}_{i}}^{u}}$ (resp. $\mathit{x}\leq{{{p}_{i}}^{u}}$) while
each constraint of the form $\mathit{x}>{{p}_{i}}$ (resp.
$\mathit{x}\geq{{p}_{i}}$) is replaced with $\mathit{x}>{{{p}_{i}}^{l}}$
(resp. $\mathit{x}\geq{{{p}_{i}}^{l}}$); $\mathit{x}={{p}_{i}}$ is replaced
with ${{{p}_{i}}^{l}}\leq\mathit{x}\leq{{{p}_{i}}^{u}}$.

The idea is that the PTA $\mathcal{P}$ is exactly equivalent to our
construction with duplicated parameters only when
${{{p}_{1}}^{l}}={{{p}_{1}}^{u}}$ and ${{{p}_{2}}^{l}}={{{p}_{2}}^{u}}$. The
crux of the rest of this proof is that we will “rule out” any parameter
valuation not satisfying these equalities, so as to use directly the
undecidability result of [11, Theorem 3.12].

Now, consider the extension of $\mathcal{P}$ given in Fig. 6, and let
$\mathcal{P}^{\prime}$ be this extension. We assume that $\mathit{x}$ is an
extra clock not used in $\mathcal{P}$. The syntax
“$\mathbb{X}\setminus\\{\mathit{x}\\}\leftarrow 0$” denotes that all clocks of
the original pta $\mathcal{P}$ are reset—but not the new clock $\mathit{x}$.
The guard on the transition from $\mathrm{\mathrm{\ell}_{0}}^{\prime}$ to
$\mathrm{\ell}_{4}$ stands for 2 different transitions guarded with
${{{p}_{1}}^{l}}<\mathit{x}\leq{{{p}_{1}}^{u}}$, and
${{{p}_{2}}^{l}}<\mathit{x}\leq{{{p}_{2}}^{u}}$, respectively.

Let us first make the following observations:

  1. 1.

for any parameter valuation, one can take the transition from
$\mathrm{\mathrm{\ell}_{0}}^{\prime}$ to
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ at time $2$ and then to
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$ in 0-time (i.e., at time 2), i.e.,
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$ is always reachable in time $2$ while
visiting location $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$; put differently,
$\\{2\\}\subseteq\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))$ for
any parameter valuation $v$;

  2. 2.

the original automaton $\mathcal{P}$ can only be entered whenever
${{{p}_{1}}^{l}}\leq{{{p}_{1}}^{u}}$ and ${{{p}_{2}}^{l}}\leq{{{p}_{2}}^{u}}$;
going from $\mathrm{\mathrm{\ell}_{0}}^{\prime}$ to
$\mathrm{\mathrm{\ell}_{0}}$ takes exactly $1$ time unit (due to the
$\mathit{x}=1$ guard);

  3. 3.

to reach $\mathrm{\mathrm{\ell}_{f}}^{\prime}$ without visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$, a run must go through $\mathcal{P}$
and visit $\mathrm{\mathrm{\ell}_{f}}$, and its duration is necessarily $2$;
put differently,
$D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))\subseteq\\{2\\}$
for any parameter valuation $v$;

  4. 4.

from [11, Theorem 3.12], it is undecidable whether there exists a parameter
valuation for which there exists a run reaching $\mathrm{\mathrm{\ell}_{f}}$
from $\mathrm{\mathrm{\ell}_{0}}$ in time $\leq 1$, i.e., reaching
$\mathrm{\mathrm{\ell}_{f}}$ from $\mathrm{\mathrm{\ell}_{0}}^{\prime}$ in
time $\leq 2$.

Let us consider the following cases depending on the valuations:

  1. 1.

for valuations $v$ such that ${{{p}_{1}}^{l}}>{{{p}_{1}}^{u}}$ or
${{{p}_{2}}^{l}}>{{{p}_{2}}^{u}}$, then thanks to the transitions from
$\mathrm{\mathrm{\ell}_{0}}^{\prime}$ to $\mathrm{\mathrm{\ell}_{0}}$, there
is no way to enter the original pta $\mathcal{P}$ (and therefore to reach
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$ without visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$); hence,
$D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\emptyset$,
and therefore
$\\{2\\}\subseteq\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))\not\subseteq
D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))$, i.e.,
$\mathcal{P}^{\prime}$ is not weakly *opaque for any of these valuations.

  2. 2.

for valuations $v$ such that ${{{p}_{1}}^{l}}<{{{p}_{1}}^{u}}$ or
${{{p}_{2}}^{l}}<{{{p}_{2}}^{u}}$, then the transition from
$\mathrm{\mathrm{\ell}_{0}}^{\prime}$ to $\mathrm{\ell}_{4}$ can be taken, and
therefore there exist runs reaching $\mathrm{\mathrm{\ell}_{f}}^{\prime}$
after a duration $>2$ (for example of duration 3) and visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$. Since no run can reach
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$ without visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ for a duration $\neq 2$, then
$\\{3\\}\subseteq\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))\not\subseteq
D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))\subseteq\\{2\\}$
and again $\mathcal{P}^{\prime}$ is not weakly *opaque for any of these
valuations.

  3. 3.

for valuations such that ${{{p}_{1}}^{l}}={{{p}_{1}}^{u}}$ and
${{{p}_{2}}^{l}}={{{p}_{2}}^{u}}$, then the behavior of the modified
$\mathcal{P}$ (with duplicate parameters) is exactly the one of the original
$\mathcal{P}$. Also, note that the transition from
$\mathrm{\mathrm{\ell}_{0}}^{\prime}$ to $\mathrm{\ell}_{4}$ cannot be taken.
In contrast, the transition from $\mathrm{\mathrm{\ell}_{0}}^{\prime}$ to
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ can still be taken, and therefore
there exists a run of duration $2$ visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ and reaching
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$. Hence,
$\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\\{2\\}$ for any
such valuation $v$.

     * •

Now, assume there exists such a parameter valuation $v$ for which there exists
a run of $v(\mathcal{P})$ of duration $\leq 1$ reaching
$\mathrm{\mathrm{\ell}_{f}}$. And, as a consequence, there exists a run of
$v(\mathcal{P}^{\prime})$ of duration $2$ (including the $1$ time unit to go
from $\mathrm{\mathrm{\ell}_{0}}^{\prime}$ to $\mathrm{\mathrm{\ell}_{0}}$)
reaching $\mathrm{\mathrm{\ell}_{f}}^{\prime}$ without visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$. Hence,
$D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\\{2\\}$.
Therefore
$D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\\{2\\}$.

As a consequence, the modified automaton $\mathcal{P}^{\prime}$ is weakly
*opaque (and actually fully *opaque—which plays no role in this proof) for
such a parameter valuation.

     * •

Conversely, assume there exists no parameter valuation for which there exists
a run of $\mathcal{P}$ of duration $\leq 1$ reaching
$\mathrm{\mathrm{\ell}_{f}}$. In that case,
$\mathrm{\mathrm{\ell}_{f}}^{\prime}$ can never be reached without visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$:
$D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))=\emptyset$,
and therefore
$\\{2\\}\subseteq\mathit{DVisit}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))\not\subseteq
D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}^{\prime}))$, i.e.,
$v(\mathcal{P}^{\prime})$ is not fully *opaque for any such parameter
valuation $v$.

As a consequence, there exists a parameter valuation $v^{\prime}$ for which
$v^{\prime}(\mathcal{P}^{\prime})$ is weakly *opaque iff there exists a
parameter valuation $v$ for which there exists a run in $v(\mathcal{P})$ of
duration $\leq 1$ reaching $\mathrm{\mathrm{\ell}_{f}}$—which is undecidable
from [11, Theorem 3.12]. ∎

######  Corollary 5.

The weak *opacity p-synthesis problem is unsolvable for lupta.

##  5 Expiring execution-time opacity problems

In [5], the authors consider a time-bounded notion of the opacity of [20],
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_. The rationale is that retrieving a secret “too late” is useless; this
is understandable, e.g., when the secret depends of the status of the memory;
if the cache was overwritten since, then knowing the secret is probably
useless in most situations. In addition, the analysis in [5] is carried over a
time-bounded horizon; this means there are two time bounds in [5]: one for the
secret expiration date, and one for the bounded-time execution of the system.

In this section, we review a recent work of ours [9] in which we incorporate
this secret expiration date into our notion of opacity: we only consider the
former notion of time bound from [5] (the secret expiration date), and lift
the assumption regarding the latter (the bounded-time execution of the
system). More precisely, we consider an _expiring version of opacity_ , where
the secret is subject to an expiration date; this can be seen as a combination
of both concepts from [10] and [5]. That is, we consider that an attack is
successful only when the attacker can decide that the secret location was
entered less than $\Delta$ time units before the system completion.
Conversely, if the attacker exhibits an execution time ${d}$ for which it is
certain that the secret location was visited, but this location was entered
strictly more than $\Delta$ time units prior to the system completion, then
this attack is useless, and can be seen as a failed attack. The system is
therefore _fully_ tempopaque if the set of execution times for which the
private location was entered within $\Delta$ time units prior to system
completion is exactly equal to the set of execution times for which the
private location was either not visited or entered $>\Delta$ time units prior
to system completion.

In addition, when the former (secret) set of execution times is _included_
into the latter (non-secret) set of times, we say that the system is _weakly_
tempopaque; this encodes situations when the attacker might be able to deduce
that no secret location was visited, but is not able to confirm that the
secret location _was_ indeed visited.

Table 3: Summary of the definitions for opacity and expiring opacity [10, 9]

|  Secret runs |  Non-secret runs
---|---|---
opacity |  Runs visiting the private location ($=$ private runs) |  Runs not visiting the private location ($=$ public runs)
tempopacity |  Runs visiting the private location $\leq\Delta$ time units before the system completion |  (i) Runs not visiting the private location and
(ii) Runs visiting the private location $>\Delta$ time units before the system
completion

The system is | if
---|---
(resp. expiring) |
opaque | $\\{\text{secret runs}\\}\cap\\{\text{non-secret runs}\\}\neq\emptyset$
weakly *opaque | $\\{\text{secret runs}\\}\subseteq\\{\text{non-secret runs}\\}$
full *opacity | $\\{\text{secret runs}\\}=\\{\text{non-secret runs}\\}$

On the one hand, our attacker model is _less powerful_ than [5], because our
attacker has only access to the execution time (and to the input model); in
that sense, our attacker capability is identical to [10]. On the other hand,
we lift the time-bounded horizon analysis from [5], allowing to analyze
systems without any assumption on their execution time; therefore, we only
import from [5] the notion of _expiring secret_.

We summarize in Table 3 our different notions of opacity and expiring opacity;
we will define formally expiring opacity in the following.

###  5.1 tempopacity

Let us first introduce some notions dedicated to expiring opacity (hereafter
referred to as tempopacity). Let $\mathbb{R}^{\infty}_{\geq
0}=\mathbb{R}_{\geq 0}\cup\\{+\infty\\}$. Given a ta $\mathcal{A}$ and a
finite run $\rho$ in $\mathfrak{T}_{\mathcal{A}}$, the _duration_ between two
states of
$\rho:\mathfrak{s}_{0},(d_{0},e_{0}),\mathfrak{s}_{1},\cdots,\mathfrak{s}_{k}$
is $\mathit{dur}_{\rho}(\mathfrak{s}_{i},\mathfrak{s}_{j})=\sum_{i\leq m\leq
j-1}d_{m}$. We also define the _duration_ between two locations
$\mathrm{\mathrm{\ell}_{1}}$ and $\mathrm{\mathrm{\ell}_{2}}$ as the duration
$\mathit{dur}_{\rho}(\mathrm{\mathrm{\ell}_{1}},\mathrm{\mathrm{\ell}_{2}})=\mathit{dur}_{\rho}(\mathfrak{s}_{i},\mathfrak{s}_{j})$
with
$\rho:\mathfrak{s}_{0},(d_{0},e_{0}),\mathfrak{s}_{1},\cdots,\mathfrak{s}_{i},\cdots,\mathfrak{s}_{j},\cdots,\mathfrak{s}_{k}$
where $\mathfrak{s}_{j}$ the first occurrence of a state with location
$\mathrm{\mathrm{\ell}_{2}}$ and $\mathfrak{s}_{i}$ is the last state of
$\rho$ with location $\mathrm{\mathrm{\ell}_{1}}$ before $\mathfrak{s}_{j}$.
We choose this definition to coincide with the definitions of opacity that we
will define in the following Definition 11. Indeed, we want to make sure that
revealing a secret ($\mathrm{\mathrm{\ell}_{1}}$ in this definition) is not a
failure if it is done after a given time. Thus, as soon as the system reaches
its final state ($\mathrm{\ell}_{2}$), we will be interested in knowing how
long the secret has been present, and thus the last time it was entered
($\mathfrak{s}_{i}$).

Given $\Delta\in\mathbb{R}^{\infty}_{\geq 0}$, we define
$\mathit{Visit}^{\mathit{priv}}_{\leq\Delta}(\mathcal{A})$ (resp.
$\mathit{Visit}^{\mathit{priv}}_{>\Delta}(\mathcal{A})$) as the set of runs
$\rho\in\mathit{Visit}^{\mathit{priv}}(\mathcal{A})$ s.t.
$\mathit{dur}_{\rho}(\mathrm{\mathrm{\ell}_{\mathit{priv}}},\mathrm{\mathrm{\ell}_{f}})\leq\Delta$
(resp.
$\mathit{dur}_{\rho}(\mathrm{\mathrm{\ell}_{\mathit{priv}}},\mathrm{\mathrm{\ell}_{f}})>\Delta$).
We refer to the runs of
$\mathit{Visit}^{\mathit{priv}}_{\leq\Delta}(\mathcal{A})$ as _secret_ runs;
their durations are denoted by
$\mathit{DVisit}^{\mathit{priv}}_{\leq\Delta}(\mathcal{A})$. Similarly, the
durations of the runs of
$\mathit{Visit}^{\mathit{priv}}_{>\Delta}(\mathcal{A})$ are denoted by
$\mathit{DVisit}^{\mathit{priv}}_{>\Delta}(\mathcal{A})$.

We define below two notions of opacity w.r.t. a time bound $\Delta$. We will
compare two sets:

  1. 1.

the set of execution times for which the private location was entered at most
$\Delta$ time units prior to system completion; and

  2. 2.

the set of execution times for which either the private location was not
visited at all, or it was last entered more than $\Delta$ time units prior to
system completion (which, in our setting, is somehow similar to _not_ visiting
the private location, in the sense that entering it “too early” is considered
of little interest).

If both sets match, the system is fully ($\leq$ $\Delta$)-*opaque. If the
former is included into the latter, then the system is weakly ($\leq$
$\Delta$)-*opaque.

######  Definition 11 (*tempopacity).

Given a ta $\mathcal{A}$ and a bound (i.e., an expiration date for the secret)
$\Delta\in\mathbb{R}^{\infty}_{\geq 0}$ we say that $\mathcal{A}$ is _fully
*tempopaque_ w.r.t. the expiration date $\Delta$, denoted by _fully ( $\leq$
$\Delta$)-*opaque_, if

$\mathit{DVisit}^{\mathit{priv}}_{\leq\Delta}(\mathcal{A})=\mathit{DVisit}^{\mathit{priv}}_{>\Delta}(\mathcal{A})\cup
D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A}).$

Moreover, $\mathcal{A}$ is _weakly *tempopaque_ w.r.t. the expiration date
$\Delta$, denoted by _weakly ( $\leq$ $\Delta$)-*opaque_, if

$\mathit{DVisit}^{\mathit{priv}}_{\leq\Delta}(\mathcal{A})\subseteq\mathit{DVisit}^{\mathit{priv}}_{>\Delta}(\mathcal{A})\cup
D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A}).$

Finally, $\mathcal{A}$ is _$\exists$ -*opaque_ w.r.t. the expiration date
$\Delta$, denoted by _$\exists$ -($\leq$ $\Delta$)-*opaque_, if

$\mathit{DVisit}^{\mathit{priv}}_{\leq\Delta}(\mathcal{A})\cap(\mathit{DVisit}^{\mathit{priv}}_{>\Delta}(\mathcal{A})\cup
D\overline{\mathit{Visit}}^{\mathit{priv}}(\mathcal{A}))\neq\emptyset.$

######  Example 9.

Consider again the pta in Fig. 2; let $v$ be such that $v({{p}_{1}})=1$ and
$v({{p}_{2}})=2.5$. Fix $\Delta=1$.

We have:

  * •

$D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}))=[0,3]$

  * •

$\mathit{DVisit}^{\mathit{priv}}_{>\Delta}(v(\mathcal{P}))=(2,2.5]$

  * •

$\mathit{DVisit}^{\mathit{priv}}_{\leq\Delta}(v(\mathcal{P}))=[1,2.5]$

Therefore, we say that $v(\mathcal{P})$ is:

  * •

$\exists$-($\leq$ $1$)-*opaque, as
$[1,2.5]\cap\big{(}(2,2.5]\cup[0,3]\big{)}\neq\emptyset$

  * •

weakly ($\leq$ $1$)-*opaque, as
$[1,2.5]\subseteq\big{(}(2,2.5]\cup[0,3]\big{)}$

  * •

not fully ($\leq$ $1$)-*opaque, as $[1,2.5]\neq\big{(}(2,2.5]\cup[0,3]\big{)}$

As noted in Remark 3, despite the weak ($\leq$ $1$)-*opacity of $\mathcal{A}$,
the attacker can deduce some information about the visit of the private
location for some execution times. For example, if a run has a duration of 3
time units, it cannot be a private run, and therefore the attacker can deduce
that the private location was not visited at all.

###  5.2 tempopacity problems in timed automata

####  5.2.1 Problem definitions

We define seven different problems in the context of (non-parametric) ta:

$\exists$-*tempopacity decision problem:
Input: A ta $\mathcal{A}$ and a bound $\Delta\in\mathbb{R}^{\infty}_{\geq 0}$
Problem: Decide whether $\mathcal{A}$ is $\exists$-($\leq$ $\Delta$)-*opaque.

Full (resp. weak) *tempopacity decision problem:
Input: A ta $\mathcal{A}$ and a bound $\Delta\in\mathbb{R}^{\infty}_{\geq 0}$
Problem: Decide whether $\mathcal{A}$ is fully (resp. weakly) ($\leq$
$\Delta$)-*opaque.

Full (resp. weak) *tempopacity $\Delta$-emptiness problem:
Input: A ta $\mathcal{A}$ Problem: Decide the emptiness of the set of bounds
$\Delta$ such that $\mathcal{A}$ is fully (resp. weakly) ($\leq$
$\Delta$)-*opaque.

Full (resp. weak) *tempopacity $\Delta$-computation problem:
Input: A ta $\mathcal{A}$ Problem: Compute the maximal set $\mathcal{D}$ of
bounds such that $\mathcal{A}$ is fully (resp. weakly) ($\leq$
$\Delta$)-*opaque for all $\Delta\in\mathcal{D}$.

######  Example 10.

Consider again the pta in Fig. 2; let $v$ be such that $v({{p}_{1}})=1$ and
$v({{p}_{2}})=2.5$ (as in Example 9). Let us exemplify some of the problems
defined above.

  * •

Given $\Delta=1$, the weak *tempopacity decision problem asks whether
$v(\mathcal{P})$ is weakly ($\leq$ $1$)-*opaque—the answer is “yes” from
Example 9.

  * •

The answer to the weak *tempopacity $\Delta$-emptiness problem is therefore
“no” because the set of bounds $\Delta$ such that $v(\mathcal{P})$ is weakly
($\leq$ $\Delta$)-*opaque is not empty.

  * •

Finally, the weak *tempopacity $\Delta$-computation problem asks to compute
all the corresponding bounds: in this example, the solution is
${\Delta\in\mathbb{R}^{\infty}_{\geq 0}}$, i.e., the solution is the set all
possible (non-negative) values for $\Delta$.

##### Relations with the opacity problems

Note that, when considering $\Delta=+\infty$,
$\mathit{DVisit}^{\mathit{priv}}_{>\Delta}(\mathcal{A})=\emptyset$ and all the
execution times of runs visiting $\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ are
in $\mathit{DVisit}^{\mathit{priv}}_{\leq\Delta}(\mathcal{A})$. Therefore,
full ($\leq$ $+\infty$)-*opacity matches the full *opacity. We can therefore
notice that answering the full *tempopacity decision problem for
$\Delta=+\infty$ is decidable (Proposition 3). However, the emptiness and
computation problems cannot be reduced to full *opacity problems from Section
4.1.3.

Conversely, it is possible to answer the full *opacity decision problem by
checking the full *tempopacity decision problem with $\Delta=+\infty$.
Moreover, the *opacity t-computation problem reduces to the full *tempopacity
$\Delta$-computation problem: if $+\infty\in\mathcal{D}$, we get the answer.

Recall that we summarize our different definitions of (expiring) opacity in
Table 3.

####  5.2.2 Results

In general, the link between the full and weak notions of the three
aforementioned problems is not obvious. However, for a fixed value of
$\Delta$, we establish the following theorem.

######  Theorem 7 ([9, Theorem 1]).

The full *tempopacity decision problem reduces to the weak *tempopacity
decision problem.

We can now study the aforementioned problems.

######  Theorem 8 (Decidability of full (resp. weak) *tempopacity decision
problem [9, Theorems 2 and 5]).

The full (resp. weak) *tempopacity decision problem is decidable in NEXPTIME.

######  Remark 5.

In Proposition 3, we established that the full ($\leq$ $+\infty$)-*opacity
decision problem is in 5EXPTIME. Theorem 8 thus extends our former results in
three ways:

  1. 1.

by including the parameter $\Delta$,

  2. 2.

by reducing the complexity and

  3. 3.

by considering as well the _weak_ notion of ET-opacity (considered separately
in Proposition 4).

We complete these results from [9] with the following result analog to
Proposition 2.

######  Theorem 9 (Decidability of $\exists$-*tempopacity decision problem).

The $\exists$-*tempopacity decision problem is decidable in PSPACE.

###### Proof.

The full (resp. weak) *tempopacity decision problem was solved in [9] by
building two non-deterministic finite automata whose languages represented the
secret and the non-secret durations of the system, respectively. These
automata being of exponential size and with a unary language, testing the
equality or inclusion of languages led to the NEXPTIME algorithm quoted in
Theorem 8. Similarly, the $\exists$-*tempopacity decision problem can be
decided by testing whether the intersection of the languages of these automata
is empty. This can be done in NLOGSPACE in the size of the automata
(classically, by first building the product between these two automata, and
then by checking the reachability of a pair of final states), hence the PSPACE
algorithm. ∎

######  Theorem 10 (Solvability of weak *tempopacity $\Delta$-computation
problem [9, Theorems 3 and 5]).

The weak *tempopacity $\Delta$-computation problem is solvable.

######  Corollary 6 (Decidability of weak *tempopacity $\Delta$-emptiness
problem [9, Corollary 1]).

The weak *tempopacity $\Delta$-emptiness problem is decidable.

In contrast to the weak *tempopacity $\Delta$-computation problem, we only
show below that the full *tempopacity $\Delta$-emptiness problem is decidable;
the computation problem remains open.

######  Theorem 11 (Decidability of the full *tempopacity $\Delta$-emptiness
problem [9, Theorems 4 and 5]).

The full *tempopacity $\Delta$-emptiness problem is decidable.

###  5.3 tempopacity in *pta

We now study tempopacity problems for pta: we will be interested in the
synthesis and in the emptiness of the valuations set ensuring that a system is
fully (resp. weakly) *tempopaque.

####  5.3.1 Definitions

We define the following problems, where we ask for parameter valuations $v$
and for valuations of $\Delta$ s.t. $v(\mathcal{P})$ is fully (resp. weakly)
($\leq$ $\Delta$)-*opaque.

Full (resp. weak) *tempopacity $\Delta$-p-emptiness problem:
Input: A pta $\mathcal{P}$ Problem: Decide whether the set of parameter
valuations $v$ and valuations of $\Delta$ such that $v(\mathcal{P})$ is fully
(resp. weakly) ($\leq$ $\Delta$)-*opaque is empty

Full (resp. weak) *tempopacity $\Delta$-p-synthesis problem:
Input: A pta $\mathcal{P}$ Problem: Synthesize the set of parameter valuations
$v$ and valuations of $\Delta$ such that $v(\mathcal{P})$ is fully (resp.
weakly) ($\leq$ $\Delta$)-*opaque

######  Example 11.

Consider again the pta $\mathcal{P}$ in Fig. 2.

For this pta, the answer to the weak *tempopacity $\Delta$-p-emptiness problem
is false, as there exists such a valuation (e.g., the valuation given in
Example 10).

Moreover, we can show that, for all $\Delta$ and $v$:

  * •

$D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}))=[0,3]$

  * •

if $v({{p}_{1}})>3$ or $v({{p}_{1}})>v({{p}_{2}})$, it is not possible to
reach $\mathrm{\mathrm{\ell}_{f}}$ with a run visiting
$\mathrm{\mathrm{\ell}_{\mathit{priv}}}$ and therefore
$\mathit{DVisit}^{\mathit{priv}}_{>\Delta}(v(\mathcal{P}))=\mathit{DVisit}^{\mathit{priv}}_{\leq\Delta}(v(\mathcal{P}))=\emptyset$

  * •

if $v({{p}_{1}})\leq 3$ and $v({{p}_{1}})\leq v({{p}_{2}})$

    * –

$\mathit{DVisit}^{\mathit{priv}}_{>\Delta}(v(\mathcal{P}))=(v({{p}_{1}})+\Delta,v({{p}_{2}})]$

    * –

$\mathit{DVisit}^{\mathit{priv}}_{\leq\Delta}(v(\mathcal{P}))=[v({{p}_{1}}),\min(\Delta+3,v({{p}_{2}}))]$

Recall that the full *tempopacity $\Delta$-p-synthesis problem aims at
synthesizing the valuations such that
$\mathit{DVisit}^{\mathit{priv}}_{\leq\Delta}(v(\mathcal{P}))=\mathit{DVisit}^{\mathit{priv}}_{>\Delta}(v(\mathcal{P}))\cup
D\overline{\mathit{Visit}}^{\mathit{priv}}(v(\mathcal{P}))$. The answer to
this problem is therefore the set of valuations of timing parameters and of
$\Delta$ s.t.:

$v({{p}_{1}})=0\wedge\Big{(}\big{(}\Delta\leq 3\wedge 3\leq
v({{p}_{2}})\leq\Delta+3\big{)}\vee\big{(}v({{p}_{2}})<\Delta\wedge
v({{p}_{2}})=3\big{)}\Big{)}\text{.}$

####  5.3.2 Results

##### The subclass of *lupta

######  Theorem 12 (Undecidability of full (resp. weak) *tempopacity
$\Delta$-p-emptiness problem [9, Theorem 6]).

The full (resp. weak) *tempopacity $\Delta$-p-emptiness problem is undecidable
for lupta.

The synthesis problems are therefore immediately unsolvable as well.

######  Corollary 7 ([9, Corollary 2]).

The full (resp. weak) *tempopacity $\Delta$-p-synthesis problem is unsolvable
for lupta.

##### The full class of *pta

The undecidability of the emptiness problems for lupta proved above (Theorem
12) immediately implies undecidability for the larger class of pta. However,
as in Remark 4, the full proof (given in [9]) of the result stated below uses
less clocks and parameters than for lupta (Theorem 12).

######  Theorem 13 (Undecidability of full (resp. weak) *tempopacity
$\Delta$-p-emptiness problem [9, Theorem 7]).

The full (resp. weak) *tempopacity $\Delta$-p-emptiness problem is undecidable
for general pta.

Again, the synthesis problems are therefore immediately unsolvable as well.

######  Corollary 8 ([9, Corollary 3]).

The full (resp. weak) *tempopacity $\Delta$-p-synthesis problem is unsolvable
for pta.

##  6 Implementation and application to Java programs

A motivation for the works on opacity (described in Sections 3 and 4) is the
analysis of programs. More precisely, we are interested in deciding whether a
program, e.g., written in Java, is opaque, i.e., whether an attacker is
incapable of deducing internal behavior by only looking at its execution time.
A second motivation is the _configuration_ of internal timing values from a
program, e.g., changing some internal delays, or tuning some Thread.sleep()
statements in the program, so that the program becomes opaque—justifying
notably the results in Section 4.

##### Semi-algorithm and implementation

Despite the negative theoretical results (notably Theorem 1), we addressed in
[10] the $\exists$-*opacity p-synthesis problem for the full class of pta. Our
method may not terminate (due to the undecidability) but, if it does, its
result is correct. Our workflow [10] can be summarized as follows.

  1. 1.

We slightly modify the original pta (by adding a Boolean flag $b$ and a final
synchronization action);

  2. 2.

We perform _self-composition_ (i.e., parallel composition with a copy of
itself) of this modified pta, a method commonly used in security analyses [33,
16];

  3. 3.

We perform reachability-synthesis (i.e., the synthesis of parameter valuations
for which a given location is reachable) on $\mathrm{\mathrm{\ell}_{f}}$ with
contradictory values of $b$.

Reachability-synthesis is implemented in IMITATOR [7], a parametric timed
model checker taking as inputs networks of (extensions of) parametric timed
automata, and synthesizing parameter valuations for which a number of
properties (including reachability) hold.

##### Analysis of Java programs

In addition, we are interested in analyzing programs too. In order to apply
our method to the analysis of programs, we need a systematic way of
translating a program (e.g., a Java program) into a pta. In general, precisely
modeling the execution time of a program using models like ta is highly non-
trivial due to complication of hardware pipelining, caching, OS scheduling,
etc. The readers are referred to the rich literature in, e.g., [30, 21]. In
[10], we instead make the following simplistic assumption on execution time of
a program statement and focus on solving the parameter synthesis problem. We
assume that the execution time of a program statement other than
Thread.sleep(n) is within a range $[0,\epsilon]$ where $\epsilon$ is a small
integer constant (in milliseconds), whereas the execution time of statement
Thread.sleep(n) is within a range $[n,n+\epsilon]$. In fact, we choose to keep
$\epsilon$ _parametric_ to be as general as possible, and to not depend on
particular architectures.

Our test subject is a set of benchmark programs from the DARPA Space/Time
Analysis for Cybersecurity (STAC) program.111https://github.com/Apogee-
Research/STAC/ These programs are being released publicly to facilitate
researchers to develop methods and tools for identifying STAC vulnerabilities
in the programs. These programs are simple yet non-trivial, and were built on
purpose to highlight vulnerabilities that can be easily missed by existing
security analysis tools. We _manually_ translated these programs to pta,
following the method described above, and using a number of assumptions (such
as collapsing loops with predefined duration).

In addition, we applied our method to a set of pta examples from the
literature, notably from [28, 25, 17, 35].

Experiments reported in [10] show that we can decide whether these benchmarks
(including the programs) are fully *opaque or $\exists$-*opaque. When adding
timing parameters, we additionally answer the $\exists$-*opacity p-synthesis
problem, i.e., we synthesize the parameter valuations $v$ and the associated
execution times $D$ such that $v(\mathcal{P})$ is opaque. Our method allows to
exhibit cases when the system can never be made opaque, including by tuning
internal delays, or is always opaque, or is opaque only for some execution
times and internal timing parameters.

To summarize, the following problems can be answered using our framework:

  * •

$\exists$-*opacity decision problem

  * •

full *opacity decision problem

  * •

weak *opacity decision problem (not considered in our experiments in [10], but
can be easily adapted)

  * •

$\exists$-*opacity p-synthesis problem, but without guarantee of termination,
due to the undecidability of Theorem 1.

However, our procedure cannot in its current form answer neither the full
*opacity p-synthesis problem nor the weak *opacity p-synthesis problem. The
expiring opacity problems in Section 5 were not addressed either.

##  7 Conclusion and perspectives

In this paper, we recalled (and proved a few original) results related to the
opacity in ta. Our notion of opacity consists in considering an attacker model
that can only observe the execution time of the system, i.e., the time from
the initial location to a final location. The secret consists in deciding
whether a special private location was visited or not. In contrast to another
notion of opacity with a more powerful attacker able to observe some actions
together with their timestamps, which led to the undecidability of the
decision problem for ta [20], our notion of opacity yields decidability
results for ta. Parameterizing the problems using timing parameters brings
undecidability for pta, but the subclass of lupta gives mildly positive
results.

When in addition we consider that the secret has an expiration date, similarly
to the concepts introduced in [5], we are able to not only _decide_ problems
for ta, but also to _synthesize_ valuations for the expiration date such that
the ta is weakly *tempopaque. However, problems extended with timing
parameters all become undecidable.

Recall that we summarized in Tables 1 and 2 the decidability results recalled
in this paper, with a bold emphasis on the original results of this paper.

We also reported here on an implementation using IMITATOR, which is able to
answer non-parametric problems ($\exists$-*opacity decision problem, full
*opacity decision problem, weak *opacity decision problem), and also answering
a parameter synthesis problem ($\exists$-*opacity p-synthesis problem) without
guarantee of termination for the latter problem.

##### Perspectives

The main theoretical future work is the open problems in Table 2 (mainly the
full *tempopacity $\Delta$-computation problem): it is unclear whether we can
_compute_ the exact set of expiration dates $\Delta$ for which a ta is fully
($\leq$ $\Delta$)-*opaque.

In terms of synthesis, we have so far no procedure able (whenever it
terminates) to answer the full *opacity p-synthesis problem or the weak
*opacity p-synthesis problem. Synthesis procedures to answer expiring opacity
problems (defined in Section 5) for pta remain to be designed too. These
procedures cannot be both exact and guaranteed to terminate due to the
aforementioned undecidability results.

Exact analysis of opacity for programs, including a more precise modeling of
the cache, is also on our agenda, following works such as [21, 22].

A different direction is that of _control_ : can we turn a non-opaque system
into an opaque system, by restraining its possible behaviors? A first step
with our notion of opacity was presented in [8], with only an _untimed_
controller. In addition, in [25], Gardey et al. propose several definitions of
non-interference, related to various notions of simulation: they consider not
only the _verification_ problem (“is the system non-interferent?”) but also
the (timed) _control_ problem (“synthesize a controller that will restrict the
system in order to enforce non-interference”). Extending our current line
works on opacity to _timed_ controllers remains to be done.

##### Acknowledgments

We are grateful to Clemens Dubslaff and Maurice ter Beek for the opportunity
to give an invited talk at TiCSA 2023, and for useful suggestions on this
manuscript.

## References

  * [1]
  * [2] Rajeev Alur & David L. Dill (1994): _A theory of timed automata_.  Theoretical Computer Science 126(2), pp. 183–235, 10.1016/0304-3975(94)90010-8.
  * [3] Rajeev Alur, Limor Fix & Thomas A. Henzinger (1999): _Event-Clock Automata: A Determinizable Class of Timed Automata_.  Theoretical Computer Science 211(1-2), pp. 253–273, 10.1016/S0304-3975(97)00173-4.
  * [4] Rajeev Alur, Thomas A. Henzinger & Moshe Y. Vardi (1993): _Parametric real-time reasoning_.  In S. Rao Kosaraju, David S. Johnson & Alok Aggarwal, editors: STOC, ACM, New York, NY, USA, pp. 592–601, 10.1145/167088.167242.
  * [5] Ikhlass Ammar, Yamen El Touati, Moez Yeddes & John Mullins (2021): _Bounded opacity for timed systems_.  Journal of Information Security and Applications 61, pp. 1–13, 10.1016/j.jisa.2021.102926.
  * [6] Étienne André (2019): _What’s decidable about parametric timed automata?_ International Journal on Software Tools for Technology Transfer 21(2), pp. 203–219, 10.1007/s10009-017-0467-0.
  * [7] Étienne André (2021): _IMITATOR 3: Synthesis of timing parameters beyond decidability_.  In Rustan Leino & Alexandra Silva, editors: CAV, Lecture Notes in Computer Science 12759, Springer, pp. 1–14, 10.1007/978-3-030-81685-8_26.
  * [8] Étienne André, Shapagat Bolat, Engel Lefaucheux & Dylan Marinho (2022): _strategFTO: Untimed control for timed opacity_.  In Cyrille Artho & Peter Ölveczky, editors: FTSCS, ACM, pp. 27–33, 10.1145/3563822.3568013.
  * [9] Étienne André, Engel Lefaucheux & Dylan Marinho (2023): _Expiring opacity problems in parametric timed automata_.  In Yamine Ait-Ameur & Ferhat Khendek, editors: ICECCS.  To appear.
  * [10] Étienne André, Didier Lime, Dylan Marinho & Jun Sun (2022): _Guaranteeing timed opacity using parametric timed model checking_.  ACM Transactions on Software Engineering and Methodology 31(4), pp. 1–36, 10.1145/3502851.
  * [11] Étienne André, Didier Lime & Nicolas Markey (2020): _Language Preservation Problems in Parametric Timed Automata_.  Logical Methods in Computer Science 16(1), 10.23638/LMCS-16(1:5)2020.  Available at https://lmcs.episciences.org/6042.
  * [12] Étienne André, Didier Lime & Mathias Ramparison (2018): _TCTL model checking lower/upper-bound parametric timed automata without invariants_.  In David N. Jansen & Pavithra Prabhakar, editors: FORMATS, Lecture Notes in Computer Science 11022, Springer, pp. 1–17, 10.1007/978-3-030-00151-3_3.
  * [13] Étienne André, Didier Lime & Olivier H. Roux (2022): _Reachability and liveness in parametric timed automata_.  Logical Methods in Computer Science 18(1), pp. 31:1–31:41, 10.46298/lmcs-18(1:31)2022.  Available at https://lmcs.episciences.org/9070/pdf.
  * [14] Johan Arcile & Étienne André (2023): _Timed automata as a formalism for expressing security: A survey on theory and practice_.  ACM Computing Surveys 55(6), pp. 1–36, 10.1145/3534967.
  * [15] Roberto Bagnara, Patricia M. Hill & Enea Zaffanella (2008): _The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems_.  Science of Computer Programming 72(1–2), pp. 3–21, 10.1016/j.scico.2007.08.001.
  * [16] Gilles Barthe, Pedro R. D’Argenio & Tamara Rezk (2011): _Secure information flow by self-composition_.  Mathematical Structures in Computer Science 21(6), pp. 1207–1252, 10.1017/S0960129511000193.
  * [17] Gilles Benattar, Franck Cassez, Didier Lime & Olivier H. Roux (2015): _Control and synthesis of non-interferent timed systems_.  International Journal of Control 88(2), pp. 217–236, 10.1080/00207179.2014.944356.
  * [18] Laura Bozzelli & Salvatore La Torre (2009): _Decision problems for lower/upper bound parametric timed automata_.  Formal Methods in System Design 35(2), pp. 121–151, 10.1007/s10703-009-0074-0.
  * [19] Véronique Bruyère, Emmanuel Dall’Olio & Jean-Francois Raskin (2008): _Durations and parametric model-checking in timed automata_.  ACM Transactions on Computational Logic 9(2), pp. 12:1–12:23, 10.1145/1342991.1342996.
  * [20] Franck Cassez (2009): _The Dark Side of Timed Opacity_.  In Jong Hyuk Park, Hsiao-Hwa Chen, Mohammed Atiquzzaman, Changhoon Lee, Tai-Hoon Kim & Sang-Soo Yeo, editors: ISA, Lecture Notes in Computer Science 5576, Springer, pp. 21–30, 10.1007/978-3-642-02617-1_3.
  * [21] Franck Cassez & Jean-Luc Béchennec (2013): _Timing Analysis of Binary Programs with UPPAAL_.  In Josep Carmona, Mihai T. Lazarescu & Marta Pietkiewicz-Koutny, editors: ACSD, IEEE Computer Society, pp. 41–50, 10.1109/ACSD.2013.7.
  * [22] Duc-Hiep Chu, Joxan Jaffar & Rasool Maghareh (2016): _Precise Cache Timing Analysis via Symbolic Execution_.  In: RTAS, IEEE Computer Society, pp. 293–304, 10.1109/RTAS.2016.7461358.
  * [23] Shuwen Deng, Wenjie Xiong & Jakub Szefer (2018): _Cache timing side-channel vulnerability checking with computation tree logic_.  In Jakub Szefer, Weidong Shi & Ruby B. Lee, editors: ISCA, ACM, pp. 2:1–2:8, 10.1145/3214292.3214294.
  * [24] Goran Doychev, Boris Köpf, Laurent Mauborgne & Jan Reineke (2015): _CacheAudit: A Tool for the Static Analysis of Cache Side Channels_.  ACM Transactions on Information and System Security 18(1), pp. 4:1–4:32, 10.1145/2756550.
  * [25] Guillaume Gardey, John Mullins & Olivier H. Roux (2007): _Non-Interference Control Synthesis for Security Timed Automata_.  Electronic Notes in Theoretical Computer Science 180(1), pp. 35–53, 10.1016/j.entcs.2005.05.046.
  * [26] Shengjian Guo, Meng Wu & Chao Wang (2018): _Adversarial symbolic execution for detecting concurrency-related cache timing leaks_.  In Gary T. Leavens, Alessandro Garcia & Corina S. Pasareanu, editors: ESEC/SIGSOFT FSE, ACM, pp. 377–388, 10.1145/3236024.3236028.
  * [27] Thomas A. Henzinger, Zohar Manna & Amir Pnueli (1992): _Timed Transition Systems_.  In J. W. de Bakker, Cornelis Huizing, Willem P. de Roever & Grzegorz Rozenberg, editors: REX, Lecture Notes in Computer Science 600, Springer, pp. 226–251, 10.1007/BFb0031995.
  * [28] Thomas Hune, Judi Romijn, Mariëlle Stoelinga & Frits W. Vaandrager (2002): _Linear parametric model checking of timed automata_.  Journal of Logic and Algebraic Programming 52-53, pp. 183–220, 10.1016/S1567-8326(02)00037-1.
  * [29] Aleksandra Jovanović, Didier Lime & Olivier H. Roux (2015): _Integer Parameter Synthesis for Real-Time Systems_.  IEEE Transactions on Software Engineering 41(5), pp. 445–461, 10.1109/TSE.2014.2357445.
  * [30] Mingsong Lv, Wang Yi, Nan Guan & Ge Yu (2010): _Combining Abstract Interpretation with Model Checking for Timing Analysis of Multicore Software_.  In: RTSS, IEEE Computer Society, pp. 339–349, 10.1109/RTSS.2010.30.
  * [31] Joseph S. Miller (2000): _Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata_.  In Nancy A. Lynch & Bruce H. Krogh, editors: HSCC, Lecture Notes in Computer Science 1790, Springer, pp. 296–309, 10.1007/3-540-46430-1_26.
  * [32] Quoc-Sang Phan, Lucas Bang, Corina S. Pasareanu, Pasquale Malacaria & Tevfik Bultan (2017): _Synthesis of Adaptive Side-Channel Attacks_.  In: CSF, IEEE Computer Society, pp. 328–342, 10.1109/CSF.2017.8.
  * [33] Tachio Terauchi & Alexander Aiken (2005): _Secure Information Flow as a Safety Problem_.  In Chris Hankin & Igor Siveroni, editors: Proceedings of the 12th International Symposium on Static Analysis (SAS 2005), Lecture Notes in Computer Science 3672, Springer, pp. 352–367, 10.1007/11547662_24.
  * [34] Saeid Tizpaz-Niari, Pavol Cerný & Ashutosh Trivedi (2019): _Quantitative Mitigation of Timing Side Channels_.  In Işil Dillig & Serdar Tasiran, editors: CAV, Part I, Lecture Notes in Computer Science 11561, Springer, pp. 140–160, 10.1007/978-3-030-25540-4_8.
  * [35] Panagiotis Vasilikos, Flemming Nielson & Hanne Riis Nielson (2018): _Secure Information Release in Timed Automata_.  In Lujo Bauer & Ralf Küsters, editors: POST, Lecture Notes in Computer Science 10804, Springer, pp. 28–52, 10.1007/978-3-319-89722-6_2.
  * [36] Panagiotis Vasilikos, Hanne Riis Nielson, Flemming Nielson & Boris Köpf (2019): _Timing Leaks and Coarse-Grained Clocks_.  In: CSF, IEEE, pp. 32–47, 10.1109/CSF.2019.00010.
  * [37] Lingtai Wang & Naijun Zhan (2018): _Decidability of the Initial-State Opacity of Real-Time Automata_.  In Cliff B. Jones, Ji Wang & Naijun Zhan, editors: Symposium on Real-Time and Hybrid Systems - Essays Dedicated to Professor Chaochen Zhou on the Occasion of His 80th Birthday, Lecture Notes in Computer Science 11180, Springer, pp. 44–60, 10.1007/978-3-030-01461-2_3.
  * [38] Lingtai Wang, Naijun Zhan & Jie An (2018): _The Opacity of Real-Time Automata_.  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37(11), pp. 2845–2856, 10.1109/TCAD.2018.2857363.
  * [39] Meng Wu, Shengjian Guo, Patrick Schaumont & Chao Wang (2018): _Eliminating timing side-channel leaks using program repair_.  In Frank Tip & Eric Bodden, editors: ISSTA, ACM, pp. 15–26, 10.1145/3213846.3213851.