¹Center for Secure and Dependable Systems, University of Idaho, P. O. Box 441008, Moscow, Idaho 83844-1008, USA
²Division of Natural Sciences and Mathematics, Lewis-Clark State College, 500 8th Avenue, Lewiston, Idaho 83501-2691, USA

---

Abstract—Verified and validated security policies are essential components of high assurance computer systems. The design and implementation of security policies are fundamental processes in the development, deployment, and maintenance of such systems. In this paper, we introduce an expert system that helps with the design and implementation of security policies. We show how Prolog is used to verify system correctness with respect to policies using a theorem prover. Managing and visualizing information in high assurance computer systems are challenging tasks. To simplify these tasks, we show how a graph-based visualization tool is used to validate policies and provide system security managers with a process that enables policy reviews and visualizes interactions between the system’s entities. The tool provides not only a representation of the formal model, but also its execution. The introduced executable model is a formal specification and knowledge representation method.

Index Terms—Logic, security policy, validation, verification, visualization

[PDF]

Cite: Luay A. Wahsheh, Daniel Conte de Leon, Jim Alves-Foss, "Formal Verification and Visualization of Security Policies," Journal of Computers vol. 3, no. 6, pp. 22-31, 2008.