近日，中国科学院软件研究所天基综合信息系统全国重点实验室安杰副研究员（第一作者）的论文The Opacity of Timed Automata被形式化方法领域顶级国际学术会议International Symposium on Formal Methods (FM 2024)接收。论文关注实时系统的不透明性（Opacity）这一信息安全性质，针对广泛使用的实时系统形式模型时间自动机（Timed Automata）的不透明性可判定问题进行了系统讨论，同时给出了时间自动机任意子类不透明性的可判定充分条件和必要条件来刻画出可判定的边界。
不透明性是描述系统内信息流安全性、保密性和隐私性的一类超性质(Hyperproperty)。它是指系统外部观察者不能通过系统的可观测行为推理出系统的秘密。传统系统的不透明性通常是可判定的，但实时系统的行为涉及到时限信息，其不透明性更为复杂、往往不可判定。2009年，实时系统验证领域知名学者F. Cassez基于时间自动机普遍性（Universality）问题不可判定这一经典结论，将时间自动机的普遍性问题归约为时间自动机的不透明性问题，证明出时间自动机的不透明性是不可判定的。
在上述研究的基础上，研究团队进一步探究发现，由于已有经典结论指出单时钟时间自动机的普遍性问题是可判定的，那么Cassez的证明便无法适用单时钟时间自动机的不透明性判定。为此，研究团队探索了一种新的证明方法：首先形式化定义时间自动机的三种常见不透明性，即基于语言不透明性（Language-Based Timed Opacity, LBTO）、基于起始状态的不透明性（Initial-Location Timed Opacity, ILTO）和基于当前状态的不透明性（Current-Location Timed Opacity, CLTO），并理论证明了三者之间的转换关系。受到Cassez原始证明的启发，研究团队将带有epsilon迁移的单时钟时间自动机的普遍性（Universality）问题归约为单时钟时间自动机的CLTO问题，根据经典结论已指出前者是不可判定的，证明了单时钟时间自动机的CLTO问题的不可判定。结合三种不透明性的转化关系，从而证明出单时钟自动机的ILTO和LBTO同样不可判定。
此外，研究团队构造性证明了Cassez在研究中遗留的猜想——离散时间语义下时间自动机不透明性的可判定。团队通过在离散时间语义下，借助整型自动机（Integral Automata）的Tick语言，将时间自动机的LBTO问题转化为带有epsilon迁移的非确定有穷自动机的语言包含（Language Inclusion）问题，基于经典结论指出后者是可判定的，从而证明了LBTO问题的可判定；结合LBTO和ILTO、CLTO的转化关系，推证出离散时间语义下时间自动机的ILTO和CLTO问题也是可判定的。
那么，哪些时间自动机子集的不透明性是可判定的？不透明性的可判定边界在哪里？为进一步探索时间自动机子集的不透明性可判定问题，研究团队借助时间自动机基本原理和经典性质，给出并证明了任意时间自动机子集不透明性可判定的充分条件和必要条件——充分条件要求该子集在乘积、取补和投影运算下封闭，必要条件则需要该子集的普遍性问题是可判定的，刻画出了不透明性的可判定边界，为设计具有不透明性的实时系统迈出关键一步。
可判定边界充分条件和必要条件示意图
供稿：天基综合信息系统全国重点实验室
END
编辑 | 龙梦姣
责编 | 张欢
