{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:19:47Z","timestamp":1783009187722,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":74,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,13]],"date-time":"2022-11-13T00:00:00Z","timestamp":1668297600000},"content-version":"vor","delay-in-days":366,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA","award":["HR001120C0087"],"award-info":[{"award-number":["HR001120C0087"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,12]]},"DOI":"10.1145\/3460120.3484795","type":"proceedings-article","created":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T12:05:34Z","timestamp":1636805134000},"page":"2951-2967","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Zero Knowledge Static Program Analysis"],"prefix":"10.1145","author":[{"given":"Zhiyong","family":"Fang","sequence":"first","affiliation":[{"name":"Texas A&M University, College Station, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Darais","sequence":"additional","affiliation":[{"name":"Galois, Inc, Portland, OR, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joseph P.","family":"Near","sequence":"additional","affiliation":[{"name":"University of Vermont, Burlington, VT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yupeng","family":"Zhang","sequence":"additional","affiliation":[{"name":"Texas A&M University, College Station, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,11,13]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"[n.d.]. Buffet. https:\/\/github.com\/pepper-project\/releases."},{"key":"e_1_3_2_2_2_1","unstructured":"[n.d.]. California Consumer Privacy Act (CCPA). https:\/\/oag.ca.gov\/privacy\/ccpa."},{"key":"e_1_3_2_2_3_1","unstructured":"[n.d.]. Children's Online Privacy Protection Rule (\"COPPA\"). https:\/\/www.ftc.gov\/enforcement\/rules\/rulemaking-regulatory-reform-proceedings\/childrens-online-privacy-protection-rule."},{"key":"e_1_3_2_2_4_1","unstructured":"[n.d.]. DroidBench 2.0. https:\/\/github.com\/secure-software-engineering\/DroidBench. Accessed: 2020--12-03."},{"key":"e_1_3_2_2_5_1","unstructured":"[n.d.]. General Data Protection Regulation (GDPR) - Official Legal Text. https:\/\/gdpr-info.eu\/."},{"key":"e_1_3_2_2_6_1","volume-title":"Health Insurance Portability and Accountability Act of","year":"1996","unstructured":"[n.d.]. Health Insurance Portability and Accountability Act of 1996. https:\/\/www.hhs.gov\/hipaa\/index.html."},{"key":"e_1_3_2_2_7_1","unstructured":"[n.d.]. Pequin: An end-to-end toolchain for verifiable computation SNARKs and probabilistic proofs. https:\/\/github.com\/pepper-project\/pequin. Accessed: 2020--12-03."},{"key":"e_1_3_2_2_8_1","unstructured":"[n.d.]. Reachability. https:\/\/github.com\/ilyasergey\/reachability."},{"key":"e_1_3_2_2_9_1","volume-title":"WCET Project Benchmarks","unstructured":"[n.d.]. WCET Project Benchmarks. http:\/\/www.mrtc.mdh.se\/projects\/wcet\/benchmarks.html. Accessed: 2020--12-03."},{"key":"e_1_3_2_2_10_1","unstructured":"2014. libsnark: a C++ library for zkSNARK proofs. https:\/\/github.com\/scipr-lab\/libsnark."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134104"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29011-4_17"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-26954-8_23"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40084-1_6"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--17653--2_4"},{"key":"e_1_3_2_2_16_1","volume-title":"Proceedings of the USENIX Security Symposium","author":"Ben-Sasson Eli","year":"2014","unstructured":"Eli Ben-Sasson, Alessandro Chiesa, Eran Tromer, and Madars Virza. [n.d.]. Succinct Non-Interactive Zero Knowledge for a von Neumann Architecture. In Proceedings of the USENIX Security Symposium, 2014."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44381-1_16"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01185212"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49896-5_12"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70700-6_12"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03326-2_20"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522733"},{"key":"e_1_3_2_2_23_1","volume-title":"Bulletproofs: Short Proofs for Confidential Transactions and More. In Proceedings of the Symposium on Security and Privacy (SP)","volume":"00","author":"B\u00fcnz B.","year":"2018","unstructured":"B. B\u00fcnz, J. Bootle, D. Boneh, A. Poelstra, P. Wuille, and G. Maxwell. [n.d.]. Bulletproofs: Short Proofs for Confidential Transactions and More. In Proceedings of the Symposium on Security and Privacy (SP), 2018, Vol. 00. 319--338."},{"key":"e_1_3_2_2_24_1","volume-title":"CCS","author":"Campanelli Matteo","year":"2019","unstructured":"Matteo Campanelli, Dario Fiore, and Ana\u00efs Querol. [n.d.]. LegoSNARK: Modular Design and Composition of Succinct Zero-Knowledge Proofs.. In CCS 2019."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45721-1_26"},{"key":"e_1_3_2_2_26_1","volume-title":"Terminator: Beyond Safety","author":"Cook Byron","year":"2006","unstructured":"Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Terminator: Beyond Safety. In Computer Aided Verification, Thomas Ball and Robert B. Jones (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 415--418."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.23"},{"key":"e_1_3_2_2_28_1","volume-title":"The Calculational Design of a Generic Abstract Interpreter","author":"Cousot P.","unstructured":"P. Cousot. 1999. The Calculational Design of a Generic Abstract Interpreter. In Calculational System Design, M. Broy and R. Steinbr\u00fcggen (Eds.). NATO ASI Series F. IOS Press, Amsterdam."},{"key":"e_1_3_2_2_29_1","volume-title":"Proceedings of the Second International Symposium on Programming. Dunod","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot. 1976. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming. Dunod, Paris, France, 106--130."},{"key":"e_1_3_2_2_30_1","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, Los Angeles, California, 238--252."},{"key":"e_1_3_2_2_31_1","volume-title":"Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot. 1979. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, San Antonio, Texas, 269--282."},{"key":"e_1_3_2_2_32_1","volume-title":"Semantics and Abstract Interpretation. In Conference Record of the Ninthteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot. 1992. Inductive Definitions, Semantics and Abstract Interpretation. In Conference Record of the Ninthteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, Albuquerque, New Mexico, 83--94."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2537850"},{"key":"e_1_3_2_2_34_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP'05)","volume":"30","author":"Cousot P.","unstructured":"P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min\u00e9, D. Monniaux, and X. Rival. 2005. The ASTR\u00c9E Analyser. In Proceedings of the European Symposium on Programming (ESOP'05) (Lecture Notes in Computer Science, Vol. 3444), M. Sagiv (Ed.). \u00a9Springer, Edinburgh, Scotland, 21--30."},{"key":"e_1_3_2_2_35_1","volume-title":"Theory of cryptography conference","author":"Dwork Cynthia","unstructured":"Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith. 2006. Calibrating noise to sensitivity in private data analysis. In Theory of cryptography conference. Springer, 265--284."},{"key":"e_1_3_2_2_36_1","volume-title":"Building the","author":"Ferdinand Christian","unstructured":"Christian Ferdinand and Reinhold Heckmann. 2004. aiT: Worst-Case Execution Time Prediction by Static Program Analysis. In Building the Information Society, Ren\u00e8 Jacquart (Ed.). Springer US, Boston, MA, 377--383."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978368"},{"key":"e_1_3_2_2_38_1","volume-title":"Program Verification","author":"Floyd Robert W","unstructured":"Robert W Floyd. 1993. Assigning meanings to programs. In Program Verification. Springer, 65--81."},{"key":"e_1_3_2_2_39_1","series-title":"SIAM Journal on computing 18, 1","volume-title":"The knowledge complexity of interactive proof systems","author":"Goldwasser Shafi","year":"1989","unstructured":"Shafi Goldwasser, Silvio Micali, and Charles Rackoff. 1989. The knowledge complexity of interactive proof systems. SIAM Journal on computing 18, 1 (1989), 186--208."},{"key":"e_1_3_2_2_40_1","volume-title":"Robustness Analysis of Finite Precision Implementations","author":"Goubault Eric","unstructured":"Eric Goubault and Sylvie Putot. 2013. Robustness Analysis of Finite Precision Implementations. In Programming Languages and Systems, Chung-chieh Shan (Ed.). Springer International Publishing, Cham, 50--57."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03356-8_12"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49896-5_11"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45727-3_19"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_15"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/321921.321938"},{"key":"e_1_3_2_2_47_1","unstructured":"Ken Kennedy. 1979. A survey of data flow analysis techniques. IBM Thomas J. Watson Research Division."},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129782"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_2_51_1","volume-title":"Spectre Attacks: Exploiting Speculative Execution. In 40th IEEE Symposium on Security and Privacy (S&P'19)","author":"Kocher Paul","year":"2019","unstructured":"Paul Kocher, Jann Horn, Anders Fogh, , Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. In 40th IEEE Symposium on Security and Privacy (S&P'19)."},{"key":"e_1_3_2_2_52_1","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Lipp Moritz","year":"2018","unstructured":"Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown: Reading Kernel Memory from User Space. In 27th USENIX Security Symposium (USENIX Security 18)."},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3339817"},{"key":"e_1_3_2_2_54_1","series-title":"SIAM J. Comput. (2000)","volume-title":"Computationally Sound Proofs","author":"Micali Silvio","unstructured":"Silvio Micali. 2000. Computationally Sound Proofs. SIAM J. Comput. (2000)."},{"key":"e_1_3_2_2_55_1","volume-title":"A Calculational Approach to Control-Flow Analysis by Abstract Interpretation","author":"Midtgaard Jan","unstructured":"Jan Midtgaard and Thomas Jensen. 2008. A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In Static Analysis, Mar\u00eda Alpuente and Germ\u00e1n Vidal (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 347--362."},{"key":"e_1_3_2_2_56_1","volume-title":"Principles of Program Analysis","author":"Nielson Flemming","unstructured":"Flemming Nielson, Hanne R. Nielson, and Chris Hankin. 2010. Principles of Program Analysis. Springer Publishing Company, Incorporated."},{"key":"e_1_3_2_2_57_1","volume-title":"Pinocchio: Nearly practical verifiable computation. In S&P","author":"Parno Bryan","year":"2013","unstructured":"Bryan Parno, Jon Howell, Craig Gentry, and Mariana Raykova. 2013. Pinocchio: Nearly practical verifiable computation. In S&P 2013. 238--252."},{"key":"e_1_3_2_2_58_1","unstructured":"David Pichardie. 2005. Interpr\u00e9tation abstraite en logique intuitionniste : extraction d'analyseurs Java certifi\u00e9s. Ph.D. Dissertation. Universit\u00e9 Rennes 1. In french."},{"key":"e_1_3_2_2_59_1","volume-title":"Mathworks","author":"Prover Polyspace Code","year":"2014","unstructured":"Polyspace Code Prover. 2014. Static Analysis with Polyspace Products. Mathworks, June (2014)."},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09519-5_72"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-56877-1_25"},{"key":"e_1_3_2_2_62_1","volume-title":"13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18)","author":"Setty Srinath","year":"2018","unstructured":"Srinath Setty, Sebastian Angel, Trinabh Gupta, and Jonathan Lee. 2018. Proving the correct execution of concurrent services in zero-knowledge. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18). 339--356."},{"key":"e_1_3_2_2_63_1","unstructured":"Olin Grigsby Shivers. 1991. Control-Flow Analysis of Higher-Order Languages of Taming Lambda. Ph.D. Dissertation. USA. UMI Order No. GAX91--26964."},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","unstructured":"Julien Signoles Pascal Cuoq Florent Kirchner Nikolai Kosmatov Virgile Prevosto and Boris Yakobowski. 2012. Frama-c: a Software Analysis Perspective. Formal Aspects of Computing 27. https:\/\/doi.org\/10.1007\/s00165-014-0326--7","DOI":"10.1007\/s00165-014-0326--7"},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/996893.996869"},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2015.23097"},{"key":"e_1_3_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00060"},{"key":"e_1_3_2_2_68_1","unstructured":"Guannan Wei Yuxuan Chen and Tiark Rompf. 2019. Staged Abstract Interpreters. (2019)."},{"key":"e_1_3_2_2_69_1","volume-title":"Libra: Succinct Zero-Knowledge Proofs with Optimal Prover Computation. In Advances in Cryptology (CRYPTO).","author":"Xie Tiacheng","year":"2019","unstructured":"Tiacheng Xie, Jiaheng Zhang, Yupeng Zhang, Charalampos Papamanthou, and Dawn Song. 2019. Libra: Succinct Zero-Knowledge Proofs with Optimal Prover Computation. In Advances in Cryptology (CRYPTO)."},{"key":"e_1_3_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00052"},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.43"},{"key":"e_1_3_2_2_72_1","unstructured":"Yupeng Zhang Daniel Genkin Jonathan Katz Dimitrios Papadopoulos and Charalampos Papamanthou. 2017. A Zero-Knowledge Version of vSQL. Cryptology ePrint."},{"key":"e_1_3_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00013"},{"key":"e_1_3_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09519-5_73"}],"event":{"name":"CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security","location":"Virtual Event Republic of Korea","acronym":"CCS '21","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484795","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484795","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484795","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T20:53:56Z","timestamp":1763499236000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484795"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,12]]},"references-count":74,"alternative-id":["10.1145\/3460120.3484795","10.1145\/3460120"],"URL":"https:\/\/doi.org\/10.1145\/3460120.3484795","relation":{},"subject":[],"published":{"date-parts":[[2021,11,12]]},"assertion":[{"value":"2021-11-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}