Verifying Opacity of Discrete-Timed Automata Artifact

Opacity is a powerful confidentiality property that holds if a system cannot leak secret information through observable behavior. In recent years, time has become an increasingly popular attack vector. The notion of opacity has therefore been extended to timed automata (TA). However, the verification of opacity of TA has been proven to be undecidable for the commonly used dense time model. To make the problem decidable, state of the art approaches consider weaker notions of opacity or heavily restrict the class of considered TA, resulting in unrealistic threat models.<br>We address the problem of verifying opacity of TA without restrictions. For this purpose, we consider a discrete time setting. We present a novel algorithm to transform TA to equivalent finite automata (FA) and then use known methods to verify opacity of the resulting FA. To improve the efficiency of our algorithm, we use a novel time abstraction that significantly reduces the state space of the resulting FA, improving the scalability of our approach. We validate our method using randomized systems, as well as four case studies from the literature showing that our approach is applicable in practice.<br><br>We provide a VM with all software pre-installed to run our evaluation.<br>The code is also provided in our gitlab repository: https://gitlab.com/julianklein/opacity-verification-of-discrete-timed-automataThe VM has commit b3b18a0f8bb071a6c0e0b29be5c11e5a1caa4c84 (on main branch) installed.

不透明性（Opacity）是一项关键的机密性属性，当系统无法通过可观测行为泄露机密信息时，该属性成立。近年来，时间已逐渐成为愈发常见的攻击载体。因此，不透明性的概念已被拓展至时间自动机（Timed Automata, TA）领域。然而，针对当前常用的稠密时间模型，时间自动机的不透明性验证已被证明是不可判定的。为使该问题变为可判定问题，现有主流方法要么采用弱化版的不透明性概念，要么对所研究的时间自动机类别施加严格限制，这会导致威胁模型脱离实际场景。
本研究针对无限制条件下的时间自动机不透明性验证问题展开探索。为此，我们采用离散时间设定进行建模。我们提出一种全新算法，可将时间自动机转换为等价的有限自动机（Finite Automata, FA），随后借助已有方法对转换得到的有限自动机进行不透明性验证。为提升算法效率，我们引入一种新颖的时间抽象方法，可大幅缩减转换后有限自动机的状态空间，进而提升本方法的可扩展性。我们通过随机系统以及来自现有文献的4项案例研究对本方法进行验证，结果表明本方法在实际场景中具备可应用性。

我们提供了预安装所有评估所需软件的虚拟机（Virtual Machine, VM）。相关代码已上传至我们的GitLab代码仓库：https://gitlab.com/julianklein/opacity-verification-of-discrete-timed-automata。该虚拟机已安装主分支上提交标识为b3b18a0f8bb071a6c0e0b29be5c11e5a1caa4c84的代码版本。