[MTV] Dylan Marinho (LORIA) - Ensuring opacity in timed systems
Information leakage can have dramatic consequences on the security of complex timed systems.
Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on timing information.
First, We propose a definition of timed opacity w.r.t. execution time, where a system is opaque whenever the attacker is unable to deduce the reachability of some private state solely based on the execution time. We also extend this definition to a notion of expiring opacity, where the secrecy is violated only when the private state was entered ''recently'', ie. within a given time bound (or expiration date) prior to system completion.
We study here execution-time opacity problems (with or without expiring secrecy) in timed automata. Then, we study the decidability of several parameterized problems, when some internal timing constants become timing parameters of unknown constant values.
We finally address the control of timed systems to avoid timing leaks. We focus on the exhibition of a controller, ie. a set of allowed actions, such that the system restricted to those actions is execution-time opaque for all its execution times.
We first show that this problem is not more complex than the simple check of the opacity, and then we propose an algorithm, implemented and evaluated in practice.
This presentation is mainly based on publications at ACM TOSEM (2022), FTSCS 2022 and ICECCS 2023, and on join works with Étienne André, Shapagat Bolat, Engel Lefaucheux, Didier Lime and Sun Jun.