抽象携带代码中证书大小的缩减
Certificate size reduction in Abstraction-Carrying Code
摘要：
携带代码（ACC）最近被提出作为移动代码安全的框架，其中代码供应商提供程序连同抽象（或程序的抽象模型），其有效性需要遵守预定义的安全策略。向代码消费者提供（定点）抽象的优点是在单次传递中检查其有效性（即，一次迭代）的基于抽象解释的检查器。使ACC在实践中有用的一个主要挑战是尽可能减少证书的大小，同时不增加检查时间。直观的想法是只在证书中包含检查器在不迭代的情况下无法复制的信息。我们引入了减少证书的概念，其特征在于检查器需要的抽象的子集，以验证（和重建）在一个单一的通行证的完整证书。基于这一概念，我们仪器的通用分析算法与必要的扩展，以确定相关的检查器的信息。有趣的是，简化的证书省略了（部分）抽象，这一事实在检查器的设计中有一定的意义。我们提供的充分条件，使我们能够确保：1）如果检查器成功验证证书，则证书对程序有效（正确性）; 2）检查器将成功验证任何有效的简化证书（完整性）。我们的方法已经在ciaopp系统中实现并进行了基准测试。实验结果表明，我们的方案在实践中能够大大减少证书的大小。
英文摘要：
Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The advantage of providing a (fixpoint) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certificate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certificate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certificate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker. Interestingly, the fact that the reduced certificate omits (parts of) the abstraction has implications in the design of the checker. We provide the sufficient conditions which allow us to ensure that 1) if the checker succeeds in validating the certificate, then the certificate is valid for the program (correctness) and 2) the checker will succeed for any reduced certificate which is valid (completeness). Our approach has been implemented and benchmarked within the ciaopp system. The experimental results show that our proposal is able to greatly reduce the size of certificates in practice.To appear in Theory and Practice of Logic Programming (TPLP).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
