Encoding the program correctness proofs as programs in PCC technology

被引：0
|
作者：
Pirzadeh, Heidar [1 ]
Dube, Danny [2 ]
机构：
[1] Univ Montreal, DIRO, CP 6128 Succ Ctr Ville, Montreal, PQ H3C 3J7, Canada
[2] Univ Laval, Dept Dinformatique genie logical, Quebec City, PQ G1K 7P4, Canada
来源：
SIXTH ANNUAL CONFERENCE ON PRIVACY, SECURITY AND TRUST, PROCEEDINGS | 2008年
基金：
加拿大自然科学与工程研究理事会;
关键词：
D O I：
10.1109/PST.2008.20
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
One of the key issues with the practical applicability of Proof-Carrying Code (PCC) and its related methods is the difficulty in communi. eating and storing the proofs which are inherently large. The approaches proposed to alleviate this, suffer from drawbacks of their own especially the enlargement of the Trusted Computing Base, in which any bug may cause an unsafe program to be accepted. We propose a generic extended PCC framework (EPCC) in which, instead of the proof a proof generator for the program in question is transmitted. This framework enables the execution of the proof generator and the recovery of the proof on the consumer side in a secure manner
引用
收藏
页码：121 / +
页数：2
相关论文
共 50 条
12345