关于增量抽象传递代码的一些问题
摘要：递归抽象码（ACC）最近被提出作为携带证明代码（PCC）的框架，其中代码供应商提供了一个程序和一个抽象（或者程序的抽象模型），其有效性表明符合预定义的安全策略。因此，抽象起到了安全证书的作用，其生成（和验证）由一个不动点分析器自动进行。现有的PCC方法是在假设消费者一次性读取和验证整个程序和完整证书的基础上开发的，以非增量方式进行。在本文摘要中，我们概述了增量ACC的主要问题。特别是在逻辑编程的背景下，我们讨论了增量证书的生成以及用于不受信任的程序更新的增量检查算法的设计，即当生产者提供先前经过验证的程序的修订版本时。在这里，更新是指对程序的任意更改，例如用新的谓词扩展程序、删除现有谓词以及用新版本的谓词替换现有谓词。我们还讨论了每种更新方式对增量扩展的准确性和正确性的影响。
作者：Elvira Albert, Puri Arenas, German Puebla
论文ID：cs/0701111
分类：Programming Languages
分类简称：cs.PL
提交时间：2007-05-23