Verification of Resilient Current-State Opacity Against Dynamic Sensor-Enabling Attacks

• 成果类型: Article
• 署名作者: Ma, Ziyue; Tong, Yin; Yin, Xiang
• 署名单位: Xidian University; Zhejiang University; Southwest Jiaotong University; Shanghai Jiao Tong University; Shanghai Jiao Tong University
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2026.3684361
• 发表日期: 2026
• 关键词: Supervisory control; diagnosability

摘要

In this article, we study the problem of verifying resilient opacity in discrete-event systems in the presence of dynamic sensor attacks. The system contains several secret states, each assigned a secret level. The system is vulnerable to sensor-enabling attacks by potential intruders: such attacks allow the intruder to make certain originally unobservable events temporarily observable. We propose the notion of resilient current-state opacity (R-CSO), which is a property that ensures an intruder cannot definitively determine that the system is currently in a secret state with a secret level $k$ by performing fewer than $k$ attacks. To verify R-CSO in a given system, we propose a novel type of bipartite transition system (BTS), called the R-CSO BTS, which models the interaction between the system and the intruder. Based on R-CSO BTS, we then derive a necessary and sufficient condition for verifying R-CSO. Finally, we prove that if the sensor mask is distinct, i.e., the intruder has the capability to differentiate between originally observable and attackable events, then the R-CSO verification can be simplified by only encoding binary attack decisions into the R-CSO BTS.