高级检索

    动态安全策略逻辑语言及安全属性验证问题的研究

    Logic-Based Dynamical Security Policy Language and Verification

    • 摘要: 针对动态安全策略在策略表达、判决和验证等方面具有的重要意义,提出了一种可用于动态安全策略表达、决策和验证的逻辑系统SSML.首先,给出了SSML逻辑系统的语法和语义,并且证明了一般意义上的SSML逻辑系统查询评估问题是不可判定的,从而表明不存在通用的SSML安全策略语义查询评估算法.其次,研究SSML子语言特性,发现两类语法受限的SSML动态安全策略——NDel型安全策略和TDel型安全策略.虽然前者不允许在安全策略中出现删除规则,后者只允许完全信任的管理人员执行删除规则,但它们的查询评估问题是可判定的,并且分别构造出它们的查询评估算法—— OLDTE和OLDTT.最后,通过实例说明如何使用OLDTE或OLDTT实现安全策略验证,从而证明这两类动态安全策略具有广泛的应用前景,对动态安全策略及其安全性分析方法的研究具有重要意义.

       

      Abstract: Expression, query evaluation and verification are great significant to dynamical security policy management, but they are very difficult to solve at present. This paper proposes a logic system, called SSML, which can be used to declare, evaluate and verify dynamic security policy. Firstly, we propose the syntax and the semantic of SSML (simple state modifying logic) based on logic programming theory, which shows that an SSML security policy can dynamically insert facts into itself or delete facts from itself. Then, we prove that the query evaluation problem of logic systems based on SSML is undecidable in general, which shows that there is no general algorithm to be able to evaluate all SSML security policies. So we turn to research on its sub-languages, and find two types of SSML security policies with limited syntax-NDel security policies and TDel security policies, and they have decidable evaluation algorithms. We actually give their query evaluation algorithms-OLDTE and OLDTT. They are complete and sound, and have polynomial computation complexity. Eventually, we show how to use SSML to verify a security policy through an actual example. We claim that OLDTE and OLDTT can be widely used in security policy management and verification.

       

    /

    返回文章
    返回