Microsoft proves Pinocchio's a real boy with proofs tool
'Geppetto' gives verifiable computation a boost
Microsoft cloud wonks have developed a tool for developers capable of practical generation of proofs that an outsourced job has been crunched securely.
The team of eight including Craig Costello; Cedric Fournet; Jon Howell; Markulf Kohlweiss ; Michael Naehrig, and Bryan Parno together with University of Virginia boffins Benjamin Kreuter and Samee Zahur produced "Geppetto", a tool that nails Verifiable Computation, a technique that allows computation jobs to be securely outsourced from weak to strong clients, while zero proofs verify the work without knowing that machine's inputs.
An hypothetical example advanced in a Geppetto: Versatile Verifiable Computation (paper (PDF) ) describing the tool describes a patient seeking to ensure the US Federal Drug Administration really did sign a given chunk of medical data analysis, and that the analysis was correctly applied to the patient’s data, without knowledge leaking out about the proprietary algorithm used.
Alternative systems can do the job, the team says, but are far from practical, costing up to three to six orders of magnitude more to generate a proof than that of the original computation. Two of these are based on the Pinocchio protocol for cryptographic back end work which itself relies on the Quadratic Algorithmic Programs.
Geppetto uses tricks capable of substantially reducing the overheads while increasing flexibility on provers, the authors say in the paper. Here's how it happens:
With Multi-QAPs, Geppetto reduces the cost of sharing state between computations (e.g., for MapReduce) or within a single computation by up to two orders of magnitude.
Via a careful choice of cryptographic primitives, Geppetto’s instantiation of bounded proof bootstrapping improves on prior bootstrapped systems by up to five orders of magnitude, albeit at some cost in universality.
Geppetto also efficiently verifies the correct execution of proprietary (i.e., secret) algorithms. Finally, Geppetto’s use of energy- saving circuits brings the prover’s costs more in line with the program’s actual (rather than worst-case) execution time.
The team says the platform's interlocked overhead-shattering techniques include a new techniques including 'Multi- QAPs' for sharing state between or within computations, and a method of energy-saving circuits that means the prover’s costs grow with actual rather than worst-case execution times. ®