Execution-time opacity problems in one-clock parametric timed automata

TL;DR

This paper investigates the decidability of execution-time opacity in one-clock parametric timed automata, showing decidability for single parameters and undecidability for multiple parameters, with implications for system security analysis.

Contribution

It establishes the decidability boundary of full execution-time opacity in one-clock PTAs, providing effective synthesis methods for single-parameter cases and undecidability results for multiple parameters.

Findings

Decidability for single-parameter PTAs with exact synthesis.

Undecidability for multi-parameter PTAs.

Decidability of an existential variant of execution-time opacity.

Abstract

Parametric timed automata (PTAs) extend the concept of timed automata, by allowing timing delays not only specified by concrete values but also by parameters, allowing the analysis of systems with uncertainty regarding timing behaviors. The full execution-time opacity is defined as the problem in which an attacker must never be able to deduce whether some private location was visited, by only observing the execution time. The problem of full ET-opacity emptiness (i.e., the emptiness over the parameter valuations for which full execution-time opacity is satisfied) is known to be undecidable for general PTAs. We therefore focus here on one-clock PTAs with integer-valued parameters over dense time. We show that the full ET-opacity emptiness is undecidable for a sufficiently large number of parameters, but is decidable for a single parameter, and exact synthesis can be effectively achieved. Our proofs rely on a novel construction as well as on variants of Presburger arithmetics. We finally prove an additional decidability result on an existential variant of execution-time opacity.