基于良基语义的安全策略表达与验证方法

软件学报ＩＳＳＮ　１０００—９８２５，ＣＯＤＥＮ　ＲＵＸＵＥＷ　Ｊｏｕｒｎａｌ　ｏｆＳｏｆｔｗａｒｅ，２０１２，２３（４）：９１２—９２７［ｄｏｉ：１０．３７２４／ＳＰ．Ｊ．１００１．２０１２．０４０２３】　＠中国科学院软件研究所版权所有．　Ｅ—ｍａｉｌ：ｊｏｓ＠ｉｓｃａｓ．ａｃ．ｃｎ　ｈｔｔｏ：／／ｗｗｗ．ｊｏｓ．ｏｒｇ．ｃａ　Ｔｂｌ／Ｆａｘ：＋８６—１０．６２５６２５６３　基于良基语义的安全策略表达与验证方法　包义保　３＋，殷丽华　，方滨兴　，郭莉　（中国科学院计算技术研究所，北京　１００１９０）　（解放军信息工程大学电子技术学院，河南郑州（中国科学院研究生院，北京　１０００４９）　４５０００４）　Ａｐｐｒｏａｃｈ　ｏｆ　Ｓｅｃｕｒｉｔｙ　Ｐｏｌｉｃｙ　Ｅｘｐｒｅｓｓｉｏｎ　ａｎｄ　Ｖｅｒｉｆｉｃａｔｉｏｎ　Ｂａｓｅｄ　ｏｎ　Ｗｅｌｌ—Ｆｏｕｎｄｅｄ　Ｓｅｍａｎｔｉｃ　ＢＡＯ　Ｙｉ．Ｂａｏ　，　，　，ＹＩＮ　Ｌｉ．Ｈｕａ　，ＦＡＮＧ　Ｂｉｎ．Ｘｉｎｇ　，ＧＵＯ　Ｌｉ　（Ｉｎｓｔｉｔｕｔｅ　ｏｆＣｏｍｐｕｔｉｎｇＴｅｃｈｎｏｌｏｇｙ，ＴｈｅＣｈｉｎｅｓｅＡｃａｄｅｍｙ　ｏｆＳｃｉｅｎｃｅｓ，Ｂ确ｉｎｇ　１００１９０，Ｃｈｉｎａ）　（Ｉｎｓｔｉｔｕｔｅ　ｏｆＥｌｅｃｔｒｏｎｉｃ　Ｔｅｃｈｎｏｌｏｇｙ，Ｉｎｆｏｒｍａｔｉｏｎ　Ｅｎｇｉｎｅｅｒｉｎｇ　Ｕｎｉｖｅｒｓｉｔｙ　ｏｆＰＬＡ，Ｚｈｅｎｇｚｈｏｕ　４５０００４，Ｃｈｉｎａ）　（Ｇｒａｄｕａｔｅ　Ｕｎｉｖｅｒｓｉｔｙ，Ｔｈｅ　Ｃｈｉｎｅｓｅ　Ａｃａｄｅｍｙ　ｏｆ　Ｓｃｉｅｎｃｅｓ，Ｂｅｉｊｉｎｇ　１０００４９，Ｃｈｉｎａ）　＋Ｃｏｒｒｅｓｐｏｎｄｉｎｇ　ａｕｔｈｏｒ：Ｅ－ｍａｉｌ：ｂａｏｙｉｂａｏ＠ｓｏｆｔｗａｒｅ．ｉｃｔ．ａｃ．ｃｎ　Ｂａｏ　ＹＢ，Ｙｉｎ　ＬＨ，Ｆａｎｇ　ＢＸ，Ｇｕｏ　Ｌ．Ａｐｐｒｏａｃｈ　ｏｆ　ｓｅｃｕｒｉｔｙ　ｐｏｌｉｃｙ　ｅｘｐｒｅｓｓｉｏｎ　ａｎｄ　ｖｅｒｉｆｉｃａｔｉｏｎ　ｂａｓｅｄ　ｏｎ　ｗｅｌｌ—　ｆｏｕｎｄｅｄ　ｓｅｍａｎｔｉｃ．Ｊｏｕｒｎａｌ　ｏｆＳｏｆｔｗａｒｅ，２０１２，２３（４）：９１２－９２７．ｈｔｔｐ：／／ｗｗｗ．ｊｏｓ．ｏｒｇ．ｃｒｄ１０００－９８２５／４０２３．ｈｔｍ　Ａｂｓｔｒａｃｔ：Ｔｈｉｓ　ｓｔｕｄｙ　ｐｒｏｐｏｓｅｓ　ａ　ｌｏｇｉｃ—ｂａｓｅｄ　ｓｅｃｕｒｉｔｙ　ｐｏｌｉｃｙ　ｆｒａｍｅｗｏｒｋ．Ｆｉｒｓｔ，ｔｈｅ　ｓｔｕｄｙ　ｐｒｏｐｏｓｅｓ　ｔｈｅ　ｓｅｃｕｒｉｔｙ　ｐｏｌｉｃｙ　ｓｙｎｔａｘ　ａｎｄ　ｓｅｍａｎｔｉｃ．Ｎｅｘｔ，ｆｏｕｒ　ａｌｇｏｒｉｔｍｓ　ａｒｅ　ｐｒｏｐｏｓｅｄ　ｔｏ　ｔｒａｎｓｆｅｒ　ｆｉｒｓｔ－ｏｒｄｅｒ　ｌｏｇｉｃ　ｂａｓｅｄ　ｓｅｃｕｒｉｔｙ　ｐｏｌｉｃｉｅｓ　ｉｎｔｏ　ｅｘｔｅｎｄｅｄ　ｌｏｇｉｃ　ｐｒｏｇｒａｍｓ　ｔｏ　ｅｖａｌｕａｔｅ　ｑｕｅｒｉｅｓ　ｗｉｔｈ　ｓｉｍｐｌｅ　ｇｏａｌｓ，ｔｏ　ｔｒａｎｓｆｅｒ　ｃｏｍｐｌｅｘ　ｑｕｅｒｉｅｓ　ｉｎｔｏ　ｓｉｍｐｌｅ　ｏｎｅｓ，　ａｎｄ　ｔｏ　ｖｅｒｉｆｙ　ｓｅｃｕｒｉｙ　ｐｏｌｉｃｉｔｅｓ　ａｇａｉｎｓｔ　ｃｏｍｐｌｅｘ　ｓｅｃｕｒｉｔｙ　ｐｒｏｐｅｒｔｉｅｓ．Ｕｎｄｅｒ　ｗｅｌｌ－ｆｏｕｎｄｅｄ　ｓｅｍａｎｔｉｃｓ．ａｎ　ｔｈｅ　ａｌｇｏｒｉｔｈｍｓ　ａｒｅ　ｓｏｕｎｄ　ａｎｄ　ｃｏｍｐｌｅｔｅｄ，ａｎｄ　ｔｈｅｉｒ　ｃｏｍｐｕｔａｔｉｏｎａｌ　ｃｏｍｐｌｅｘｉｔｉｅｓ　ａｒｅ　ｐｏｌｙｎｏｍｉａ１．Ｉｎ　ｔｈｉｓ　ｆｒａｍｅｗｏｒｋ，ｓｅｃｕｒｉｔｙ　ｐｏｌｉｃｙ　ｄｅｃｌａｒａｔｉｏｎ，ｅｖａｌｕａｔｉｏｎ　ａｎｄ　ｖｅｒｉｆｉｃａｔｉｏｎ　ａｒｅ　ｅｘｅｃｕｔｅｄ　ｕｎｄｅｒ　ｔｈｅ　ｓａｍｅ　ｓｅｍａｎｔｉｃｓ，ｗｈｉｃｈ　ｉｓ　ｓｉｇｎｉｆｉｃａｎｔ　ｆｏｒ　ｓｅｃｕｒｉｙ　ｔｐｏｌｉｃｙ　ｍａｎａｇｅｍｅｎｔ．Ｆｕｒｔｈｍｏｒｅ，ｔｈｅ　ｆｒａｍｅｗｏｒｋ　ｃａｎ　ｍａｎａｇｅ　ｔｈｅ　ｓｅｃｕｒｉｔｙ　ｐｏｌｉｃｉｅｓ　ｗｉｔｈ　ａｄｖａｎｃｅｄ　ｆｅａｔｕｒｅｓ，ｓｕｃｈ　ａｓ　ｎｏｎ—ｍｂｎｏｔｏｎｙ　ａｎｄ　ｒｅｃｕｒｓｉｏｎ，ｗｈｉｃｈ　ｉｓ　ｎｏｔ　ｓｕｐｐｏｒｔｅｄ　ｉｎ　ｍａｎｙ　ｅｘｉｓｔｅｎｔ　ｓｅｃｕｒｉｔｙ　ｐｏｌｉｃｙ　ｍａｎａｇｅｍｅｎｔ　ｆｒａｍｅｗｏｒｋｓ．　Ｋｅｙ　ｗｏｒｄｓ：　ｓｅｃｕｒｉｙ　ｐｏｌｉｔｃｙ；ｓｅｃｕｒｉｙ　ｍａｎａｇｅｍｅｎｔ；ｗｅｌｔｌ－ｆｏｕｎｄｅｄ　ｓｅｍａｎｔｉｃ；ｐｏｌｉｃｙ　ｖｅｒｉｆｉｃａｔｉｏｎ；ｌｏｇｉｃ　ｐｒｏｇｒａｍｍｉｎｇ　摘要：　提出了一种基于一阶逻辑的安全策略管理框架．首先，研究安全策略的语法和语义，给出将安全策略转换　成扩展型逻辑程序的算法＇进而构造出安全策略基本查询算法；其次，给出将安全策略复杂查询转换成基本查询的算　法，进而构造出安全策略验证算法．在良基语义下，上述算法是可终止的、可靠的和完备的，且计算复杂度都是多项式　级的．该框架可以在统一的良基语义下实现安全策略表达、语义查询和验证，保证安全策略验证的有效性．此外，该框　架不仅兼容现有主流的安全策略语言，还能够管理具有非单调和递归等高级特性的安全策略．　关键词：　安全策略；安全管理；良基语义；策略验证；逻辑编程　中图法分类号：ＴＰ３９３　文献标识码：Ａ　・基金项目：国家自然科学基金（６ｌＯ７０１８６）；国家高技术研究发展计划（８６３）（２００９ＡＡＯｌｚ４３８，２００９ＡＡ０１Ｚ４３）；国家重点基础研　收稿时间：２０１０．０９—１５；修改时间：２０１１－０１．３１；定稿时间：２０１１－０３—２１　究发展计划（９７３）（２００７Ｃ８３　１　１　１　００）　包义保等：基于良基语义的安全策略表达与验证方法　９１３　近年来，信息安全研究领域逐渐从安全技术扩展到安全管理，基于策略的安全管理是研究的重点．在安全策　略管理研究领域，如何表达安全策略、如何利用安全策略蕴涵的语义提供安全服务以及如何保障安全策略自身　的安全性，这是３个基本而又重要的问题．由这３个基本问题延伸出３个重要的研究方向，即安全策略表达、安　全策略语义查询和安全策略验证．　在安全策略表达方面，目前的主流方法是使用形式化的语言描述安全策略．文献【ｌ】对安全策略语言进行了　总结，认为基于逻辑的安全策略语言最容易被人们接受，文献【２—８】中提出的语言就是这类语言．文献［２］首次设　计了一种基于逻辑的分布式安全策略语言，其语法与扩展型逻辑程序等价，但没有讨论复杂查询的计算方法，无　法用于安全策略验证．文献［３，４】提出了一种基于分层逻辑程序［９］的安全策略语言，称为ＦＡＦ，它使用稳定语义【ｊ　Ｕ】　作为安全策略的语义．ＦＡＦ严格限制“非”的使用，不支持负递归（ｎｅｇａｔｉｖｅ　ｒｅｃｕｒｓｉｏｎ），不支持量词，描述的安全策略　也不够精炼，因而使用起来并不方便．由于已有的逻辑程序稳定语义查询算法的计算复杂度较高，因此ＦＡＦ语义　查询效率较低．文献［５】使用约束逻辑程序表达安全策略，约束逻辑程序的约束域能够方便地表达数值计算等特　性，但其策略决策的计算复杂度较高．文献［６］基于动态逻辑提出了一种可用于表达职责和动态授权的安全策略　语言，其安全策略验证问题是不可判定的．文献【７，８】仅讨论了安全策略语言的语法、语义及策略决策算法，并不　支持安全策略验证这一关键特性．　虽然目前已经存在多种基于逻辑的安全策略语言，但这些语言基本上都是基于逻辑程序『９】的，局限于逻辑　程序的语法，某些情况下无法容易地描述出一些安全策略．文献［１１］提出了一种基于一阶逻辑的安全策略语言　Ｌｉｔｈｉｕｍ．为了有限度地支持量词，Ｌｉｔｈｉｕｍ对其语法进行了严格的限制，普通管理人员难以理解，并且表达能力有　限．但是，Ｌｉｔｈｉｕｍ在用一阶逻辑表达安全策略方面进行了有益的尝试．　在安全策略语义查询方面，安全策略究竟表达什么样的语义（即所谓的正则语义）以及在该语义下的查询算　法是研究的重点．事实上，如何定义安全策略的正则语义是一个非常复杂的问题【　】．现有的一些文献一般仅讨论　具有特殊语法结构的安全策略语言，从而可以容易地定义其语义．例如，文献［１】仅讨论能够表示成Ｄａｔａｌｏｇ程　序ｆＪ　的安全策略，这是因为Ｄａｔａｌｏｇ程序具有公认的正则语义．对于语法较为复杂的安全策略语言，其语义的研　究往往被忽略了．例如，文献【２，７，１１】中提出的安全策略语言要比文献【１］中提出的安全策略语言复杂得多，但却　没有深入探讨安全策略语义问题．安全策略语义查询算法的设计难度取决于安全策略语言的复杂程度，一般来　说，安全策略语言越复杂，语义查询算法的设计就越困难，计算复杂度也越高．因此，现有安全策略语言一般仅局　限于具有特殊语法结构的逻辑系统．例如，文献【１］使用Ｄａｔａｌｏｇ的语义查询算法作为安全策略的语义查询算法，　其计算复杂度是多项式级的．文献［２，７，１１］则没有明确地讨论语义查询问题．　在安全策略验证方面，目前己存在多种安全策略验证技术【１，１４，１５］．这些技术的基本思想是：首先将待验证安　全策略转换成抽象模型并通过形式化建模语言描述出来，同时将待验证安全属性转换成形式化的安全属性不　变式，然后将它们输入到验证工具中完成验证．这需要保证不同表达方式之间转换的等价性，然而，①有时从理　论上无法实现不同表达方式之间转换的等价性；②即使可以从理论上保证转换的等价性，但对于普通安全策　略管理人员来说，保证实际转换过程的等价性也是非常困难的：⑧安全策略验证算法和安全策略语义查询算　法采用的语义可能并不一致，从而有可能导致验证失效等问题的产生．　综上所述，安全策略表达、语义查询和安全策略验证之间是相互制约、相辅相成的．因此，在统一的安全策　略管理框架中实现上述功能具有一定的优势，但也面临着巨大的挑战．现有安全策略语言大部分仅考虑到语义　查询问题，而没有考虑到安全策略验证问题，而现有的验证技术又与安全策略语言严重脱节，因而有可能存在验　证失效等问题．从公开的文献中还没有发现将上述三者统一起来进行形式化研究的成果，相关研究也不多见，一　般仅关注于某些特定类型的安全策略，不具有普适性．例如，文献［１６】介绍了一种在访问控制空间理论下研究系　统特权安全问题的方法，指出隐式授权可能导致系统存在不必要的特权滥用风险．然而，隐式授权是现代安全策　略系统中一种常用的授权方式，现有安全策略语言无一例外都支持隐式授权．文献【１６］使用一种称为快速构造　授权图的算法检测是否存在特权滥用，可以认为这是一种特殊类型的安全策略验证算法，但不支持负递归和非　单调推理等特性．本文提出的方法可用于解决文献［１６］中提出的问题，且具有更好的通用性．　９１４　Ｊｏｕｒｎａｌ　ｏｆ　Ｓｏｆｔｗａｒｅ软件学报Ｖｏ１．２３，Ｎｏ．４，Ａｐｒｉｌ　２０１２　基于上述考虑，本文提出了一种基于一阶逻辑的安全策略管理框架ＷＦ．ＳＰｅｖｆ，￣以在统一的良基语义ｎ　下　实现安全策略表达、语义查询和验证．一阶逻辑具有足够强的表达能力，良基语义具备一系列优良的特性（参见　第１．２节和文献［１７１），这使得ＷＦ．ＳＰｅｖｆ具有强大的表达能力，其所表达出的每个安全策略具有精确的语义定义　方式和高效的语义查询算法及验证算法．　１预备知识　本文假定读者熟悉一阶逻辑【　．为了便于阅读，本节简要介绍本文所使用的各种术语、符号与约定．有关逻　辑程序及其良基语义的详细讨论可参考文献［１７】．　１．１一阶逻辑及相关术语　本文讨论的一阶逻辑系统的字母表岫下列７种类型的符号集合构成：　①常元符号集；　②变元符号集；　③函数符号集；　④谓词符号集；　⑤逻辑连接符集　｛～，Ａ，ｖ，＜－－，Ｈ，一｝；　⑥量题符号集｛ｖ，了｝；　⑦标点符号集．　本文所用术语，如项、原子、文字、表达式、自由变元、约束变元、闭式、Ｈｅｒｂｒａｎｄ域、Ｈｅｒｂｒａｎｄ基、　Ｈｅｒｂｒａｎｄ解释、语义等的详细定义可参考文献［９，１８】．为了简单起见，本文约定：　①助有限集：　②所有常元符号都用首字母小写的字符串表示：　③所有变元符号都用首字母大写的字符串表示：　④函数符号集为空集：　⑤所有谓词符号也都用首字母小写的字符串表示；　⑥　，ｊ；，　等符号表示变元序列，　，　，　等符号表示常元序列，　等符号表示项序列；　⑦设墨，．．．　Ｆ　的全称闭式，为一阶逻辑表达式Ｆ中全部的自由变元，则Ｖ　．．　Ｘ（Ｆ）称为　简写为ｎ　（　，ｊ　．　矗（．Ｆ）称为Ｆ的存在闭式，简写为ｊ（　．　定义ｌ（－－值语义）．设　为由若干个一阶逻辑表达式构成的集合，日　为　上的Ｈｅｒｂｒａｎｄ基’，为风上的　Ｈｅｒｂｒａｎｄ解释（即，为基本原子集合且Ｉ　）．如果　中的每个表达式Ｇ在，中的真值都为真，即　Ｇ，则』是　的一个二值Ｈｅｒｂｒａｎｄ语义，简称为二值语义．　１．２扩展型逻辑程序及其语义　扩展型逻辑程序ｆ９　是一种语法受限的一阶逻辑系统．每个逻辑程序都由一系列的规则构成，每个规则都具　有　÷－三ｌＡ…ＡＬ　形式的逻辑表达式，它等价于闭式Ｖ（Ａｖ也１Ｖ…ｖ￣Ｌ　），一般写成　ｌ’．．．，　的形式．这里　为原　子，称为规则头部；厶为文字，　≥０，犯ｌ，．．．工　）称为规则体部．特别地，不含变元的规则称为基本规则．　文献［１７】从模型论的角度给出了通过三值逻辑定义扩展型逻辑程序良基语义的方法．不同于二值逻辑，三　值逻辑认为，人们对客观世界的认识是不完全的，存在一些既无法给出肯定判断也无法给出否定判断的事实，其　真值是“未定义的”．有关三值逻辑的详细描述可参考文献［１７，１９］．　定义２（－－ｆ￣）ｔ拇】．设　一阶逻辑语言，　为　的Ｈｅｒｂｒａｎｄ域，　为　的Ｈｅｒｂｒａｎｄ基，　，　尸　，且　，则序偶　（　巧为定义在　上的三值Ｈｅｒｂｒａｎｄ解释，简称为三值解释．这里，　中每个基本原　一（　ｕ厂）中每个基本原子的真值为“未定义”．如果　子的真值为“真”，厂中每个基本原子的真值为“假”，　包义保等：基于良基语义的安全策略表达与验证方法　９１５　＝　ｕ尸，则　变成二值解释．每个二值解释　都可以转化成一个三值解释　＝（　；　一　）　三值解释　（　可以等价地看成定义在　上的全函数，：　｛。，　，１），如公式（１）所示：　１．ｉｆＡ∈厂　Ｉ（Ａ）＝　，ｉｆ　∈　（１）　０。ｉｆＡ∈厂　定义在　的每个逻辑表达式的真值可递归地定义为如下形式：　定义３（逻辑表达式的真值）ｎ　．设　（　为定义在　的一个三值解释，则　（１）如果Ａ是基本原子，则Ｉｚ（　）＝，（　）；　（２）如果　是闭式，则，，（～　）＝１一Ｉｚ（　）；　（３）如果　和Ｇ都为闭式，则　（　ＡＧ）＝ｍｉｎ（Ｉｚ（　），Ｉｚ（Ｇ）），　，，　　，、　【１，ｉｆＩｚ（　）≥Ｉｚ（Ｇ）　ｌ　０，ｏｔｈｅｒｗｉｓｅ　｝．　，　（－ｓｒ　ｖ　Ｇ）＝ｍａｘ（Ｇ（　），，ｚ－（Ｇ）），　。、　（４）　对于任意的逻辑表达式　若　是　的一个自由变元，则　（Ｖ　Ｓ）＝ｒａｉｎ｛Ｉｚ（　１　）：Ｃ∈　｝，Ｉｚ（ｊ　Ｓ）＝ｍａｘ｛Ｉｚ（　Ｉｘ￣ｃ）：ｃ∈　由定义３可知，三值逻辑中的“　”和二值逻辑中的“÷＿”是不同的．在二值逻辑中，　÷－Ｇ和　～Ｇ等价，而在三　值逻辑中，　（　÷－Ｇ）和ｍａｘ（１ｚ（　），１一　（Ｇ））并不恒等，因而　Ｇ和Ｓｖ－Ｇ并不等价．为了平滑三值逻辑和经典　二值逻辑之间的差异，本文引入一个新的逻辑连接符“一”，并且规定　—Ｇ等价于　一Ｇ．　定义４（－－值语义）【　】．不防设扩展型逻辑程序　冲的规则都是基本规则（否则将其实例化），则三值解释　缇　夕构三值语义，当且仅当对于　冲任一基本规则　÷　．．，三　，公式（２）都成立．　（２）　，＾　）＞￣ｍｉｎ｛ＩＭ（Ｌ　ｆ≤　｝　显然，每个二值语义都唯一对应着一个三值语义．因此，若无特殊说明，下文中的语义指的都是三值语义．由　定义４可知，每个扩展型逻辑程序至少有一个三值语义　（　；　），也可能有多个三值语义ｆ　】１．研究人员普遍认为　良基语义是比较合理的三值语义，具有一系列良好的特性：①每个逻辑程序都具有唯一的良基语义；②良基语　义和一系列特殊类型逻辑程序公认的正则语义等同．例如，分层逻辑程序的良基语义等同于其完美语义【】　，而完　美语义被认为是分层逻辑程序的正则语义【９　；③良基语义具备支撑性语义特性［１９］．所谓支撑性语义，是指该语　义中任意一个基本文字都是由扩展型逻辑程序中某个相应的规则推理得到的．这一特性保证了安全策略描述　安全需求的有效性；④存在高效的基于良基语义的语义查询算法，如ＳＬＧ算法［２０，２１１，具备良好的实用性．因此，　本文选择良基语义作为扩展型逻辑程序的正则语义．　ＳＬＧ算法是由Ｓｔｏｎｙ　Ｂｒｏｏｋ大学的Ｃｈｅｎ和Ｗａｒｒｅｎ等人提出的一种高效的基于良基语义的逻辑程序语义　查询算法．文献［２０，２１１详细讨论了ＳＬＧ算法及其计算复杂度、可靠性和完备性等问题：ＳＬＧ算法的计算复杂度　是多项式级的；对于ｎｏｎ．Ｆｌｏｕｎｄｅｒｉｎｇ查询，ＳＬＧ算法是可靠的和完备的；对于Ｆｌｏｕｎｄｅｒｉｎｇ查询，ＳＬＧ算法是可靠　的，但不是完备的．所谓Ｆｌｏｕｎｄｅｒｉｎｇ查询，是指ＳＬＧ算法在消解查询目标的过程中，如果按照某种原则选取出的　子目标是负文字，且不是基本文字，则称这样的查询为Ｆｌｏｕｎｄｅｒｉｎｇ查询．从公开的研究资料来看，几乎所有的语　义查询算法都无法保证Ｆｌｏｕｎｄｅｒｉｎｇ查询的完备性．有关Ｆｌｏｕｎｄｅｒｉｎｇ及ｎｏｎ－Ｆｌｏｕｎｄｅｒｉｎｇ查询的详细讨论超出了　本文的范围，但ＳＬＧ算法在语义查询的过程中具备判定一个查询是否为Ｆｌｏｕｎｄｅｒｉｎｇ查询的能力．如果ＳＬＧ断　定某个查询是Ｆｌｏｕｎｄｅｒｉｎｇ查询，则报警并给出原因，然后退出语义查询过程．ＸＳＢ系统是目前被广泛认可而又有　效的实现ＳＬＧ算法的逻辑程序引擎．　２安全策略语言　鉴于已有安全策略语言描述能力及对安全策略验证支持上的不足，本文基于一阶逻辑提出了一种支持安　９１６　Ｊｏｕｒｎａｌ　ｏｆ　Ｓｏｆｔｗａｒｅ软件学报Ｖｏ１．２３，Ｎｏ．４，Ａｐｒｉｌ　２０１２　全策略验证的新型安全策略语言，简记为ＳＰＬ．从语法形式上来看，ＳＰＬ兼容绝大数现有的安全策略语言，并且比　它们具有更强的描述能力．　定义５（规则）．设ｗｆｆ为不含“　”逻辑连接符的一阶逻辑表达式　为原子，则称公式（３）形式的逻辑表达式为　规则．公式（３）一般简写成Ａ￣ｗｆｆ的形式．若　７７ｒ为空，则可简写成　÷－或　．此时　也称为事实．　Ｖ　（３）　定义６（安全策略）．在本文中，由有限个公式（３）形式的规则构成的集合称为安全策略．　给定安全策略　它通过下列方式唯一地定义了一个与劂有常元符号构成　的常元符号集；②在跚应的一阶逻辑系统　：①在　砷出现的所　出现的所有谓词符号构成　的谓词符号集；③函数符号集为　空集．因而，　也可简记为　上述类型的逻辑系统中使用的一阶语言，称为安全策略语言，简记为ＳＰＬ．　由定义６可知，每个扩展型逻辑程序都是一个ＳＰＬ安全策略．由定义６还可以知道，ＳＰＬ兼容绝大多数已有　的安全策略语言．例如，它兼容文献［２—８】中提出的安全策略语言．　安全策略语言关注两个方面的表达能力：总体表达能力和个体表达能力．前者指通过规则的不同组合最终　能够达到的表达能力，一般直接称为表达能力；后者是指单个规则最终能够达到的表达能力，一般简称为描述能　力．从安全策略管理的角度来看，具有相同表达能力的两种安全策略语言，描述能力越强的安全策略语言越容易　受到安全管理人员的欢迎．由于安全策略语言直接面向安全管理员，因而目前的研究都非常注重安全策略语言　的描述能力．　对于任意给定的安全策略　设　表达式的集合，　（　）为　序规则的集合．由定义５可知，　为其对应的一阶逻辑系统，Ｆ（　）为　能够表达的所有一阶逻辑　（　）　（　）．因而，从语　能够表达的所有安全策略规则的集合，　（　）为　声能够表达的所有逻辑程　（　）ｃ：ｚＦ（　）．同样，由第１．２节的内容可知，　法的角度来看，ＳＰＬ的描述能力弱于相应的一阶逻辑语言，但强于相应的逻辑程序语言．此外，由本文定理２和定　理３不难发现，ＳＰＬ的表达能力等价于扩展逻辑程序的表达能力．　３安全策略良基语义　直接定义安全策略语义面临着巨大困难，为此，本文首先将安全策略转换成扩展型逻辑程序，然后利用扩展　型逻辑程序的良基语义定义安全策略的良基语义．算法ｌ通过转换运算①至转换运算⑩，将安全策略中的规则　转换成扩展型逻辑程序中的规则，从而将安全策略转换成扩展型逻辑程序．　算法１．安全策略转换（ｓｅｃｕｒｉｔｙ　ｐｏｌｉｃｙ　ｔｒａｎｓｆｏｒｍａｔｉｏｎ）．　ＰｏｌｉｃｙＴｒａｎｓ（，ＳＹ￣）　Ｆｏｒ　ｅａｃｈ　ｒｕｌｅ，ｉｎ　ａｐｐｌｙ　ｏｎｅ　ｏｆ　ｔｈｅ　ｆｏｌｌｏｗｉｎｇ　ｔｒａｎｓｆｏｒｍａｔｉｏｎｓ　ｔｏ，．　①　Ｒｅｐｌａｃｅ　ｂｙ　ａｎｄ　÷－　＾～（　ｚ，ＯＡＷｒ　＼￣　～　②　Ｒｅｐｌａｃｅ　ｂｙ　ａｎｄ　（　＾　～　⑧　Ｒｅｐｌａｃｅ　ｂｙ　一　～（　，＋　＾　÷－　～　④　Ｒｅｐｌａｃｅ　ｂｙ　ａｎｄ　÷－　＾（　＾　＾　⑤　Ｒｅｐｌａｃｅ　ｂｙ　÷＿　～（　＾～　＾　～　ｒ＾　包义保等：基于良基语义的安全策略表达与验证方法　９１７　⑨　Ｒｅｐｌａｃｅ　ｂｙ　一　，＾　⑦　Ｒｅｐｌａｃｅ　Ａ　ＡＶ置…Ｖ　Ｗ＾　ｂｙ　（　Ｒｅｐｌａｃｅ　÷－　＾～ｊ　…３　（￣　）＾　Ａ七一　＾～　…Ｖｘ　ＷＡ　．ｂｙ　⑨　Ｒｅｐｌａｃｅ　Ａ÷－　ｂｙ　一　＾ｊ置…３　（￣Ｗ）＾　Ａｊ　…３ｘＷＡ　．＾Ｗ　Ｚ１．．．，　卜÷　＾　ｗｈｅｒｅ　Ｚｌ，．．．，　ａｒｅ　ｄｉｓｔｉｎｃｔ　ｖａｒｉａｂｌｅｓ　ｔｈａｔ　ａｒｅ　ｎｏｔ　ｆｒｅｅｌｙ　ｏｃｃｕｒｒｉｎｇ　ｉｎ　Ａ，　ａｎｄ　Ｗｒ．　（　Ｒｅｐｌａｃｅ　Ａ　＾一３　…３ｘ　＾　Ｗ　．ｂｙ　ａｎｄ　（Ｙｌ，．．．，　＾Ｗｒ　ｐ（　，…，　）七一了　…３ｘＷ　．ｗｈｅｒｅｐ／ｋ　ｉｓ　ａ　ｎｅｗ　ｋ－ａｒｉｔｙ　ｐｒｅｄｉｃａｔｅ　ｎｏｔ　ｏｃｃｕｒｒｉｎｇ　ｉｎ　Ｓ＇Ｐ　ａｎｄ　ｒｌ，…，Ｙｋ　ａｒｅ　ａｌｌ　ｔｈｅ　ｆｒｅｅ　ｖａｒｉａｂｌｅｓ　ｉｎ　ｊ　…ｊ　．　Ｕｎｔｉｌ　ｎｏ　ｔｒａｎｓｆｏｒｍａｔｉｏｎ　ｃａｎ　ｂｅ　ａｐｐｌｉｅｄ　ｔｏ　Ｅｎｄ．　Ｎｏｔｅ：　ｈａｓ　ｔｈｅ　ｆｏｒｍ　Ｌ１＾…ＡＬ　ｗｈｅｒｅ　Ｌｆ　ｉｓ　ａ　ｌｉｔｅｒａ１．　Ｖａｎｄ　ｗｒ　ａｒｅ　ｆｉｒｓｔ—ｏｒｄｅｒ　ｆｏｒｍｕｌａｓ．　定理１证明了算法１的可终止性和计算复杂度．这里，ＬｗｆＪｌ为表达式ｗｆｆ中的原子数目、“一”连接符号数　目、“ｖ”连接符号数目、“ｊ”连接符号数目、“　”连接符号数目及“～”连接符号数目之和，称为表达式ｗｆｆ的尺寸．　若黝一个安全策略，则称１　５＂ｆ　ｌ＝∑，　舻ｆ　ｒ　ｆ为蹦尺寸．　定理ｌ（算法１的可终止性）．对于任意给定的安全策略　算法１可在有限步内执行完毕，并且其转换结果　是一个扩展型逻辑程序．设　卿规则数目为Ｖ，…Ｖ’连接符号数目为ｍ，“　”连接符号数目为　，ｕ＝ｍａｘ｛［ｒ［［ｒｅ，５￣，ｋ　为使得“≤２　的最小值，则最坏情况下，算法１总的转换次数不大于ｖ．２　。＋　＋　；平均情况下，算法１总的转换次　数不大于ｖ．（“＋　．２Ｌ１），因而具有较好的实用价值．　证明：设　七一　为卿的任一规则，算法１应用于　的转换运算为　同时，粥　换为　１）　若ｆ为转换运算①、转换运算②、转换运算④或转换运算⑩，则得到两个新规则，设为　１　嘲Ａ２（－－ｗｆＡ．不难发现，１ｗｆＡ－＜　ｆ＜ｆ嘲；　和　２）　若沩转换运算③、转换运算⑥或转换运算⑨，则得到一个新规则，设为　１÷．　．不难发现，｝嘲｛＜ｆ嘲，　因而ＩＳＰｄ＜ｌ，ｓ￣；　３）　若　转换运算⑧，则得到一个新规则，设为　１　嘲，容易看出，ＩＷｆＡ［＝１嗍．但转换运算⑧后面紧跟着　的转换运算一定是转换运算⑨，设其转换结果为　２卜　，容易看出，Ｉ　ｌ＜ｌ嘲Ｉ＝Ｉ　；　４）　若确转换运算⑤，则所得结果一定为一个新规则，设为Ａ。＜－ｗ￣ｉ，容易看出，ＩＷｆＡ［＝１ｗｆｆ．若无后续转换　运算可作用于　，则转换结束，即算法１可在有限次转换运算后终止；否则，在所有后续转换运算中，　转换运算⑤最多出现　一１次．这是因为，每应用一次转换运算⑤，都会使得原。　砷“ｖ”连接符号至少　减少一个，而所有其他的转换运算都不会引入“ｖ”连接符号；　５）　若『为转换运算⑦，则得到一个新规则，设为Ａ１　嘲，容易看出，ＩＷｆｆｄ＝［Ｗ￣＋１．但转换运算⑦后面紧跟　着的转换运算一定是转换运算⑩，设其转换结果为　２　啦和　３七一　ｊ，并且ｌ嗽１≤ＩＷｆｆｄ一１＝Ｉ嗍，　Ｉ　Ｉ≤ｌＷｆＡＩ一１＝ＩＷｆｊ］．同样，若无后续转换运算可作用于　则转换结束；否则，在所有后续转换运算　中，转换运算⑦最多出现ｎ一１次．这是因为，每应用一次转换运算⑦，都会使得原　砷“ｖ”连接符至少　减少一个，而所有其他的转换运算都不会引入“Ｖ”连接符号．　综合上述步骤１）～步骤５）的分析可知，转换运算腰么使得Ｊ　钎Ｉ＜Ｉ嗍（即转换得到的新规则的尺寸小于原规　９１８　Ｊｏｕｒｎａｌ　ｏｆ　Ｓｏｆｔｗａｒｅ软件学报Ｖｏ１．２３，Ｎｏ．４，Ａｐｒｉｌ　２０１２　则的尺寸），要么使得Ｉ　＝Ｉ　．由于使得ＩＳＰ，Ｉ＝Ｉ，Ｓ＇￣的转换运算　整个转换运算序列中最多出现ｍ＋ｎ次，因而　对于任一安全策略　算法ｌ一定可在有限步转换运算后将其转换成逻辑程序　并终止．如果　不是逻辑程　序，则　中一定存在可以继续应用转换运算的规则，因而算法１还没有终止，这显然是矛盾的．　在极端情况下，算法１选择的转换运算序列中的每个转换运算都使一个尺寸为ｉ的规则分裂为尺寸为ｆ一１　的两个规则．因而，针对每个规则的转换运算序列最大长度不超过ｖ．２　＋　＋ｎ，转换结果　中规则数目最多不　超过ｖ．ｕ个．在现实世界中，这种极端情况极其罕见，因而转换运算序列长度的平均值更具有参考价值．　在平均情况下，算法１针对每个规则选择的转换运算序列中的每个转换运算，使一个尺寸为ｉ的规则转换成　尺寸为卜１的另一个规则，或分裂为尺寸为ｌ　ｆ／２　Ｉ的两个规则，因而总的转换次数不超过　ｖ・（“＋２・ｆ兰］＋２　・ｆ参］＋…＋２　・ｆ拳］）≤ｖ・（“＋２・萼＋２　・　＋…＋２　・蒡］＝ｖ・　“＋　・２　一－，．　口　Ｉｚ　一ｙ　；Ｉ　，　这个值非常接近于（　１）．Ｕ　由下述引理１～引理４可以看出算法１中转换运算①～转换运算⑩的正确性．　引理１．下述表达式在三值逻辑中是恒等式：　（￣　＾ｒｖ））ｓＩｚ　Ｖｖ～　），　（　Ｖ　））；Ｉｚ（￣　＾一　），　（Ｖ　…Ｖ以　）－－／ｚ（￣ｊ置…ｊ　（￣　）），　（￣Ｖ　…Ｖ　）　证明：利用定义３即可完成证明．设纳三值解释．　（１）　（２）　（３）　（４）　（一～　）；１一　（一　）　１一（１一Ｉｚ（　））；　（　）；　（ｊ置…ｊ　（～　）），　（　—Ｗ）；Ｉｚ（Ｖｖ～ｒｖ）．　（￣（Ｖ＾ｒｖ））；ｌ一　（　＾　）　１一ｍｉｎ（／ｚ（　），易（　））；ｍａｘ（１一／ｚ（　），１一／ｚ（　））ｓ　（￣（Ｖｖ　））；１一　（￣ｊ　Ｖ　）＝１一ｍａｘ（Ｉｚ（　），Ｉｚ（　））　ｒａｉｎ（１一Ｉｚ（　），ｌ—Ｉｚ（　））　Ｖｖ～　）；　（￣Ｖ）ＡＩｉ（￣　）；　））　１一　（｜　（￣　））ｓ１一ｍａｘ｛￣ｚ　ｒｘ￣ｃ）：Ｃ∈　）　ｍｉｎ｛１一／ｚ　ＷＩｘ￣ｏ）：Ｃ∈　｝　ａｉｒｎ｛１一（１一／ｚ（　Ｊ　Ｈ　））：ｃ∈　｝Ｅｍｉｎ｛／ｚ（ｒｖｌ　）：Ｃ∈　｝ｉ／ｚ（　（　））；　（５）Ｉｚ（￣ＶｘＷ）；ｌ一　（Ｖ　）；１一ｍｉｌｌ｛Ｉｚ（ｒＶＩｘ￣ｏ）：Ｃ∈　）；ｍａｘ｛１一Ｉｚ（ｒｖＩｘ￣ｃ）：Ｃ∈厶　｝　；ｍａｘ｛ｌｚ（～　Ｉ　卜÷。）：Ｃ∈／－／ｇ）ｉＩｚ（ｊ　（￣　））．　（６）由“一”逻辑连接符的含义可立即得到　（　一　）；Ｉｚ（Ｖｖ一　）．　引理２．设ｒ：Ａ￣－ＷＭ＾（Ｖ＾　＾　仅当　１和ｔ＂２的语义．　口　ｒ的语义，当且　１：　ｒ２：　＾　（夕　）为三值解释．维证明：“　”的证明：７６妨设　为一个基本原子．　（１）　若　∈　口Ｉｚ（　）＝ｌ，由Ｉｚ的定义可知，　）≥　（　＾Ｖ＾　）且　（　）≥Ｉｚ（　＾　＾　）．由定义　３可知，易（，ｉ）：ｌ，　（　）＝１，因而篪ｒ１和ｒ２的语义；　（２）Ａ￣２Ｎ＿　仨　即　（　）＝去．由于疆，．的语义，则由定义３可知，　（　＾（Ｖｖ　）＾　）≤寺，因而　（　），　（　），　（　ｖ　Ｗ）中必有一个不大于去：　ａ）若　（　）≤　１或　（　）≤寺，则　（　＾　＾　）≤　１且　（　＾　＾　）≤寺；　ｂ）若　（　）＞￣１ｔ　（　）＞｛，即　（　）＝１且　（　）＝ｌ，则　．包义保等：基于良基语义的安全策略表达与验证方法　９１９　（　Ｖ　Ｗ）＝ｍａｘ（￣（　），Ｉｚ（　））≤÷．　因而乞（　）≤　且　（　）≤　，从而可得　（　＾ＶＡ　）≤　且　（　＾　＾　）≤　；　由上述ａ）和ｂ）可知，Ｉｚ（　）≥Ｉｚ（　ＡＶＡ　）且　（　）≥　（　ＡＷＡ　）．由定义３可知，　（　）＝ｌ，　（　）＝１．因而维ｒ１和　的语义；　（３）若　∈　即Ｉｚ（　）＝０．由于缇，的模型，则由定义３可知，　（　＾（ＶｖＷ）Ａ　）＝０，因而Ｉｚ（　），　（　），　（　Ｖ　Ｗ）中必有一个为０：　ａ）若　（　）＝０或　（　）＝０，则　（　＾Ｖ＾　）：０且易（　＾Ｗ＾　）＝ｏ；　ｂ）若　（　）≠０且　（　）≠０，则　ｖＷ）：ｍａｘ（Ｓ　（　），Ｉ　（　））＝０，因而　（　）＝Ｉｚ（　）＝０，从而　可得　（　＾ＶＡ　）＝０且　（　＾Ｗ＾　）＝０；　由上述ａ）和ｂ）可知，Ｉｚ（　）≥Ｉｚ（　Ａ　Ａ　）且　（　）≥　（　ＡＷＡ　）．由定义３可知，Ｉｚ（　）＝１，　（ｒ２）＝１，因而维ｒｌ和１＂２的语义．　“乍”的证明与“＝＝＞”证明的逆过程类似，这里不再赘述．　口　引理３．设，：　÷＿　了　ＷＡＷｒ，，ｉ：Ａ÷－　ＡＷ１　ｚ＾　，变量Ｚ不在规则ｒ中出现，．２　（　）为三值解释．．Ｚ．　是ｒ的语义，当且仅当　ｒ　的语义．　证明：　，的语义营Ｉｚ（　）≥Ｉｚ（　Ａ３ｘＷＡ　）　营　（　）≥ｍｉｎ（／ｚ（　），ｒｌｆａｘ｛　Ｉｘ￣ｏ）：ｃ∈　｝，　（　））　营Ｉｚ（　）≥ｍｉｎ（Ｉｚ（　），Ｉｚ（　ｌ　ｚ），　（　））　§Ｉｚ（　）≥　（　＾Ｗ　卜÷ｚ＾　）　§　是　１的语义．　口　引理４．设ｒ：　÷－　～ｊ　ＷＡＷＴ）ｒｌ：Ａ（－－－ＷＨＡ￣ｐ（ＹＩ，．．．，　ＡＷＴ，ｒ２：Ｐ（ＹＩ，．．．，　（　）为三值解释．这里，　ｐ／ｋ为新引入的　元谓词，它不在表达式　，　～了　及　中出现，ｙ】…．，　为　中的全部自由变元．那么，绳，　的语义，当且仅当　＝（　；尸）是　１和／＇２的语义．这里，　＝　ｕ｛ｐ（ｃ　．．，　）１　ｃ１，－．．，　∈　，　（　ＷＩ　卜÷ｑ…　）＝１｝，　厂　＝厂ｕ｛Ｐ（ｑ，．．．，　）ｌ　Ｃ１，．．．，　∈　，　（ｊ　ＷＩ　ｑ．．．，　ｑ）＝Ｏ｝．　证明：“＝＝＞”的证明：由于　，显然　ｎ　＝　．容易验证ｒ２在．Ｚ－　中的真值为“真”，即　，（　）：１．下面证明　，（，ｉ）＝１．不妨设　为一个基本原子．由于ｐ／后是新引入的谓词，则由　的定义可知：　（　）＝　ｔ（　），　（　）＝　，（　），　（　）＝　，（　），　ｊ　Ｗ）＝　，　ｊ　）．　由于瘫ｒ的语义，则　（１）若Ａ∈　即　（　）＝　，（　）＝１，因而一定有　，（　）≥　，（　＾一ｐ（　，．．．，ＹＤ＾　）．由定义３可知，　，（　）＝ｌ，ＯＰ．Ｚ－＇是　１和　的语义；　（２）若　ｇ殂　硭　即　（　）＝　，　）＝｛．由于维，．的模型，则由定义３可知，　（　＾～ｊ　＾　）≤去，　因而Ｉｚ（　），　（　），　（～　）中至少有一个小于或等于去：　ａ）若　（　）≤　或　（　）≤　，则一定有　，（　）≤　或易，（　）≤　，因而一定有　１　，（　Ａ—ｐ（　，…，　）Ａ　）≤÷．　ｂ）若　（％）＝ｌ且　（　）＝ｌ，则　（￣ｊ　Ｗ）＝　，　ｊ　Ｗ）≤｛，即　，（ｊ　）＝１一　，（￣了　）≥　１．由　９２０　Ｊｏｕｒｎａｌ　ｏｆ　Ｓｏｆｔｗａｒｅ软件学报Ｖｏ１．２３，Ｎｏ．４，Ａｐｒｉｌ　２０１２　于　，（　）＝１，即　，（ｐ（　９　ｏ　ｏ￣￣　））≥　，（　Ｗ）≥寺，因而　，（￣ｐ（　，．．．，　））＝１一　，（ｐ（ＹＩ，．．．，　））≤去，　二　Ｚ　１　即Ｉｚ，（　＾一ｐ（　，…，　）＾　）≤÷．　由上述ａ）和ｂ）可知，　，（　）≥　，（　＾一　（　，．．．，　）＾　）．由定义３可知，Ｉｚ．（，ｉ）＝１，即　是ｒ１的语义；　（３）若Ａｅｆ，，￣ｒｌ　（　）＝　，（　）＝０．由于　是ｒ的模型，则由定义３可知，　（　＾～　∥＾　）＝０，因而　Ｉｚ（　），Ｉｚ（　），　了　）中必有一个为０：　（　＾～ｐ（　，…，　）＾　）＝０．　ａ）若　（　）＝０或　（　）＝０，则一定有　，（　）＝０或　，（　）＝０，因而一定有　，ｂ）若　（　）≠０且　（　）≠０，则Ｉｚ（￣｜　Ｗ）＝　，（￣ｊ　Ｗ）＝０，即　，（　ｒ）＝１一　，　ｊ　）：１．由于　（ｒ２）＝１，即Ｉｚ，（ｐ（　，．．．，　））≥　，（　）＝１，因而　，（￣ｐ（　，．．．，　））＝１一　，（ｐ（　，．．．，　））＝０，即　．　（　＾一ｐ（　，…，　）＾　）：０．　由上述ａ）和ｂ）可知，　，（　）＝　．（　＾～ｐ（　，．．．，　）＾　）．由定义３可知，　，（，ｉ）＝１，即．Ｚ＿　是，１的语义．　综上所述，若　跫，．的语义，则　是　】和ｒ２的语义．　“仁”的证明过程与“　”证明的逆过程类似，这里不再赘述．　口　定理２说明，算法１在转换安全策略的过程中引入的新谓词虽然向原安全策略的语义中增加了一些新的基　本原子，但这对原安全策略的语义并不构成实质性的影响，因而是可靠的．定理３说明，算法１具有保持安全策略　语义的能力，因而是完备的．由引理１～引理４，容易证明算法ｌ的可靠性和完备性．　定理２（算法１的可靠性）．设　哟一个安全策略，　算法ｌ转换后所得结果为‘５　，　＝＜７’；厂，＞为　，　的一个三值语义朋证明：由　转换过程中由转换运算⑩新引入的所有谓词构成的集合，则　（　，　厂　，因而　）是　．　一个三值语　义．这里，　＝　一｛ｐ（　）ＩＰ∈Ａ／＂，ｐ（　）∈　｝，尸＝　一｛ｐ（ｔ一）ＩＰ∈Ａ／＂，ｐ（　）∈厂　｝．　：（　尸）为三值模型可得，　ｎ尸＝　，容易看出厂　由引理１一引理４可直接推导出，　的每个规则在　＝（　；尸＞中的真值都为真．　的每个规则在　绅的真值也都为真．　口　由于集合　和　仅是从　’和尸’中去除了那些对　绅规则的真值赋值不会产生影响的基本原子ｆ这是因　为这些原子所对应的谓词都是在转换过程中新引入的），因而卿综上所述，　（　是　啪一个三值语义．　定理３（算法１的完备性）．设　黝安全策略，　（　则存在　＝（　；尸），其中，　日　，　）为　啪三值语义，　是　算法ｌ转换后所得结果　，　尸　日　，　的三值语义．　证明：由定理ｌ可知，算法１可在有限步内转换完毕．设算法１应用于　构成的序列依次为『１，．．．，　．设　造方法如下所示：　的转换次数为ｍ，且这些转换运算　＝（乃　构　过前ｉ－１次转换后所得到的安全策略记为　－１，令　＝　１）　若　为转换运算①一转换运算⑨，令　＝／　＿１．由引理ｌ一引理３可知，若／　一１是　的语义；　２）　若　为转换运算⑩，则被转换的规则为　的全部自由变元．令　＝（　乃，其中，　１的语义，则／　是　一　Ｗ＾Ｗｒ，ｐｉ／ｋ为新引入的　元谓词，　，．．．，　为ｊ　中　＝　１　ｕ｛Ｐｉ（ｑ，．．．，　）Ｉ　Ｃ１，．．．，Ｃｋ∈　，　（ｊ　ｌ　＝　ｌ　ｕ　（ｃ　．．，Ｃｋ）ｌ　Ｃ１，．．．，Ｃｋ∈　，　（　由引理４可知，若　一１是　１的语义，则　是　的语义．　Ｉ　．．，　）＝１），　＂　）＝０）．　口　，　＝：＜　；厂　＞为　定理２和定理３保证了通过扩展型逻辑程序的良基语义定义安全策略语义的合理性．　定义７（安全策略的良基语义）．设　哟安全策略，臃这里．　算法１转换后所得结果为　的良基语义，　为转换过程中由转换运算⑩新引入的所有谓词构成的集合，则称．／ｔ４＝－＜　）是　良基语义．　包义保等：基于良基语义的安全策略表达与验证方法　９２１　７－＝　一｛ｐｆｆ）ｆＰ∈　，ｐ（　）∈７－　｝，厂＝尸　一｛ｐｆｆ）ｆＰ∈Ａ／＂，ｐ（　）∈　）　４安全策略语义查询与验证　本节讨论基于良基语义的安全策略语义查询问题，进而构造出安全策略决策算法和验证算法．首先讨论查　询目标为　ｐＱ＂）形式的表达式（即基本查询目标）时安全策略语义查询问题，并给出相应的算法，该算法可应用　于安全策略决策等方面；其次，讨论查询目标为一阶逻辑表达式（即复杂查询目标）时安全策略语义查询问题，并　给出相应的算法，该算法可应用于安全策略验证等方面．　４．１安全策略基本查询及安全策略决策　设　安全策略，　为劂良基语义，ｐ／ｎ为跚的一个谓词，ｐ（ｉ－）为ｎ元原子．那么存在哪些ｎ元基本置　换阿以使得ｐｆｆ）Ｏ为　于　逻辑结果呢？这个问题称为安全策略基本查询问题．本节基于算法１给出了　一种安全策略基本查询问题的求解方法，其基本思想如算法２所示．这里，　为ＳＬＧ算法返回的查询结果．ＳＬＧ算　法和ＸＳＢ系统的相关信息可参考文献［２０，２１］．　（１）　如果Ｒ＝Ｏ，则说明不存在基本置换使得原子ｐｆｆ）在　良基语义中成立．由于本文认为良基语义是　扩展型逻辑程序的正则语义，因而可以断言，］（ｐ（　））在　砷是不成立的；　（２）　如果尺≠　，则说明存在基本置换使得原子ｐＱ＂）在　良基语义中成立，因而可以断言，ｊ（ｐ（　））在，ｇＰ　中是成立的：　（３）　如果ＸＳＢ系统返回Ｆｌｏｕｎｄｅｒｉｎｇ警告，则无法判定了（ｐ（　））在　砷是否成立．　算法２．安全策略语义基本查询算法．　定理４（安全策略基本查询算法的可靠性和完备　性）．ｐ（ｉ）Ｏ是　对于朋｝勺逻辑结果，当且仅当ｐ（ｉ）Ｏ是　相对于其良基语义．Ａｔ　的逻辑结果．　证明：由算法ｌ的可靠性（定理２）和完备性（定理３）可直接得证．　口　安全策略语义基本查询算法经过简单变换后可处理　ｐ（　）形式的查询目标，主要用于策略决策等方面．　４．２安全策略复杂查询及安全策略验证　安全属性不变式通常是比较复杂的一阶逻辑表达式，安全策略语义基本查询算法只能处理形式较为简单　的（仅含有一个原子的）查询目标，因而无法满足安全策略验证的需求．为了解决安全策略验证问题，本节首先给　出了将安全策略复杂查询问题转化为安全策略简单查询问题的算法（参见算法３），并且证明了该算法的可靠性　和完备性；其次，利用安全策略语义基本查询算法构造出安全策略复杂查询算法，该算法主要用于安全策略验　证，因而本文称其为安全策略验证算法．由于安全策略验证算法是基于安全策略语义基本查询算法的，因而安全　策略验证和安全策略决策使用相同的语义，可有效避免本文引言中提到的验证失效等问题的产生．　算法３．安全策略复杂查询转换．　ＱｕｅｒｙＴｒａｎｓ（（，ｈ￣，Ｑ））　ｕ｛ａｎｓ（Ｘ１，．．．　）　ａ）；　Ｒｅｔｕｒｎ（ＰｏｌｉｃｙＴｒａｎｓ（，Ｓ￣　），ａｎｓ（Ｘｌ，．．．　））　Ｅｎｄ．　设　安全策略，　伪　良基语义，Ｑ为不含“　”的任意形式的一阶逻辑表达式　，．．．　为Ｑ中的全部　自由变元，那么存在哪些ｎ元基本置换可以使得Ｑ为　于　勺逻辑结果呢？这个问题称为安全策略复杂查询　问题，记为（　Ｑ）．设ａｎｓ／ｎ为一个未在　出现过的ｎ元谓词符号，则算法３可以将（　Ｑ）转换成另一个等价　的安全策略基本查询问题（　，ａｎｓ（Ｘ１，．．．　））．这里，　”为扩展型逻辑程序．定理５证明了算法３的可靠性和完　Ｊｏｕｒｎａｌ　ｏｆ　Ｓｏｆｔｗａｒｅ软件学报Ｖｏ１．２３，Ｎｏ．４，Ａｒ＇ｒｉｌ　２０１２　备性．定理６证明了算法３的可终止性．　定理５（算法３的可靠性和完备性）．在算法３中，设　（　＿）是　＝　ｕ｛ａｎｓ（ｃ　ｃ　）Ｉｃ　ｃ　∈　＝良基语义，令　，　）＝１｝，　卜÷　）＝０），　，　（ｇＩ　，　（ｇ　Ｉ　厂ｕ｛ａｎｓ（ｃＩ，．．．，Ｃｎ）Ｉ　Ｃ１，．．．，Ｃｎ∈　则有：　（１）　（２）　＝（　；尸）是扩展型逻辑程序　的良基语义；　是　的良基语义，即上面的（１）成立．　（　（Ｑ））＝１当且仅当　肘，（３（ａｎｓ（Ｘ１，．．．，　）））＝１．　的语义，则　，（ａｎｓ（Ｘｌ　９－＊ｏ　９　）　Ｑ）＝１．若　（ｊ（Ｑ））＝１，易知　，（　（Ｑ））＝１，即　）＝１．由定义３可知：　，　．，　证明：（１）由文献［１７】的定义３．３及　和尸的构造方法可直接得出　（２）“＝＝＞”的证明：由于．／１４　是　存在基本置换　ｆ　ｌ－－￣ａｌ，．．．　卜÷　｝使得　，（Ｑ　即，　ｒ（ａｎｓ　．，口　））ｉ　朋，（３（ａｎｓ（Ｘ￣　．，　Ｉ）））＝１．　，朋，（ａｎｓ（ａ　，．，ａ　））≥　一（Ｑ　卜÷　）．　反之，若　．（３（ａｎｓ（Ｘ１，．．．，　）））＝１，不妨设　，（ａｎｓ（ａ　．．，ａ　））＝１．这里，口１，．．．，ａ　∈　由规则ａｎｓ（Ｘｌ…．　）　Ｑ推导出来，并且　造方法可知，，　（Ｑ　…　．由于ａｎｓ（ａｌ，．…ａ　）仅能　是　的良基语义，因而　，（Ｑ　卜＋　矗　）＝１．由　．．．（　；尸　）构　卜＋　）＝１，即　（　（Ｑ））＝１．　口　口　“乍”的证明与“　”证明的逆过程类似，这里不再赘述．　定理６（算法３的可终止性）．算法３可在有限步内转换完毕，其总的转换次数是多项式级的．　证明：该结论是定理１的直接推论．　至此，本文给出了将安全策略转换成扩展型逻辑程序及将安全策略查询问题转换成扩展型逻辑程序查询　问题的算法，并且证明了这些算法在良基语义下的可终止性、可靠性和完备性．下面将利用这些结论构建安全　策略验证算法．为了使验证算法具有足够高的效率，本文假设：　①安全策略中每个规则　的ｗｆｆ中不含有任何函数符号；　②待验证的安全属性都可以表示成一个不含逻辑连接符“　”和函数符号的一阶逻辑表达式；　③为了保证安全策略验证过程的可靠性和完备性，每个待验证的安全属性都是一个ｎｏｎ．Ｆｌｏｕｎｄｅｒｉｎｇ查询．　对于那些无法表示成ｎｏｎ．Ｆｌｏｕｎｄｅｒｉｎｇ查询的安全属性，则不在本文考虑的范围之内．　安全策略验证算法的结构如算法４所示．在该算法中，首先利用算法３，将安全策略　哪待验证的安全属性　不变式Ｑ构成的安全策略复杂查询问题（　Ｑ）转换成安全策略简单查询问题（　”，ａｎｓ（Ｘ１，．．．　））．由于　”是　扩展型逻辑程序，ａｎｓ（Ｘｌ…．　）是基本查询目标，因而ＸＳＢ系统可高效地计算它并返回查询结果　：　（１）　如果Ｒ＝Ｏ，则说明不存在基本置换使得安全属性不变式Ｑ在　基语义是扩展型逻辑程序的正则语义，因而可以断言，ｊ（Ｑ）在　良基语义中成立．由于本文认为良　是不成立的；　（２）　如果Ｒ＊Ｏ，则说明存在基本置换使得Ｑ在　啪良基语义中成立，因而了（Ｑ）在　砷成立；　（３）　如果ＸＳＢ系统返回Ｆｌｏｕｎｄｅｒｉｎｇ警告，则说明无法判定ｊ（Ｑ）在卿算法４．安全策略验证算法．　安全属性Ｑ　安全策略　ＱｕｅｒｙＴｒａｎｓ（，Ｙ￣，Ｑ）　是否成立．　ＳＬＧ算法　（ＸＳＢ系统）　定理７（安全策略查询算法的可靠性和完备性）．设　黾　证明：该结论是定理５的直接推论．　良基语义，则　（Ｑ）是　啪对于　ｑ逻辑结果，　口　当且仅￣（ａｎｓ（Ｘｌ，．．．　））是　”相对于其良基语义　”的逻辑结果．　至此，我们已经完成了安全策略语言的设计、安全策略语义的定义及安全策略语义查询算法和验证算法的　包义保等：基于良基语义的安全策略表达与验证方法　９２３　设计．接下来，我们将这些研究成果组合起来，形成一个切实可用的安全策略管理框架ｗＦ．ＳＰｅｖｆ．　５　ＷＦ．ＳＰｅｖｆ安全策略管理框架　ＷＦ．ＳＰｅｖｆ的整体架构如图１所示，可在统一的安全策略良基语义下实现以下主要功能：　・安全策略表达：安全管理员根据系统安全需求，通过安全策略语言ＳＰＬ制定安全策略，并存储到策略　库中：　・安全策略查询：信息系统根据具体应用场景形成基本查询目标提交给ＷＦ．ＳＰｅｖｆ．ＷＦ．ＳＰｅｖｆ根据安全策　略及查询目标，通过安全策略语义基本查询算法计算出查询结果并反馈给信息系统；　・安全属性表达：安全专家根据系统特性提炼出系统应具备的安全属性，然后通过安全策略语言ＳＰＬ表　达出来，形成安全属性不变式．值得注意的是，ＷＦ—ＳＰｅｖｆ使用相同的语言表达安全属性和安全策略，这是　ＷＦ—Ｓｐｅｖｆ与其他安全策略验证工具的一个显著不同点；　・安全策略验证：ＷＦ—ＳＰｅｖｆ根据安全策略和安全属性不变式，自动地验证两者之间的符合性．如果安全策　略满足安全属性不变式，则验证通过；否则，安全策略中存在错误或不足．此时，ＷＦ．ＳＰｅｖｆ提供完整的出　错原因，以便于安全管理员调试安全策略．值得注意的是，安全策略验证和安全策略查询使用相同的语　义，这是ＷＦ．Ｓｐｅｖｆ与其他验证技术最重要的区别．由于安全属性不变式本质上是一阶逻辑表达式，因此　ＷＦ．ＳＰｅｖｆ还可用于其他能够表达成一阶逻辑表达式的属性判定问题，如策略冲突检测等．　Ｆｉｇ．１　Ｓｅｃｕｒｉｔｙ　ｐｏｌｉｃｙ　ｆｒａｍｅｗｏｒｋ　ｏｆ　ＷＦ—ＳＰｅｖｆ　图１　ＷＦ．ＳＰｅｖｆ的安全策略框架　在ＷＦ－ＳＰｅｖｆ中，安全策略语言、安全策略语义查询算法和安全策略验证算法构成一个有机的整体．它们在　统一的语义下对外提供策略表达、策略决策、策略验证等服务．ＷＦ．ＳＰｅｖｆ具备强大的描述能力、高效的策略　决策算法及强健的策略验证能力．与现有的安全策略框架相比，具有鲜明的特色．因此有理由相信，ｗＦ—ＳＰｅｖｆ可　为管理人员提供快捷、方便和易用的安全策略管理服务．　下面通过实例说明ＷＦ—ＳＰｅｖｆ的使用方法．设信息系统中存在由下列规则构成的信息流安全策　：　规则１．对于任意给定的用户Ｕ和文件　每个文件至少具有一个祖先目录），如果Ｆ的安全级别不支配Ｕ　的安全级别，同时至少有一个管理员允许　读取Ｆ的所有祖先目录，且没有管理员禁止　读取，　Ｊｏｕｒｎａｌ　ｏｆ　Ｓｏｆｔｗａｒｅ软件学报ＶｏＬ２３，Ｎｏ．１４，Ａｒ，ｒｉｌ　２０１２　的任一祖先目录，则允许Ｕ读取　规则２．对于任意给定的用户【，和文件　如果　的安全级别不支配Ｆ的安全级别，则允许Ｕ写　规则３．系统中已有的实体（用户或文件）及其安全级别分别为　，６），　，“），　，　，　１，　，（　２，”），（　３，口），其中　为　文件，　为用户．　规则４．安全级别　｛口，ｂ，Ｕ，　Ｐ）之间的支配关系如图２（ａ）所示，它们构成格．　规则５．文件夹ｔ为文件　的祖先，且管理员ａｄｍｌ和ａｄｍ２授予用户　１和Ｓ２读取文件夹ｔ的权限．　（ａ）局生谓词　上构成格（箭头表示支配关系）　（ｂ）　允许出现该信息流（箭头表示信息流向）　（ｃ）在　冲查找到一条不安全信息流路径（箭头表示信息流向）　Ｆｉｇ．２　Ａｎ　ｉｎｓｅｃｕｒｉｔｙ　ｉｎｆｏｒｍａｔｉｏｎ　ｆｌｏｗ　ｉｎ　ｓｅｃｕｒｉ￣ｃ）ｒ　ｐｏｌｉｃｙ　图２安全策略绅安全级的构成及不安全的信息流路径　（１）用ＳＰＬ表示安全策略　文献［２—８］中提出的安全策略语言不支持量词，无法简单地表示上述安全策略．然而，ＳＰＬ可简单地将上述安　全策略表示成下列形式：　置：ｐｅｒｍｉｔ（Ｕ，．Ｆ，ｒｅａｄ）＜－－－ｓｅｃＬｅｖｅｌ（Ｕ￣，　）＾ｓｅｃＬｅｖｅｌ（Ｆ，　）＾～厶，＿＜　Ａ　３ｏａｎｃｅｓｔｏｒ（Ｏ，Ｆ）＾　ｚＶＤ［（ａｕｔｈｏｚ（Ｕ，Ｄ，ｒｅａｄ，Ｚ）＾～３ｚ，ｄｅｎｙ（Ｕ，Ｄ，ｒｅａｄ，Ｚ　））Ｈ　ａｎｃｅｓｔｏｒ（Ｏ，Ｆｙ．１　互：ａｎｃｅｓｔｏｒ（ｔ，　）　：ａｎｃｅｓｔｏｒ（Ｌ，　）　：ａｎｃｅｓｔｏｒ（ｔ，．　）　：ａｕｔｈｏｚ（ｓ￣，ｔ，ｒｅａｄ，ａｄｍ１）　：ｐｅｒｍｉｔ（Ｕ，Ｆ，ｗｒｉｔｅＪ＇　ｓｅｃＬｅｖｅｌ（Ｕ，厶，），ｓｅｃＬｅｖｅｌ（Ｆ，　）．，～　Ｇ：ｓｅｃＬｅｖｅｌ（ｆ￣，ｂ）　＝　Ｃ２：ｓｅｃＬｅｖｅｌ（ｆ￣，“）　Ｇ：ｓｅｃＬｅｖｅｌ（ｆ３，ｄ）　：ｓｅｃＬｅｖｅｌ（ｓｌ，ｄ）　Ｃ５：ｓｅｃＬｅｖｅｌ（ｓ２：，Ｕ）　ｃ６：ｓｅｃＬｅｖｅｌ（ｓ３，ａ）　：ａｕｔｈｏｚ（ｓ２．，ｆ，ｒｅａｄ，ａｄｍ２）　瓦：ｄｅｎｙ（ｓ３，ｆ，ｒｅａｄ，口批）　其中，　ｌ对应规则ｌ，　２对应规则２，Ｃｌ￣ｃ６对应规则３，Ｄｌ￣Ｄ６对应规则４，Ｅ１—Ｅ６对应规则５．ｐｅｒｍｉｔ￣３，ａｎｃｅｓｔｏｒ￣２，　ａｕｔｈｅｎ／２．，ａｕｔｈｏｚ／４，ｄｅｎｙ￣４，ｓｅｃＬｅｖｅｌ／２和＿＜／２都为谓词符号，表达的含义是不言自明的．　（２）安全策略决策　判断夕堤否允许Ｓ】读取　的过程如下（参见算法２）：首先，利用算法１将　转换成扩展型逻辑程序　慷Ｓ后，利　用ＸＳＢ系统评估查询（　，ｐｅｒｍｉｔ（ｓｌ【　，ｒｅａｄ）），即可获得最终的判决结果．　利用算法ｌ转换　冲Ｒ　的过程如下所示：连续３次应用转换运算⑨后　１可被转换成公式（４）所示的规则：　ｐｅｒｍｉｔ（Ｕ，Ｆ，ｒｅａｄ）　ｓｅｃＬｅｖｅｌ（Ｕ，．厶，）＾ｓｅｃＬｅｖｅｌ（Ｆ，　）＾～　．＜　＾ａｎｃｅｓｔｏｒ（Ｏ，，）＾　ＶＤ［（ａｕｔｈｏｚ（Ｕ，Ｄ，ｒｅａｄ，ｚ）＾～３ｚ，ｄｅｎｙ（Ｕ，．Ｄ，ｒｅａｄ，ｚ　））Ｈ　ａｎｃｅｓｔｏｒ（Ｏ，Ｆ）】　…　一　包义保等：基于良基语义的安全策略表达与验证方法　９２５　应用转换运算⑦，公式（４）所示的规则可转换成公式（５）所示的规则：　ｐｅｒｍｉｔ（Ｕ，Ｆ，ｒｅａｄ）÷－ｓｅｃＬｅｖｅｌ（Ｕ，厶，）＾ｓｅｃＬｅｖｅｌ（Ｆ，　）＾～　一＜　＾ａｎｃｅｓｔｏｒ（Ｏ，Ｆ）＾　～　ｒｃ、　ｆ）［～（（ａｕｔｈｏｚ（Ｕ，０，ｒｅａｄ，Ｚ）＾～３ｚ，ｄｅｎｙ（Ｕ，０，ｒｅａｄ，Ｚ　））÷—　ａｎｃｅｓｔｏｒ（Ｏ，Ｆ））］　应用转换运算⑩，公式（５）所示的规则可转换成公式（６）和公式（７）所示的两个规则：　：ｐｅｒｍｉｔ（　Ｆ’ｒｅａｄ）￣－－ＳｅｃＬｅｖｅｌ（Ｕ，Ｌ　＾ＳｅｃＬｅｖｅｌ（ｕ，Ｌｕ）Ａ￣Ｌ旷也ＦＡａｎｃｅｓｔｏｒ（Ｏ，　人—ｐ（　ｚ）　ｐ（　卜ｊ０［－（（ａｕｔｈｏｚ（　０，ｒｅａｄ，Ｚ）＾３ｚ，ｄｅｎｙ（　０，ｒｅａｄ，Ｚ＇）），－－￣ａｎｃｅｓｔｏｒ（Ｏ，　）】　（６）　（７）　已经没有转换运算可应用于公式（６）．应用转换运算⑨，公式（７）所示的规则可转换为公式（８）所示的规则：　ｐ（　ｚ）￣－－－－（（ａｕｔｈｏｚ（　０，ｒｅａｄ，　Ａ３ｒｄｅｎｙ（　０，ｒｅａｄ，Ｚ＇））＊－￣ａｎｃｅｓｔｏｒ（Ｏ，　）　（８）　应用转换运算③，公式（８）所示的规则可转换成公式（９）所示的规则：　（　Ｚ）￣－－－（ａｕｔｈｏｚ（　０，ｒｅａｄ，）Ｚ＾３￣ｄｅｎｙ（　０，ｒｅａｄ，Ｚ＇））Ａａｎｃｅｓｔｏｒ（Ｏ，　（９）　应用转换运算①，公式（９）所示规则可转换成公式（１０）和公式（１１）所示的两个规则：　：ｐ（　ｚ）＋－－－ａｕｔｈｏｚ（　０，ｒｅａｄ，Ｚ）Ｉ＾ａｎｃｅｓｔｏｒ（Ｏ，　（１Ｏ）　ｐ（　ｚ）　ｊ　ｄｅｎｙ（　０，ｒｅａｄ，Ｚ＇）＾ａｎｃｅｓｔｏｒ（Ｏ，　（１１）　已经没有转换运算可应用于公式（１Ｏ）．应用转换运算⑨，公式（１１）所示规则可转换成公式（１２）所示的规则：　：　（　ｚ）￣－－ｄｅｎｙ（　０，ｒｅａｄ，Ｚ＇）＾ａｎｃｅｓｔｏｒ（Ｏ，　（１２）　已经没有转换运算可应用于公式（１２），转换过程结束，因而　１被转换成３个扩展型逻辑程序规则｛Ｔ１，Ｔｚ，Ｔ３）．　最终，算法１将　本专换成扩展型逻辑程序　＝（Ｐ－－｛Ｒｌ｝）Ｕ｛　，Ｔ２，／＇３）．　将　＝｛专换成　后，利用ＸＳＢ逻辑程序查询引擎评估查询（　，ｐｅｒｍｉｔ（ｓｌ　，ｒｅａｄ）），查询结果集为空集，具体的查　询评估过程参见文献［２０，２１］．这说明，　允许　】直接读取　，如图２（ｂ）所示．　ｆ３１安全属性验证　．　’　一个信息流安全策略．从信息流的角度来看，为了保护机密性，高安全级别客体中的信息应无法流向低　安全级别的客体，即　砬该能够满足ＳＰＬ安全属性不变式Ｑ：　Ｑ＝Ｖｑ，与，ｏ２，上２　（ｃａｎＦｌｏｗＴｏ（Ｏ１，０２）＾ｓｅｃＬｅｖｅｌ（Ｑ，厶）ＡｓｅｃＬｅｖｅｌ（０２，　）ＡＬ２　厶））．　这里，安全属性不变式　表示“高安全级别客体中的信息应无法流向低安全级别的客体”．为了判定　否　满足Ｑ，需要向原安全策略刀书加入下列两个用于刻画信息流向的规则：　：ｃａｎＦｌｏｗＴｏ（Ｏ１，０２）４－－－ｐｅｒｍｉｔ（Ｓ，Ｏｌ，ｒｅａｄ），ｐｅｒｍｉｔ（Ｓ，０２，ｗｒｉｔｅ），　：ｃａｎＦｌｏｗＴｏ（ｑ，Ｄ３）　ｃａｎＦｌｏｗＴｏ（Ｏｚ，０２），ｃａｎＦｌｏｗＴｏ（Ｏｚ，０３），　其中，规则　表示，对于给定的用户　、客体０１和Ｄ２，如果　能够读取Ｄ１，同时　能够向Ｄ２中写入信息，则０ｌ　中的信息能够流向０：；规则　表示信息流向具有传递性．显然，将　和　加入绅不会改变　有的安全属性．　令　”＝Ｐｕ｛Ｖ１，Ｖ２｝，验证　堤否满足Ｑ的过程如下所示（参见算法４）：　首先，利用算法３将复杂查询（　”，Ｑ）转换成基本查询（　。　，ｔｍｐ）．由算法３和算法１容易得到扩展型逻辑程　序　，其中，ｔｍｐ和Ｐ是在转换（　”，Ｑ）的过程中新引入的０元谓词；　＝ＰｏｌｉｃｙＴｒａｎｓ（Ｐ　ｕ｛ｔａｒｐ　Ｑ））　：　，ｕ｛　．…　　』Ｉ　÷Ｐ＜－－ｃａｎＦｌ－～ｐ　ｏｗＴｏ（Ｏｚ，０２）Ａ　ｓｅｃＬｅｖｅｌ（Ｏ￣，厶）ＡｓｅｃＬｅｖｅｌ（Ｏ２，　）＾Ｌ２＿＜厶Ｊｌ　　然后，利用算法２评估查询（　。　，ｔｍｐ）．如果　”能够满足Ｑ，则语义查询（　ｂ　，咖　）的结果集应该为空集．然而，　算法２却能够查询到一条规则序列（当ＸＳＢ系统工作于调试模式时，能够跟踪查询过程中所调用的规则序列）．　相应地，由这条规则序列可得到一条信息流，如图２（ｃ）所示．在这条信息流中，信息能够从安全级别为ｄ的客体　不安全地流向安全级别为ｂ的客体．．　由于安全级别ｄ支配安全级别６，因而席在安全隐患．　由上例可知，ｗＦ—ＳＰｅｖｆ可以高效地验证安全策略是否满足某个查询，进而判定是否满足某个安全属性．　９２６　Ｊｏｕｒｎａｌ　ｏｆ　Ｓｏｆｔｗａｒｅ软件学报Ｖｏ１．２３，Ｎｏ．４，Ａｐｒｉｌ　２０１２　６结论　本文首先定义了一种基于一阶逻辑的安全策略语言ＳＰＬ．它不仅兼容现有主流的安全策略语言，还可以表　达具有非单调和递归等高级特性的复杂安全策略；其次，本文通过安全策略转换算法（算法１）将ＳＰＬ安全策略转　换成扩展型逻辑程序，进而利用扩展型逻辑程序的良基语义给出了ＳＰＬ安全策略的语义；再次，本文利用逻辑程　序理论构造出安全策略语义基本查询算法（算法２），可用于处理简单查询目标，主要应用于安全策略决策．在此　基础上，本文给出了将安全策略语义复杂查询问题转换成安全策略语义基本查询问题的算法（算法３），进而构造　出安全策略验证算法（算法４）．显然，安全策略验证算法和安全策略决策算法基于相同的语义，有效地保证了安　全策略验证的有效性；最后，本文将上述研究成果组合起来，形成安全策略管理框架ＷＦ．ＳＰｅｖｆ．总体来说，　ＷＦ．ＳＰｅｖｆ可在统一的良基语义基础上实现安全策略表达、语义查询和安全策略验证，具有强大的策略描述能　力、高效的策略决策能力以及可靠的策略验证能力，可应用于各种类型的策略管理系统中．　Ｒｅｆｅｒｅｎｃｅｓ＂　［１】　Ｂｏｎａｔｔｉ　ＰＡ，Ｓｈａｈｍｅｈｒｉ　Ｎ，Ｄｕｍａ　Ｃ，Ｏｌｍｅｄｉｌｌａ　Ｄ，Ｎｅｊｄｌ　Ｗ，Ｂａｌｄｏｎｉ　Ｍ，Ｂａｒｏｇｌｉｏ　Ｃ，Ｍａｒｔｅｌｌｉ　Ａ，Ｐａｔｔｉ　Ｖ，Ｃｏｒａｇｇｉｏ　Ｐ，Ａｎｔｏｎｉｏｕ　Ｇ，　Ｐｅｅｒ　Ｊ，Ｆｕｃｈｓ　ＮＥ．Ｒｕｌｅ—Ｂａｓｅｄ　ｐｏｌｉｃｙ　ｓｐｅｃｉｉｆｃａｔｉｏｎ：Ｓｔａｔｅ　ｏｆ　ｔｈｅ　ａｒｔ　ａｎｄ　ｆｕｔｕｒｅ　ｗｏｒｋ．Ｔｅｃｈｎｉｃａｌ　Ｒｅｐｏｒｔ，ＩＳＴ５０６７７９，Ｐｒｏｊｅｃｔ　Ｄｅｌｉｖｅｒａｂｌｅ　ＤＩ，Ｗｏｒｋｉｎｇ　Ｇｒｏｕｐ　１２．２００４．ｈｔｔｐ：／／ｒｅｗｅｒｓｅ．ｎｅｔ／ｄｅｌｉｖｅｒａｂｌｅｓ／ｉ２一ｄ１．ｐｄｆ　［２】Ｗｏｏ　ＴＹＣ，Ｌａｍ　ＳＳ．Ａｕｔｈｏｒｉｚａｔｉｏｎ　ｉｎ　ｄｉｓｔｉｒｂｕｔｅｄ　ｓｙｓｔｅｍｓ：Ａ　ｎｅｗ　ａｐｐｒｏａｃｈ．Ｊｏｕｒｎａｌ　ｏｆＣｏｍｐｕｔｅｒ　Ｓｅｃｕｒｉｔｙ，１９９３，２（２・３）：１０７—１３６．　［３】Ｊａｊｏｄｉａ　Ｓ，Ｓａｍａｒａｔｉ　Ｐ，Ｓａｐｉｎｏ　ＭＬ，Ｓｕｂｒａｈｍａｎｉａｎ　ＶＳ．Ｆｌｅｘｉｂｌｅ　ｓｕｐｐｏｒｔ　ｆｏｒ　ｍｕｌｔｉｐｌｅ　ａｃｃｅｓｓ　ｃｏｎｔｒｏｌ　ｐｏｌｉｃｉｅｓ．ＡＣＭ　Ｔｒａｎｓ．ｏｎ　Ｄａｔａｂａｓｅ　Ｓｙｓｔｅｍ，２００１，２６（２）：２１４－２６０．［ｄｏｉ：１０．１　１４５／３８３８９１．３８３８９４】　【４】Ｊａｊｏｄｉａ　Ｓ，Ｓａｍａｒａｔｉ　Ｐ，Ｓｕｂｒａｈｍａｎｉａｎ　ＶＳ，Ｂｅｒｔｉｎｏ　Ｅ．Ａ　ｕｎｉｉｆｅｄ　ｆｒａｍｅｗｏｒｋ　ｆｏｒ　ｅｎｆｏｒｃｉｎｇ　ｍｕｌｔｉｐｌｅ　ａｃｃｅｓｓ　ｃｏｎｔｒｏｌ　ｐｏｌｉｃｉｅｓ．Ｉｎ：　Ｐｅｃｋｍａｎ　ＪＭ，Ｆｒａｎｋｌｉｎ　Ｍ，ｅｄｓ．Ｐｒｏｃ．ｏｆ　ｔｈｅ　ＡＣＭ　ＳＩＧＭＯＤ　Ｉｎｔ’１　Ｃｏｎｆ．ｏｎ　Ｍａｎａｇｅｍｅｎｔ　ｏｆ　Ｄａｔａ（ＳＩＧＭＯＤ’９７）．Ｎｅｗ　Ｙｏｒｋ：ＡＣＭ，　１９９７．４７４－４８５．［ｄｏｉ：１０．１　１４５／２５３２６０．２５３３６４】　・　［５］Ｂａｒｋｅｒ　Ｓ，Ｓｔｕｃｋｅｙ　ＰＪ．Ｆｌｅｘｉｂｌｅ　ａＣＣｅＳＳ　ｃｏｎｔｒｏｌ　ｐｏｌｉｃｙ　ｓｐｅｃｉｉｆｃａｔｉｏｎ　ｗｉｔｈ　ｃｏｎｓｔｒａｉｎｔ　ｌｏｇｉｃ　ｐｒｏｇｒａｍｍｉｎｇ．ＡＣＭ　Ｔｒａｎｓ．ｏｎ　Ｉｎｆｏｒｍａｔｉｏｎ　Ｓｙｓｔｅｍ　Ｓｅｃｕｒｉｔｙ，２００３，６（４）：５０１—５４６＿【ｄｏｉ：１０．１　１４５／９５０１９１．９５０１９４】　【６】Ｇｅｌｆｏｎｄ　Ｍ，Ｌｏｂｏ　Ｊ．Ａｕｔｈｏｒｉｚａｔｉｏｎ　ａｎｄ　ｏｂｌｉｇａｔｉｏｎ　ｐｏｌｉｃｉｅｓ　ｉｎ　ｄｙｎａｍｉｃ　ｓｙｓｔｅｍｓ．Ｉｎ：Ｄｅ　Ｌａ　Ｂａｎｄａ　ＭＧ，Ｐｏｎｔｅｌｌｉ　Ｅ，ｅｄｓ．Ｐｒｏｃ．ｏｆ　ｈｅ　ｔ２４ｔｈ　Ｉｎｔ’１　Ｃｏｎｆ．ｏｎ　Ｌｏｇｉｃ　Ｐｒｏｇｒａｍｍｉｎｇ．ＬＮＣＳ　５３６６，Ｂｅｒｌｉｎ，Ｈｅｉｄｅｌｂｅｒｇ：Ｓｐｒｉｎｇｅｒ—Ｖｅｒｌａｇ，２００８．２２—３６．［ｄｏｉ：１０．１００７／９７８－３－５４０—　８９９８２—２＿７］　［７】Ｂｅｃｋｅｒ　ＭＹ，Ｆｏｕｒｎｅｔ　Ｃ，Ｇｏｒｄｏｎ　ＡＤ．Ｄｅｓｉｇｎ　ａｎｄ　ｓｅｍａｎｔｉｃｓ　ｏｆ　ａ　ｄｅｃｅｎｔｒａｌｉｚｅｄ　ａｕｔｈｏｒｉｚａｔｉｏｎ　ｌａｎｇｕａｇｅ．Ｉｎ：Ｐｒｏｃ．ｏｆ　ｔｈｅ　２０ｔｈ　ＩＥＥＥ　Ｃｏｍｐｕｔｅｒ　Ｓｅｃｕｒｉｔｙ　Ｆｏｕｎｄａｔｉｏｎｓ　Ｓｙｍｐ．（ＣＳＦ　２００７）．Ｗａｓｈｉｎｇｔｏｎ：ＩＥＥＥ　Ｃｏｍｐｕｔｅｒ　Ｓｏｃｉｅｔｙ，２００７．ｈｔｔｐ：／／ｄ１．ａｃｍ．ｏｒｇ／ｃｉｔａｔｉｏｎ．ｃｆｍ？ｉｄ　１２７０６３９［ｄｏｉ：１０．１　１０９／ＣＳＦ．２００７．１８】　【８】Ｇｕｒｅｖｉｃｈ　Ｙ，Ｎｅｅｍａｎ　Ｉ．ＤＫＡＬ：Ｄｉｓｔｒｉｂｕｔｅｄ－Ｋｎｏｗｌｅｄｇｅ　ａｕｔｈｏｒｉｚａｔｉｏｎ　ｌａｎｇｕａｇｅ．Ｉｎ：Ｐｒｏｃ．ｏｆ　ｔｈｅ　２１ｓｔ　ＩＥＥＥ　Ｃｏｍｐｕｔｅｒ　Ｓｅｃｕｒｉｔｙ　Ｆｏｕｎｄａｔｉｏｎｓ　Ｓｙｍｐ．Ｗａｓｈｉｎｇｔｏｎ：ＩＥＥＥ　Ｃｏｍｐｕｔｅｒ　Ｓｏｃｉｅｔｙ，２００８．１４９—１６２．ｈｔｔｐ：／／ｄ１．ａｅｍ．ｏｒｇ／ｃｉｔａｔｉｏｎ．ｅｆｍ？ｉｄ＝１３８１２５１【ｄｏｉ：１０．　１　１０９／ＣＳＦ．２００８．８】　【９】Ｌｌｏｙｄ　ＪＷ．Ｆｏｕｎｄａｔｉｏｎｓ　ｏｆＬｏｇｉｃ　Ｐｒｏｇｒａｍｍｉｎｇ．２ｎｄ　ｅｄ．，Ｎｅｗ　Ｙｏｒｋ：Ｓｐｒｉｎｇｅｒ－Ｖｅｒｌａｇ，１９９３．　［１０］Ｇｅｌｆｏｎｄ　Ｍ，Ｌｉｆｓｃｈｉｔｚ　Ｖ．Ｔｈｅ　ｓｔａｂｌｅ　ｍｏｄｅｌ　ｓｅｍａｎｔｉｃｓ　ｆｏｒ　ｌｏｇｉｃ　ｐｒｏｇｒａｍｍｉｎｇ．Ｉｎ：Ｋｏｗａｌｓｋｉ　Ｒ，Ｂｏｗｅｎ　ＫＡ，ｅｄｓ．Ｐｒｏｃ．ｏｆｔｈｅ　５ｔｈ　Ｉｎｔ’１　Ｃｏｎｅ　ｏｎ　Ｌｏｇｉｃ　Ｐｒｏｇｒａｍｍｉｎｇ．ＭＩＴ　Ｐｒｅｓｓ．１９８８．１０７０－１０８０．ｈｔｔｐ：／／ｗｗｗ．ｍｅｎｄｅｌｅｙ．ｃｏｒｎ／ｒｅｓｅａｒｃｈ／ｔｈｅ—ｓｔａｂｌｅ‘ｍｏｄｅｌ。ｓｅｍａｎｔｉｃｓ—ｆｕｒ。　ｌｏｇｉｃ—ｐｒｏｇｒａｍｍｉｎｇ／　［１　１］Ｈａｌｐｅｒｎ　ＪＹ，Ｗｅｉｓｓｍａｎ　Ｖ．Ｕｓｉｎｇ　ｆｉｒｓｔ－ｏｒｄｅｒ　ｌｏｇｉｃ　ｔｏ　ｒｅａｓｏｎ　ａｂｏｕｔ　ｐｏｌｉｃｉｅｓ．ＡＣＭ　Ｔｒａｎｓ．ｏｎ　Ｉｎｆｏｒｍａｔｉｏｎ　Ｓｙｓｔｅｍ　Ｓｅｃｕｒｉｔｙ，２００８，　１１（４）：１－４１．【ｄｏｉ：１０．１１４５／１３８０５６４．１３８０５６９】　［１２］Ｚｈｏｕ　ＡＹ，Ｓｈｉ　Ｂ．Ｔｈｅ　ｆｉｘｐｏｉｎｔ　ｃｈａｒａｃｔｅｒｉｓｔｉｃ　ｏｆ　ｓｅｍａｎｔｉｃｓ　ｏｆ　ｄａｔａｌｏｇ　ｗｉｔｈ　ｎｅｇａｔｉｏｎ．Ｊｏｕｒｎａｌ　ｏｆ　Ｓｏｆｔｗａｒｅ，１９９５，６（５）：２５７～２６４（ｉｎ　Ｃｈｉｎｅｓｅ　ｗｉｔｈ　Ｅｎｇｌｉｓｈ　ａｂｓｔｒａｃｔ）．ｈｔｔｐ：／／ｗｗｗ．ｊｏｓ．ｏｒｇ．ｃｎ／１０００—９８２５／１９９５０５０１．ｈｔｍ　【１３］　Ｃｅｒｉ　Ｓ，Ｇｏｔｔｌｏｂ　Ｇ，Ｔａｎｃａ　Ｌ．Ｗｈａｔ　ｙｏｕ　ａｌｗａｙｓ　ｗａｎｔｅｄ　ｔｏ　ｋｎｏｗ　ａｂｏｕｔ　ｄａｔａｌｏｇ（ａｎｄ　ｎｅｖｅｒ　ｄａｒｅｄ　ｔｏ　ａｓｋ）．ＩＥＥＥ　Ｔｒａｎｓ．ｏｎ　Ｋｎｏｗｌｅｄｇｅ　ｎｄ　ａＤａｔａ　Ｅｎｇｉｎｅｅｒｉｎｇ，１９８９，１（１）：１４６—１６６．【ｄｏｉ：１０．１　１０９／６９．４３４１０】　［１４】Ｊａｅｇｅｒ　Ｔ，Ｓａｉｌｅｒ　Ｒ，Ｚｈａｎｇ　ＸＬ．Ａｎａｌｙｚｉｎｇ　ｉｎｔｅｇｒｉｔｙ　ｐｒｏｔｅｃｔｉｏｎ　ｉｎ　ｔｈｅ　ＳＥＬｉｎｕｘ　ｅｘａｍｐｌｅ　ｐｏｌｉｃｙ．Ｉｎ：Ｐｒｏｃ．ｏｆ　ｔｈｅ　１２ｔｈ　Ｃｏｎｆ．ｏｎ　ＵＳＥＮＩＸ　Ｓｅｃｕｒｉｔｙ　Ｓｙｍｐ．，Ｖｏ１．１２．Ｗａｓｈｉｎｇｔｏｎ，２００３．ｈｔｔｐ：／／ｄ１．ａｃｍ．ｏｒｇ／ｃｉｔａｔｉｏｎ．ｃｆｍ？ｉｄ　１２５１３５８＆ＣＦＩＤ　８９９２４３４５＆ＣＦＴＯＫＥＮ　３４５４６７７７　包义保等：基于良基语义的安全策略表达与验证方法　９２７　ｚｍａｎｎ　ＧＪ．Ｔｈｅ　ｍｏｄｅｌ　ｃｈｅｃｋｅｒ　ＳＰＩＮ．ＩＥＥＥ　Ｔｒａｎｓ．ｏｎ　Ｓｏｆｔｗａｒｅ　Ｅｎｇｎｅｅｒｉｎｇ，１９９７，２３（５）：２７９—２９５．【ｄｏｉ：１０．１　１０９／３２．５８８５２１］　【１５］　Ｈｏｌ　ＪＹ，Ｑｉｎｇ　ＳＨ，Ｌｉｕ　Ｗ，Ｈｅ　ＪＢ．Ａｎａｌｙｓｉｓ　ｏｎ　ｉｍｐｌｉｃｉｔ　ａｕｔｈｏｒｉｚａｔｉｏｎ　ｉｎ　ｐｒｉｖｉｌｅｇｅ　ｔｈｒｏｕｇｈ　ｒｕｌｅ　ｄｅｄｕｃｔｉｏｎ．Ｊｏｕｒｎａｌ　ｏｆ　Ｓｏｆｔｗａｒｅ，　［１６】　Ｃａｉ２００８，１９（８）：２１０２～２１１３（ｉｎ　Ｃｈｉｎｅｓｅ　ｗｉｔｈ　Ｅｎｇｌｉｓｈ　ａｂｓｔｒａｃ０．ｈｔｔｐ：／／ｗｗｗ．ｊｏｓ．ｏｒｇ．ｃｎ／１０００・９８２５／１９／２１０２．ｈｔｍ　ｆｄｏｉ：１０．３７２４／ＳＰ．Ｊ．１００１．　２００８．０２１０２】　　Ａ，Ｒｏｓｓ　ＫＡ，ＳｃｈｌｉｐｆＪＳ．Ｔｈｅ　ｗｅｌｌ—ｆｏｕｎｄｅｄ　ｓｅｍａｎｔｉｃｓ　ｆｏｒ　ｇｅｎｅｒａｌ　ｌｏｇｉｃ　ｐｒｏｇｒａｍｓ．Ｊｏｕｒｎａｌ　ｏｆＡＣＭ，１９９１，３８（３）：６２０—６５０　［１７］　Ｖａｎ　Ｇｅｌｄｅｒ［ｄｏｉ：１０．１　１４５／１　１６８２５．１　１６８３８］　ｏｎ　ＨＢ．Ｉｎｔｒｏｄｕｃｅ　ｔｏ　Ｍａｔｈｅｍａｔｉｃａｌ　Ｌｏｇｉｃ．２ｎｄ　ｅｄ．，Ｓａｎ　Ｄｉｅｇｏ：Ａｃａｄｅｍｉｃ　Ｐｒｅｓｓ，２００１．　【１８］　Ｅｎｄｅｒｔｚｙｍｕｓｉｎｓｋｉ　Ｔ．Ｗｅｌｌ・Ｆｏｕｎｄｅｄ　ｓｅｍａｎｔｉｃｓ　ｃｏｉｎｃｉｄｅｓ　ｗｉｈ　ｔｔｈｒｅｅ－ｖａｌｕｅｄ　ｓｔａｂｌｅ　ｓｅｍａｎｔｉｃｓ．Ｆｕｎｄａｍｅｎｔａ　Ｉｎｆｏｒｍａｔｉｃａｅ，１９９０，１３（４）：　【１９］　Ｐｒ４４５－４６３．　ＷＤ．Ｗａｒｒｅｎ　ＤＳ．Ｔａｂｌｅｄ　ｅｖａｌｕａｔｉｏｎ　ｗｉｈ　ｔｄｅｌａｙｉｎｇ　ｆｏｒ　ｇｅｎｅｒａｌ　ｌｏｇｉｃ　ｐｒｏｇｒａｍｓ．Ｊｏｕｒｎａｌ　ｏｆ　ＡＣＭ，１９９６，４３（１）：２０—７４．【ｄｏｉ：１０．　［２０］　Ｃｈｅｎ　１　１　４５／２２７５９５　２２７５９７］　ｕａｔｉｏｎ　ｕｎｄｅｒ　ｔｈｅ　ｗｅｌｌ—ｆｏｕｎｄｅｄ　ｓｅｍａｎｔｉｃｓ．Ｉｎ：Ｐｒｏｃ．ｏｆ　ｔｈｅ　１２ｔｈ　ＡＣＭ　ＳＩＧＡＣＴ—ＳＩＧＭＯＤ＿　【２１］　Ｃｈｅｎ　ＷＤ，Ｗａ￣ｅｎ　ＤＳ．Ｑｕｅｒｙ　ｅｖａｌＳＩＧＡＲＴ　Ｓｙｒｕｐ．ｏｎ　Ｐｒｉｎｃｉｐｌｅｓ　ｏｆＤａｔａｂａｓｅ　Ｓｙｓｔｅｍｓ．Ｗａｓｈｉｎｇｔｏｎ，１９９３．［ｄｏｉ：１０．１　１４５／１５３８５０．１５３８６５】　ｌｉｏｔｔ　ＢＤ，Ｐａｄｕｌａ　Ｌ，Ｌｅｏｎａｒｄ　Ｊ．Ｓｅｃｕｒｅ　ｃｏｍｐｕｔｅｒ　ｓｙｓｔｅｍ：Ｕｎｉｆｉｅｄ　ｅｘｐｏｓｉｔｉｏｎ　ａｎｄ　ｍｕｌｔｉｃｓ　ｉｎｔｅｒｐｒｅｔａｔｉｏｎ．Ｔｅｃｈｎｉｃａｌ　Ｒｅｐｏｒｔ，　【２２］　ＥｌＥＳＤ—ＴＲ．７５—３０６，ＭＩＴＲＥ　Ｃｏｒｐｏｒａｔｉｏｎ，１　９７６．　附中文参考文献：　【１２］周傲英，施伯乐．带否定的ＤＡＴＡＬＯＧ的语义的不动点特性．软件学报，１９９５，６（５）：２５７—２６４．ｈｔｔｐ：／／ｗｗｗ．ｊｏｓ．ｏｒｇ．ｃｎ／ｌＯ００－９８２５／　ｌ９９５０５０１．ｈｔｍ　［１６］蔡嘉勇，卿斯汉，刘伟，何建波．基于规则推导的特权隐式授权分析．软件学报，２００８，１９（８）：２１０２—２１１３．ｈｔｔｐ：／／ｗｗｗ．ｊｏｓ．ｏｒｇ．ｃｎ／１０００－　９８２５／１９／２１０２．ｈｔｍ［ｄｏｉ：１０．３７２４／ＳＰ．Ｊ．１００１．２００８．０２１０２］　■一包义保（１９７６一），男，安徽无为人，博士生，　方滨兴（１９６０一），男，博士，教授，博士生导　师，中国工程院院士，ＣＣＦ高级会员，主要　研究领域为网络安全，信息内容安全，并行　处理．互联网技术．　讲师，主要研究领域为智能安全，网络　安全　殷丽华（１９７３一），女，博士，副研究员，ＣＣＦ　郭莉（１９６９一），女，高级工程师，ＣＣＦ会员　主要研究领域为网络与信息安全．　会员，主要研究领域为网络安全，安全性　分析．