PinocchioQ is a certified compiler for verifiable computation.

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.

Based on CompCert and developed in Coq, PinocchioQ targets an architecture whose instructions consist solely of quadratic equations over a large finite field, amenable to succinct verification using the Pinocchio cryptographic scheme.


This is joint work with Cédric Fournet and Vincent Laporte.

Companion paper

This work has been published at the IEEE Computer Security Foundations Symposium in 2016:
      A Certified Compiler for Verifiable Computing, with Cédric Fournet and Vincent Laporte, CSF - 29th IEEE Computer Security Foundations Symposium - 2016. PDF, BIBTEX
Home Research Studies Teaching Miscellaneous

Last update: Sep. 28th 2019