Formal enforcement of security policies on concurrent systems

This paper introduces a formal and modular technique allowing to automatically enforce a security policy on a given concurrent system. Given a concurrent program P and a security policy ϕ, we automatically generate another program P′ that satisfies ϕ and behaves like P, except that it stops when P tries to violate the security policy ϕ. We use extended version of process algebra ACP (Algebra of Communicating Process) and BPA (Basic Process Algebra) as formal languages to specify both concurrent system and security policy.