K-memory-embedded insertion mechanism for opacity enforcement

Opacity is a privacy property which aims to determine whether the "secret" of a system can be deduced by an outside intruder. In this paper, we investigate the enforcement of opacity using insertion functions which insert additional events if necessary to modify the output of the system. Inspired by the existing insertion mechanisms, we propose a mechanism named k-memory-embedded insertion mechanism for the enforcement of opacity. In our k-memory-embedded insertion mechanism, the insertion functions are determined based on the knowledge of system's exact states and the stored next sequence of events with length k. Especially, we define the property of i(k)-E-enforceability that a k-memory-embedded insertion function needs to satisfy for opacity enforcement, and further construct a verifier to determine whether a given opacity notion of the system is i(k)-E-enforceable or not. Our mechanism improves the embedded insertion mechanism by applying to a broader class of systems. Also, we improve the k-memory insertion mechanism by requiring a smaller number of consecutive events which need to be stored. (C) 2020 Elsevier B.V. All rights reserved.