اجرای سیاست های امنیتی خودکار در سیستم های کامپیوتری Automatic security policy enforcement in computer systems

1 Introduction There are various solutions for securing computer systems, including operating system tools, third party applications, hardware devices, etc. In general, the difficulty of the issue is directly proportional with the complexity of the system. Some aspects of the security posture are straightforward and can be easily addressed by referring to best practices, templates and white papers. However, such documents only provide guidelines for the most common configurations, which are rarely fit for complex and large computer system. Once the requirements have been determined, the resulting policies are translated into available security mechanisms, implemented, tested and certified (or at least they should be). The human factor intervenes in policy definition, implementation and evaluation. It plays a crucial role in the more or less successful protection of computer networks. Although human intervention is necessary in the definition of security policies, its role in their enforcement on computer systems must be minimized and the task should preferably be performed by an automatic process. The final aim is to reduce or even eliminate implementation errors. Formal methods are well positioned to address such concerns since they can be used to generate enforcement processes that can be proven correct. The scope of the present work is mainly focused on a security policy enforcement method based on the notions of protected boundaries and controlled process movement. The resulting framework allows us to specify systems, express security policies, assess policy compliance and automatically calculate necessary enforcements for non-compliant systems. Given a process P (representing a system) and a formula Φ (corresponding to a desired security policy), then changes (denoted by an enforcement process X) may be required so that the resulting system ( P X , read as P enforced by X) satisfies Φ. The concepts and techniques apply to small and large networks alike, regardless of the number of nodes and the complexity of the topology.