Security policies enforcement using finite and pushdown 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 a 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) and deterministic context-free edit automata (i.e. finite edit automata extended with a stack). We prove that the properties enforceable by finite edit automata are a sub-class of regular sets. Moreover, given a 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. Moreover, we prove that safety policies are always enforced by a deterministic context-free edit automaton. We also prove that it is possible to check if a policy is a safety policy in \(O(n^4)\). Finally, we give a topological condition on the deterministic automaton expressing a regular policy enforceable by a deterministic context-free edit automaton.