Security policies enforcement using finite and pushdown edit automata

• Published in: International journal of information security 2013-08, Vol.12 (4), p.319-336
• Main Authors: Beauquier, Danièle, Cohen, Joëlle, Lanotte, Ruggero
• Format: Article
• Language: English
• Subjects: Algorithms; Applied sciences; Automatic control; Automation; Coding and Information Theory; Communications Engineering; Computer Communication Networks; Computer information security; Computer Science; Computer science; control theory; systems; Computer systems and distributed systems. User interface; Cryptology; Cybersecurity; Enforcement; Exact sciences and technology; Management of Computing and Information Systems; Mathematical analysis; Memory and file management (including protection and security); Memory organisation. Data processing; Monitors; Networks; Operating Systems; Policies; Regular Contribution; Safety; Security; Software; Studies; Taxonomy
• ISSN: 1615-5262; 1615-5270
• DOI: 10.1007/s10207-013-0195-8

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 , one can decide in time , whether is enforceable by a finite edit automaton (where is the number of states of the finite automaton recognizing ) 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 . Finally, we give a topological condition on the deterministic automaton expressing a regular policy enforceable by a deterministic context-free edit automaton.