{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:15:49Z","timestamp":1763968549053,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":82,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T00:00:00Z","timestamp":1732147200000},"content-version":"vor","delay-in-days":372,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100007297","name":"Office of Naval Research Global","doi-asserted-by":"publisher","award":["N62909-18-1-2049"],"award-info":[{"award-number":["N62909-18-1-2049"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-1718713"],"award-info":[{"award-number":["CNS-1718713"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008812","name":"Defence Science and Technology Group","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100008812","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,11,15]]},"DOI":"10.1145\/3576915.3623141","type":"proceedings-article","created":{"date-parts":[[2023,11,21]],"date-time":"2023-11-21T12:35:13Z","timestamp":1700570113000},"page":"1746-1760","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8271-0289","authenticated-orcid":false,"given":"Toby","family":"Murray","sequence":"first","affiliation":[{"name":"University of Melbourne, Melbourne, VIC, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5373-9659","authenticated-orcid":false,"given":"Mukesh","family":"Tiwari","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3289-5764","authenticated-orcid":false,"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[{"name":"LMU Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7634-6150","authenticated-orcid":false,"given":"David A.","family":"Naumann","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, Hoboken, NJ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Martin Abadi Andy Chu Ian Goodfellow H Brendan McMahan Ilya Mironov Kunal Talwar and Li Zhang. 2016. Deep learning with differential privacy. In ACM CCS. 308--318.","DOI":"10.1145\/2976749.2978318"},{"key":"e_1_3_2_1_2_1","unstructured":"Jos\u00e9 Bacelar Almeida Manuel Barbosa Gilles Barthe Fran\u00e7ois Dupressoir and Michael Emmi. 2016. Verifying constant-time implementations. In USENIX Security. 53--70."},{"key":"e_1_3_2_1_3_1","volume-title":"White Paper. ARM","author":"Alves Tiago","year":"2004","unstructured":"Tiago Alves and Don Felton. 2004. TrustZone: Integrated Hardware and Software Security, White Paper. ARM, July (2004)."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Miguel E. Andr\u00e9s Nicol\u00e1s E. Bordenabe Konstantinos Chatzikokolakis and Catuscia Palamidessi. 2013. Geo-Indistinguishability: Differential Privacy for Location-Based Systems. In ACM CCS. 901--914.","DOI":"10.1145\/2508859.2516735"},{"volume-title":"Learning is change in knowledge: Knowledge-based security for dynamic policies","author":"Askarov Aslan","key":"e_1_3_2_1_5_1","unstructured":"Aslan Askarov and Stephen Chong. 2012. Learning is change in knowledge: Knowledge-based security for dynamic policies. In IEEE CSF. 308--322."},{"volume-title":"Hybrid Monitors for Concurrent Noninterference","author":"Askarov Aslan","key":"e_1_3_2_1_6_1","unstructured":"Aslan Askarov, Stephen Chong, and Heiko Mantel. 2015. Hybrid Monitors for Concurrent Noninterference. In IEEE CSF. 137--151."},{"key":"e_1_3_2_1_7_1","volume-title":"Gradual Release: Unifying Declassification, Encryption and Key Release Policies","author":"Askarov Aslan","year":"2007","unstructured":"Aslan Askarov and Andrei Sabelfeld. 2007. Gradual Release: Unifying Declassification, Encryption and Key Release Policies. In IEEE S&P. 207--221."},{"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 ACM PLAS.","DOI":"10.1145\/2166956.2166962"},{"volume-title":"Expressive declassification policies and modular static enforcement","author":"Banerjee Anindya","key":"e_1_3_2_1_9_1","unstructured":"Anindya Banerjee, David A Naumann, and Stan Rosenberg. 2008. Expressive declassification policies and modular static enforcement. In IEEE S&P. 339--353."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Marco Gaboardi Benjamin Gr\u00e9goire Justin Hsu and Pierre-Yves Strub. 2016. Proving differential privacy via probabilistic couplings. In LICS. 749--758.","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_2_1_11_1","volume-title":"Andrei Popescu, and Franco Raimondi.","author":"Bauerei\u00df Thomas","year":"2017","unstructured":"Thomas Bauerei\u00df, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. 2017. CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. In IEEE S&P. 729--748."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9443-3"},{"key":"e_1_3_2_1_13_1","volume-title":"End-to-end Multilevel Hybrid Information Flow Control. In Asian Symposium on Programming Languages and Systems (APLAS). 50--65","author":"Beringer Lennart","year":"2012","unstructured":"Lennart Beringer. 2012. End-to-end Multilevel Hybrid Information Flow Control. In Asian Symposium on Programming Languages and Systems (APLAS). 50--65."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22969-0_6"},{"key":"e_1_3_2_1_15_1","unstructured":"Ferdinand Brasser Urs M\u00fcller Alexandra Dmitrienko Kari Kostiainen Srdjan Capkun and Ahmad-Reza Sadeghi. 2017. Software Grand Exposure: SGX Cache Attacks Are Practical. In USENIX WOOT. 11."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Niklas Broberg and David Sands. 2009. Flow-sensitive semantics for dynamic information flow policies. In ACM PLAS. 101--112.","DOI":"10.1145\/1554339.1554352"},{"key":"e_1_3_2_1_17_1","first-page":"431","article-title":"Paralocks: role-based information flow control and beyond","volume":"45","author":"Broberg Niklas","year":"2010","unstructured":"Niklas Broberg and David Sands. 2010. Paralocks: role-based information flow control and beyond. In POPL, Vol. 45. 431--444.","journal-title":"POPL"},{"volume-title":"The anatomy and facets of dynamic policies","author":"Broberg Niklas","key":"e_1_3_2_1_18_1","unstructured":"Niklas Broberg, Bart van Delft, and David Sands. 2015. The anatomy and facets of dynamic policies. In IEEE CSF. 122--136."},{"key":"e_1_3_2_1_19_1","volume-title":"Michael Schwarz, Moritz Lipp","author":"Canella Claudio","year":"2019","unstructured":"Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Benjamin Von Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2019. A systematic evaluation of transient execution attacks and defenses. In USENIX Security. 249--266."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad S Wahby John Renner Benjamin Gr\u00e9goire Gilles Barthe Ranjit Jhala and Deian Stefan. 2019. FaCT: a DSL for timing-sensitive computation. In PLDI. 174--189.","DOI":"10.1145\/3314221.3314605"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Konstantinos Chatzikokolakis Catuscia Palamidessi and Marco Stronati. 2014. A Predictive Differentially-Private Mechanism for Mobility Traces. In PETS. 21--41.","DOI":"10.1007\/978-3-319-08506-7_2"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1257\/pandp.20191109"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Raj Chetty John N Friedman Nathaniel Hendren Maggie R Jones and Sonya R Porter. 2018. The opportunity atlas: Mapping the childhood roots of social mobility. Technical Report. National Bureau of Economic Research.","DOI":"10.3386\/w25147"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/qje\/qju022"},{"key":"e_1_3_2_1_25_1","volume-title":"Naumann","author":"Chudnov Andrey","year":"2014","unstructured":"Andrey Chudnov, George Kuan, and David A. Naumann. 2014. Information Flow Monitoring as Abstract Interpretation for Relational Logic. In IEEE CSF. 48--62."},{"volume-title":"Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies","author":"Chudnov Andrey","key":"e_1_3_2_1_26_1","unstructured":"Andrey Chudnov and David A Naumann. 2018. Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies. In IEEE CSF. 189--203."},{"key":"e_1_3_2_1_27_1","volume-title":"Formal Aspects in Sec. and Trust (LNCS)","volume":"5491","author":"Clark David","year":"2008","unstructured":"David Clark and Sebastian Hunt. 2008. Non-Interference for Deterministic Interactive Programs. In Formal Aspects in Sec. and Trust (LNCS), Vol. 5491."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"David Costanzo and Zhong Shao. 2014. A separation logic for enforcing declarative information flow control policies. In POST. 179--198.","DOI":"10.1007\/978-3-642-54792-8_10"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"David Costanzo Zhong Shao and Ronghui Gu. 2016. End-to-end verification of information-flow security for C and assembly programs. In PLDI. 648--664.","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Mads Dam. 2006. Decidability and proof systems for language-based noninterference relations. In POPL. 67--78.","DOI":"10.1145\/1111037.1111044"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.radonc.2019.11.019"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-140508"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Cynthia Dwork. 2006. Differential Privacy. In ICALP. 1--12.","DOI":"10.1007\/11787006_1"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0430-6"},{"volume-title":"Modular Product Programs","author":"Eilers Marco","key":"e_1_3_2_1_35_1","unstructured":"Marco Eilers, Peter M\u00fcller, and Samuel Hitz. 2018. Modular Product Programs. In ESOP. Springer, 502--529."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19849-6_4"},{"key":"e_1_3_2_1_37_1","volume-title":"SecCSL: Security Concurrent Separation Logic. In International Conference on Computer Aided Verification (CAV). 208--230","author":"Ernst Gidon","year":"2019","unstructured":"Gidon Ernst and Toby Murray. 2019. SecCSL: Security Concurrent Separation Logic. In International Conference on Computer Aided Verification (CAV). 208--230."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3-where programs meet provers. In ESOP. 125--128.","DOI":"10.1007\/978-3-642-37036-6_8"},{"volume-title":"Compositional Non-Interference for Fine-Grained Concurrent Programs","author":"Frumin Dan","key":"e_1_3_2_1_39_1","unstructured":"Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2021. Compositional Non-Interference for Fine-Grained Concurrent Programs. In IEEE S&P. 1416--1433."},{"volume-title":"Security Policies and Security Models","author":"Goguen Joseph","key":"e_1_3_2_1_40_1","unstructured":"Joseph Goguen and Jos\u00e9 Meseguer. 1982. Security Policies and Security Models. In IEEE S&P. 11--20."},{"key":"e_1_3_2_1_41_1","first-page":"171","article-title":"Precision and the conjunction rule in concurrent separation logic","volume":"276","author":"Gotsman Alexey","year":"2011","unstructured":"Alexey Gotsman, Josh Berdine, and Byron Cook. 2011. Precision and the conjunction rule in concurrent separation logic. ENTCS, Vol. 276 (2011), 171--190.","journal-title":"ENTCS"},{"key":"e_1_3_2_1_42_1","volume-title":"Chiron: Privacy-preserving machine learning as a service. arXiv preprint arXiv:1803.05961","author":"Hunt Tyler","year":"2018","unstructured":"Tyler Hunt, Congzheng Song, Reza Shokri, Vitaly Shmatikov, and Emmett Witchel. 2018. Chiron: Privacy-preserving machine learning as a service. arXiv preprint arXiv:1803.05961 (2018)."},{"key":"e_1_3_2_1_43_1","volume-title":"Efficient Deep Learning on Multi-Source Private Data. arxiv","author":"Hynes Nick","year":"1807","unstructured":"Nick Hynes, Raymond Cheng, and Dawn Song. 2018. Efficient Deep Learning on Multi-Source Private Data. arxiv: 1807.06689 [cs.LG]"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(3:19)2015"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Aleksandr Karbyshev Kasper Svendsen Aslan Askarov and Lars Birkedal. 2018. Compositional Non-Interference for Concurrent Programs via Separation and Framing. In POST.","DOI":"10.1007\/978-3-319-89722-6_3"},{"key":"e_1_3_2_1_47_1","unstructured":"David Kohlbrenner and Hovav Shacham. 2017. On the effectiveness of mitigations against floating-point timing channels. In USENIX Security. 69--81."},{"key":"e_1_3_2_1_48_1","volume-title":"Franz Gregor, Sergei Arnautov, Pramod Bhatotia, and Christof Fetzer.","author":"Kunkel Roland","year":"2019","unstructured":"Roland Kunkel, Do Le Quoc, Franz Gregor, Sergei Arnautov, Pramod Bhatotia, and Christof Fetzer. 2019. TensorSCONE: A Secure TensorFlow Framework using Intel SGX. arxiv: 1902.04413 [cs.CR]"},{"key":"e_1_3_2_1_49_1","unstructured":"Sangho Lee Ming-Wei Shih Prasun Gera Taesoo Kim Hyesoon Kim and Marcus Peinado. 2017. Inferring fine-grained control flow inside SGX enclaves with branch shadowing. In USENIX Security. 557--574."},{"key":"e_1_3_2_1_50_1","volume-title":"Dafny: An automatic program verifier for functional correctness. In LPAR. 348--370.","author":"Leino K Rustan M","year":"2010","unstructured":"K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In LPAR. 348--370."},{"key":"e_1_3_2_1_51_1","volume-title":"Usable Verification Workshop. http:\/\/fm.csl.sri.com\/UV10","author":"Leino K Rustan M","year":"2010","unstructured":"K Rustan M Leino and Micha\u0142 Moskal. 2010. Usable auto-active verification. In Usable Verification Workshop. http:\/\/fm.csl.sri.com\/UV10."},{"volume-title":"A Secure and Formally Verified Linux KVM Hypervisor","author":"Li Shih-Wei","key":"e_1_3_2_1_52_1","unstructured":"Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. A Secure and Formally Verified Linux KVM Hypervisor. In IEEE S&P."},{"volume-title":"Assumptions and Guarantees for Compositional Noninterference","author":"Mantel Heiko","key":"e_1_3_2_1_53_1","unstructured":"Heiko Mantel, David Sands, and Henning Sudbrock. 2011. Assumptions and Guarantees for Compositional Noninterference. In IEEE CSF. 218--232."},{"key":"e_1_3_2_1_54_1","volume-title":"Savagaonkar","author":"McKeen Frank","year":"2013","unstructured":"Frank McKeen, Ilya Alexandrovich, Alex Berenzon, Carlos V. Rozas, Hisham Shafi, Vedvyas Shanbhogue, and Uday R. Savagaonkar. 2013. Innovative Instructions and Software Model for Isolated Execution. In HASP. Article 10, 1 pages."},{"key":"e_1_3_2_1_55_1","volume-title":"PPFL: privacy-preserving federated learning with trusted execution environments. arXiv preprint arXiv:2104.14380","author":"Mo Fan","year":"2021","unstructured":"Fan Mo, Hamed Haddadi, Kleomenis Katevas, Eduard Marin, Diego Perino, and Nicolas Kourtellis. 2021. PPFL: privacy-preserving federated learning with trusted execution environments. arXiv preprint arXiv:2104.14380 (2021)."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66787-4_4"},{"key":"e_1_3_2_1_57_1","volume-title":"Nadia Heninger, Frank Piessens, and Berk Sunar.","author":"Moghimi Daniel","year":"2020","unstructured":"Daniel Moghimi, Jo Van Bulck, Nadia Heninger, Frank Piessens, and Berk Sunar. 2020. CopyCat: Controlled Instruction-Level Attacks on Enclaves. In USENIX Security. 469--486."},{"key":"e_1_3_2_1_58_1","volume-title":"Viper: A verification infrastructure for permission-based reasoning. In VMCAI. 41--62.","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J Summers. 2016. Viper: A verification infrastructure for permission-based reasoning. In VMCAI. 41--62."},{"volume-title":"seL4: from General Purpose to a Proof of Information Flow Enforcement","author":"Murray Toby","key":"e_1_3_2_1_59_1","unstructured":"Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. 2013. seL4: from General Purpose to a Proof of Information Flow Enforcement. In IEEE S&P. 415--429."},{"key":"e_1_3_2_1_60_1","volume-title":"COVERN: A Logic for Compositional Verification of Information Flow Control. In EuroS&P.","author":"Murray Toby","year":"2018","unstructured":"Toby Murray, Robert Sison, and Kai Engelhardt. 2018. COVERN: A Logic for Compositional Verification of Information Flow Control. In EuroS&P."},{"key":"e_1_3_2_1_61_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 (Extended Version). arxiv: 2309.03442 [cs.CR]"},{"volume-title":"IEEE Cybersecurity Development Conference (SecDev). IEEE.","author":"Murray Toby","key":"e_1_3_2_1_62_1","unstructured":"Toby Murray and Paul C. van Oorschot. 2018. BP: Formal Proofs, the Fine Print and Side Effects. In IEEE Cybersecurity Development Conference (SecDev). IEEE."},{"key":"e_1_3_2_1_63_1","volume-title":"International Conference on Concurrency Theory (CONCUR). Springer, 49--67","author":"O'Hearn Peter W","year":"2004","unstructured":"Peter W O'Hearn. 2004. Resources, concurrency and local reasoning. In International Conference on Concurrency Theory (CONCUR). Springer, 49--67."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_33"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"crossref","unstructured":"Willem Penninckx Amin Timany and Bart Jacobs. 2019. Specifying I\/O using abstract nested Hoare triples in separation logic. In FTfJP. 1--7.","DOI":"10.1145\/3340672.3341118"},{"key":"e_1_3_2_1_66_1","unstructured":"Andrei Popescu Thomas Bauereiss and Peter Lammich. 2021a. Bounded-deducibility security. In ITP."},{"key":"e_1_3_2_1_67_1","volume-title":"CoCon: A conference management system with formally verified document confidentiality. J. Automated Reasoning","volume":"65","author":"Popescu Andrei","year":"2021","unstructured":"Andrei Popescu, Peter Lammich, and Ping Hou. 2021b. CoCon: A conference management system with formally verified document confidentiality. J. Automated Reasoning, Vol. 65, 2 (2021), 321--356."},{"key":"e_1_3_2_1_68_1","volume-title":"Frontal Attack: Leaking Control-Flow in SGX via the CPU Frontend. In USENIX Security. 663--680.","author":"Puddu Ivan","year":"2020","unstructured":"Ivan Puddu, Moritz Schneider, Miro Haller, and Srdjan Capkun. 2020. Frontal Attack: Leaking Control-Flow in SGX via the CPU Frontend. In USENIX Security. 663--680."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"crossref","unstructured":"John C Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. 55--74.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_70_1","unstructured":"Alejandro Russo. 2008. Language Support for Controlling Timing-Based Covert Channels. Ph.D. Dissertation. Chalmers University of Technology."},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2000.856937"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/1662658.1662659"},{"volume-title":"textscVERONICA: Expressive and Precise Concurrent Information Flow Security","author":"Schoepe Daniel","key":"e_1_3_2_1_73_1","unstructured":"Daniel Schoepe, Toby Murray, and Andrei Sabelfeld. 2020. textscVERONICA: Expressive and Precise Concurrent Information Flow Security. In IEEE CSF. 79--94."},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"crossref","unstructured":"Basavesh Ammanaghatta Shivakumar Gilles Barthe Benjamin Gr\u00e9goire Vincent Laporte and Swarn Priya. 2022. Enforcing Fine-grained Constant-time Policies. In ACM CCS. 83--96.","DOI":"10.1145\/3548606.3560689"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"crossref","unstructured":"Graeme Smith. 2022. Declassification Predicates for Controlled Information Release. In ICFEM. 298--315.","DOI":"10.1007\/978-3-031-17244-1_18"},{"key":"e_1_3_2_1_76_1","volume-title":"International Conference on Learning Representations (ICLR). https:\/\/arxiv.org\/abs\/1806","author":"Tram\u00e8r Florian","year":"2019","unstructured":"Florian Tram\u00e8r and Dan Boneh. 2019. Slalom: Fast, Verifiable and Private Execution of Neural Networks in Trusted Hardware. arXiv preprint arXiv:1806.03287. In International Conference on Learning Representations (ICLR). https:\/\/arxiv.org\/abs\/1806.03287"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"crossref","unstructured":"Viktor Vafeiadis. 2011. Concurrent Separation Logic and Operational Semantics. In Mathematical Foundations of Programming Semantics (MFPS). 335--351.","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"crossref","unstructured":"Bart van Delft Sebastian Hunt and David Sands. 2015. Very static enforcement of dynamic policies. In POST. 32--52.","DOI":"10.1007\/978-3-662-46666-7_3"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2020.2988575"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485476"},{"key":"e_1_3_2_1_81_1","unstructured":"Jean Yang. 2015. Preventing information leaks with policy-agnostic programming. Ph.D. Dissertation. Massachusetts Institute of Technology."},{"key":"e_1_3_2_1_82_1","volume-title":"Int. Symp. on Trustworthy Global Computing (TGC). 227--241","author":"Zhang Chenyi","year":"2011","unstructured":"Chenyi Zhang. 2011. Conditional information flow policies and unwinding relations. In Int. Symp. on Trustworthy Global Computing (TGC). 227--241."}],"event":{"name":"CCS '23: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Copenhagen Denmark","acronym":"CCS '23"},"container-title":["Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623141","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3576915.3623141","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3576915.3623141","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T01:43:54Z","timestamp":1755740634000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623141"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,15]]},"references-count":82,"alternative-id":["10.1145\/3576915.3623141","10.1145\/3576915"],"URL":"https:\/\/doi.org\/10.1145\/3576915.3623141","relation":{},"subject":[],"published":{"date-parts":[[2023,11,15]]},"assertion":[{"value":"2023-11-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}