Opacity Enforcement by Edit Functions Under Incomparable Observations

TL;DR

This paper introduces a method for enforcing opacity in discrete event systems using edit functions, even when the intruder and defender observe different, incomparable event subsets, by modeling the problem as a two-player game with imperfect information.

Contribution

It generalizes opacity enforcement by considering incomparable observations and develops a game-based synthesis approach for edit functions to enforce opacity.

Findings

A new notion of ic-enforceability is proposed.

A two-player game model with imperfect information is used for enforcement.

A synthesis method for edit functions is developed.

Abstract

As an information-flow privacy property, opacity characterizes whether a malicious external observer (referred to as an intruder) is able to infer the secret behavior of a system. This paper addresses the problem of opacity enforcement using edit functions in discrete event systems modeled by partially observed deterministic finite automata. A defender uses the edit function as an interface at the output of a system to manipulate actual observations through insertion, substitution, and deletion operations so that the intruder will be prevented from inferring the secret behavior of the system. Unlike existing work which usually assumes that the observation capabilities of the intruder and the defender are identical, we consider a more general setting where they may observe incomparable subsets of events generated by the system.To characterize whether the defender has the ability to enforce opacity of the system under this setting, the notion of \emph{$ic$-enforceability} is introduced. Then, the opacity enforcement problem is transformed to a two-player game, with imperfect information between the system and the defender, which can be used to determine a feasible decision-making strategy for the defender. Within the game scheme, an edit mechanism is constructed to enumerate all feasible edit actions following system behavior. We further show that an $ic$-enforcing edit function (if one exists) can be synthesized from the edit mechanism to enforce opacity.