Formalization of Security Properties: Enforcement for MAC Operating Systems and Verification of Dynamic MAC Policies

Date Added: Jun 2010
Format: PDF

Enforcement of security properties by Operating Systems is an open problem. To the best of the authors' knowledge, the solution presented in this paper is the first one that enables a wide range of integrity and confidentiality properties to be enforced. A unified formalization is proposed for the major properties of the literature and new ones are defined using a Security Property Language. Complex and precise security properties can be defined easily using the SPL language but the system includes 13 predefined protection templates. Enforcement of the requested properties is supported through a compiler that computes all the illegal activities associated with an existing MAC policy.