{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,23]],"date-time":"2026-09-23T16:08:45Z","timestamp":1790179725591,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":56,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,12,2]],"date-time":"2024-12-02T00:00:00Z","timestamp":1733097600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,12,2]]},"DOI":"10.1145\/3658644.3690303","type":"proceedings-article","created":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T12:19:20Z","timestamp":1733746760000},"page":"4-18","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifiable Security Policies for Distributed Systems"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8573-2387","authenticated-orcid":false,"given":"Felix A.","family":"Wolf","sequence":"first","affiliation":[{"name":"Department of Computer Science, ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"Department of Computer Science, ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,12,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Sound Verification of Security Protocols: From Design to Interoperable Implementations","author":"Arquint Linard","unstructured":"Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David A. Basin, and Peter M\u00fcller. 2023. Sound Verification of Security Protocols: From Design to Interoperable Implementations. In SP. IEEE, 1077--1093."},{"key":"e_1_3_2_1_2_1","volume-title":"Learning is Change in Knowledge: Knowledge-Based Security for Dynamic Policies","author":"Askarov Aslan","unstructured":"Aslan Askarov and Stephen Chong. 2012. Learning is Change in Knowledge: Knowledge-Based Security for Dynamic Policies. In CSF. IEEE Computer Society, 308--322."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88313-5_22"},{"key":"e_1_3_2_1_4_1","volume-title":"Myers","author":"Askarov Aslan","year":"2010","unstructured":"Aslan Askarov and Andrew C. Myers. 2010. A Semantic Framework for Declassification and Endorsement. In ESOP (LNCS, Vol. 6012). Springer, 64--84."},{"key":"e_1_3_2_1_5_1","volume-title":"S&P","author":"Askarov Aslan","unstructured":"Aslan Askarov and Andrei Sabelfeld. 2007 a. Gradual Release: Unifying Declassification, Encryption and Key Release Policies. In S&P. IEEE Computer Society, 207--221."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Aslan Askarov and Andrei Sabelfeld. 2007 b. Localized delimited release: combining the what and where dimensions of information release. In PLAS. ACM 53--60.","DOI":"10.1145\/1255329.1255339"},{"key":"e_1_3_2_1_7_1","volume-title":"Tight Enforcement of Information-Release Policies for Dynamic Languages","author":"Askarov Aslan","unstructured":"Aslan Askarov and Andrei Sabelfeld. 2009. Tight Enforcement of Information-Release Policies for Dynamic Languages. In CSF. IEEE Computer Society, 43--59."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Musard Balliu Mads Dam and Gurvan Le Guernic. 2011. Epistemic temporal logic for information flow security. In PLAS. ACM 6.","DOI":"10.1145\/2166956.2166962"},{"key":"e_1_3_2_1_9_1","volume-title":"Expressive Declassification Policies and Modular Static Enforcement","author":"Banerjee Anindya","unstructured":"Anindya Banerjee, David A. Naumann, and Stan Rosenberg. 2008. Expressive Declassification Policies and Modular Static Enforcement. In SP. IEEE Computer Society, 339--353."},{"key":"e_1_3_2_1_10_1","volume-title":"Tractable Enforcement of Declassification Policies","author":"Barthe Gilles","unstructured":"Gilles Barthe, Salvador Cavadini, and Tamara Rezk. 2008. Tractable Enforcement of Declassification Policies. In CSF. IEEE Computer Society, 83--97."},{"key":"e_1_3_2_1_11_1","volume-title":"Juan Manuel Crespo, and C\u00e9sar Kunz","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe, Juan Manuel Crespo, and C\u00e9sar Kunz. 2011. Relational Verification Using Product Programs. In FM (LNCS, Vol. 6664). Springer, 200--214."},{"key":"e_1_3_2_1_12_1","volume-title":"Juan Manuel Crespo, and C\u00e9sar Kunz","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 LFCS (LNCS, Vol. 7734). Springer, 29--43."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2022.3154689"},{"key":"e_1_3_2_1_15_1","volume-title":"Arch. Formal Proofs","volume":"2021","author":"Bauereiss Thomas","year":"2021","unstructured":"Thomas Bauereiss and Andrei Popescu. 2021. CoSMed: A confidentiality-verified social media platform. Arch. Formal Proofs, Vol. 2021 (2021)."},{"key":"e_1_3_2_1_16_1","volume-title":"Arch. Formal Proofs","volume":"2021","author":"Bauereiss Thomas","year":"2021","unstructured":"Thomas Bauereiss and Andrei Popescu. 2021. CoSMeDis: A confidentiality-verified distributed social media platform. Arch. Formal Proofs, Vol. 2021 (2021)."},{"key":"e_1_3_2_1_17_1","unstructured":"Ken Biba. 1977. Integrity Considerations for Secure Computer Systems. (1977)."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_13"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Niklas Broberg and David Sands. 2009. Flow-sensitive semantics for dynamic information flow policies. In PLAS. ACM 101--112.","DOI":"10.1145\/1554339.1554352"},{"key":"e_1_3_2_1_20_1","volume-title":"The Anatomy and Facets of Dynamic Policies","author":"Broberg Niklas","unstructured":"Niklas Broberg, Bart van Delft, and David Sands. 2015. The Anatomy and Facets of Dynamic Policies. In CSF. IEEE Computer Society, 122--136."},{"key":"e_1_3_2_1_21_1","volume-title":"Naumann","author":"Chudnov Andrey","year":"2018","unstructured":"Andrey Chudnov and David A. Naumann. 2018. Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies. In CSF. IEEE Computer Society, 189--203."},{"key":"e_1_3_2_1_22_1","volume-title":"Schneider","author":"Clarkson Michael R.","year":"2008","unstructured":"Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. In CSF. IEEE Computer Society, 51--65."},{"key":"e_1_3_2_1_23_1","volume-title":"Go Implementation of WireGuard. https:\/\/git.zx2c4.com\/wireguard-go. [Online","author":"Donenfeld Jason A.","year":"2021","unstructured":"Jason A. Donenfeld. [n.,d.]. Go Implementation of WireGuard. https:\/\/git.zx2c4.com\/wireguard-go. [Online; accessed 11-March-2021]."},{"key":"e_1_3_2_1_24_1","volume-title":"CAV (1) (LNCS","author":"Eilers Marco","unstructured":"Marco Eilers, Severin Meier, and Peter M\u00fcller. 2021. Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. In CAV (1) (LNCS, Vol. 12759). Springer, 718--741."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_18"},{"key":"e_1_3_2_1_26_1","volume-title":"CAV (2) (LNCS","author":"Ernst Gidon","unstructured":"Gidon Ernst and Toby Murray. 2019. SecCSL: Security Concurrent Separation Logic. In CAV (2) (LNCS, Vol. 11562). Springer, 208--230."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0243-x"},{"key":"e_1_3_2_1_28_1","volume-title":"Goguen and Jos\u00e9 Meseguer","author":"Joseph","year":"1984","unstructured":"Joseph A. Goguen and Jos\u00e9 Meseguer. 1984. Unwinding and Inference Control. In S&P. IEEE Computer Society, 75--87."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_12"},{"key":"e_1_3_2_1_30_1","volume-title":"Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. ACM, 637--650.","author":"Jung Ralf","year":"2015","unstructured":"Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. ACM, 637--650."},{"key":"e_1_3_2_1_31_1","volume-title":"A uniform framework for the formal specification and verification of information flow security. Ph.,D. Dissertation","author":"Mantel Heiko","unstructured":"Heiko Mantel. 2003. A uniform framework for the formal specification and verification of information flow security. Ph.,D. Dissertation. Saarland University, Saarbr\u00fccken, Germany."},{"key":"e_1_3_2_1_32_1","volume-title":"Assumptions and Guarantees for Compositional Noninterference","author":"Mantel Heiko","unstructured":"Heiko Mantel, David Sands, and Henning Sudbrock. 2011. Assumptions and Guarantees for Compositional Noninterference. In CSF. IEEE Computer Society, 218--232."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2699855.2699858"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586041"},{"key":"e_1_3_2_1_35_1","volume-title":"Naumann","author":"Murray Toby","year":"2023","unstructured":"Toby Murray, Mukesh Tiwari, Gidon Ernst, and David A. Naumann. 2023. Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. In CCS. ACM, 1746--1760."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11863908_18"},{"key":"e_1_3_2_1_37_1","volume-title":"Information-Flow Security for Interactive Programs","author":"O'Neill Kevin R.","unstructured":"Kevin R. O'Neill, Michael R. Clarkson, and Stephen Chong. 2006. Information-Flow Security for Interactive Programs. In CSFW. IEEE Computer Society, 190--201."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34968-4_22"},{"key":"e_1_3_2_1_39_1","volume-title":"Modular and Compositional Verification of the Input\/Output Behavior of Programs. In ESOP (LNCS","volume":"182","author":"Penninckx Willem","year":"2015","unstructured":"Willem Penninckx, Bart Jacobs, and Frank Piessens. 2015. Sound, Modular and Compositional Verification of the Input\/Output Behavior of Programs. In ESOP (LNCS, Vol. 9032). Springer, 158--182."},{"key":"e_1_3_2_1_40_1","first-page":"1","article-title":"Bounded-Deducibility Security (Invited Paper). In ITP (LIPIcs, Vol. 193)","volume":"3","author":"Popescu Andrei","year":"2021","unstructured":"Andrei Popescu, Thomas Bauereiss, and Peter Lammich. 2021. Bounded-Deducibility Security (Invited Paper). In ITP (LIPIcs, Vol. 193). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 3:1--3:20.","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_3_2_1_41_1","volume-title":"CoCon: A Confidentiality-Verified Conference Management System. Arch. Formal Proofs","volume":"2021","author":"Popescu Andrei","year":"2021","unstructured":"Andrei Popescu, Peter Lammich, and Thomas Bauereiss. 2021. CoCon: A Confidentiality-Verified Conference Management System. Arch. Formal Proofs, Vol. 2021 (2021)."},{"key":"e_1_3_2_1_42_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. IEEE Computer Society, 55--74."},{"key":"e_1_3_2_1_43_1","volume-title":"S&P","author":"Roscoe A. W.","unstructured":"A. W. Roscoe. 1995. CSP and determinism in security modelling. In S&P. IEEE Computer Society, 114--127."},{"key":"e_1_3_2_1_44_1","series-title":"Cryptology and Information Security Series","volume-title":"Formal Models and Techniques for Analyzing Security Protocols","author":"Ryan Mark Dermot","unstructured":"Mark Dermot Ryan and Ben Smyth. 2011. Applied pi calculus. In Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series, Vol. 5. IOS Press, 112--142."},{"key":"e_1_3_2_1_45_1","volume-title":"Myers","author":"Sabelfeld Andrei","year":"2003","unstructured":"Andrei Sabelfeld and Andrew C. Myers. 2003. A Model for Delimited Information Release. In ISSS (LNCS, Vol. 3233). Springer, 174--191."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2000.856937"},{"key":"e_1_3_2_1_47_1","volume-title":"Dimensions and Principles of Declassification","author":"Sabelfeld Andrei","unstructured":"Andrei Sabelfeld and David Sands. 2005. Dimensions and Principles of Declassification. In CSFW. IEEE Computer Society, 255--269."},{"key":"e_1_3_2_1_48_1","volume-title":"VERONICA: Expressive and Precise Concurrent Information Flow Security","author":"Schoepe Daniel","year":"2020","unstructured":"Daniel Schoepe, Toby Murray, and Andrei Sabelfeld. 2020. VERONICA: Expressive and Precise Concurrent Information Flow Security. In CSF. IEEE, 79--94."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_18"},{"key":"e_1_3_2_1_51_1","volume-title":"Volpano","author":"Smith Geoffrey","year":"1998","unstructured":"Geoffrey Smith and Dennis M. Volpano. 1998. Secure Information Flow in a Multi-Threaded Imperative Language. In POPL. ACM, 355--364."},{"key":"e_1_3_2_1_52_1","volume-title":"Proc. ACM Program. Lang.","volume":"4","author":"Sprenger Christoph","year":"2020","unstructured":"Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter M\u00fcller, Martin Clochard, and David A. Basin. 2020. Igloo: soundly linking compositional refinement and separation logic for distributed system verification. Proc. ACM Program. Lang., Vol. 4, OOPSLA (2020), 152:1--152:31."},{"key":"e_1_3_2_1_53_1","volume-title":"Jo ao Carlos Pereira, and Peter M\u00fcller","author":"Wolf Felix A.","year":"2021","unstructured":"Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, Jo ao Carlos Pereira, and Peter M\u00fcller. 2021. Gobra: Modular Specification and Verification of Go Programs. In CAV (1) (LNCS, Vol. 12759). Springer, 367--379."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.13686927"},{"key":"e_1_3_2_1_55_1","volume-title":"Proc. ACM Program. Lang.","volume":"4","author":"Zakowski Yannick","year":"2020","unstructured":"Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., Vol. 4, POPL (2020), 51:1--51:32."},{"key":"e_1_3_2_1_56_1","volume-title":"Myers","author":"Zdancewic Steve","year":"2001","unstructured":"Steve Zdancewic and Andrew C. Myers. 2001. Robust Declassification. In CSFW. IEEE Computer Society, 15--23."}],"event":{"name":"CCS '24: ACM SIGSAC Conference on Computer and Communications Security","location":"Salt Lake City UT USA","acronym":"CCS '24","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690303","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3658644.3690303","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T06:13:34Z","timestamp":1755843214000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690303"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,2]]},"references-count":56,"alternative-id":["10.1145\/3658644.3690303","10.1145\/3658644"],"URL":"https:\/\/doi.org\/10.1145\/3658644.3690303","relation":{},"subject":[],"published":{"date-parts":[[2024,12,2]]},"assertion":[{"value":"2024-12-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}