| Each organization or company, having its own purposes and goals for its projects, needs to establish security policies for various reasons: information protection, regulations, contracts, and legal issues. The process of establishing security policies is more important than the document itself and the purpose of these policies is to ensure that the final result actually provides a secure service. Most approaches for enforcing and verifying security policies fall short of the goal due to the use of informal specifications that might lead to ambiguity, inconsistency, and incompleteness. Due to the ambiguity and imprecision of informal specification, it is difficult to verify the correctness of the system.; This research presents a framework for formally specifying, enforcing, and verifying security policies. A security policy is specified as predicate logic formulas on a set of executions based on grouping finite sets of classes, entities, relations, atomic predicate formulas, and some auxiliary elements that help to build predicate formulas. The enforcement approach is called Security State Machines (SSMs), and it helps to formally enforce and verify computer security polices. Using Security State Machines is a flexible technique that can enforce a collection of security policies. They have a set of states and rules for making transitions from one state to another. The transitions between states are directed by the actual policy being enforced. The enforcement technique works by allowing any execution that satisfies the security policy and terminating any execution that violates it.; Security policies enforced by SSMs can be verified using different models. In this research we use one of the famous models of verification called CTL model checking. Model checking is one of the recent methods of formal verification that has been applied in computer security, specifically in network protocols verification, to discover the security flaws. CTL model checking allows us to formally examine the properties of existing and novel security architectures through relatively simple methods that allow a high degree of automation. |
