A Data-Driven Approach to Approximate Opacity Verification

Recent results in the verification of cyber-physical systems have focused not just in giving guarantees of properties such as safety, but also in ensuring that these systems are secure. One such notion of security is that of initial-state opacity, where one seeks to ensure that an outside intruder is not able to determine some sensitive information about the initial-state of the system by observing the output traces. An existing approach to verify the initial-state opacity of a system relies on finding a barrier certificate over an appropriately constructed augmented system. However this search for a barrier certificate relies on the dynamics of the system being known. Unfortunately, in many scenarios, it may be difficult or infeasible to determine the dynamics of a given system. We thus consider the problem of determining whether a system is opaque when its dynamics are unknown. To do so, we recast the conditions of opacity on the augmented system as a robust program with uncountably many constraints. By collecting data from the system's trajectories, we construct a corresponding scenario program. We show that if a feasible solution of the scenario program satisfies some conditions, then the original system with unknown dynamics is opaque under reasonable assumptions. We show the effectiveness of the proposed approach by demonstrating the opacity of a room-temperature model.