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 sys?tem. Given a concurrent program P and a security policy φ, we automatically generate another program P' that satisfies φ and be?haves like P, except that it stops when P tries to violate the security policy 0. We use extended version of process algebra ACP (Alge?bra of Communicating Process) and BPA (Basic Process Algebra) as formal languages to specify both concurrent system and security policy.