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:LAVAL/oai:corpus.ulaval.ca:20.500.11794/25555
Date20 April 2018
CreatorsPirzadeh Tabari, Seyed Heidar
ContributorsDubé, Danny
Source SetsUniversité Laval
LanguageEnglish
Detected LanguageFrench
Typemémoire de maîtrise, COAR1_1::Texte::Thèse::Mémoire de maîtrise
Format1 ressource en ligne (x, 89 pages), application/pdf
Rightshttp://purl.org/coar/access_right/c_abf2

Page generated in 0.0023 seconds