A Certified Compiler for Verifiable Computing

Cédric Fournet 1 Chantal Keller 2 Vincent Laporte 3, 4
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
3 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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

https://hal.inria.fr/hal-01397680
Contributeur : Chantal Keller <>
Soumis le : mercredi 23 novembre 2016 - 10:55:10
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : jeudi 16 mars 2017 - 17:09:55

Fichier

csf16.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01397680, version 1

Citation

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〉

Partager

Métriques

Consultations de la notice

471

Téléchargements de fichiers

307