PinocchioQ
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.
Authors
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
Last update: Sep. 28th 2019