Through Modeling to Synthesis of Security Automata 1

We define a set of process algebra operators, that we call controller operators, able to mimic the behavior of security automata introduced by Schneider in [Schneider, F. B., Enforceable security policies, ACM Transactions on Information and System Security 3 (2000), pp. 30–50] and by Ligatti and al. in [Bauer, L., J. Ligatti and D. Walker, More enforceable security policies, in: I. Cervesato, editor, Foundations of Computer Security: proceedings of the FLoC'02 workshop on Foundations of Computer Security (2002), pp. 95–104]. Security automata are mechanisms for enforcing security policies that specify acceptable executions of programs.Here we give the semantics of four controllers that act by monitoring possible un-trusted component of a system in order to enforce certain security policies. Moreover, exploiting satisfiability results for temporal logic, we show how to automatically build these controllers for a given security policy.