实时自动机的不透明性

Lingtai Wang, Naijun Zhan and Jie An (2018)：The opacity of real-time automata. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, 37(11): 2845-2856

背景：随着互联网和数据科学的发展，信息安全和隐私已经成为计算机科学的基本科学问题之一。多数信息安全和隐私问题均可以归结为系统不透明性问题，即入侵者不能够根据系统可观察状态或者行为推理出隐私状态或者行为，前者成为状态不透明，后者称为语言不透明性。已有工作表明不考虑时间因素，如果系统的行为适用有穷状态自动机，系统的状态不透明性和语言不透明性均是可判定的。

科学难题：实际许多系统或者协议的均与时间相关，如何考虑在实时条件下系统的不透明性是一个具有重要理论意义和实际价值的科学问题。但是已有工作表明在实时条件下许多系统的不透明性变得不可判定，例如时间自动机的不透明性变得不可判定，甚至它的真子集——事件记录时间自动机（event recorded timed automata）的状态不透明性和语言不透明性均是不可判定的。能否找到时间自动机一个子集，它的表达能力足够描述多数通讯协议，但是它的各种不透明性问题仍旧是可以判定的是一个挑战性科学问题。

重要突破：我们研究了实时自动机（Real-time Automata，RTA）的初始状态不透明性问题，在外界侵入者只具有部分观察能力的条件下，给定若干初始状态作为系统的秘密，要求在系统的任意运行中，入侵者不能确定此次运行一定是从秘密的初始状态开始的。我们还考虑了语言不透明性问题，指在外界侵入者具有部分观察能力的条件下，给定若干系统运行轨迹作为系统的秘密，要求在系统的任意运行中，侵入者不能确定此次运行的轨迹一定是秘密的运行轨迹。为此，我们提出了轨迹等价性关系，将实时自动机转化为满足轨迹等价性的有限状态自动机，并且给出这类自动机的投影的计算方法，从而通过已有的有限状态自动机的乘法运算和补运算，来解决实时自动机的不透明性问题。从而得到结论，对于实时自动机来说，初始状态不透明性问题，以及语言不透明性问题，都是可判定的。这是关于实时系统不透明性可判定的第一个结果，初步结果发表在嵌入式系统方面著名会议EMSOFT 2018上，全文发表在著名杂志IEEE TCAD上。