Study on Computational Logic-based Methodologies for Building Secure Systems

本研究项目的总体目标是使用转换验证方法构建一种基于计算逻辑的复杂软件系统验证方法；我们使用逻辑程序来表示给定的系统和我们想要证明的正确性属性，然后将其应用于对系统和要验证的属性进行编码的逻辑程序，即保持该属性有效性的转换序列。我们得到了以下三个主要结果：(1)我们证明了文献中提出的局部分层规划的负展开并不总是正确的，并提出了一个新的负展开规则，它保证了给定程序的意义不变。(2)我们提出了分层规划的展开/折叠变换的扩展框架，其中包括扩展的负展开。提出了一种新的协同逻辑程序展开/折叠变换框架，并证明了该变换系统保持了协同逻辑程序的预期语义。实例表明，我们的变换验证方法可以简洁地验证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