Execution-time opacity control for timed automata
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.