基于语义技术的软件用户访问控制方法

在应用软件中广泛使用的访问控制模型不能根据用户上下文来动态改变资源的访问权限。针对上述问题提出一种基于语义技术的访问控制方法,实现了对用户的动态授权。提出基于语义信息的用户模型和资源模型并构建面向用户模型和资源模型的基础本体,定义一组与访问控制相关的语义规则及推理规则,并设计基于语义推理过程的判定算法。访问控制过程是接收并分析访问请求,根据语义规则从显示的本体知识中获取相关联的用户信息,调用判定算法得出用户与资源间的访问权限关系。最后通过某综合减灾应用系统案例来验证该方法的有效性。     

基于权限验证图的Web应用访问控制漏洞检测

针对Web应用中的访问控制漏洞缺乏有效检测手段的问题，提出了一种基于权限验证图的检测算法。首先，在程序控制流图（CFG）的基础上，识别权限验证节点和资源节点，通过T和F边将节点连成权限验证图。然后，遍历资源节点对应的所有权限验证路径，计算路径验证权限，与资源节点访问权限比较，检测是否存在访问控制漏洞。实验结果表明，在7个Web应用中，发现了8个已知和未知漏洞，相比较于已有的访问控制漏洞检测算法，该算法可以有效检测4种访问控制漏洞，扩大了漏洞检测范围。     

物联网应用中访问控制智能合约的形式化验证

蓝牙、WiFi等网络技术的进步推动物联网（IoT）的发展,然而IoT在方便了人们生活的同时也存在严重的安全隐患。若无安全的访问控制,非法接入IoT的访问可能给用户带来各方面的损失。传统的访问控制方法需要一个可信任的中心节点,不适合节点分散的IoT环境。区块链及智能合约的出现为IoT应用的访问控制提供了更有效的解决方案,但用一般测试方法难以保证实现IoT应用的访问控制智能合约的正确性。针对这个问题,提出一种利用模型检测工具Verds对访问控制智能合约进行形式化验证从而保障合约正确性的方法。该方法利用状态迁移系统定义Solidity智能合约的语义,应用计算树逻辑（CTL）公式描述所要验证的性质,并对智能合约交互及用户行为进行建模,从而形成Verds的输入模型及所要验证性质,然后利用Verds验证待测性质的正确性。方法核心是Solidity合约子集到Verds输入模型的转换。对两个IoT资源访问控制智能合约的实验结果表明,该方法可以对访问控制合约的典型场景及期望性质进行验证,提升了智能合约的可靠性。     

访问控制系统的规则集模型及其检测算法

针对访问控制系统规则存在漏洞问题,提出一个建立在系统读写规则集基础之上的访问控制系统规则集模型及相应的模型检测算法,通过对系统状态的遍历,判断目标在权限提供某些许可的情况下是否可完成,并在目标可完成的情况下输出相应的策略。实验结果证明,在中等规模的系统中该算法有效。     

基于FSA和重排序的访问控制策略评估方案

针对访问控制策略评估效率问题,提出基于有限状态自动机(finite state automaton, FSA)和重排序的访问控制策略评估方案。以四元组的形式表示策略,构建FSA策略模型检测策略异常,消除策略中的冲突规则以及冗余规则,实现策略评估的前期优化;提出基于重排序的策略评估算法,重排序策略中的规则以及每个规则中的属性-值对(attribute-value pairs, AVP),减少评估访问请求过程中遍历的规则数和属性比较次数。实验结果表明,与传统策略评估引擎相比,该方案检测策略异常效率以及评估效率均有很大提升。     

同步协同应用访问控制

提出了一个同步协同访问控制结构、协同小组共有权限算法,应用规则资源编码方法进行动态信息的访问控制策略制定,解决了同步协同应用信息共享引起的非法访问问题、访问决策效率问题和协同动态信息访问控制问题。应用表明,同步协同应用访问控制结构能够减少访问控制通信量50%以上,共有权限算法和规则资源编码方法是实用的。     

工作流业务规则语义的完整性验证技术

