{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:52:46Z","timestamp":1770277966391,"version":"3.49.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T00:00:00Z","timestamp":1574294400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100019167","name":"Zurich Information Security and Privacy Center","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100019167","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2020,3,31]]},"abstract":"<jats:p>Many interesting program properties like determinism or information flow security are hyperproperties, that is, they relate multiple executions of the same program. Hyperproperties can be verified using relational logics, but these logics require dedicated tool support and are difficult to automate. Alternatively, constructions such as self-composition represent multiple executions of a program by one product program, thereby reducing hyperproperties of the original program to trace properties of the product. However, existing constructions do not fully support procedure specifications, for instance, to derive the determinism of a caller from the determinism of a callee, making verification non-modular.<\/jats:p>\n          <jats:p>We present modular product programs, a novel kind of product program that permits hyperproperties in procedure specifications and, thus, can reason about calls modularly. We provide a general formalization of our product construction and prove it sound and complete. We demonstrate its expressiveness by applying it to information flow security with advanced features such as declassification and termination-sensitivity. Modular product programs can be verified using off-the-shelf verifiers; we have implemented our approach for both secure information flow and general hyperproperties using the Viper verification infrastructure. Our evaluation demonstrates that modular product programs can be used to prove hyperproperties for challenging examples in reasonable time.<\/jats:p>","DOI":"10.1145\/3324783","type":"journal-article","created":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T13:35:22Z","timestamp":1574343322000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Modular Product Programs"],"prefix":"10.1145","volume":"42","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4891-6950","authenticated-orcid":false,"given":"Marco","family":"Eilers","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samuel","family":"Hitz","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,11,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"e_1_2_1_3_1","volume-title":"15th IEEE Computer Security Foundations Workshop (CSFW-15'02)","author":"Banerjee Anindya","year":"2002","unstructured":"Anindya Banerjee and David A. Naumann. 2002. Secure information flow and pointer confinement in a Java-like language. In 15th IEEE Computer Security Foundations Workshop (CSFW-15'02), (24--26 June 2002, Cape Breton, Nova Scotia, Canada). 253."},{"key":"e_1_2_1_4_1","volume-title":"36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016","author":"Banerjee Anindya","year":"2016","unstructured":"Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. 2016. Relational logic with framing and hypotheses. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, (December 13--15, 2016, Chennai, India). 11:1--11:16."},{"key":"e_1_2_1_5_1","volume-title":"Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.","author":"Barnett Michael","year":"2005","unstructured":"Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A modular reusable verifier for object-oriented programs. In FMCO (Lecture Notes in Computer Science), Vol. 4111. Springer, 364--387."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_2_1_7_1","volume-title":"International Symposium, LFCS 2013","author":"Barthe Gilles","year":"2013","unstructured":"Gilles Barthe, Juan Manuel Crespo, and C\u00e9sar Kunz. 2013. Beyond 2-safety: Asymmetric product programs for relational program verification. In Logical Foundations of Computer Science, International Symposium, LFCS 2013, (San Diego, CA, January 6--8, 2013). 29--43."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_16"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"David Costanzo and Zhong Shao. 2014. A separation logic for enforcing declarative information flow control policies. In Principles of Security and Trust - 3rd International Conference (POST'14) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS'14) (Grenoble France April 5--13 2014). 179--198.","DOI":"10.1007\/978-3-642-54792-8_10"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2004.1310736"},{"key":"e_1_2_1_18_1","unstructured":"Marco Eilers Peter M\u00fcller and Samuel Hitz. 2018. Modular product programs. In Programming Languages and Systems - 27th European Symposium on Programming (ESOP'18) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS'18) (Thessaloniki Greece April 14--20 2018). 502--529."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0234-3"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642987"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-014-0257-6"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_20"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3162070"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.28"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491452"},{"key":"e_1_2_1_26_1","volume-title":"17th European Symposium on Programming, (ESOP'08), Held as Part of the Joint European Conferences on Theory and Practice of Software, (ETAPS'08)","author":"K. Rustan","year":"2008","unstructured":"K. Rustan M. Leino and Peter M\u00fcller. 2008. Verification of equivalent-results methods. In Programming Languages and Systems, 17th European Symposium on Programming, (ESOP'08), Held as Part of the Joint European Conferences on Theory and Practice of Software, (ETAPS'08), (Budapest, Hungary, March 29-April 6, 2008). 307--321."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040319"},{"key":"e_1_2_1_28_1","volume-title":"Summers","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Automatic verification of iterated separating conjunctions using symbolic execution. In Computer Aided Verification - 28th International Conference, (CAV'16), (Toronto, ON, Canada, July 17--23, 2016), Part I. 405--425."},{"key":"e_1_2_1_29_1","volume-title":"VMCAI 2016, St. Petersburg, FL, USA, January 17--19, 2016. Proceedings. 41--62","author":"M\u00fcller Peter","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A verification infrastructure for permission-based reasoning. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17--19, 2016. Proceedings. 41--62."},{"key":"e_1_2_1_30_1","volume-title":"11th European Symposium on Research in Computer Security","author":"Naumann David A.","year":"2006","unstructured":"David A. Naumann. 2006. From coupling relations to mated invariants for checking information flow. In Computer Security - (ESORICS'06), 11th European Symposium on Research in Computer Security, (Hamburg, Germany, September 18--20, 2006). 279--296."},{"key":"e_1_2_1_31_1","volume-title":"CAV 2018, Held as Part of the Federated Logic Conference, (FloC'18)","author":"Pick Lauren","year":"2018","unstructured":"Lauren Pick, Grigory Fedyukovich, and Aarti Gupta. 2018. Exploiting synchrony and symmetry in relational verification. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, (FloC'18), (Oxford, UK, July 14--17, 2018), Part I. 164--182."},{"key":"e_1_2_1_32_1","volume-title":"Benedict Lee, and Wei-Ngan Chin.","author":"Prabawa Adi","year":"2018","unstructured":"Adi Prabawa, Mahmudul Faisal Al Ameen, Benedict Lee, and Wei-Ngan Chin. 2018. A logical system for modular information flow verification. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, (VMCAI'18), (Los Angeles, CA, January 7--9, 2018). 430--451."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_34_1","volume-title":"2nd Mext-NSF-JSPS International Symposium, (ISSS'03)","author":"Sabelfeld Andrei","year":"2003","unstructured":"Andrei Sabelfeld and Andrew C. Myers. 2003. A model for delimited information release. In Software Security - Theories and Systems, 2nd Mext-NSF-JSPS International Symposium, (ISSS'03), (Tokyo, Japan, November 4--6, 2003), Revised Papers. 174--191."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2005.15"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31762-0_15"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Geoffrey Smith. 2007. Principles of secure information flow analysis. In Malware Detection. 291--307.","DOI":"10.1007\/978-0-387-44599-1_13"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_2_1_40_1","volume-title":"12th International Symposium, (SAS'05)","author":"Terauchi Tachio","year":"2005","unstructured":"Tachio Terauchi and Alexander Aiken. 2005. Secure information flow as a safety problem. In Static Analysis, 12th International Symposium, (SAS'05), (London, UK, September 7--9, 2005). 352--367."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324783","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3324783","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:54:13Z","timestamp":1750204453000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324783"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,21]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,3,31]]}},"alternative-id":["10.1145\/3324783"],"URL":"https:\/\/doi.org\/10.1145\/3324783","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,21]]},"assertion":[{"value":"2018-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}