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 behavior. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. It can be decided whether a TA is opaque in this setting. In this work, we tackle control, and show that we are able to decide whether a TA can be controlled at runtime to ensure opacity. Our method is constructive, in the sense that we can exhibit such a controller. This is joint work with Etienne André, Marie Duflot and Engel Lefaucheux.

Authors

• Laetitia Laversa

Keywords

No keywords are indexed for this paper.