技术摘要：定时不透明性的光明面

1. 问题陈述

本文研究了**定时自动机（Timed Automata, TAs）的定时不透明性（timed opacity）**问题。定时不透明性形式化了在攻击者观察一组带有时间戳的动作子集的情况下，关于系统中指定“私有”位置的信息泄露缺失情况。核心安全目标是确保攻击者无法确定地推断出系统执行过程中是否访问了某个私有位置。

该问题的研究动机源于 Cassez [Cas09] 的开创性工作，该工作确立了定时不透明性对于一般的 TAs 是不可判定的，甚至对于受限的**事件记录自动机（Event-Recording Automata, ERAs）**也是如此。这种不可判定性源于攻击者为了关联时间戳而需要无界的内存，以及 TAs 具有无限状态空间。作者旨在通过限制系统模型或攻击者的能力来寻找该问题的“光明面”，从而恢复可判定性。

本文根据私有运行生成的轨迹集（$Tr_{priv}$）与公共运行生成的轨迹集（$Tr_{pub}$）之间的关系，定义了三种不透明性变体：

1. $\exists$-不透明性（$\exists$-opacity）： 存在至少一个同时属于私有运行和公共运行的轨迹（最弱的形式）。
2. 弱不透明性（Weak opacity）： 每个私有轨迹也是公共轨迹（$Tr_{priv} \subseteq Tr_{pub}$）。
3. 完全不透明性（Full opacity）： 私有轨迹集与公共轨迹集完全相同（$Tr_{priv} = Tr_{pub}$）。

2. 研究方法

作者结合使用了自动机理论构造、向经典 TA 问题（可达性、语言包含问题）的归约以及复杂度分析。

2.1. 互归约框架

一个基础性的方法论贡献是建立了不透明性变体与经典 TA 问题之间的互归约性（inter-reducibility）：

• 弱不透明性 vs. 完全不透明性： 被证明可以通过一种交换私有运行与公共运行的构造进行互归约（定理 4.5）。这使得作者可以专注于其中一种变体（通常是弱不透明性）来进行可判定性证明。
• $\exists$-不透明性 vs. 可达性： 被证明是互归约的。由于可达性对于 TAs 是 PSPACE 完全的，这确立了 $\exists$-不透明性的复杂度。
• 弱不透明性 vs. 语言包含问题： 被证明是互归约的。由于语言包含问题对于一般的 TAs 是不可判定的，这解释了弱/完全不透明性在一般情况下的不可判定性。

2.2. 子类分析

作者分析了特定 TA 子类的不可透明性：

• 单动作 TA（One-action TAs）： 减少字母表大小。
• 单时钟 TA（One-clock TAs）： 减少时钟数量，包括带有和不带有 $\epsilon$-转移的情况。
• 离散时间 TA（Discrete Time TAs）： 将时钟取值限制为自然数（$\mathbb{N}$）而非实数（$\mathbb{R}_{\ge 0}$）。
• 可观测 ERA（Observable ERAs, oERAs）： 一个新的子类，其中所有重置时钟的动作都是可观测的（没有隐藏的重置时钟的 $\epsilon$-转移）。

2.3. 攻击者预算削减

为了处理完整的 TA 类，作者引入了一种新的方法论，即限制攻击者的“预算”。他们定义了时间选择函数（time selection functions）（$\sigma$），用于决定攻击者何时观察系统。研究分析了三种特定的设置：

1. 前 $N$ 次观察： 攻击者仅观察前 $N$ 个可观测动作。
2. $N$ 个静态时间戳： 攻击者预先选择 $N$ 个时间点，并观察每个时间点之后发生的第一个动作。
3. $N$ 个动态时间戳： 攻击者根据之前的观察结果，自适应地选择下一个观察时间。

为了证明这些受限设置下的可判定性，作者引入了一种**“滴答”（tick）构造**。这涉及在 TA 中增加一个全局“滴答”时钟和辅助时钟，将时间词的等价类（基于整数部分和分数部分的相对顺序）编码进一个**无时间（untimed）**轨迹中。这通过将受限观察下的定时语言包含问题转化为有限正则自动机（具体为 $N$-有界语言）的语言包含问题，实现了问题的转化。

