{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T17:13:23Z","timestamp":1718903603247},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,12,13]],"date-time":"2018-12-13T00:00:00Z","timestamp":1544659200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"CONICYT FONDECYT Regular Project","award":["1150017"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2018,12,31]]},"abstract":"In security-typed programming languages, types statically enforce noninterference between potentially conspiring values, such as the arguments and results of functions. But to adopt static security types, like other advanced type disciplines, programmers face a steep wholesale transition, often forcing them to refactor working code just to satisfy their type checker. To provide a gentler path to security typing that supports safe and stylish but hard-to-verify programming idioms, researchers have designed languages that blend static and dynamic checking of security types. Unfortunately, most of the resulting languages only support static, type-based reasoning about noninterference if a program is entirely statically secured. This limitation substantially weakens the benefits that dynamic enforcement brings to static security typing. Additionally, current proposals are focused on languages with explicit casts and therefore do not fulfill the vision of gradual typing, according to which the boundaries between static and dynamic checking only arise from the (im)precision of type annotations and are transparently mediated by implicit checks.<\/jats:p>\n \n In this article, we present GSL\n Ref<\/jats:sub>\n , a gradual security-typed higher-order language with references. As a gradual language, GSL\n Ref<\/jats:sub>\n supports the range of static-to-dynamic security checking exclusively driven by type annotations, without resorting to explicit casts. Additionally, GSL\n Ref<\/jats:sub>\n lets programmers use types to reason statically about termination-insensitive noninterference in\n all<\/jats:italic>\n programs, even those that enforce security dynamically. We prove that GSL\n Ref<\/jats:sub>\n satisfies all but one of Siek et al.\u2019s criteria for gradually-typed languages, which ensure that programs can seamlessly transition between simple typing and security typing. A notable exception regards the dynamic gradual guarantee, which some specific programs must violate if they are to satisfy noninterference; it remains an open question whether such a language could fully satisfy the dynamic gradual guarantee. To realize this design, we were led to draw a sharp distinction between syntactic type\n safety<\/jats:italic>\n and semantic type\n soundness<\/jats:italic>\n , each of which constrains the design of the gradual language.\n <\/jats:p>","DOI":"10.1145\/3229061","type":"journal-article","created":{"date-parts":[[2018,12,13]],"date-time":"2018-12-13T15:45:03Z","timestamp":1544715903000},"page":"1-55","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Type-Driven Gradual Security with References"],"prefix":"10.1145","volume":"40","author":[{"given":"Mat\u00edas","family":"Toro","sequence":"first","affiliation":[{"name":"PLEIAD Laboratory, Computer Science Department (DCC), University of Chile, Beauchef, Santiago, Chile"}]},{"given":"Ronald","family":"Garcia","sequence":"additional","affiliation":[{"name":"Software Practices Laboratory, University of British Columbia, Vancouver, Canada"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"PLEIAD Laboratory, Computer Science Department (DCC), University of Chile, Beauchef, Santiago, Chile"}]}],"member":"320","published-online":{"date-parts":[[2018,12,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1554339.1554353"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1814217.1814220"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103677"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3024086"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628149"},{"key":"e_1_2_2_10_1","volume-title":"Gradual type-and-effect systems. J. Funct. Program. 26 (Sept","author":"Schwerter Felipe Ba\u00f1ados","year":"2016","unstructured":"Felipe Ba\u00f1ados Schwerter, Ronald Garcia, and \u00c9ric Tanter. 2016. Gradual type-and-effect systems. J. Funct. Program. 26 (Sept. 2016), 19:1--19:69."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784758"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the 23rd Annual Computer Security Applications Conference (ACSAC\u201907)","author":"Chandra D.","unstructured":"D. Chandra and M. Franz. 2007. Fine-grained information flow analysis and enforcement in a Java virtual machine. In Proceedings of the 23rd Annual Computer Security Applications Conference (ACSAC\u201907). 463--475."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_2_2_18_1","volume-title":"Proceedings of the International Workshop on Scripts to Programs.","author":"Disney Tim","year":"2011","unstructured":"Tim Disney and Cormac Flanagan. 2011. Gradual information flow typing. In Proceedings of the International Workshop on Scripts to Programs."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.22"},{"key":"e_1_2_2_20_1","volume-title":"Proceedings of the 30th European Conference on Object-oriented Programming (ECOOP\u201916)","author":"Fennell Luminous","year":"2016","unstructured":"Luminous Fennell and Peter Thiemann. 2016. LJGS: Gradual security types for object-oriented languages. In Proceedings of the 30th European Conference on Object-oriented Programming (ECOOP\u201916) (LNCS). Springer-Verlag, Rome, Italy."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_23_1","unstructured":"Ronald Garcia and \u00c9ric Tanter. 2015. Deriving a Simple Gradual Security Language. Retrieved from http:\/\/arxiv.org\/abs\/1511.01399."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319848"},{"key":"e_1_2_2_26_1","volume-title":"Proceedings of the 1982 IEEE Symposium on Security and Privacy. 11--20","author":"Joseph","unstructured":"Joseph A. Goguen and Jos\u00e9 Meseguer. 1982. Security policies and security models. In Proceedings of the 1982 IEEE Symposium on Security and Privacy. 11--20."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.19"},{"key":"e_1_2_2_28_1","volume-title":"NATO Science for Peace and Security Series D: Information and Communication Security","author":"Hedin Daniel","unstructured":"Daniel Hedin and Andrei Sabelfeld. 2012b. A perspective on information-flow control. In NATO Science for Peace and Security Series D: Information and Communication Security. IOS Press, 319--347."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268976"},{"key":"e_1_2_2_30_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"Howard William A.","year":"1969","unstructured":"William A. Howard. 1980. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, J. P. Seldin and J. R. Hindley (Eds.). Academic Press, New York, 479--490. Reprint of 1969 article."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111045"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110284"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009865"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.17"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292561"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266669"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363526"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_2_2_41_1","volume-title":"Proceedings of the IFIP Congress. 513--523","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In Proceedings of the IFIP Congress. 513--523."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.20"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/1662658.1662659"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_29"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.20"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_2_49_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop. 81--92","author":"Jeremy","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop. 81--92."},{"key":"e_1_2_2_50_1","volume-title":"Proceedings of the 1st Summit on Advances in Programming Languages (SNAPL\u201915)","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined criteria for gradual typing. In Proceedings of the 1st Summit on Advances in Programming Languages (SNAPL\u201915). 274--293."},{"key":"e_1_2_2_51_1","volume-title":"Flexible dynamic information flow control in the presence of exceptions. J. Funct. Program. 27","author":"Stefan Deian","year":"2017","unstructured":"Deian Stefan, David Mazi\u00e8res, John C. Mitchell, and Alejandro Russo. 2017. Flexible dynamic information flow control in the presence of exceptions. J. Funct. Program. 27 (2017)."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_4"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814315"},{"key":"e_1_2_2_55_1","volume-title":"Proceedings of the 24th Static Analysis Symposium (SAS\u201917)","volume":"10422","author":"Mat\u00edas","unstructured":"Mat\u00edas Toro and \u00c9ric Tanter. 2017. A gradual interpretation of union types. In Proceedings of the 24th Static Analysis Symposium (SAS\u201917) (Lecture Notes in Computer Science), Vol. 10422. Springer-Verlag, New York City, NY, 382--404."},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032497.2032529"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.5555\/645395.651931"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0019-9"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3229061","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:14:45Z","timestamp":1707520485000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3229061"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,13]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,12,31]]}},"alternative-id":["10.1145\/3229061"],"URL":"https:\/\/doi.org\/10.1145\/3229061","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12,13]]},"assertion":[{"value":"2017-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}