{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T05:49:06Z","timestamp":1784180946566,"version":"3.55.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1763922"],"award-info":[{"award-number":["1763922"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            Languages with gradual information-flow control combine static and dynamic techniques to prevent security leaks. Gradual languages should satisfy the gradual guarantee: programs that only differ in the precision of their type annotations should behave the same modulo cast errors. Unfortunately,\n            <jats:xref ref-type=\"bibr\">Toro et al.<\/jats:xref>\n            [\n            <jats:xref ref-type=\"bibr\">2018<\/jats:xref>\n            ] identify a tension between the gradual guarantee and information security; they were unable to satisfy both properties in the language GSL\n            <jats:monospace>\n              <jats:sub>Ref<\/jats:sub>\n            <\/jats:monospace>\n            and had to settle for only satisfying information-flow security.\n            <jats:xref ref-type=\"bibr\">Azevedo de Amorim et al.<\/jats:xref>\n            [\n            <jats:xref ref-type=\"bibr\">2020<\/jats:xref>\n            ] show that by sacrificing type-guided classification, one obtains a language that satisfies both noninterference and the gradual guarantee.\n            <jats:xref ref-type=\"bibr\">Bichhawat et al.<\/jats:xref>\n            [\n            <jats:xref ref-type=\"bibr\">2021<\/jats:xref>\n            ] show that both properties can be satisfied by sacrificing the no-sensitive-upgrade mechanism, replacing it with a static analysis.\n          <\/jats:p>\n          <jats:p>\n            In this paper we present a language design,\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi>\u03bb<\/mml:mi>\n                  <mml:mrow>\n                    <mml:mtext>IFC<\/mml:mtext>\n                  <\/mml:mrow>\n                  <mml:mo>\u2605<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , that satisfies both noninterference and the gradual guarantee without making any sacrifices. We keep the type-guided classification of GSL\n            <jats:monospace>\n              <jats:sub>Ref<\/jats:sub>\n            <\/jats:monospace>\n            and use the standard no-sensitive-upgrade mechanism to prevent implicit flows through mutable references. The key to the design of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi>\u03bb<\/mml:mi>\n                  <mml:mrow>\n                    <mml:mtext>IFC<\/mml:mtext>\n                  <\/mml:mrow>\n                  <mml:mo>\u2605<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            is to walk back the decision in GSL\n            <jats:monospace>\n              <jats:sub>Ref<\/jats:sub>\n            <\/jats:monospace>\n            to include the unknown label\n            <jats:styled-content style=\"color:brown\">\u2605<\/jats:styled-content>\n            among the runtime security labels. We give a formal definition of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi>\u03bb<\/mml:mi>\n                  <mml:mrow>\n                    <mml:mtext>IFC<\/mml:mtext>\n                  <\/mml:mrow>\n                  <mml:mo>\u2605<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , prove the gradual guarantee, and prove noninterference. Of technical note, the semantics of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi>\u03bb<\/mml:mi>\n                  <mml:mrow>\n                    <mml:mtext>IFC<\/mml:mtext>\n                  <\/mml:mrow>\n                  <mml:mo>\u2605<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            is the first gradual information-flow control language to be specified using coercion calculi (a la Henglein), thereby expanding the coercion-based theory of gradual typing.\n          <\/jats:p>","DOI":"10.1145\/3656442","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1609-1632","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Quest Complete: The Holy Grail of Gradual Security"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-3279-5971","authenticated-orcid":false,"given":"Tianyu","family":"Chen","sequence":"first","affiliation":[{"name":"Indiana University, Bloomington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9894-4856","authenticated-orcid":false,"given":"Jeremy G.","family":"Siek","sequence":"additional","affiliation":[{"name":"Indiana University, Bloomington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Aslan Askarov and Andrei Sabelfeld. 2009. Tight Enforcement of Information-Release Policies for Dynamic Languages. In 2009 22nd IEEE Computer Security Foundations Symposium. 43\u201359. https:\/\/doi.org\/10.1109\/CSF.2009.22 10.1109\/CSF.2009.22","DOI":"10.1109\/CSF.2009.22"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","unstructured":"Thomas H Austin and Cormac Flanagan. 2009. Efficient purely-dynamic information flow analysis. In Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security. 113\u2013124. https:\/\/doi.org\/10.1145\/1554339.1554353 10.1145\/1554339.1554353","DOI":"10.1145\/1554339.1554353"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3024086"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Arthur Azevedo de Amorim Matt Fredrikson and Limin Jia. 2020. Reconciling noninterference and gradual typing. In Logic in Computer Science (LICS). https:\/\/doi.org\/10.1145\/3373718.3394778 10.1145\/3373718.3394778","DOI":"10.1145\/3373718.3394778"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","unstructured":"Abhishek Bichhawat McKenna McCall and Limin Jia. 2021. Gradual Security Types and Gradual Guarantees. In 2021 IEEE 34th Computer Security Foundations Symposium (CSF). IEEE 1\u201316. https:\/\/doi.org\/10.1109\/CSF51468.2021.00015 10.1109\/CSF51468.2021.00015","DOI":"10.1109\/CSF51468.2021.00015"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784758"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Deepak Chandra and Michael Franz. 2007. Fine-Grained Information Flow Analysis and Enforcement in a Java Virtual Machine. In Twenty-Third Annual Computer Security Applications Conference (ACSAC 2007). 463\u2013475. https:\/\/doi.org\/10.1109\/ACSAC.2007.37 10.1109\/ACSAC.2007.37","DOI":"10.1109\/ACSAC.2007.37"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","unstructured":"Tianyu Chen. 2024. cty12\/pldi2024-ae: PLDI Release 2. https:\/\/doi.org\/10.5281\/zenodo.10933110 10.5281\/zenodo.10933110.","DOI":"10.5281\/zenodo.10933110"},{"key":"e_1_3_2_10_1","unstructured":"Tianyu Chen and Jeremy G. Siek. 2022. Mechanized Noninterference for Gradual Security. arXiv:2211.15745 [cs.PL]"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Dominique Devriese and Frank Piessens. 2010. Noninterference through Secure Multi-execution. In 2010 IEEE Symposium on Security and Privacy. 109\u2013124. https:\/\/doi.org\/10.1109\/SP.2010.15 10.1109\/SP.2010.15","DOI":"10.1109\/SP.2010.15"},{"key":"e_1_3_2_13_1","unstructured":"Tim Disney and Cormac Flanagan. 2011. Gradual Information Flow Typing. In Workshop on Script to Program Evolution."},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","unstructured":"L. Fennell and P. Thiemann. 2013. Gradual Security Typing with References. In 2013 IEEE 26th Computer Security Foundations Symposium. 224\u2013239. https:\/\/doi.org\/10.1109\/CSF.2013.22 10.1109\/CSF.2013.22","DOI":"10.1109\/CSF.2013.22"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","unstructured":"Luminous Fennell and Peter Thiemann. 2015. LJGS: Gradual Security Types for Object-Oriented Languages. In Workshop on Foundations of Computer Security (FCS). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2016.9 10.4230\/LIPIcs.ECOOP.2016.9","DOI":"10.4230\/LIPIcs.ECOOP.2016.9"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","unstructured":"Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for Higher-Order Functions. Technical Report NU-CCS-02-05. Northeastern University. https:\/\/doi.org\/10.1145\/2502508.2502521 10.1145\/2502508.2502521","DOI":"10.1145\/2502508.2502521"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_3_2_18_1","unstructured":"Michael Greenberg. 2014. Space-Efficient Manifest Contracts. CoRR abs\/1410.2813 (2014). http:\/\/arxiv.org\/abs\/1410.2813"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"Gurvan Le Guernic. 2007. Automaton-based confidentiality monitoring of concurrent programs. In 20th IEEE Computer Security Foundations Symposium (CSF\u201907). IEEE 218\u2013232. https:\/\/doi.org\/10.1109\/CSF.2007.10 10.1109\/CSF.2007.10","DOI":"10.1109\/CSF.2007.10"},{"key":"e_1_3_2_22_1","unstructured":"Gurvan Le Guernic and Thomas Jensen. 2005. Monitoring information flow. In Proc. Workshop on Foundations of Computer Security. 19\u201330."},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.01.025"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","unstructured":"Scott Moore and Stephen Chong. 2011. Static analysis for efficient hybrid information-flow control. In 2011 IEEE 24th Computer Security Foundations Symposium. IEEE 146\u2013160. https:\/\/doi.org\/10.1109\/CSF.2011.17 10.1109\/CSF.2011.17","DOI":"10.1109\/CSF.2011.17"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Andrew C Myers. 1999. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages. 228\u2013241. https:\/\/doi.org\/10.1145\/292540.292561 10.1145\/292540.292561","DOI":"10.1145\/292540.292561"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/269005.266669"},{"key":"e_1_3_2_27_1","unstructured":"Andrew C. Myers Lantian Zheng Steve Zdancewic Stephen Chong and Nathaniel Nystrom. 2006. Jif 3.0: Java information flow. http:\/\/www.cs.cornell.edu\/jif"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Alejandro Russo and Andrei Sabelfeld. 2010. Dynamic vs. static flow-sensitive security analysis. In 2010 23rd IEEE Computer Security Foundations Symposium. IEEE 186\u2013199. https:\/\/doi.org\/10.1109\/CSF.2010.20 10.1109\/CSF.2010.20","DOI":"10.1109\/CSF.2010.20"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.20"},{"key":"e_1_3_2_30_1","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Scheme and Functional Programming Workshop. 81\u201392."},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","unstructured":"Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. In European Conference on Object-Oriented Programming (LCNS Vol. 4609). 2\u201327. https:\/\/doi.org\/10.1007\/978-3-540-73589-2_2 10.1007\/978-3-540-73589-2_2","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","unstructured":"Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In SNAPL: Summit on Advances in Programming Languages (LIPIcs: Leibniz International Proceedings in Informatics). https:\/\/doi.org\/10.4230\/LIPIcs.SNAPL.2015.274 10.4230\/LIPIcs.SNAPL.2015.274","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000241"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"Deian Stefan Alejandro Russo John C Mitchell and David Mazi\u00e8res. 2011. Flexible dynamic information flow control in Haskell. In Proceedings of the 4th ACM symposium on Haskell. 95\u2013106.https:\/\/doi.org\/10.1145\/2034675.2034688 10.1145\/2034675.2034688","DOI":"10.1145\/2034675.2034688"},{"key":"e_1_3_2_35_1","unstructured":"Deian Stefan Alejandro Russo John C Mitchell and David Mazi\u00e8res. 2012. Flexible dynamic information flow control in the presence of exceptions. arXiv preprint arXiv:1207.1457 (2012)."},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","unstructured":"Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme. In Symposium on Principles of Programming Languages. https:\/\/doi.org\/10.1145\/1328897.1328486 10.1145\/1328897.1328486","DOI":"10.1145\/1328897.1328486"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"Philip Wadler and Robert Bruce Findler. 2009. Well-typed programs can\u2019t be blamed. In European Symposium on Programming (ESOP). 1\u201316. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_1 10.1007\/978-3-642-00590-9_1","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"Preston Tunnell Wilson Ben Greenman Justin Pombrio and Shriram Krishnamurthi. 2018. The Behavior of Gradual Types A User Study. In Dynamic Languages Symposium. https:\/\/doi.org\/10.1145\/3393673.3276947 10.1145\/3393673.3276947","DOI":"10.1145\/3393673.3276947"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00002"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656442","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656442","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:41:22Z","timestamp":1751661682000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656442"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":41,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656442"],"URL":"https:\/\/doi.org\/10.1145\/3656442","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}