An On-the-Fly Approach for the Verification of Opacity in Critical Systems

Opacity is an important security property dealing with the hiding and keeping secret, a subset of a system\´s behaviour from external observers. A system is characterised as "opaque" if it can effectively hide specific actions from an intruder or attacker. As the need for opacity, and similar fundamental secrecy properties may arise in a wide range of applications and sectors, like health care, banking, trading and voting systems, ... etc., providing efficient tools for its verification becomes important, especially for large-scale real-world systems. In this paper, we formulate opacity, based on labeled transition systems models, and provide an efficient verification algorithm within the framework of a hybrid on-the-fly approach. Our verification strategy is based on the construction of a symbolic observation graph, allowing for the abstraction of the system\´s behaviour, while preserving the necessary structure needed for the checking of the opacity property dealt with in this paper. The preliminary implementation of our algorithm and the provided experimental results are promising, and demonstrate its effectiveness in face of the exponential state explosion problem, compared with existing techniques.