可视化的安全策略形式化描述与验证系统

通过分析安全策略中可能出现的问题，对安全策略的一致性与完备性进行形式化定义。通过构造安全策略的状态模型，提出策略的一致性与完备性验证算法。基于可扩展访问控制标记语言，设计并实现一种安全策略的形式化描述与验证系统。该系统将形式化的验证过程自动化，以可视化的形式为普通用户提供一种高效的策略验证工具。

Visual System of Formal Specification and Verification of Security Policy

This paper analyzes the possible faults in policy, formally defines the consistency and completeness of the security policy. By building the state model of security policy, the algorithm for formally verifying security policy is proposed. Based on the eXtensible Access Control Markup Language(XACML), a system to formally specify and verify the security policy is designed and implemented. This system makes the process of the formal verification automatic, and provides an efficient tool for a normal user to verify the security policy in a visual form.