The Efficient Server Audit Problem, Deduplicated Re-execution, and the Web

ABSTRACT

You put a program on a concurrent server, but you don't trust the server; later, you get a trace of the actual requests that the server received from its clients and the responses that it delivered. You separately get logs from the server; these are untrusted. How can you use the logs to efficiently verify that the responses were derived from running the program on the requests? This is the Efficient Server Audit Problem, which abstracts real-world scenarios, including running a web application on an untrusted provider. We give a solution based on several new techniques, including simultaneous replay and efficient verification of concurrent executions. We implement the solution for PHP web applications. For several applications, our verifier achieves 5.6-10.9x speedup versus simply re-executing, with <10% overhead for the server.

References

1. Amazon Web Services (AWS). https://aws.amazon.com/.
2. CentOS forum. https://www.centos.org/forums/.
3. LAMP (software bundle). https://en.wikipedia.org/wiki/LAMP_(software_bundle).
4. PHP manual. http://php.net/manual/en/index.php.
5. SIMD. https://en.wikipedia.org/wiki/SIMD.
6. Transaction isolation levels. https://dev.mysql.com/doc/refman/5.6/en/innodb-transaction-isolation-levels.html.
7. A virtual machine designed for executing programs written in Hack and PHP. https://github.com/facebook/hhvm.
8. The process of ACM Sigcomm 2009. http//:www.sigcomm.org/conference-planning/the-process-of-acm-sigcomm-2009.
9. J. Alglave, D. Kroening, V. Nimal, and D. Poetzl. Don't sit on the fence: A static analysis approach to automatic fence insertion. In Computer Aided Verification (CAV), July 2014.
10. J. Alglave and L. Maranget. Stability in weak memory models. In Computer Aided Verification (CAV), July 2011.
11. G. Altekar and I. Stoica. ODR: output-deterministic replay for multicore debugging. In ACM Symposium on Operating Systems Principles (SOSP), Oct. 2009.
12. S. Ames, C. Hazay, Y. Ishai, and M. Venkitasubramaniam. Ligero: Lightweight sublinear arguments without a trusted setup. In ACM Conference on Computer and Communications Security (CCS), Oct. 2017.
13. E. Anderson, X. Li, M. A. Shah, J. Tucek, and J. J. Wylie. What consistency does your key-value store actually provide? In USENIX Workshop on Hot Topics in System Dependability (HotDep), Oct. 2010. Full version: Technical Report HPL-2010-98, Hewlett-Packard Laboratories, 2010.
14. S. Arnautov, B. Trach, F. Gregor, T. Knauth, A. Martin, C. Priebe, J. Lind, D. Muthukumaran, D. O'Keeffe, M. L. Stillwell, D. Goltzsche, D. Eyers, R. Kapitza, P. Pietzuch, and C. Fetzer. SCONE: Secure Linux containers with Intel SGX. In Symposium on Operating Systems Design and Implementation (OSDI), Nov. 2016.
15. L. Babai, L. Fortnow, L. A. Levin, and M. Szegedy. Checking computations in polylogarithmic time. In ACM Symposium on the Theory of Computing (STOC), May 1991.
16. P. Bailis. Linearizability versus serializability. http//:www.bailis.org/blog/linearizability-versus-serializability/, Sept. 2014.
17. A. Baumann, M. Peinado, and G. Hunt. Shielding applications from an untrusted cloud with Haven. In Symposium on Operating Systems Design and Implementation (OSDI), Oct. 2014.
18. E. Ben-Sasson, I. Ben-Tov, A. Chiesa, A. Gabizon, D. Genkin, M. Hamilis, E. Pergament, M. Riabzev, M. Silberstein, E. Tromer, and M. Virza. Computational integrity with a public random string from quasi-linear PCPs. In Annual International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT), Apr. 2017.
19. E. Ben-Sasson, A. Chiesa, D. Genkin, E. Tromer, and M. Virza. SNARKs for C: Verifying program executions succinctly and in zero knowledge. In IACR International Cryptology Conference (CRYPTO), Aug. 2013.
20. E. Ben-Sasson, A. Chiesa, E. Tromer, and M. Virza. Succinct non-interactive zero knowledge for a von Neumann architecture. In USENIX Security, Aug. 2014.
21. P. A. Bernstein, D. W. Shipman, and W. S. Wong. Formal aspects of serializability in database concurrency control. IEEE Transactions on Software Engineering, SE-5(3), May 1979.
22. P. Bhatotia, P. Fonseca, U. A. Acar, B. B. Brandenburg, and R. Rodrigues. iThreads: A threading library for parallel incremental computation. In ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Mar. 2015.
23. B. Braun, A. J. Feldman, Z. Ren, S. Setty, A. J. Blumberg, and M. Walfish. Verifying computations with state. In ACM Symposium on Operating Systems Principles (SOSP), Nov. 2013.
24. T. C. Bressoud and F. B. Schneider. Hypervisor-based fault-tolerance. ACM Transactions on Computer Systems (TOCS), 14(1):80--107, 1996.
25. M. Castro and B. Liskov. Practical Byzantine fault tolerance and proactive recovery. ACM Transactions on Computer Systems (TOCS), 20(4):398--461, 2002.
26. R. Chandra, T. Kim, M. Shah, N. Narula, and N. Zeldovich. Intrusion recovery for database-backed web applications. In ACM Symposium on Operating Systems Principles (SOSP), Oct. 2011.
27. C. Chen, P. Maniatis, A. Perrig, A. Vasudevan, and V. Sekar. Towards verifiable resource accounting for outsourced computation. In ACM Virtual Execution Environments (VEE), Mar. 2013.
28. X. Chen, T. Garfinkel, E. C. Lewis, P. Subrahmanyam, C. A. Waldspurger, D. Boneh, J. Dwoskin, and D. R. K. Ports. Overshadow: a virtualization-based approach to retrofitting protection in commodity operating systems. ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Mar. 2008.
29. Y. Chen and H. Chen. Scalable deterministic replay in a parallel full-system emulator. In ACM Symposium on Principles and Practice of Parallel Programming (PPoPP), Feb. 2013.
30. J. Cheng. NebuAd, ISPs sued over DPI snooping, ad-targeting program. Ars Technica, Nov. 2008. https://arstechnica.com/tech-policy/2008/11/nebuad-isps-sued-over-dpi-snooping-ad-targeting-program/.
31. T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms, third edition. The MIT Press, Cambridge, MA, 2009.
32. G. Cormode, M. Mitzenmacher, and J. Thaler. Practical verified computation with streaming interactive proofs. In Innovations in Theoretical Computer Science (ITCS), Jan. 2012.
33. F. Cornelis, A. Georges, M. Christiaens, M. Ronsse, T. Ghesquiere, and K. D. Bosschere. A taxonomy of execution replay systems. In International Conference on Advances in Infrastructure for Electronic Business, Education, Science, Medicine, and Mobile Technologies on the Internet, 2003.
34. C. Dionne, M. Feeley, and J. Desbiens. A taxonomy of distributed debuggers based on execution replay. In Proceedings of the International Conference on Parallel and Distributed Processing Techniques (PDPTA), Aug. 1996.
35. G. W. Dunlap, S. T. King, S. Cinar, M. A. Basrai, and P. M. Chen. ReVirt: Enabling intrusion analysis through virtual-machine logging and replay. In Symposium on Operating Systems Design and Implementation (OSDI), Dec. 2002.
36. G. W. Dunlap, D. Lucchetti, P. M. Chen, and M. Fetterman. Execution replay for multiprocessor virtual machines. In ACM Virtual Execution Environments (VEE), Mar. 2008.
37. R. Gennaro, C. Gentry, and B. Parno. Non-interactive verifiable computing: Outsourcing computation to untrusted workers. In IACR International Cryptology Conference (CRYPTO), Aug. 2010.
38. R. Gennaro, C. Gentry, B. Parno, and M. Raykova. Quadratic span programs and succinct NIZKs without PCPs. In Annual International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT), May 2013.
39. P. B. Gibbons and E. Korach. Testing shared memories. SIAM Journal on Computing, 26(4):1208--1244, 1997.
40. A. Goel, K. Farhadi, K. Po, and W. Feng. Reconstructing system state for intrusion analysis. ACM SIGOPS Operating Systems Review, 42(3):21--28, Apr. 2008.
41. W. Golab, X. Li, and M. Shah. Analyzing consistency properties for fun and profit. In PODC, June 2011.
42. S. Goldwasser, Y. T. Kalai, and G. N. Rothblum. Delegating computation: Interactive proofs for muggles. Journal of the ACM, 62(4):27:1--27:64, Aug. 2015. Prelim version STOC 2008.
43. A. Haeberlen, P. Aditya, R. Rodrigues, and P. Druschel. Accountable virtual machines. In Symposium on Operating Systems Design and Implementation (OSDI), Oct. 2010.
44. C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad apps: End-to-end security via automated full-system verification. In Symposium on Operating Systems Design and Implementation (OSDI), Oct. 2014.
45. M. P. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems (TOPLAS), 12(3), July 1990.
46. O. S. Hofmann, S. Kim, A. M. Dunn, M. Z. Lee, and E. Witchel. InkTag: secure applications on an untrusted operating system. ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 265--278, Mar. 2013.
47. J. Huang, P. Liu, and C. Zhang. LEAP: The lightweight deterministic multi-processor replay of concurrent Java programs. In ACM Symposium on the Foundations of Software Engineering (FSE), Feb. 2010.
48. T. Hunt, Z. Zhu, Y. Xu, S. Peter, and E. Witchel. Ryoan: A distributed sandbox for untrusted computation on secret data. In Symposium on Operating Systems Design and Implementation (OSDI), Nov. 2016.
49. Intel. Intel software guard extensions programming reference. https://software.intel.com/sites/default/files/managed/48/88/329298-002.pdf.
50. S. Jana and V. Shmatikov. EVE: Verifying correct execution of cloud-hosted web applications. In USENIX HotCloud Workshop, June 2011.
51. N. Karapanos, A. Filios, R. A. Popa, and S. Capkun. Verena: End-to-end integrity protection for web applications. In IEEE Symposium on Security and Privacy, May 2016.
52. T. Kim, R. Chandra, and N. Zeldovich. Efficient patch-based auditing for web applications. In Symposium on Operating Systems Design and Implementation (OSDI), Oct. 2012.
53. O. Laadan, N. Viennot, and J. Nieh. Transparent, lightweight application execution replay on commodity multiprocessor operating systems. In SIGMETRICS, June 2010.
54. L. Lamport. On interprocess communication, parts I and II. Distributed Computing, 1(2):77--101, 1986.
55. T. J. LeBlanc and J. M. Mellor-Crummey. Debugging parallel programs with Instant Replay. IEEE Transactions on Computers, C-36(4):471--482, 1987.
56. D. Lee, B. Wester, K. Veeraraghavan, S. Narayanasamy, P. M. Chen, and J. Flinn. Respec: Efficient online multiprocessor replay via speculation and external determinism. In ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Mar. 2010.
57. M. Maurer and D. Brumley. Tachyon: tandem execution for efficient live patch testing. USENIX Security, pages 617--630, Aug. 2012.
58. J. M. McCune, Y. Li, N. Qu, Z. Zhou, A. Datta, V. Gligor, and A. Perrig. TrustVisor: Efficient TCB reduction and attestation. In IEEE Symposium on Security and Privacy, May 2010.
59. J. M. McCune, B. J. Parno, A. Perrig, M. K. Reiter, and H. Isozaki. Flicker: An execution infrastructure for TCB minimization. In European Conference on Computer Systems (EuroSys), Apr. 2008.
60. S. Micali. Computationally sound proofs. SIAM Journal on Computing, 30(4):1253--1298, 2000.
61. Oracle flashback technology. http//:www.oracle.com/technetwork/database/features/availability/flashback-overview-082751.html.
62. C. H. Papadimitriou. The serializability of concurrent database updates. Journal of the ACM, 26(4), Oct. 1979.
63. D. Papagiannaki and L. Rizzio. The ACM SIGCOMM 2009 Technical Program Committee Process. ACM CCR, 39(3):43--48, July 2009.
64. S. Park, Y. Zhou, W. Xiong, Z. Yin, R. Kaushik, K. H. Lee, and S. Lu. PRES: probabilistic replay with execution sketching on multiprocessors. In ACM Symposium on Operating Systems Principles (SOSP), Oct. 2009.
65. B. Parno, C. Gentry, J. Howell, and M. Raykova. Pinocchio: Nearly practical verifiable computation. In IEEE Symposium on Security and Privacy, May 2013.
66. B. Parno, J. M. McCune, and A. Perrig. Bootstrapping Trust in Modern Computers. Springer, 2011.
67. B. Parno, J. M. McCune, D. Wendlandt, D. G. Andersen, and A. Perrig. CLAMP: Practical prevention of large-scale data leaks. In IEEE Symposium on Security and Privacy, May 2009.
68. R. A. Popa, C. Redfield, N. Zeldovich, and H. Balakrishnan. CryptDB: protecting confidentiality with encrypted query processing. In ACM Symposium on Operating Systems Principles (SOSP), Oct. 2011.
69. C. Reis, S. D. Gribble, T. Kohno, and N. C. Weaver. Detecting in-flight page changes with Web Tripwires. In Symposium on Networked Systems Design and Implementation (NSDI), Apr. 2008.
70. M. Ronsse and K. D. Bosschere. RecPlay: a fully integrated practical record/replay system. ACM Transactions on Computer Systems (TOCS), 17(2):133--152, 1999.
71. R. Sailer, X. Zhang, T. Jaeger, and L. van Doorn. Design and implementation of a TCG-based integrity measurement architecture. In USENIX Security, Aug. 2004.
72. D. Schultz and B. Liskov. Ifdb: decentralized information flow control for databases. In European Conference on Computer Systems (EuroSys), Apr. 2013.
73. F. Schuster, M. Costa, C. Fournet, C. Gkantsidis, M. Peinado, G. Mainar-Ruiz, and M. Russinovich. VC3: Trustworthy data analytics in the cloud using SGX. In IEEE Symposium on Security and Privacy, May 2015.
74. A. Seshadri, M. Luk, E. Shi, A. Perrig, L. van Doorn, and P. Khosla. Pioneer: Verifying integrity and guaranteeing execution of code on legacy platforms. In ACM Symposium on Operating Systems Principles (SOSP), Oct. 2005.
75. S. Setty, R. McPherson, A. J. Blumberg, and M. Walfish. Making argument systems for outsourced computation practical (sometimes). In Network and Distributed System Security Symposium (NDSS), Feb. 2012.
76. D. Shasha and M. Snir. Efficient and correct execution of parallel programs that share memory. ACM Transactions on Programming Languages and Systems (TOPLAS), 10(2):282--312, Apr. 1988.
77. S. Shinde, D. Le Tien, S. Tople, and P. Saxena. Panoply: Low-tcb linux applications with sgx enclaves. In Network and Distributed System Security Symposium (NDSS), Feb. 2017.
78. R. Sinha, M. Costa, A. Lal, N. P. Lopes, S. Rajamani, S. A. Seshia, and K. Vaswani. A design and verification methodology for secure isolated regions. June 2016.
79. E. G. Sirer, W. de Bruijn, P. Reynolds, A. Shieh, K. Walsh, D. Williams, and F. B. Schneider. Logical attestation: An authorization architecture for trustworthy computing. In ACM Symposium on Operating Systems Principles (SOSP), Oct. 2011.
80. R. T. Snodgrass and I. Ahn. Temporal databases. IEEE Computer, 19(9):35--42, Sept. 1986.
81. C. Tan, L. Yu, J. B. Leners, and M. Walfish. The efficient server audit problem, deduplicated re-execution, and the web (extended version). arXiv:1709.08501, http://arxiv.org/abs/1709.08501, Sept. 2017.
82. Y. Tang and J. Yang. Secure deduplication of general computations. In USENIX Annual Technical Conference, July 2015.
83. H.-W. Tseng and D. M. Tullsen. Data-triggered threads: Eliminating redundant computation. In IEEE International Symposium on High Performance Computer Architecture (HPCA), Feb. 2011.
84. J. Tucek, W. Xiong, and Y. Zhou. Efficient online validation with delta execution. In ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Mar. 2009.
85. G. Urdaneta, G. Pierre, and M. Van Steen. Wikipedia workload analysis for decentralized hosting. Computer Networks, 53(11):1830--1845, 2009.
86. K. Veeraraghavan, D. Lee, B. Wester, J. Ouyang, P. M. Chen, J. Flinn, and S. Narayanasamy. DoublePlay: Parallelizing sequential logging and replay. ACM Transactions on Computer Systems (TOCS), 30(1):3, 2012.
87. K. Vikram, A. Prateek, and B. Livshits. Ripley: Automatically securing web 2.0 applications through replicated execution. In ACM Conference on Computer and Communications Security (CCS), Nov. 2009.
88. R. S. Wahby, Y. Ji, A. J. Blumberg, abhi shelat, J. Thaler, M. Walfish, and T. Wies. Full accounting for verifiable outsourcing. In ACM Conference on Computer and Communications Security (CCS), Oct. 2017.
89. M. Walfish and A. J. Blumberg. Verifying computations without reexecuting them: from theoretical possibility to near practicality. Communications of the ACM (CACM), 58(2):74--84, Feb. 2015.
90. J. M. Wing and C. Gong. Testing and verifying concurrent objects. Journal of Parallel and Distributed Computing, 17:164--182, 1993.
91. R. Wray. BT drops plan to use Phorm targeted ad service after outcry over privacy. The Guardian, July 2009. https://www.theguardian.com/business/2009/jul/06/btgroup-privacy-and-the-net.
92. Z. Yang, M. Yang, L. Xu, H. Chen, and B. Zang. ORDER: Object centRic DEterministic Replay for Java. In USENIX Annual Technical Conference, June 2011.
93. A. Yip, X. Wang, N. Zeldovich, and M. F. Kaashoek. Improving application security with data flow assertions. In ACM Symposium on Operating Systems Principles (SOSP), Oct. 2009.
94. C. Zamfir, G. Altekar, and I. Stoica. Automating the debugging of datacenter applications with ADDA. In Dependable Systems and Networks (DSN), June 2013.
95. F. Zhang, J. Chen, H. Chen, and B. Zang. Cloudvisor: retrofitting protection of virtual machines in multi-tenant cloud with nested virtualization. In ACM Symposium on Operating Systems Principles (SOSP), Oct. 2011.
96. Y. Zhang, D. Genkin, J. Katz, D. Papadopoulos, and C. Papamanthou. vSQL: Verifying arbitrary SQL queries over dynamic outsourced databases. In IEEE Symposium on Security and Privacy, May 2017.