...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Automated software engineering >Interactive and Probabilistic Proof of Mobile Code Safety
【24h】

Interactive and Probabilistic Proof of Mobile Code Safety

机译：移动代码安全性的交互式和概率证明

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This paper proposes a new proof-based approach to safe evolution of distributed software systems. Specifically, it extends the simple certification mechanism of proof-carrying code (PCC) to make it interactive and probabilistic, thereby devising interactive proof-carrying code (iPCC). With iPCC, a code consumer is convinced, with overwhelming probability, of the existence and validity of a safety proof of a transmitted code through interaction with a code producer. The iPCC mechanism theoretically solves the problem of proof explosion with PCC and can be used to efficiently prove a greater variety of safety properties that may require longer proofs. Technically, the class (PSPACE) of safety properties that are efficiently provable by iPCC is larger than the class (NP) efficiently provable by PCC. To illustrate the power of iPCC, this paper demonstrates that the verification of certain basic safety properties of typical machine instruction codes needs co-NP-complete computation, and shows how these safety properties can be efficiently verified by the iPCC mechanism.
机译：本文提出了一种基于证明的新方法来安全地开发分布式软件系统。具体来说，它扩展了携带证明代码（PCC）的简单认证机制，使其具有交互性和概率性，从而设计了交互式携带证明代码（iPCC）。使用iPCC，代码使用者可以通过与代码生成者的交互以极大的可能性确信所传输代码的安全性证明的存在和有效性。 iPCC机制从理论上解决了PCC的证明爆炸问题，可用于有效证明可能需要更长证明的各种安全特性。从技术上讲，iPCC可有效证明的安全性等级（PSPACE）大于PCC可有效证明的等级（NP）。为了说明iPCC的功能，本文证明了对典型机器指令代码的某些基本安全属性的验证需要进行NP完整计算，并说明如何通过iPCC机制有效地验证这些安全属性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号