Sciweavers

PST
2008

Encoding the Program Correctness Proofs as Programs in PCC Technology

14 years 1 months ago
Encoding the Program Correctness Proofs as Programs in PCC Technology
One of the key issues with the practical applicability of Proof-Carrying Code (PCC) and its related methods is the difficulty in communicating 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.
Heidar Pirzadeh, Danny Dubé
Added 30 Oct 2010
Updated 30 Oct 2010
Type Conference
Year 2008
Where PST
Authors Heidar Pirzadeh, Danny Dubé
Comments (0)