3. 核心贡献与结果

3.1. 互归约与复杂度

• 弱不透明性与完全不透明性的等价性： 作者证明了判定弱不透明性在多项式时间内等价于判定完全不透明性。这简化了对子类的分析。
• $\exists$-不透明性的复杂度： 该问题对于一般的 TAs 是 PSPACE 完全的。对于单时钟 TAs，作者证明其仍然是 PSPace 完全的（定理 5.1），从而精细化了之前的界限。

3.2. 子类的可判定性

本文精确地划定了弱/完全不透明性的可判定性边界：

• 不可判定：
  • 具有单个动作的 TA（即使没有 $\epsilon$-转移）（定理 5.2）。
  • 具有两个或更多时钟的 TA（定理 5.7）。
  • 带有 $\epsilon$-转移的单时钟 TA（定理 5.4）。
• 可判定：
  • 不带 $\epsilon$-转移的单时钟 TA：具有**非原始递归（non-primitive recursive）**复杂度（定理 5.5）。
  • 离散时间 TA：具有 EXPSPACE 完全复杂度（推论 5.14）。
  • 可观测 ERA (oERA)：具有 PSPACE 完全复杂度（定理 5.16）。

注：本文还确立了离散时间 TA 的定时语言包含问题是 EXPSPACE 完全的，这是一个此前已知可判定但精确复杂度未知的结论。

3.3. 有限攻击者预算（主要贡献）

最重要的贡献是证明了如果攻击者的观察预算限制为 $N$ 次观察，那么不透明性对于整个 TA 类都是可判定的。

• 设置： 该结果适用于所有三种攻击者模型：前 $N$ 个事件、$N$ 个静态时间戳以及 $N$ 个动态时间戳。
• 复杂度： 这三种设置下的判定问题均为 Co-NEXPTIME 完全（定理 6.19, 推论 6.20, 定理 6.31, 定理 6.33）。
• 机制： 证明依赖于“滴答”构造，将定时问题归约为 $N$-有界定时语言的包含问题，并证明该问题是 Co-NEXPTIME 完全的。

3.4. 组合限制

作者还分析了模型限制（如单时钟、离散时间）与攻击者预算的结合情况。

• 对于具有 $N$ 次观察的单动作 TA，问题仍然是 Co-NEXPTIME 完全的。
• 对于具有 $N$ 次观察的单时钟 TA，问题是 PSPACE 硬且属于 Co-NEXPTIME（定理 6.35）。
• 对于具有 $N$ 次观察的 oERA，问题是 PSPACE 完全的（定理 6.37）。

4. 重要性与主张

本文声称提供了一个关于定时不透明性可判定性图谱的全面刻画，超越了 Cassez [Cas09] 的负面结果。

• 明确边界： 本研究精确识别了触发不可判定性的最小条件（例如，单时钟 TA 中的 $\epsilon$-转移，或动作的数量）。
• 实际应用中的可判定性： 通过引入有限观察（有限攻击者预算）的概念，作者展示了只要攻击者无法观察到无限序列的事件，不透明性对于**整个类别的定时自动机（TA）**都是可判定的。这模拟了攻击者资源或监控能力有限的现实场景。
• 复杂度的紧致性： 本文为各种设置提供了精确的复杂度类（PSPACE, EXPSPACE, Co-NEXPTIME），精细化了对验证不透明性计算成本的理解。
• 方法论创新： “滴答”构造和时间选择函数的使用，为分析部分观测下的定时系统提供了新工具，弥合了稠密时间语义与有限状态验证技术之间的鸿隙。

作者总结道，虽然在高度表达性的设置下（具有无界观察的一般 TA）不可判定性依然存在，但通过将攻击者的能力限制在有限预算内，可以获得一个适用于整个 TA 形式化体系的稳健的可判定框架。