Study on Computational Logic-based Methodologies for Building Secure Systems

本研究计画的总体目标是建构一套以计算逻辑为基础的方法论，以转换式验证法来验证复杂的软体系统;我们使用逻辑程序来表示给定的系统和我们想要证明的正确性属性，然后应用于对系统和要验证的属性进行编码的逻辑程序，保持该属性有效性的一系列变换。我们得到了以下三个主要结果：（1）证明了文献中提出的局部分层规划的负开折并不总是正确的，并提出了一个新的负开折规则，该规则保证了给定规划的意义保持。(2)我们已经提出了一个扩展的框架展开/折叠变换的分层程序，包括，除其他外，一个扩展的负展开。它使规则的适用条件更一般化，从而使转换验证方法更具有适用性。(3)我们提出了一个新的框架展开/折叠转换的协同逻辑程序，并证明了我们的转换系统保持预期的语义协同逻辑程序。通过一些例子表明，我们的变换验证方法可以简洁地用于验证Buchi自动机的一些性质

The overall objective of this research project is to construct a computational-logic based methodology for the verification of complex software systems using the transformational verification method ; we use logic programs to represent a given system and a correctness property we want to prove, and then apply to a logic program encoding the system and the property to be verified, a sequence of transformations that preserve the validity of that property. We have obtained the following three main results :(1) We have shown that negative unfolding for locally stratified programs proposed in the literature is not always correct, and proposed a new negative unfolding rule which guarantees the preservation of the meaning of a given program.(2) We have proposed an extended framework for unfold/fold transformation of stratified programs, including, among others, an extended negative unfolding. It makes the application conditions of the rule more general, thereby making the transformational verification method more applicable.(3) We have proposed a new framework for unfold/fold transformation of co-logic programs, and proved that our transformation system preserves the intended semantics of co-logic programs. We have shown by some examples that our transformational verification method can be used for verifying some properties of Buchi automata in a succinct way