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 metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01397680
Contributor : Chantal Keller <>
Submitted on : Wednesday, November 23, 2016 - 10:55:10 AM
Last modification on : Thursday, February 7, 2019 - 2:59:42 PM
Long-term archiving on : Thursday, March 16, 2017 - 5:09:55 PM

File

csf16.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-01397680⟩

Share

Metrics

Record views

729

Files downloads

606