Execution-time opacity control for timed automata

TL;DR

This paper investigates runtime control strategies for timed automata to ensure execution-time opacity, addressing the decidability and construction of such strategies, including extensions to weak opacity and limited observation precision.

Contribution

It proves the undecidability of strategy existence in general, provides an EXPSPACE decision procedure for meta-strategies, and offers a constructive method to synthesize such strategies.

Findings

Deciding the existence of opacity-enforcing strategies is undecidable in general.

A constructive EXPSPACE algorithm for meta-strategy synthesis is developed.

The method extends to weak opacity and limited observation scenarios.

Abstract

Timing leaks in timed automata (TA) can occur whenever an attacker is able to deduce a secret by observing some timed behaviour. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. In earlier work, it was shown that it can be decided whether a TA is opaque in this setting. In this work, we address control, and investigate whether a TA can be controlled by a strategy at runtime to ensure opacity, by enabling or disabling some controllable actions over time. We first show that, in general, it is undecidable to determine whether such a strategy exists. Second, we show that deciding whether a meta-strategy ensuring opacity exists can be done in EXPSPACE. Such a meta-strategy is a set of strategies allowing an arbitrarily large -- yet finite -- number of strategy changes per time unit, and with only weak ordering relations between such changes. Our method is constructive, in the sense that we can exhibit such a meta-strategy. We also extend our method to the case of weak opacity, when it is harmless that the attacker deduces that the private location was not visited. Finally, we consider a variant where the attacker cannot have an infinite precision in its observations.