Parametric Timed Model Checking for Guaranteeing Timed Opacity
This addresses timing information leakage in security-critical systems, providing a method to guarantee timed opacity, though it appears incremental as it builds on existing timed automata frameworks.
The paper tackles the problem of synthesizing execution times in timed systems where attackers cannot deduce secret behaviors from timing information, solving it for timed automata and extending to parametric timed automata with decidability analysis and algorithms.
Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on the system execution time. We address the following problem: given a timed system, synthesize the execution times for which one cannot deduce whether the system performed some secret behavior. We solve this problem in the setting of timed automata (TAs). We first provide a general solution, and then extend the problem to parametric TAs, by synthesizing internal timings making the TA secure. We study decidability, devise algorithms, and show that our method can also apply to program analysis.