发表机构
Institut Polytechnique de Paris; Sorbonne Université; Université Paris Est Créteil（巴黎理工学院; 索邦大学; 巴黎东克雷泰伊大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对定时系统中执行时间泄露机密的问题，提出执行时间不透明性逻辑（ETOL），通过区域模型检查实现可判定验证，并在ATM案例中验证其高效性。
AI 中文摘要
确保网络物理系统中的机密性至关重要，尤其是当攻击者利用执行时间来推断敏感信息时。传统的透明性模型不足以应对定时系统，因为在定时自动机中验证透明性是不可判定的。为了应对这一挑战，我们提出了执行时间不透明性逻辑（ETOL），这是一种新的形式化方法，通过要求对于每个满足秘密公式的执行，存在另一个相同持续时间的执行不满足该公式来指定不透明性。ETOL保证时间观察不能揭示机密的智能体活动。我们提出了一种基于区域模型检查的可判定且高效的验证框架，并辅以专门算法，系统地识别持续时间等价的执行。我们的方法通过ATM案例研究得到验证，表明ETOL能够在定时攻击下高效验证执行时间机密性。我们还开发了一个支持定时系统符号模型检查的ETOL逻辑原型工具，允许用户基于时钟约束的执行路径验证ETOL公式。
英文摘要
Ensuring confidentiality in Cyber-Physical Systems is critical, especially when attackers exploit execution times to infer sensitiveinformation. Traditional opacity models are inadequate for timed systems, as verifying opacity in Timed Automata is undecidable. To address this challenge, we propose Execution-Time Opacity Logic (ETOL), a new formalism that specifies opacity by requiring that for every execution satisfying a secret formula, there exists another execution of the same duration that does not satisfy it. ETOL guarantees that timing observations cannot reveal confidential agent activities. We present a decidable and efficient verification framework based on zone-based model checking, supported by a dedicated algorithm that systematically identifies duration-equivalent executions. Our approach is validated through an ATM case study, showing that ETOL enables efficient verification of execution-time confidentiality under timing attacks. We also developed a prototype tool for the ETOL logic that supports symbolic model checking over timed systems. It allows users to verify ETOL formulas based on clock-constrained execution paths.
