Return to search

Encoding the program correctness proofs as programs in PCC technology

L'une des difficultés de l'application pratique du code incorporant une preuve (Proof-Carrying Code (PCC)) est la difficulté de communiquer les preuves car celles-ci sont généralement d'une taille importante.
Les approches proposées pour atténuer ce problème engendrent de nouveaux problèmes, notamment celui de l'élargissement de la base de confiance (Trusted Computing Base): un bogue peut alors provoquer l'acceptation d'un programme malicieux.
Au lieu de transmettre une preuve avec le code, nous proposons de transmettre un générateur de preuve dans un cadre générique et étendu de PCC (EPCC) (Extended Proof-Carrying Code). Un générateur est un programme dont la seule fonction est de produire une preuve; c'est-à-dire la preuve que le code qu'elle accompagne est correct. Le générateur a pour but principal d'être une représentation plus compacte de la preuve qu'il sert à générer.
Le cadre de EPCC permet l'exécution du générateur de preuve du côté client d'une manière sécurisée. / One of the key issues with the practical applicability of Proof-Carrying Code (PCC) and its related
methods is the difficulty in communicating the proofs which are inherently large.
The approaches proposed to alleviate this, suffer with 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 to transmit, instead, a proof generator for the program in question in a generic extended
PCC framework (EPCC).
A proof generator aims to be a more compact representation of its resulting proof.
The EPCC framework enables the execution of the proof generator at the consumer side in a
secure manner.

Identiferoai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2008/25562
Date08 1900
CreatorsPirzadeh Tabari, Seyed Heidar
ContributorsDubé, Danny
PublisherUniversité Laval
Source SetsLibrary and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada
LanguageEnglish
Detected LanguageFrench
TypeElectronic Thesis or Dissertation
Formattext/html, application/pdf
Rights© Seyed Heidar Pirzadeh Tabari, 2008

Page generated in 0.0014 seconds