Opacity is a powerful confidentiality property which guarantees that secret information of a system cannot be inferred from its observable behavior. To account for timing attacks, opacity has been extended to continuous-time systems, but the verification problem was proven to be generally undecidable. As a result, multiple recent works study the opacity verification problem of discrete-timed automata. The advantage of a discrete time setting is that it can discretize any timed automaton as a discrete-state system, where opacity can be verified. However, such verification methods usually rely on separating time steps into distinct hybrid states. This results in state explosion and limited scalability for real-world problems. In this paper, we present a new, more efficient verification method for opacity in a discrete time setting that avoids the state explosion problem. Our verification method groups multiple time steps to intervals, instead of evaluating each time step individually. We define four timed opacity notions and show that our method is capable of verifying all of them in a unified manner. We analyze the efficiency of our method on a case study of a wireless sensor network and randomized systems.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Unified Method to Efficiently Verify Opacity of Discrete-Timed Automata

  • Julian Klein,
  • Kuize Zhang,
  • Sabine Glesner

摘要

Opacity is a powerful confidentiality property which guarantees that secret information of a system cannot be inferred from its observable behavior. To account for timing attacks, opacity has been extended to continuous-time systems, but the verification problem was proven to be generally undecidable. As a result, multiple recent works study the opacity verification problem of discrete-timed automata. The advantage of a discrete time setting is that it can discretize any timed automaton as a discrete-state system, where opacity can be verified. However, such verification methods usually rely on separating time steps into distinct hybrid states. This results in state explosion and limited scalability for real-world problems. In this paper, we present a new, more efficient verification method for opacity in a discrete time setting that avoids the state explosion problem. Our verification method groups multiple time steps to intervals, instead of evaluating each time step individually. We define four timed opacity notions and show that our method is capable of verifying all of them in a unified manner. We analyze the efficiency of our method on a case study of a wireless sensor network and randomized systems.