Home // International Journal On Advances in Security, volume 2, number 4, 2009 // View article

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

Authors:
Jérémy Briffaut
Jean-François Lalande
Christian Toinard

Keywords: Security Properties, Protection, Mandatory Access Control, Verification

Abstract:
Enforcement of security properties by Operating Systems is an open problem. To the best of our knowledge, the solution presented in this paper1 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. Thus, we provide a SPLinux kernel that enforces all the requested Security Properties. When the MAC policies are dynamic, it becomes difficult to compute all the possible illegal activities. Our paper proposes a solution to that problem. A meta-policy includes evolution constraints for the MAC policies. A verification tool computes the requested security properties that are defined through the SPL language. That tool provides the illegal activities for all the possible MAC dynamic policies. Thus, the security administrator can verify the MAC policies and can optimize the requested security properties. It helps him to evaluate the memory and processor load associated with the enforcement of the request security properties. Efficiency is presented for protecting high-interaction honeypots.

Pages: 325 to 343

Copyright: Copyright (c) to authors, 2009. Used with permission.

Publication date: March 17, 2010

Published in: journal

ISSN: 1942-2636