Insertion Functions with Memory for Opacity Enforcement

We investigate the enforcement of opacity, an information-flow privacy property, using insertion sequences that modify the output of the system by event insertions. Previous work considered the problem of enforcing opacity under the assumption that the insertion functions were based on the observed system strings. Now, we investigate an extension of the previous method introducing a k-memory insertion mechanism. In this case, we store k consecutive events and we compute an insertion function for a k length event sequence. The k-memory insertion mechanism can be applied to a broader class of systems than the previously proposed insertion mechanism. The first contribution of this paper is the introduction of ik-enforceability. A system is ik-enforceable if we can apply k-memory insertion mechanism to enforce privacy. The second contribution of this paper is the development of a verification algorithm for ik-enforceability.