Security policies are one of the most fundamental elements of computer security. For secure interoperation and sharing resources among heterogeneous systems, local policies should correspondingly be integrated for designing a global policy. This paper addresses the problem in a formal way. It uses extended Petri net process to specify and verify security policies in a modular way. It defines four types of policy compositions such that the integrated policy is capable of handling resources sharing, simultaneously executing operations and embedding sub-policies into main policies in multiple heterogeneous systems. Furthermore, the global policy can preserve the fundamental policy properties, i.e., completeness, termination, consistency and confluence, and satisfy policy autonomy and security principles that are required for secure interoperation.