Research On Security Verification Method Of XML Query Based On Model Checking

With the increasing activity of e-commerce,mobile applications,and social networks,data that is semi-structured,such as e-mail,personal medical information,and Weibo,are emerging.XML has good self-described and dynamic scalability,making it the primary choice for describing and organizing semi-structured data.Therefore,in the XML query processing,it is necessary to verify whether the query satisfies the security property,that is,to ensure that sensitive information is not obtained illegally.Model checking is a very important formal verification method.It exhaustively searches all possible system states to verify whether a given Kripke model satisfies specific properties.The thesis is inspired by the establishment of a research topic that uses model checking technology to verify the security of XML queries.How to build a validated model,use temporal logic to describe the desired security properties,and give a model checking algorithm to verify the security of the query is the core research content of the thesis.The paper constructs an automaton model based on data tree for XML value query.The research then proposes to describe the security nature of XML query using the LTL formula.In order to simplify formula writing process,a SPS based on LTL formula of XPath path expression is proposed.The key content of the research is embodied in the process of verifying the security of XML queries by applying the linear temporal logic model checking.It is proposed that the views given in the query automata have the reasoning path of the security nature of sensitive information as the basis for query security.Finally,in order to solve the problem of state space explosion in model checking.the query optimization methods based on XML structure query and value query are studied separately.According to these research contents,the progress of the paper is as follows:(1)An XML data tree automaton is proposed as an input model for model checking.First,in order to represent an infinite value field of an XML data tree attribute value,a variable is introduced to replace a specific data value,and a variable tree mode is defined recursively.Second,build an automaton running on the data tree for the value query of the target node of the XPath path expression,which is limited to equal and unequal query evaluation.Finally,the feasibility and rationality of constructing a data tree automaton based on XPath path target node value query are given.(2)In order to describe the security properties to be verified,a method of using a linear temporal logic formula to express the security of XML queries is proposed.First of all,the paper puts forward that the nature of query security is a Linear-Time Properties,that is,whether there is inference of sensitive information in the query view.Second,we study the transformation of the safety properties given by using XPath path expressions into linear temporal logic formulas.Finally· in order to template the LTL formula writing process and simplify its verbose form,it is proposed to introduce a pattern description system to construct an LTL formula template that describes the security properties.(3)A method based on model checking to verify the security of XML query is proposed.First of all,the idea is to use query rewriting methods to determine whether the query view has a sensitive information inference path for the query and external knowledge.Then,a query automata is put forward,that is,the query view is represented by the accepted run of an automaton.Therefore,determining the query security is equivalent to the model checking based on the automata null value determination method.(4)In order to solve the problem of model state space explosion,a method based on query optimization is proposed to reduce the state space scale of the model.According to the XML structure query and the value query,the logic optimization method and the physical optimization method are respectively studied.Firstly,based on the simulation equivalence,the structure partition is obtained by solving the bisimulation quotient space to optimize the query.Secondly,based on the cost estimation,we propose to calculate the residuals from the attribute tag space to obtain the data similarity aggregation and to optimize the query.Finally,we use the data similarity of equivalence classes to study the rationality of the division.