工作流模型的验证技术主要包括语法验证、结构验证和语义验证,其中语义验证是层次最高、最为严格的验证,验证的范围十分广泛,也是难点所在,目前尚缺乏有效的方法.而且,语义的正确性会影响工作流模型的控制逻辑.也是结构合理性的影响因素之一.从工作流模型表达的语义出发,通过分析工作流模型刻画的业务规则以及相应的约束集部分,基于对约束集语义的形式化,问题转换为对约束集语义的完整性验证.如果工作流模型中的条件节点所描述的约束集语义有遗漏、冗余或者无意义,也决定了模型错误的拓扑结构.提出全域覆盖性判定定理及基于判定树的验证算法.通过验证工作流业务规则语义的完整性,对工作流模型结构的合理性也给予了保证.这种验证方法具有很强的通用性.不依赖于具体的建模方法,适用范围广泛.     

基于静态分析的强制访问控制框架的正确性验证

现阶段对操作系统的强制访问控制框架的正确性验证的研究主要集中于对授权钩子放置的验证.文中基于TrustedBSD MAC框架对强制访问控制框架的正确性验证问题进行了研究,在授权钩子放置验证的基础上,提出了安全标记的完全初始化验证和完全销毁验证.为了实现上述验证,文中提出了一个路径敏感的、基于用户自定义检查规则的静态分析方法.该方法通过对集成于编译器的静态分析工具mygcc进行扩展来验证强制访问控制框架的钩子放置的准确性和完备性.该方法具有完全的路径覆盖性.且具有低的误报率和时间开销.     

基于静态分析的XSM正确性验证

XSM(Xen Security Module)是虚拟机Xen的安全模型框架,对系统的安全性具有决定性的作用。目前,对类似的强制访问框架的正确性验证研究主要集中于对钩子函数放置的验证。现有检测方法通常路径覆盖不够完整,或者有较高的误报率。对XSM框架的正确性验证问题进行分析,提出一种过程间流敏感、过程内路径敏感的,适用于XSM框架的静态分析方法。该方法通过扩展静态分析工具Saturn,实现了对XSM框架的钩子函数设置的正确性和完备性的验证。经实验验证,该方法具有完全的路径覆盖性,并且具有较高的精确度。     

基于模型检测的工作流访问控制策略验证*

访问控制策略的有效性对工作流管理系统的安全稳定运行具有重要影响,针对这一问题,提出了一种基于模型检测的工作流管理系统访问控制策略验证方法。建立了工作流管理系统的访问控制策略模型与工作流执行主体任务权限状态模型,并在此基础上对访问控制策略的有效性进行验证。实验表明该算法具有有效性和合理性,为访问控制策略的验证提供了一条新的解决途径。     

基于时态逻辑的UML交互模型检测研究

该文详细介绍了统一建模语言和模型检测技术,在此基础上,该文研究了基于交互自动机和时态逻辑的UML交互模型性质检测方法,提出了模型检测所需的Marking算法。该算法通过对交互自动机全部状态的遍历,检测各状态的时态逻辑公式(CTL公式)的真值,以判断用户设计的UML交互模型是否符合计算机软件系统应满足的性质及规范。     

Behavioral modeling and formal verification of a resource discovery approach in Grid computing

Grid computing is the federation of resources from multiple locations to facilitate resource sharing and problem solving over the Internet. The challenge of finding services or resources in Grid environments has recently been the subject of many papers and researches. These researches and papers evaluate their approaches only by simulation and experiments. Therefore, it is possible that some part of the state space of the problem is not analyzed and checked well. To overcome this defect, model checking as an automatic technique for the verification of the systems is a suitable solution. In this paper, an adopted type of resource discovery approach to address multi-attribute and range queries has been presented. Unlike the papers in this scope, this paper decouple resource discovery behavior model to data gathering, discovery and control behavior. Also it facilitates the mapping process between three behaviors by means of the formal verification approach based on Binary Decision Diagram (BDD). The formal approach extracts the expected properties of resource discovery approach from control behavior in the form of CTL and LTL temporal logic formulas, and verifies the properties in data gathering and discovery behaviors comprehensively. Moreover, analyzing and evaluating the logical problems such as soundness, completeness, and consistency of the considered resource discovery approach is provided. To implement the behavior models of resource discovery approach the ArgoUML tool and the NuSMV model checker are employed. The results show that the adopted resource discovery approach can discovers multi-attribute and range queries very fast and detects logical problems such as soundness, completeness, and consistency.     

