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

Visual System of Formal Specification and Verification of Security Policy

作　　者：雷新锋[1] 刘军[1] 肖军模[1] 周海刚[1] 张一丹[1] 

机构地区：[1]解放军理工大学通信工程学院,南京210007

出　　处：《计算机工程》2008年第24期162-164,共3页Computer Engineering

基　　金：江苏省自然科学基金资助项目(BK2008090)

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

关 键 词：安全策略 一致性 完备性 扩展访问控制标记语言 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]