ISSN : 1796-203X
Volume : 3 Issue : 6 Date : June 2008
Formal Verification and Visualization of Security Policies
Luay A. Wahsheh, Daniel Conte de Leon, and Jim Alves-Foss
Page(s): 22-31
Full Text: PDF (650 KB)
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.