基于事件确定有限自动机的UML2.0 序列图描述与验证

为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性.     

Verifying Temporal Properties of Reactive Systems: A STeP Tutorial

We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion. We verify the classic two-process algorithm and simple variants, as well as an atomic parameterized version. The methods used include deductive verification rules, verification diagrams, automatic invariant generation, and finite-state model checking and abstraction.     

QRDChecker:一个QRDC模型检验工具

反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporal logic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将其实现为一个针对时段时序逻辑QRDC(quantified RDC (restricted duration calculus))的检验工具QRDChecker.QRDChecker可以检验QRDC公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将QRDC公式转换成模型检验系统Spin能够接受的自动机的形式,从而可以检查反应式系统是否满足用QRDC公式表达的性质.     

UML状态机模型形式化验证技术研究

系统建模是系统开发经常用到的分析设计方法,如何保证模型的正确性一直是人们关注的话题.为了验证系统设计的模型正确性,进而提高整个系统的质量,提出了一种通过模型检查技术对UML状态机模型进行动态语义验证的方法.对状态机模型进行形式化描述,根据定义的映射规则将图形信息映射成模型检查器可以读取的语言,分析待验证的性质内容,通过使用模型检查器得到验证结果.     

多智能体系统时态认知规范高效符号模型检测的算法研究

Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法.这些方法是非常有效的,能用于验证许多具有极大状态空间的实际系统(状态个数可以超过1020).但是,这些方法不能检测知识逻辑.而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范.文章首先讨论了Kripke结构和mu演算的扩展,然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法.     

基于事件图的离散事件仿真模型并行检验方法

非形式化仿真模型验证方法易受主观因素的影响且具有不完备性,而传统的形式化模型检验方法由于受到状态空间爆炸问题的影响,很难处理大规模的仿真模型.并行模型检验方法以其完备性、高效性已经在工业界中得到了成功的应用,但是由于涉及到形式化规约、逻辑学以及并行计算等多项技术,应用难度较大.针对上述问题,提出了基于事件图的离散事件仿真模型并行检验方法.该方法首先对事件图在模型同步方面进行了扩展,给出了扩展事件图的形式化定义、语法及语义;然后将扩展事件图模型转换到分布并行验证环境的DVE模型,成功地将并行模型检验方法应用于仿真模型验证领域.该方法使得仿真人员无须学习新的形式化验证语言就能采用并行模型检验方法对仿真模型进行形式化验证,可降低模型并行验证的难度,从而有效提高模型验证的效率和完备性.实验结果表明了该方法的有效性,有利于扩展并行模型检验方法在仿真领域中的应用.     

行为时序逻辑中四级公平性下的活性推理规则

公平性是行为时序逻辑用于表达系统活性的形式,直接影响到系统描述的正确性与完整性,对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时,却缺乏相应的、运用于性质验证的推理规则。针对这一问题,通过对公平性内涵的分析,给出了四级公平性体系下的活性推理规则,并分别进行了证明。作为示例,运用新的活性推理规则,对一个程序实例进行了推理验证。在建立起相应的活性推理规则后,四级公平性才能够被有效运用到实际的系统描述与验证中。     

工作流时序约束模型分析与验证方法

为了解决工作流时间建模与时序一致性验证问题,以时序逻辑和模型检查为基础,提出了一种工作流时间建模与时序一致性验证方法.该方法用一阶逻辑描述工作流模型及其时间信息,用时序逻辑描述工作流的时序约束,用模型检查算法对时序约束进行验证与分析.该方法不是针对某一种时序约束提出来的,而是能够验证任何用时序逻辑描述的工作流时序约束.该方法还能够对未通过验证的时序约束提供工作流运行实例作为反例,帮助用户定位模型的问题.以一个工作流时间建模和时序一致性验证的实例证实了所提出方法的有效性.