Verifying computations without reexecuting them

Abstract

From theoretical possibility to near practicality.

References

1. Arora, S., Lund, C., Motwani, R., Sudan, M. and Szegedy, M. Proof verification and the hardness of approximation problems. JACM 45, 3 (May 1998), 501--555, (Prelim. version FOCS 1992).
2. Arora, S. and Safra, S. Probabilistic checking of proofs: A new characterization of NP. JACM 45, 1 (Jan. 1998), 70--122. (Prelim. version FOCS 1992).
3. Babai, L. Trading group theory for randomness. In Proceedings of STOC, 1985.
4. Babai, L., Fortnow, L., Levin, A. and Szegedy, M. Checking computations in polylogarithmic time. In Proceedings of STOC, 1991.
5. Ben-Sasson, E. et al. Decentralized anonymous payments from Bitcoin. IEEE Symposium on Security and Privacy, 2014.
6. Ben-Sasson, E., Chiesa, A., Genkin, D. and Tromer, E. Fast reductions from RAMs to delegatable succinct constraint satisfaction problems. In Proceedings of ITCS, Jan. 2013.
7. Ben-Sasson, E., Chiesa, A., Genkin, D. and Tromer, E. SNARKs for C: Verifying program executions succinctly and in zero knowledge. In Proceedings of CRYPTO, Aug. 2013.
8. Ben-Sasson, E., Chiesa, A., Tromer, E. and Virza, M. Scalable zero knowledge via cycles of elliptic curves. In Proceedings of CRYPTO, Aug. 2014.
9. Ben-Sasson, E., Chiesa, A., Tromer, E. and Virza, M. Succinct non-interactive zero knowledge for a von Neumann architecture. USENIX Security, (Aug. 2014).
10. Ben-Sasson, E., Goldreich, O., Harsha, P., Sudan, M. and S. Vadhan, S. Robust PCPs of proximity, shorter PCPs and applications to coding. SIAM J. on Comp. 36, 4 (Dec. 2006), 889--974.
11. Bitansky, N., Canetti, R., Chiesa, A. and Tromer, E. Recursive composition and bootstrapping for SNARKs and proof-carrying data. In Proceedings of STOC, June 2013.
12. Bitansky, N., Chiesa, A., Ishai, Y., Ostrovsky, R. and Paneth, O. Succinct non-interactive arguments via linear interactive proofs. In Proceedings of IACR TCC, Mar. 2013.
13. Brassard, G., Chaum, D. and Crépeau, C. Minimum disclosure proofs of knowledge. J. Comp. and Sys. Sciences 37, 2 (Oct. 1988), 156--189.
14. Braun, B., Feldman, A.J., Ren, Z., Setty, S., Blumberg, A.J., and Walfish, M. Verifying computations with state. In Proceedings of SOSP, Nov. 2013.
15. Canetti, R., Riva, B. and Rothblum, G. Practical delegation of computation using multiple servers. ACM CCS, 2011.
16. Castro, M. and Liskov, B. Practical Byzantine fault tolerance and proactive recovery. ACM Trans. on Comp. Sys. 20, 4 (Nov. 2002), 398--461.
17. Chung, K.M., Kalai, Y. and Vadhan, S. Improved delegation of computation using fully homomorphic encryption. In Proceedings of CRYPTO, 2010.
18. Cormode, G., Mitzenmacher, M. and Thaler, J. Practical verified computation with streaming interactive proofs. In Proceedings of ITCS, 2012.
19. Danezis, G., Fournet, C., Kohlweiss, M. and Parno, B. Pinocchio coin: Building zerocoin from a succinct pairing-based proof system. In Proceedings of the Workshop on Language Support for Privacy-enhancing Technologies, Nov. 2013.
20. Dinur. I. The PCP theorem by gap amplification. JACM 54, 3 (June 2007), 2:1--12:44.
21. Gennaro, R., Gentry, C. and Parno, B. Non-interactive verifiable computing: Outsourcing computation to untrusted workers. In Proceedings of CRYPTO, 2010.
22. Gennaro, R., Gentry, C. and Parno, B. and Raykova, M. Quadratic span programs and succinct NIZKs without PCPs. In Proceedings of EUROCRYPT, May 2013.
23. Gentry, C. A fully homomorphic encryption scheme. PhD thesis, Stanford University, 2009.
24. Goldreich, O. Probabilistic proof systems---A primer. Foundations and Trends in Theoretical Computer Science 3, 1 (2007), 1--91.
25. Goldwasser, S., Kalai, Y.T. and Rothblum, G.N. Delegating computation: Interactive proofs for muggles. In Proceedings of STOC, May 2008.
26. Goldwasser, S., Micali, S. and Rackoff, C. The knowledge complexity of interactive proof systems. SIAM J. on Comp. 18, 1 (1989), 186--208.
27. Håstad, J. Some optimal inapproximability results. JACM 48, 4 (July 2001), 798--859. (Prelim. version STOC 1997).
28. Huang, Y., Evans, D., Katz, J. and Malka, L. Faster secure two-party computation using garbled circuits. In USENIX Security, 2011.
29. Ishai, Y., Kushilevitz, E., and Ostrovsky, R. Efficient arguments without short PCPs. In Proceedings of the Conference on Computational Complexity (CCC), 2007.
30. Kilian, J. A note on efficient zero-knowledge proofs and arguments (extended abstract). In Proceedings of STOC, 1992.
31. Kreuter, B., shelat, a. and Shen, C.H. Billion-gate secure computation with malicious adversaries. USENIX Security (Aug. 2012).
32. Lund, C., Fortnow, L., Karloff, H.J., and Nisan, N. Algebraic methods for interactive proof systems. JACM 39, 4 (1992), 859--868.
33. Mahajan, P. et al. Depot: Cloud storage with minimal trust. ACM Trans. on Comp. Sys. 29, 4 (Dec. 2011).
34. Malkhi, D. and Reiter, M. Byzantine quorum systems. Distributed Computing 11, 4 (Oct. 1998), 203--213. (Prelim. version Proceedings of STOC 1997).
35. Narayan, A. and Haeberlen, A. DJoin: Differentially private join queries over distributed databases. In Proceedings of OSDI, 2012.
36. Parno, B., Gentry, C., Howell, J. and Raykova, M. Pinocchio: Nearly practical verifiable computation. IEEE Symposium on Security and Privacy, (May 2013).
37. Parno, B., McCune, J.M. and Perrig, A. Bootstrapping Trust in Modern Computers. Springer, 2011.
38. Popa, R.A., Redfield, C.M.S., Zeldovich, N. and Balakrishnan, H. CryptDB: Protecting confidentiality with encrypted query processing. In Proceedings of SOSP, 2011.
39. Sadeghi, A.R., Schneider, T., and Winandy, M. Token-based cloud computing: Secure outsourcing of data and arbitrary computations with lower latency. In Proceedings of TRUST, 2010.
40. Setty, S., Blumberg, A.J. and Walfish, M. Toward practical and unconditional verification of remote computations. In Proceedings of HotOS, May 2011.
41. Setty, S., Braun, B., Vu, V., Blumberg, A.J., Parno, B. and Walfish, M. Resolving the conflict between generality and plausibility in verified computation. In Proceedings of EuroSys, Apr. 2013.
42. Setty, S., McPherson, R., Blumberg, A.J., and Walfish, M. Making argument systems for outsourced computation practical (sometimes). In Proceedings of NDSS, 2012.
43. Setty, S., Vu, V., Panpalia, N., Braun, B., Blumberg, A.J. and Walfish, M. Taking proof-based verified computation a few steps closer to practicality. USENIX Security, Aug. 2012.
44. Sudan, M. Probabilistically checkable proofs. Commun. ACM 52, 3 (Mar. 2009), 76--84.
45. Thaler, J. Time-optimal interactive proofs for circuit evaluation. In Proceedings of CRYPTO, Aug. 2013.
46. Thaler, J., Roberts, M., Mitzenmacher, M. and Pfister, H. Verifiable computation with massively parallel interactive proofs. In Proceedings of USENIX HotCloud Workshop, (June 2012).
47. Vu, V., Setty, S., Blumberg, A.J. and Walfish, M. A hybrid architecture for interactive verifiable computation. IEEE Symposium on Security and Privacy, (May 2013).
48. Wahby, R.S., Setty, S., Ren, Z., Blumberg, A.J. and Walfish, M. Efficient RAM and control flow in verifiable outsourced computation. In Proceedings of NDSS, Feb. 2015.
49. Wolinsky, D.I., Corrigan-Gibbs, H., Ford, B. and Johnson, A. Dissent in numbers: Making strong anonymity scale. In Proceedings of OSDI, 2012.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Information systems

  • Information systems applications

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program verification