{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:10:33Z","timestamp":1750306233461,"version":"3.41.0"},"reference-count":88,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,3,10]],"date-time":"2017-03-10T00:00:00Z","timestamp":1489104000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"German Research Foundation (DFG) within the Collaborative Research Centre \u201cOn-The-Fly Computing\u201d","award":["SFB 901"],"award-info":[{"award-number":["SFB 901"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2017,6,30]]},"abstract":"<jats:p>\n            Today, software is traded worldwide on global markets, with apps being downloaded to smartphones within minutes or seconds. This poses, more than ever, the challenge of ensuring safety of software in the face of (1) unknown or untrusted software providers together with (2) resource-limited software consumers. The concept of Proof-Carrying Code (PCC), years ago suggested by Necula, provides one framework for securing the execution of untrusted code. PCC techniques attach safety proofs, constructed by software producers, to code. Based on the assumption that\n            <jats:italic>checking<\/jats:italic>\n            proofs is usually much simpler than\n            <jats:italic>constructing<\/jats:italic>\n            proofs, software consumers should thus be able to quickly check the safety of software. However, PCC techniques often suffer from the size of\n            <jats:italic>certificates<\/jats:italic>\n            (i.e., the attached proofs), making PCC techniques inefficient in practice.\n          <\/jats:p>\n          <jats:p>\n            In this article, we introduce a new framework for the safe execution of untrusted code called\n            <jats:italic>Programs from Proofs<\/jats:italic>\n            (PfP). The basic assumption underlying the PfP technique is the fact that the\n            <jats:italic>structure<\/jats:italic>\n            of programs significantly influences the complexity of checking a specific safety property. Instead of attaching proofs to program code, the PfP technique transforms the program into an efficiently checkable form, thus guaranteeing quick safety checks for software consumers. For this transformation, the technique also uses a producer-side automatic proof of safety. More specifically, safety proving for the software producer proceeds via the construction of an abstract reachability graph (ARG) unfolding the control-flow automaton (CFA) up to the degree necessary for simple checking. To this end, we combine different sorts of software analysis: expensive analyses incrementally determining the degree of unfolding, and cheap analyses responsible for safety checking. Out of the abstract reachability graph we generate the new program. In its CFA structure, it is isomorphic to the graph and hence another, this time consumer-side, cheap analysis can quickly determine its safety.\n          <\/jats:p>\n          <jats:p>\n            Like PCC, Programs from Proofs is a general framework instantiable with different sorts of (expensive and cheap) analysis. Here, we present the general framework and exemplify it by some concrete examples. We have implemented different instantiations on top of the configurable program analysis tool CPA\n            <jats:sc>checker<\/jats:sc>\n            and report on experiments, in particular on comparisons with PCC techniques.\n          <\/jats:p>","DOI":"10.1145\/3014427","type":"journal-article","created":{"date-parts":[[2017,3,13]],"date-time":"2017-03-13T12:25:15Z","timestamp":1489407915000},"page":"1-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Programs from Proofs"],"prefix":"10.1145","volume":"39","author":[{"given":"Marie-Christine","family":"Jakobs","sequence":"first","affiliation":[{"name":"Paderborn University (Germany)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"Paderborn University (Germany)"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,3,10]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1007\/978-3-540-32275-7_25"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1145\/989393.989451"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/978-3-642-28641-4_20"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1145\/1629335.1629343"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1007\/978-3-540-69166-2_16"},{"unstructured":"John Barnes. 2012. SPARK - The Proven Approach to High Integrity Software. Altran Praxis. http:\/\/www.altran.co.uk UK.","key":"e_1_2_1_6_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1145\/2363.2528"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1109\/DISCEX.2003.1194942"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1007\/978-94-017-0435-9_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1007\/3-540-39185-1_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1007\/978-3-662-46681-0_31"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1007\/978-3-540-27864-1_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/978-3-540-73368-3_51"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1007\/978-3-642-22110-1_16"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.5555\/1998496.1998532"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1007\/978-3-642-37057-1_11"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/2491411.2491429"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1007\/978-3-319-23404-5_12"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1007\/978-3-319-23404-5_3"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1007\/978-3-319-19195-9_15"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1007\/978-3-319-10702-8_10"},{"key":"e_1_2_1_22_1","volume-title":"Mowbray","author":"Brown William J.","year":"1998","unstructured":"William J. Brown, Raphael C. Malveau, Hays W. McCormick III, and Thomas J. Mowbray. 1998. AntiPatterns: Refactoring Software, Architectures, and Projects in Crisis. John Wiley 8 Sons, New York, NY."},{"unstructured":"Oliver Burn (founder). 2015. Checkstyle Retrieved from http:\/\/checkstyle.sourceforge.net\/.","key":"e_1_2_1_23_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1007\/978-3-642-36742-7_7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1007\/10722167_15"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1007\/978-3-642-22110-1_26"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1007\/978-3-540-74061-2_21"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/325694.325716"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1007\/978-3-642-33826-7_16"},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.1145\/512529.512538"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1007\/11823230_27"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1109\/ReConFig.2009.31"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1109\/IPDPS.2003.1213511"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1145\/1081706.1081742"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.1007\/3-540-63166-6_10"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1002\/stvr.1536"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.1007\/11691372_34"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1145\/1542476.1542518"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1007\/3-540-57659-2_30"},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1109\/TSE.2004.1265732"},{"doi-asserted-by":"publisher","key":"e_1_2_1_42_1","DOI":"10.1007\/978-3-642-03237-0_7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_43_1","DOI":"10.1145\/964001.964021"},{"doi-asserted-by":"publisher","key":"e_1_2_1_44_1","DOI":"10.1007\/978-3-540-39910-0_16"},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.1145\/503272.503279"},{"doi-asserted-by":"publisher","key":"e_1_2_1_46_1","DOI":"10.1007\/3-540-45657-0_45"},{"doi-asserted-by":"publisher","key":"e_1_2_1_47_1","DOI":"10.1016\/j.jss.2012.08.063"},{"doi-asserted-by":"publisher","key":"e_1_2_1_48_1","DOI":"10.1145\/1052883.1052895"},{"key":"e_1_2_1_49_1","volume-title":"J. P. Seldin and J. R. Hindley (Eds)","author":"Howard William A.","year":"1980","unstructured":"William A. Howard. 1969. The formulae-as-types notion of construction. (1969). Reprinted in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley (Eds). Academic Press, 1980."},{"doi-asserted-by":"publisher","key":"e_1_2_1_50_1","DOI":"10.1145\/1111037.1111045"},{"unstructured":"IBM Research. 2015. T.J. Watson Libraries for Analysis (WALA) Retrieved from http:\/\/wala.sourceforge.net.","key":"e_1_2_1_51_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_52_1","DOI":"10.1145\/2635868.2635884"},{"doi-asserted-by":"publisher","key":"e_1_2_1_53_1","DOI":"10.1007\/978-3-319-22969-0_12"},{"doi-asserted-by":"publisher","key":"e_1_2_1_54_1","DOI":"10.1145\/2632362.2632372"},{"doi-asserted-by":"publisher","key":"e_1_2_1_55_1","DOI":"10.1145\/2695664.2695690"},{"doi-asserted-by":"publisher","key":"e_1_2_1_56_1","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_2_1_57_1","volume-title":"Article 21 (Oct.","author":"Jhala Ranjit","year":"2009","unstructured":"Ranjit Jhala and Rupak Majumdar. 2009. Software model checking. ACM Comput. Surv. 41, 4, Article 21 (Oct. 2009), 54 pages."},{"key":"e_1_2_1_58_1","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"Johnson Ralph E.","year":"1995","unstructured":"Ralph E. Johnson, Erich Gamma, John Vlissides, and Richard Helm. 1995. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Longman Publishing Co., Boston, MA."},{"doi-asserted-by":"publisher","key":"e_1_2_1_59_1","DOI":"10.1007\/BF00290339"},{"doi-asserted-by":"publisher","key":"e_1_2_1_60_1","DOI":"10.1145\/512927.512945"},{"doi-asserted-by":"publisher","key":"e_1_2_1_61_1","DOI":"10.1145\/1321631.1321691"},{"doi-asserted-by":"publisher","key":"e_1_2_1_62_1","DOI":"10.1002\/spe.438"},{"doi-asserted-by":"publisher","key":"e_1_2_1_63_1","DOI":"10.1007\/3-540-39185-1_12"},{"doi-asserted-by":"publisher","key":"e_1_2_1_64_1","DOI":"10.1007\/978-3-540-69407-6_39"},{"doi-asserted-by":"publisher","key":"e_1_2_1_65_1","DOI":"10.1016\/j.entcs.2012.10.007"},{"doi-asserted-by":"publisher","key":"e_1_2_1_66_1","DOI":"10.1007\/3-540-44585-4_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_67_1","DOI":"10.1145\/263699.263712"},{"doi-asserted-by":"publisher","key":"e_1_2_1_68_1","DOI":"10.1007\/3-540-68671-1_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_69_1","DOI":"10.1145\/503272.503286"},{"doi-asserted-by":"publisher","key":"e_1_2_1_70_1","DOI":"10.1007\/978-3-662-03811-6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_71_1","DOI":"10.1007\/3-540-45139-0_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_72_1","DOI":"10.1145\/1275497.1275501"},{"doi-asserted-by":"publisher","key":"e_1_2_1_73_1","DOI":"10.1023\/B:JARS.0000021015.15794.82"},{"unstructured":"Sriram Sankaranarayanan and Franjo Ivan\u010di\u0107. 2013. NECLA Static Analysis Benchmarks (necla-static-small) v1.1 Retrieved from http:\/\/www.nec-labs.com\/research\/system\/systems_SAV-website\/small_static_ bench-v1.1.tar.gz.","key":"e_1_2_1_74_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_75_1","DOI":"10.1007\/11823230_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_76_1","DOI":"10.1145\/800192.805690"},{"doi-asserted-by":"publisher","key":"e_1_2_1_77_1","DOI":"10.1007\/978-3-642-34188-5_15"},{"doi-asserted-by":"publisher","key":"e_1_2_1_78_1","DOI":"10.1007\/978-3-642-22110-1_57"},{"doi-asserted-by":"publisher","key":"e_1_2_1_79_1","DOI":"10.1007\/3-540-61739-6_31"},{"doi-asserted-by":"publisher","key":"e_1_2_1_80_1","DOI":"10.1145\/1356058.1356066"},{"doi-asserted-by":"publisher","key":"e_1_2_1_81_1","DOI":"10.5555\/781995.782008"},{"doi-asserted-by":"publisher","key":"e_1_2_1_82_1","DOI":"10.1007\/978-3-540-73368-3_40"},{"doi-asserted-by":"publisher","key":"e_1_2_1_83_1","DOI":"10.1007\/978-3-642-41202-8_27"},{"doi-asserted-by":"publisher","key":"e_1_2_1_84_1","DOI":"10.1007\/978-3-642-39799-8_65"},{"doi-asserted-by":"publisher","key":"e_1_2_1_85_1","DOI":"10.1007\/978-3-642-34281-3_24"},{"doi-asserted-by":"publisher","key":"e_1_2_1_86_1","DOI":"10.1007\/978-3-540-87698-4_26"},{"doi-asserted-by":"publisher","key":"e_1_2_1_87_1","DOI":"10.1109\/DSN.2009.5270355"},{"doi-asserted-by":"publisher","key":"e_1_2_1_88_1","DOI":"10.1109\/COMPSAC.2007.159"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3014427","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3014427","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:17Z","timestamp":1750220597000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3014427"}},"subtitle":["A Framework for the Safe Execution of Untrusted Software"],"short-title":[],"issued":{"date-parts":[[2017,3,10]]},"references-count":88,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,6,30]]}},"alternative-id":["10.1145\/3014427"],"URL":"https:\/\/doi.org\/10.1145\/3014427","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2017,3,10]]},"assertion":[{"value":"2015-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-03-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}