Security Policies Enforcement Using Finite Edit Automata

Edit automata have been introduced by J. Ligatti et al. as a model for security enforcement mechanisms which work at run time. In a distributed interacting system, they play a role of monitor that runs in parallel with a target program and transforms its execution sequence into a sequence that obeys the security property. In this paper we characterize security properties which are enforceable by finite edit automata, i.e. edit automata with a finite set of states. We prove that these properties are a sub-class of ∞-regular sets. Moreover given an ∞-regular set P, one can decide in time O(n^2) whether P is enforceable by a finite edit automaton (where n is the number of states of the finite automaton recognizing P) and we give an algorithm to synthesize the controller.