论文部分内容阅读
随着电子商务、移动应用、社交网络的日益活跃,如邮件、个人医疗信息以及微博等半结构化海量数据不断涌现。由于扩展标记描述语言XML具有良好的自述性和动态扩展性,这使其成为描述和组织半结构数据的首要选择。XML查询处理的广义范围包含了系统处理用户查询有关的技术。在XML查询处理中有必要验证查询是否满足安全性质,也就是保证敏感信息不被非法获取。模型检测是非常重要的形式化验证方法,它通过穷尽搜索所有可能的系统状态,验证给定的系统模型是否满足特定的性质。本论文受到启发,确立了利用模型检测技术验证XML查询安全性质的研究课题。如何构建验证的模型、使用时序逻辑描述期望的安全性质、给出验证查询安全性质的模型检测方法是本论文的核心研究内容。论文首先提出构建基于数据树的自动机模型作为模型检测的输入之一,并将其用于XML值查询过程。其次,提出将XML查询的安全性质归结为线性时序性质并应用LTL公式描述,为简化公式编写过程提出安全性质的模式描述系统。然后,论文的关键研究是应用LTL模型检测方法执行XML查询安全性的验证过程,采用查询自动机是否接受敏感信息安全性质的推理路径作为查询安全验证的依据。最后,为了解决模型检测中的状态空间爆炸问题,分别研究逻辑和物理查询优化方法,利用划分思想有效降低系统状态空间规模。论文取得工作进展如下:(1)提出以XML数据树自动机作为模型检测的输入模型。首先,为了表示XML数据树属性值的无限值域,引入变量替代具体的数据值,通过递归方式定义变量树模式。其次,构建运行于数据树上的自动机用于XPath路径表达式目标节点的值查询,这里仅限于相等和不等的查询求值。最后,给出关于XPath路径目标节点值查询构建数据树自动机可行性和合理性分析证明。(2)为了描述待验证安全性质,提出使用线性时序逻辑公式表示XML查询安全性的方法。首先,探讨了查询安全性质,也就是查询视图是否存在敏感信息的推理路径,为线性时序性质的本质。其次,研究将使用XPath路径表达式给出的安全性质转换为线性时序逻辑公式。最后,为了模板化LTL公式编写过程并简化其冗长的形式,提出引入模式描述系统构建描述安全性质的LTL公式模板。(3)提出基于查询自动机的XML查询视图安全性模型检测方法。首先,其思想是对于查询和外部知识,利用查询重写的方法判定查询视图是否存在敏感信息推理路径。然后,在具体操作中提出查询自动机,也就是将查询视图通过自动机接受运行表示。那么判定查询安全性也就等价于基于自动机空值判定方法的模型检测问题。(4)为了解决模型状态空间爆炸问题,提出基于查询优化的方法降低模型的状态空间规模。根据XML结构查询和值查询分别研究逻辑优化方法和物理优化方法。首先,基于模拟等价提出通过求解互模拟商空间得到结构划分以优化查询。其次,基于代价估计提出通过属性标记空间计算其残差得到数据相似性聚集划分以优化查询。最后,利用等价类的数据相似性来研究该划分的合理性。