Timing information leakage occurs whenever an attacker successfully deduces confidential internal information by observing some timed information such as events with timestamps. Timed automata are an extension of finite-state automata with a set of clocks evolving linearly and that can be tested or reset, making this formalism able to reason on systems involving concurrency and timing constraints. In this paper, we summarize a recent line of works using timed automata as the input formalism, in which we assume that the attacker has access (only) to the system execution time. First, we address the following execution-time opacity problem: given a timed system modeled by a timed automaton, given a secret location and a final location, synthesize the execution times from the initial location to the final location for which one cannot deduce whether the secret location was visited. This means that for any such execution time, the system is opaque: either the final location is not reachable, or it is reachable with that execution time for both a run visiting and a run not visiting the secret location. We also address the full execution-time opacity problem, asking whether the system is opaque for all execution times; we also study a weak counterpart. Second, we add timing parameters, which are a way to configure a system: we identify a subclass of parametric timed automata with some decidability results. In addition, we devise a semi-algorithm for synthesizing timing parameter valuations guaranteeing that the resulting system is opaque. Third, we report on problems when the secret has itself an expiration date, thus defining expiring execution-time opacity problems. We finally show that our method can also apply to program analysis with configurable internal timings.

翻译：时间信息泄露发生在攻击者通过观察带时间戳的事件等时序信息成功推断出机密内部信息时。时间自动机是有限状态自动机的扩展，配有一组线性演变的时钟，这些时钟可被测试或重置，使该形式化方法能够处理涉及并发和时序约束的系统。本文总结了近期以时间自动机作为输入形式化方法的一系列研究工作，其中假设攻击者仅能获取系统执行时间。首先，我们解决以下执行时间不透明性问题：给定由时间自动机建模的时序系统，以及秘密位置和最终位置，综合从初始位置到最终位置且无法推断秘密位置是否被访问过的执行时间。这意味着对于任何此类执行时间，系统是不透明的：要么最终位置不可达，要么既可被经过秘密位置的运行也可被未经过秘密位置的运行以该执行时间到达。我们还研究了完全执行时间不透明性问题，即系统对所有执行时间是否保持不透明，并探讨了其弱对应形式。其次，我们引入时间参数作为系统配置方式：识别了一类具有可判定性结果的参数化时间自动机子类。此外，我们设计了一种半算法来合成保证结果系统不透明的时间参数估值。第三，我们报告了当秘密本身具有过期时间时的问题，由此定义了过期执行时间不透明性问题。最后，我们证明该方法同样适用于具有可配置内部时序的程序分析。