论文标题
Strategfto：定时不透明度的不断控制
strategFTO: Untimed control for timed opacity
论文作者
论文摘要
我们介绍了一个原型工具strategto，该工具FARTAGE FTO解决了关键软件中安全属性的验证。我们考虑了定时不透明度的最新定义，其中攻击者的目的是在仅访问总执行时间的同时推断出一些秘密。该系统以定时自动机对建模，如果在任何执行时间内都没有相应的运行，则被认为是不透明的，或者既没有相应的运行，否则公共和私人和相应的运行。我们专注于不合时宜的控制问题：展示控制器，即一组允许的动作，使得限制在这些动作的系统是完全时机的。我们首先表明，这个问题并不比完整的定时不透明度问题更复杂，然后我们提出了一种在实践中实施和评估的算法。
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 modeled 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, i.e., 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.
