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.
