A Certified Compiler for Verifiable Computing

Abstract : In cryptology, verifiable computing aims at verifying the remote execution of a program on an untrusted machine, based on its I/O and constant-sized evidence collected during its execution. Recent cryptographic schemes and compilers enable practical verifiable computations for some programs written in C, but their soundness with regards to C semantics remains informal and poorly understood. We present the first certified, semantics-preserving compiler for verifiable computing. Based on CompCert and developed in Coq, our compiler targets an architecture whose instructions consist solely of quadratic equations over a large finite field, amenable to succinct verification using the Pinocchio cryptographic scheme. We explain how to encode the integer operations of a C program first to quadratic equations, then to a single cryptographically-checkable polynomial test. We formally prove that, when compilation succeeds, there is a correct execution of the source program for any I/O that pass this test. We link our compiler to the Pinocchio cryptographic runtime, and report experimental results as we compile, run, and verify the execution of sample C programs.
Type de document :
Communication dans un congrès
IEEE 29th Computer Security Foundations Symposium, CSF 2016, Jun 2016, Lisbonne, Portugal. 2016
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

Contributeur : Chantal Keller <>
Soumis le : mercredi 23 novembre 2016 - 10:55:10
Dernière modification le : vendredi 11 janvier 2019 - 14:25:14
Document(s) archivé(s) le : jeudi 16 mars 2017 - 17:09:55


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01397680, version 1


Cédric Fournet, Chantal Keller, Vincent Laporte. A Certified Compiler for Verifiable Computing. IEEE 29th Computer Security Foundations Symposium, CSF 2016, Jun 2016, Lisbonne, Portugal. 2016. 〈hal-01397680〉



Consultations de la notice


Téléchargements de fichiers