FORMAL VERIFICATION METHOD OF ACTIVE SOFTWARE

点击翻译按钮获取中文摘要

(1)A formal model of programs with access control based on execution history and its model checking : We defined a formal model called HBAC programs. The verification problem for HBAC programs was defined and shown to be EXPTIME-complete, while the problem is solvable in polynomial time under a reasonable assumption. The proposed method reduces the verification problem to the decision problem for a context-free grammar (cfg) that generates all the execution sequences of a given HBAC program. We also proposed a few optimization techniques that reduce the number of cfg rules useless for generating execution sequences. Experimental results showed that the verification tool we have implemented can verify practical HBAC programs within a reasonable time.(2)A static analysis using tree automata for XML access control : We proposed a static analysis method based on tree automata for determining whether a query to an XML database does not access any elements nor attributes that are prohibited by a given policy. We showed that our query model is sufficiently general by showing that the expressive power of our model is strictly greater than Neven's query automata. We also investigated a consistency problem of policies in schema transformation of XML databases and showed that the problem is decidable.(3)A formal model for stateful trust management systems : We proposed a trust management model that can represent a system with internal states. The verification problem was defined as the problem to decide whether the behavior of a system with a given policy satisfies a given verification property, and a verification method for the problem was also proposed. We implemented two verification tools, one is based on SPIN and Prolog and the other is implemented by Prolog only. Experimental results showed that the latter tool is more efficient than the former one.