Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Opacity Enforcement by Edit Functions Under Incomparable Observations

Wei Duan, Ruotian Liu, Maria Pia Fanti, Christoforos N. Hadjicostis, Zhiwu Li

TL;DR

This work addresses opacity enforcement in discrete-event systems under incomparable observations by introducing $ic$-enforceability to capture when an edit function can reliably confuse an intruder. It formulates a two-player imperfect-information game and constructs an edit mechanism that enumerates feasible edits, enabling synthesis of $ic$-enforcing edit functions from the mechanism. The approach combines system/intruder/defender observers, a formal edit game structure, and a trimmed/no-guarantees mechanism to guarantee i-availability, confidentiality, and integrity, with proofs tying the mechanism to $ic$-enforcement. Complexity is analyzed as doubly-exponential in the state space and 2-EXPTIME for the imperfect-information game, with discussion on practical reductions via abstraction and comparison to existing supervisor-based and obfuscation-based opacity methods.

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.

Opacity Enforcement by Edit Functions Under Incomparable Observations

TL;DR

This work addresses opacity enforcement in discrete-event systems under incomparable observations by introducing -enforceability to capture when an edit function can reliably confuse an intruder. It formulates a two-player imperfect-information game and constructs an edit mechanism that enumerates feasible edits, enabling synthesis of -enforcing edit functions from the mechanism. The approach combines system/intruder/defender observers, a formal edit game structure, and a trimmed/no-guarantees mechanism to guarantee i-availability, confidentiality, and integrity, with proofs tying the mechanism to -enforcement. Complexity is analyzed as doubly-exponential in the state space and 2-EXPTIME for the imperfect-information game, with discussion on practical reductions via abstraction and comparison to existing supervisor-based and obfuscation-based opacity methods.

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{-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 -enforcing edit function (if one exists) can be synthesized from the edit mechanism to enforce opacity.

Paper Structure

This paper contains 20 sections, 2 theorems, 2 equations, 7 figures, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. System Model
  4. Current-State Opacity
  5. Edit Function
  6. Current-state opacity enforcement via edit functions under incomparable observations
  7. Incomparable Observation Setting
  8. $IC$-Enforceability
  9. Problem formulation
  10. Synthesis of an edit game structure
  11. System Estimate by the Intruder and the Edit Function
  12. Edit Game Structure
  13. Utility Function
  14. Synthesis of edit mechanism
  15. Trimmed Game Structure
  16. ...and 5 more sections

Key Result

Lemma 1

An edit function is $i$-available and confidential if and only if it is synthesized from a non-empty trimmed game structure $\mathcal{TGS}$.

Figures (7)

  • Figure 1: The edit mechanism.
  • Figure 2: Comparison of observation capability between the intruder (I) and the defender (D) in different works.
  • Figure 3: Motivating example.
  • Figure 4: Illustrations of the observers.
  • Figure 5: The construction flow of an edit mechanism.
  • ...and 2 more figures

Theorems & Definitions (25)

  • Definition 1
  • Definition 2
  • Remark 1
  • Example 1
  • Definition 3
  • Definition 4
  • Definition 5
  • Remark 2
  • Definition 6
  • Definition 7
  • ...and 15 more