دانلود رایگان مقاله انگلیسی اجرای سیاست های امنیتی خودکار در سیستم های کامپیوتری - الزویر 2017

Abstract.

This paper proposes a formal framework for automatic security policy enforcement in computer systems. In this approach, systems and their interactions are formally modelled as process algebra expressions with a new dedicated calculus inspired from the ambient calculus. Security policies are specified with the aid of a dedicated modal logic. We demonstrate how, for a given security policy expressed by a logical formula, our calculus allows to verify whether the specification meets the security policy requirements. If it does not, the optimal enforcement for the system is automatically generated using our enforcement operator. A software prototype has been implemented to show the practical feasibility and the effectiveness of our security policy enforcement framework.

9 Conclusion

In this paper, we have developed a new formal framework for computer system specification and security policy enforcement. The FPE framework consists of three main components. The first is a new formalism for specifying computer systems that captures in an effective and elegant way the system’s behaviour and topology. We define a new calculus that draws from the agility of the mobile ambients and adds several original and powerful concepts such as access control for domains (access keys, protection changes) and communication interfaces. It facilitates the specification of a computer system’s current state and its evolution. The second component is a new dedicated logic for defining security policies. The logic formulas allow expressing current and desired security policies. The semantics of the logic links policy satisfaction to compliant processes. Again, the system’s evolution can be followed, in this case from the point of view of applicable constraints. The third original component is the quotient operator that allows an automatic calculation of required enforcements. Given a process P and a security policy Φ, we calculate =  X P as a first step. If X = 1, then the process P satisfies the policy Φ. Otherwise, the enforcement can be applied to update the process and make it policy compliant. The formal foundation of all components ensures that the enforcement produces a secured system, free of incomplete specifications, arbitrary interpretations or faulty implementation of policies. Note that our approach is different from previous works as it allows both the verification of policy compliance and the application of corrective actions. The automated aspect of the methodology further enhances its value. A software implementation demonstrates its effectiveness and proves its applicability to practical problems. The versatility of FPE is supported by the numerous potential uses.