基于SPIN的CSCW系统的验证

近年来,CSCW系统呈现出用户越来越多、权限关系越来越复杂、组织结构规模越来越大、处理的情况越来越复杂的趋势.因此,CSCW系统的访问控制策略以及访问控制策略的验证已成为国内外CSCW领域十分值得研究和探讨的问题.针对CSCW系统设计的特点,提出了一种验证策略.结合具体实例,使用RBAC模型描述CSCW系统的访问控制权限,利用SPIN工具将模型检测应用于验证CSCW系统属性.     

多智体系统时序认知规范的SPIN模型检测

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。     

基于角色的CSCW系统访问控制模型

针对现有的方法不能很好地满足CSCW系统对访问控制提出的新的需求,该文提出了一个基于角色的CSCW系统访问控制模型RBCSAC(role-based collaborative systems access control).该模型形式化地描述了数据、操作、权限、角色和用户等要素及其相互间的关系,提供访问控制信息的记录方法,通过分配和取消角色来完成对用户权限的授予和取消,并且提供了角色分配规则和操作合法性检查规则.该模型针对CSCW系统的多用户、交互、协作、实时、动态等特性,能较好地满足CSCW系统对访问控制的需求.     

基于SPIN的系统建模研究

模型检测由于其自动化程度高,是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器,首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理,并采用SPIN模型检测器对Promela建模进行研究。最后给出一个简单的公交车运行模型,并对实验结果进行分析。     

基于SPIN的G语言系统模型的验证

对于大型系统,为确保其运行的可靠性、稳定性及高效性,需要从两个方面对系统进行验证:业务模型和系统模型。目前,对业务模型的验证可通过BPMN来完成;对系统模型的验证可通过SPIN(Simple Promela Interpreter)工具执行。G语言是由NI公司创建的一种图形化程序框图语言,还未被加入ANSI标准,因此,文中第一步工作是提取G语言的形式、规则、文法等语言特性。由于SPIN对G语言不提供直接的支持,因此第二步工作是完成G2Promela的映射。在G2Promela的工作中,主要是基于编译器的框架,以Scanner-Parser-Optimizer-Generator(SPOG框架)为主线,根据第一步的预处理工作,按方法函数、指针、关键字、变量等分类创建G2Promela的映射规则,最终实现G2Promela的转换,完成对G语言系统模型的验证。该方法的提出弥补了G语言系统模型验证方面的空白,从而更深入地确保了G语言程序的性能。     

基于SPIN的地下建筑设备监控系统软件验证

在地下建筑智能化系统中,设备监控系统是基本的组成部分,其软件设计的正确性十分重要。提出了一种基于SPIN的地下建筑设备监控系统软件正确性验证方法。构建了基于iFIX组态软件的设备控制系统软件Promela模型,利用SPIN模型检验方法对其安全性进行了验证。还利用简化模型进行反例追踪,找出了安全性规约中存在的错误。检验结果表明提出的验证方法是有效性。     

基于SPIN／Promela的并发系统验证

并发系统安全性分析是当前计算机科学中一个重要的研究领域。模型检测是最成功的自动验证技术之一，其成功应用归功于有效验证工具的支持。SPIN是一种著名的分析验证并发系统逻辑一致性的工具。本文在阐述SPIN工作机理的基础上，详细分析了基于SPIN的系统建模语言Promela中通道操作、基本数据结构及其功能，并设计了SPIN形式化验证软件系统的基本算法，最后运用SPIN对一个并发系统实例进行验证，得出了相应验证输出图。     

WTP协议的SPIN模型检测

基于模型检测技术,使用SPIN对WTP协议进行了建模和分析．应用自动机和Promela对协议进行建模。利用LTL规范了协议需要满足的安全性,时序性。通过分析发现了协议的一个错误。     

基于SPIN的LTL属性分解方法研究

