@inproceedings{c07cb34d97e244a4af0669f73722d41a,
title = "strategFTO: Untimed Control for Timed Opacity",
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 modelled 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, ie 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.",
keywords = "control, imitator, opacity, security, timed automata, timing leak",
author = "{\'E}tienne Andr{\'e} and Shapagat Bolat and Engel Lefaucheux and Dylan Marinho",
note = "Publisher Copyright: {\textcopyright} 2022 ACM.; 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2022, co-located with the ACM SIGPLAN Conference on ; Conference date: 07-12-2022",
year = "2022",
month = nov,
day = "29",
doi = "10.1145/3563822.3568013",
language = "English",
series = "FTSCS 2022 - Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, co-located with SPLASH 2022",
publisher = "Association for Computing Machinery, Inc",
pages = "27--33",
editor = "Cyrille Artho and Olveczky, \{Peter Csaba\}",
booktitle = "FTSCS 2022 - Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, co-located with SPLASH 2022",
}