随着空间数据库、地理信息系统、基于用户位置服务和移动应用的普及和广泛应用,空间数据库管理系统的安全问题得到越来越多的关注。带有空间特性的角色访问控制模型Spatial-RBAC规定系统达到必要的安全要求须满足一定的空间约束,即空间区域约束、空间角色激活基数约束和空间职责分离约束。验证空间访问控制系统是否满足以上三种约束,对保证访问控制系统的安全性至关重要。本文采用模型检测的方法来验证空间访问控制系统规则是否满足相应的约束。模型检测技术是一种被广泛应用的验证有限状态系统满足规范的自动化分析方法,其基本思想是先建立待测系统的有限状态模型,然后通过穷尽搜索模型中的状态,判断其是否满足待测属性。本文主要内容如下:(1)提出了一种基于谓词逻辑的空间访问控制系统的描述方法。在这个方法中,系统由谓词及规则共同组成,其中谓词表示各空间类中对象之间的关系,规则反映了系统授权给用户的谓词读写权限。空间信息经映射函数处理后作为系统授权的条件之一,保证了系统描述的规范和简洁。(2)提出了待验证属性的表示方法及检测算法。将Spatial-RBAC规定的空间约束属性表示成统一的检测目标的形式,并针对这种统一形式设计了规则验证的模型检测算法。该算法利用用户对系统的认知来表示系统状态,将用户对系统变量是否具有读写权限作为状态的变迁条件,从目标状态开始由后往前遍历系统状态空间,找出完成目标需要的操作序列,若搜索成功则表示系统中存在空间约束不满足的情况。(3)改进了模型检测工具ACPEG。在对ACPEG源代码分析的基础上,加入了空间位置信息的处理能力并修改了源代码中检测算法的实现部分,使其满足空间访问控制系统规则检测的需要。最后通过一个空间访问控制系统规则检测分析的实例,验证了本文提出的检测方法的正确性及有效性。