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
相关论文
共 34 条
  • [1] [Anonymous], 1985, DEP DEF TRUST COMP S
  • [2] Foundational proof-carrying code
    Appel, AW
    [J]. 16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2001, : 247 - 256
  • [3] Appel AW, 1999, 6TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, P52, DOI 10.1145/319709.319718
  • [4] APPEL AW, 2002, CSTR64702 PRINC U
  • [5] BINDER RV, 1997, 6 SIGMA HARDWARE SI
  • [6] *CA INC, 2008, 2008 INT SEC OUTL RE
  • [7] CHENEY J, 1998, 1 ORDER TERM COMPRES
  • [8] COLBY C, 2000, P 2000 ACM C PROG LA, P95
  • [9] Effect of the web on undergraduate citation behavior: Guiding student scholarship in a networked age
    Davis, PM
    [J]. PORTAL-LIBRARIES AND THE ACADEMY, 2003, 3 (01) : 41 - 51
  • [10] Deutsch L. P., 1996, GZIP file format specification version 4.3
1234