FORMAL VERIFICATION METHOD OF ACTIVE SOFTWARE

(1)A基于执行历史的访问控制程序的形式化模型及其模型检测：我们定义了一个形式化模型HBAC程序。定义了HBAC程序的验证问题，并证明了该问题是EXPTIME-完全的，同时在合理的假设下，该问题在多项式时间内是可解的。所提出的方法减少了验证问题的决策问题的上下文无关文法（cfg），生成一个给定的HBAC程序的所有执行序列。我们还提出了一些优化技术，减少无用的cfg规则的数量生成执行序列。实验结果表明，我们已经实现的验证工具可以在合理的时间内验证实际的HBAC程序。(2)A基于树自动机的XML访问控制静态分析：提出了一种基于树自动机的静态分析方法，用于确定对XML数据库的查询是否未访问给定策略禁止的任何元素或属性。我们表明，我们的查询模型是足够的一般显示，我们的模型的表达能力是严格大于Neven的查询自动机。我们还研究了XML数据库模式转换中的策略一致性问题，并证明了该问题是可判定的。(3)A有状态信任管理系统的形式化模型：我们提出了一个信任管理模型，它可以表示一个具有内部状态的系统。将验证问题定义为判定系统在给定策略下的行为是否满足给定验证性质的问题，并给出了该问题的验证方法.我们实现了两个验证工具，一个是基于SPIN和Prolog的，另一个是只用Prolog实现的。实验结果表明，后一种工具比前一种更有效。

(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.