Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Chantal Keller Connect in order to contact the contributor
Submitted on : Wednesday, November 23, 2016 - 10:55:10 AM
Last modification on : Friday, November 18, 2022 - 9:24:21 AM
Long-term archiving on: : Thursday, March 16, 2017 - 5:09:55 PM


Files produced by the author(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. ⟨hal-01397680⟩



Record views


Files downloads