{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:06:52Z","timestamp":1755839212042,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>We present Security Relaxed Separation Logic (SecRSL), a separation logic for proving information-flow security of C11 programs in the Release-Acquire fragment with relaxed accesses. SecRSL is the first security logic that (1) supports weak-memory reasoning about programs in a high-level language; (2) inherits separation logic\u2019s virtues of compositional, local reasoning about (3) expressive security policies like value-dependent classification.<\/jats:p>\n          <jats:p>SecRSL is also, to our knowledge, the first security logic developed over an axiomatic memory model. Thus we also present the first definitions of information-flow security for an axiomatic weak memory model, against which we prove SecRSL sound. SecRSL ensures that programs satisfy a constant-time security guarantee, while being free of undefined behaviour.<\/jats:p>\n          <jats:p>We apply SecRSL to implement and verify the functional correctness and constant-time security of a range of concurrency primitives, including a spinlock module, a mixed-sensitivity mutex, and multiple synchronous channel implementations. Empirical performance evaluations of the latter demonstrate SecRSL\u2019s power to support the development of secure and performant concurrent C programs.<\/jats:p>","DOI":"10.1145\/3485476","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["SecRSL: security separation logic for C11 release-acquire concurrency"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0396-8343","authenticated-orcid":false,"given":"Pengbo","family":"Yan","sequence":"first","affiliation":[{"name":"University of Melbourne, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8271-0289","authenticated-orcid":false,"given":"Toby","family":"Murray","sequence":"additional","affiliation":[{"name":"University of Melbourne, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1991.151568"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2017.10.004"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07734-5_11"},{"volume-title":"Proceedings of the ACM on Programming Languages, 4, POPL","year":"2019","author":"Barthe Gilles","key":"e_1_2_2_5_1"},{"volume-title":"Proceedings of the ACM on Programming Languages, 2, POPL","year":"2017","author":"Barthe Gilles","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_17"},{"volume-title":"SecCSL: Security Concurrent Separation Logic. In International Conference on Computer Aided Verification (CAV). 208\u2013230","year":"2019","author":"Ernst Gidon","key":"e_1_2_2_13_1"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"volume-title":"Compositional Non-Interference for Fine-Grained Concurrent Programs. In IEEE Symposium on Security & Privacy (S&P). To appear.","year":"2021","author":"Frumin Dan","key":"e_1_2_2_15_1"},{"volume-title":"Security Policies and Security Models. In IEEE Symposium on Security & Privacy (S&P). IEEE Computer Society","year":"1982","author":"Goguen Joseph","key":"e_1_2_2_16_1"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_12"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_3"},{"volume-title":"Dependent Information Flow Types. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","year":"2015","author":"Louren\u00e7o Lu\u00edsa","key":"e_1_2_2_19_1"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"volume-title":"Proceedings of the ACM on Programming Languages, 4, POPL","year":"2019","author":"Maillard Kenji","key":"e_1_2_2_21_1"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.14"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.017"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12459-4_7"},{"volume-title":"COVERN: A Logic for Compositional Verification of Information Flow Control. In IEEE European Symposium on Security and Privacy (EuroS&P)","year":"2018","author":"Murray Toby","key":"e_1_2_2_26_1"},{"volume-title":"Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. In IEEE Computer Security Foundations Symposium (CSF). 417\u2013431","year":"2016","author":"Murray Toby","key":"e_1_2_2_27_1"},{"volume-title":"International Conference on Concurrency Theory (CONCUR). 49\u201367","year":"2004","author":"O\u2019Hearn Peter W","key":"e_1_2_2_28_1"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58618-0_55"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1995.398927"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480929"},{"volume-title":"VERONICA: Expressive and Precise Concurrent Information Flow Security. In IEEE Computer Security Foundations Symposium (CSF). 79\u201394","year":"2020","author":"Schoepe Daniel","key":"e_1_2_2_32_1"},{"volume-title":"International Conference on Interactive Theorem Proving (ITP). 27:1\u201327:19","year":"2019","author":"Sison Robert","key":"e_1_2_2_33_1"},{"volume-title":"Value-Dependent Information-Flow Security on Weak Memory Models. In International Symposium on Formal Methods (FM). 539\u2013555","year":"2019","author":"Smith Graeme","key":"e_1_2_2_34_1"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.9"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"Viktor Vafeiadis. 2011. Concurrent Separation Logic and Operational Semantics. In Mathematical Foundations of Programming Semantics (MFPS). 335\u2013351.  Viktor Vafeiadis. 2011. Concurrent Separation Logic and Operational Semantics. In Mathematical Foundations of Programming Semantics (MFPS). 335\u2013351.","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.20"},{"key":"e_1_2_2_39_1","unstructured":"Jaroslav \u0160ev\u010d\u00edk and Peter Sewell. 2016. C\/C++11 mappings to processors. https:\/\/www.cl.cam.ac.uk\/ pes20\/cpp\/cpp0xmappings.html  Jaroslav \u0160ev\u010d\u00edk and Peter Sewell. 2016. C\/C++11 mappings to processors. https:\/\/www.cl.cam.ac.uk\/ pes20\/cpp\/cpp0xmappings.html"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5493554"},{"key":"e_1_2_2_41_1","unstructured":"Pengbo Yan and Toby Murray. 2021. SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices). arxiv:2109.03602.  Pengbo Yan and Toby Murray. 2021. SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices). arxiv:2109.03602."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485476","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485476","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:15Z","timestamp":1750188615000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485476"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":42,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485476"],"URL":"https:\/\/doi.org\/10.1145\/3485476","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}