提出一种基于模型检测工具SPIN的LTL属性分解方法以解决状态空间爆炸问题。根据逻辑和时序操作符常见的组合情况,讨论不同的属性分解模式,根据子属性构建的切片准则进行程序切片,利用SPIN对切片后的等价简化模型进行检测,从而将对原模型上属性的检测转化成对复杂度较低的子模型上各子属性的分别检测。实验结果表明,该方法具有一定的有效性。     

异构分布式CSCW委托授权模型及其访问控制

基干角色和活动的重要特性,提出了一种面向CSCW环境基于角色-活动并具有时序特征和约束规则的委托授权模型RABDM for CSCW,以及CSCW访问控制体系架构和委托授权工作机制。该模型解决了基于CSCW图形图像协同处理实际应用中访问授权过于集中的问题,实现了分布式和动态时序性等特征。     

基于角色的访问控制在CSCW系统中的应用

首先介绍了RBAC模型的主要思想。针对计算机支持的协同系统用户多、权限关系复杂、组织机构规模大的特点,设计了基于角色的访问控制在CSCW中的安全模型。结合案例分析了该模型中协同环境下的角色划分、权限管理、安全策略和协同策略。最后给出了数据库实现。     

WTP协议的SPIN模型检测

基于模型检测技术,使用SPIN对WTP协议进行了建模和分析.应用自动机和Promela对协议进行建模,利用LTL规范了协议需要满足的安全性,时序性。通过分析发现了协议的一个错误。     

PROMELA语义引擎执行研究

模型检查工具SPIN的核心是PROMELA语言,对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。该文从语义角度研究了PROMELA语义引擎问题。首先给出PROMELA语法的抽象对象模型形式化定义,然后给出一个算法来实现PROMELA语法到抽象对象模型的映射,描述了PROMELA指称语义。     

Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus (FireWire) Protocol

We describe how the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol is modelled in Promela and verified using SPIN. The verification of arbitrary system configurations is discussed. Received July 2001/Accepted in revised form November 2002 Correspondence and offprint requests to: Alice Miller, Department of Computing Science, University of Glasgow, 17 Lilybank Gardens, Glasgow G12 8QQ, UK. Email: alice@dcs.gla.ac.uk     

基于SPIN的无线传感器网络安全协议建模与分析

模型检验方法在有线网安全协议的分析和设计方面取得了巨大成功。无线传感器网络对安全协议同样具有严格的要求;与有线网相比,无线传感器网络在通信环境和网络节点等方面都更为脆弱,为相应的安全协议的分析和设计提出了挑战。提出了一种适用于无线传感器网络的安全协议形式化建模分析方法。它充分借鉴了传统有线网络安全协议的建模方法,在其基础上充分考察了无线传感器网络的通信环境以及网络节点,建立起一个全面并且直观的安全协议运行模型。以A.Perrig等人提出的SPINS安全协议为例,应用模型检验工具SPIN对其认证性和机密性等安全需求进行了分析验证,发现了该协议存在的漏洞。实例分析证实了模型检验方法在分析无线传感器网络安全协议时的有效性,从而推进了其在安全协议分析方面的应用范围。     

基于SPIN的IKEv2协议高效模型检测

论文先简单介绍了互联网密钥交换协议IKEv2,然后利用著名的模型检测工具SPIN对其进行了建模和分析。在建模的过程中,作者发现现有的建模方法很难对结构复杂的协议IKEv2进行建模,而且用现有的建模方法建立的模型可读性差、自动化程度不高,验证效率也比较低,因此现有的建模方法只适用于对简单协议进行建模。针对这些不足之处,提出了一种程序可读性、自动化程度及验证效率均较好的建模方法,而且这种建模方法特别适合对复杂的安全协议进行建模。最后利用SPIN对IKEv2协议的模型进行了验证,发现IKEv2协议不能抵御主动攻击,并给出了两个攻击序列图。针对IKEv2协议不能保护发起者身份的缺陷,提出了自己的一种改进意见。