-
The 2-Dimensional Constraint Loop Problem is Decidable
Authors:
Quentin Guilmant,
Engel Lefaucheux,
Joël Ouaknine,
James Worrell
Abstract:
A linear constraint loop is specified by a system of linear
inequalities that define the relation between the values of the
program variables before and after a single execution of the loop
body. In this paper we consider the problem of determining whether
such a loop terminates, i.e., whether all maximal executions are
finite, regardless of how the loop is initialised and how the
non-…
▽ More
A linear constraint loop is specified by a system of linear
inequalities that define the relation between the values of the
program variables before and after a single execution of the loop
body. In this paper we consider the problem of determining whether
such a loop terminates, i.e., whether all maximal executions are
finite, regardless of how the loop is initialised and how the
non-determinism in the loop body is resolved. We focus on the
variant of the termination problem in which the loop variables range
over $\mathbb{R}$. Our main result is that the termination problem
is decidable over the reals in dimension~2. A more abstract
formulation of our main result is that it is decidable whether a
binary relation on $\mathbb{R}^2$ that is given as a conjunction of
linear constraints is well-founded.
△ Less
Submitted 26 April, 2024;
originally announced May 2024.
-
Expiring opacity problems in parametric timed automata
Authors:
Étienne André,
Engel Lefaucheux,
Dylan Marinho
Abstract:
Information leakage can have dramatic consequences on the security of real-time systems. Timing leaks occur when an attacker is able to infer private behavior depending on timing information. In this work, we propose a definition of expiring timed opacity w.r.t. execution time, where a system is opaque whenever the attacker is unable to deduce the reachability of some private state solely based on…
▽ More
Information leakage can have dramatic consequences on the security of real-time systems. Timing leaks occur when an attacker is able to infer private behavior depending on timing information. In this work, we propose a definition of expiring timed opacity w.r.t. execution time, where a system is opaque whenever the attacker is unable to deduce the reachability of some private state solely based on the execution time; in addition, the secrecy is violated only when the private state was entered "recently", i.e., within a given time bound (or expiration date) prior to system completion. This has an interesting parallel with concrete applications, notably cache deducibility: it may be useless for the attacker to know the cache content too late after its observance. We study here expiring timed opacity problems in timed automata. We consider the set of time bounds (or expiration dates) for which a system is opaque and show when they can be effectively computed for timed automata. We then study the decidability of several parameterized problems, when not only the bounds, but also some internal timing constants become timing parameters of unknown constant values.
△ Less
Submitted 12 March, 2024;
originally announced March 2024.
-
Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata
Authors:
Étienne André,
Engel Lefaucheux,
Didier Lime,
Dylan Marinho,
Jun Sun
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.…
▽ More
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.
△ Less
Submitted 31 October, 2023;
originally announced October 2023.
-
strategFTO: Untimed control for timed opacity
Authors:
Étienne André,
Shapagat Bolat,
Engel Lefaucheux,
Dylan Marinho
Abstract:
We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the total execution time. The system, here modeled by timed automata, is deemed opaque if for any execution time, there are either no corresponding runs, or both pu…
▽ More
We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the total execution time. The system, here modeled by timed automata, is deemed opaque if for any execution time, there are either no corresponding runs, or both public and private corresponding runs. We focus on the untimed control problem: exhibiting a controller, i.e., a set of allowed actions, such that the system restricted to those actions is fully timed-opaque. We first show that this problem is not more complex than the full timed opacity problem, and then we propose an algorithm, implemented and evaluated in practice.
△ Less
Submitted 25 November, 2022;
originally announced November 2022.
-
Model Checking Linear Dynamical Systems under Floating-point Rounding
Authors:
Engel Lefaucheux,
Joël Ouaknine,
David Purser,
Mohammadamin Sharifi
Abstract:
We consider linear dynamical systems under floating-point rounding. In these systems, a matrix is repeatedly applied to a vector, but the numbers are rounded into floating-point representation after each step (i.e., stored as a fixed-precision mantissa and an exponent). The approach more faithfully models realistic implementations of linear loops, compared to the exact arbitrary-precision setting…
▽ More
We consider linear dynamical systems under floating-point rounding. In these systems, a matrix is repeatedly applied to a vector, but the numbers are rounded into floating-point representation after each step (i.e., stored as a fixed-precision mantissa and an exponent). The approach more faithfully models realistic implementations of linear loops, compared to the exact arbitrary-precision setting often employed in the study of linear dynamical systems.
Our results are twofold: We show that for non-negative matrices there is a special structure to the sequence of vectors generated by the system: the mantissas are periodic and the exponents grow linearly. We leverage this to show decidability of $ω$-regular temporal model checking against semialgebraic predicates. This contrasts with the unrounded setting, where even the non-negative case encompasses the long-standing open Skolem and Positivity problems.
On the other hand, when negative numbers are allowed in the matrix, we show that the reachability problem is undecidable by encoding a two-counter machine. Again, this is in contrast with the unrounded setting where point-to-point reachability is known to be decidable in polynomial time.
△ Less
Submitted 27 January, 2023; v1 submitted 8 November, 2022;
originally announced November 2022.
-
Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set
Authors:
Julian D'Costa,
Engel Lefaucheux,
Eike Neumann,
Joël Ouaknine,
James Worrell
Abstract:
We study the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets. We establish a uniform upper bound on the number of iterations it takes for every orbit of a rational matrix to escape a compact semialgebraic set defined over rational data. Our bound is doubly exponential in the ambient dimension, singly exponential in the degrees of the polynomials used to de…
▽ More
We study the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets. We establish a uniform upper bound on the number of iterations it takes for every orbit of a rational matrix to escape a compact semialgebraic set defined over rational data. Our bound is doubly exponential in the ambient dimension, singly exponential in the degrees of the polynomials used to define the semialgebraic set, and singly exponential in the bitsize of the coefficients of these polynomials and the bitsize of the matrix entries. We show that our bound is tight by providing a matching lower bound.
△ Less
Submitted 5 August, 2022; v1 submitted 4 July, 2022;
originally announced July 2022.
-
The boundedness and zero isolation problems for weighted automata over nonnegative rationals
Authors:
Wojciech Czerwiński,
Engel Lefaucheux,
Filip Mazowiecki,
David Purser,
Markus A. Whiteland
Abstract:
We consider linear cost-register automata (equivalent to weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems of boundedness and zero isolation ask whether there is a sequence of words that converge to infinity and to zero, respectively. In the general model both problems are undecidable so we focus on the copyless linear restrict…
▽ More
We consider linear cost-register automata (equivalent to weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems of boundedness and zero isolation ask whether there is a sequence of words that converge to infinity and to zero, respectively. In the general model both problems are undecidable so we focus on the copyless linear restriction. There, we show that the boundedness problem is decidable.
As for the zero isolation problem we need to further restrict the class. We obtain a model, where zero isolation becomes equivalent to universal coverability of orthant vector addition systems (OVAS), a new model in the VAS family interesting on its own. In standard VAS runs are considered only in the positive orthant, while in OVAS every orthant has its own set of vectors that can be applied in that orthant. Assuming Schanuel's conjecture is true, we prove decidability of universal coverability for three-dimensional OVAS, which implies decidability of zero isolation in a model with at most three independent registers.
△ Less
Submitted 26 May, 2022;
originally announced May 2022.
-
On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets
Authors:
Julian D'Costa,
Engel Lefaucheux,
Eike Neumann,
Joël Ouaknine,
James Worrell
Abstract:
We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free $\exists \forall$-sentences without strict inequalities. We derive several equivalent chara…
▽ More
We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free $\exists \forall$-sentences without strict inequalities. We derive several equivalent characterisations of the associated complexity class which demonstrate its robustness and illustrate its expressive power. We show that the Compact Escape Problem is complete for this class.
△ Less
Submitted 5 July, 2021;
originally announced July 2021.
-
Porous Invariants
Authors:
Engel Lefaucheux,
Joël Ouaknine,
David Purser,
James Worrell
Abstract:
We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; these invariants are not necessarily convex, and can in fact contain infinitely many 'holes'. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle (non-)reachability questions for various interesting clas…
▽ More
We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; these invariants are not necessarily convex, and can in fact contain infinitely many 'holes'. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle (non-)reachability questions for various interesting classes of affine loops and target sets.
△ Less
Submitted 1 June, 2021;
originally announced June 2021.
-
The Orbit Problem for Parametric Linear Dynamical Systems
Authors:
Christel Baier,
Florian Funke,
Simon Jantsch,
Toghrul Karimov,
Engel Lefaucheux,
Florian Luca,
Joël Ouaknine,
David Purser,
Markus A. Whiteland,
James Worrell
Abstract:
We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters.
More precisely, consider a $d$-dimensional square matrix $M$ whose entries are algebraic functions in one or more real variables. Given initial and target vectors $u,v\in \mathbb{Q}^d$, the parametric poi…
▽ More
We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters.
More precisely, consider a $d$-dimensional square matrix $M$ whose entries are algebraic functions in one or more real variables. Given initial and target vectors $u,v\in \mathbb{Q}^d$, the parametric point-to-point orbit problem asks whether there exist values of the parameters giving rise to a concrete matrix $N \in \mathbb{R}^{d\times d}$, and a positive integer $n\in \mathbb{N}$, such that $N^nu = v$.
We show decidability for the case in which $M$ depends only upon a single parameter, and we exhibit a reduction from the well-known Skolem Problem for linear recurrence sequences, suggesting intractability in the case of two or more parameters.
△ Less
Submitted 13 August, 2021; v1 submitted 21 April, 2021;
originally announced April 2021.
-
Reachability in Dynamical Systems with Rounding
Authors:
Christel Baier,
Florian Funke,
Simon Jantsch,
Toghrul Karimov,
Engel Lefaucheux,
Joël Ouaknine,
Amaury Pouly,
David Purser,
Markus A. Whiteland
Abstract:
We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix $M \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose ever…
▽ More
We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix $M \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose every entry is a multiple of $g$, we are interested in the behaviour of the orbit $\mathcal{O}={<}[x], [M[x]],[M[M[x]]],\dots{>}$, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability---whether a given target $y \in\mathbb{Q}^{d}$ belongs to $\mathcal{O}$---is PSPACE-complete for hyperbolic systems (when no eigenvalue of $M$ has modulus one). We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.
△ Less
Submitted 28 September, 2020;
originally announced September 2020.
-
One-Clock Priced Timed Games with Negative Weights
Authors:
Thomas Brihaye,
Gilles Geeraerts,
Axel Haddad,
Engel Lefaucheux,
Benjamin Monmege
Abstract:
Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modelling the cost of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary integer wei…
▽ More
Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modelling the cost of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary integer weights and show that, for an important subclass of them (the so-called simple priced timed games), one can compute, in pseudo-polynomial time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called negative-reset-acyclic priced timed games (with arbitrary integer weights and one clock). The decidability status of the full class of priced timed games with one-clock and arbitrary integer weights still remains open.
△ Less
Submitted 6 August, 2022; v1 submitted 7 September, 2020;
originally announced September 2020.
-
On Positivity and Minimality for Second-Order Holonomic Sequences
Authors:
George Kenison,
Oleksiy Klurman,
Engel Lefaucheux,
Florian Luca,
Pieter Moree,
Joël Ouaknine,
Markus A. Whiteland,
James Worrell
Abstract:
An infinite sequence $\langle{u_n}\rangle_{n\in\mathbb{N}}$ of real numbers is holonomic (also known as P-recursive or P-finite) if it satisfies a linear recurrence relation with polynomial coefficients. Such a sequence is said to be positive if each $u_n \geq 0$, and minimal if, given any other linearly independent sequence $\langle{v_n}\rangle_{n \in\mathbb{N}}$ satisfying the same recurrence re…
▽ More
An infinite sequence $\langle{u_n}\rangle_{n\in\mathbb{N}}$ of real numbers is holonomic (also known as P-recursive or P-finite) if it satisfies a linear recurrence relation with polynomial coefficients. Such a sequence is said to be positive if each $u_n \geq 0$, and minimal if, given any other linearly independent sequence $\langle{v_n}\rangle_{n \in\mathbb{N}}$ satisfying the same recurrence relation, the ratio $u_n/v_n$ converges to $0$. In this paper, we focus on holonomic sequences satisfying a second-order recurrence $g_3(n)u_n = g_2(n)u_{n-1} + g_1(n)u_{n-2}$, where each coefficient $g_3, g_2,g_1 \in \mathbb{Q}[n]$ is a polynomial of degree at most $1$. We establish two main results. First, we show that deciding positivity for such sequences reduces to deciding minimality. And second, we prove that deciding minimality is equivalent to determining whether certain numerical expressions (known as periods, exponential periods, and period-like integrals) are equal to zero. Periods and related expressions are classical objects of study in algebraic geometry and number theory, and several established conjectures (notably those of Kontsevich and Zagier) imply that they have a decidable equality problem, which in turn would entail decidability of Positivity and Minimality for a large class of second-order holonomic sequences.
△ Less
Submitted 23 July, 2020;
originally announced July 2020.
-
On the Monniaux Problem in Abstract Interpretation
Authors:
Nathanaël Fijalkow,
Engel Lefaucheux,
Pierre Ohlmann,
Joël Ouaknine,
Amaury Pouly,
James Worrell
Abstract:
The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program $P$, a safety (\emph{e.g.}, non-reachability) specification $\varphi$, and an abstract domain of invariants $\mathcal{D}$, does there exist an inductive invariant $I$ in $\mathcal{D}$ guaranteeing that program $P$ meets its specification $\varphi$. The Monniaux Probl…
▽ More
The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program $P$, a safety (\emph{e.g.}, non-reachability) specification $\varphi$, and an abstract domain of invariants $\mathcal{D}$, does there exist an inductive invariant $I$ in $\mathcal{D}$ guaranteeing that program $P$ meets its specification $\varphi$. The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers. In this paper, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops.
△ Less
Submitted 18 July, 2019;
originally announced July 2019.
-
Simple Priced Timed Games Are Not That Simple
Authors:
Thomas Brihaye,
Gilles Geeraerts,
Axel Haddad,
Engel Lefaucheux,
Benjamin Monmege
Abstract:
Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modeling the costs of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary (positive a…
▽ More
Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modeling the costs of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary (positive and negative) weights and show that, for an important subclass of theirs (the so-called simple priced timed games), one can compute, in exponential time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called reset-acyclic priced timed games (with arbitrary weights and one-clock).
△ Less
Submitted 21 September, 2015; v1 submitted 14 July, 2015;
originally announced July 2015.
