{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T16:26:54Z","timestamp":1771518414246,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-C-0022"],"award-info":[{"award-number":["FA8750-16-C-0022"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1801545"],"award-info":[{"award-number":["CNS-1801545"]}],"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":[[2019,1,2]]},"abstract":"<jats:p>\n            This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enforcement library with the Yesod web programming framework. The implementation has two parts. First, we extract the core of LIO into a monad transformer (LMonad) and then apply it to Yesod\u2019s core monad. Second, we extend Yesod\u2019s table definition DSL and query functionality to permit defining and enforcing label-based policies on tables and enforcing them during query processing. LWeb\u2019s policy language is expressive, permitting dynamic per-table and per-row policies. We formalize the essence of LWeb in the \u03bb\n            <jats:sub>\n              <jats:italic>LWeb<\/jats:italic>\n            <\/jats:sub>\n            calculus and mechanize the proof of noninterference in Liquid Haskell. This mechanization constitutes the first metatheoretic proof carried out in Liquid Haskell. We also used LWeb to build a substantial web site hosting the Build it, Break it, Fix it security-oriented programming contest. The site involves 40 data tables and sophisticated policies. Compared to manually checking security policies, LWeb imposes a modest runtime overhead of between 2% to 21%. It reduces the trusted code base from the whole application to just 1% of the application code, and 21% of the code overall (when counting LWeb too).\n          <\/jats:p>","DOI":"10.1145\/3290388","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["LWeb: information flow security for multi-tier web applications"],"prefix":"10.1145","volume":"3","author":[{"given":"James","family":"Parker","sequence":"first","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}]},{"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103677"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465106.2465121"},{"key":"e_1_2_2_5_1","unstructured":"Pablo Buiras Joachim Breitner and Alejandro Russo. 2017. Securing concurrent lazy programs against information leakage. In CSF.  Pablo Buiras Joachim Breitner and Alejandro Russo. 2017. Securing concurrent lazy programs against information leakage. In CSF."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784758"},{"key":"e_1_2_2_7_1","unstructured":"Adam Chlipala. 2010. Static Checking of Dynamically-varying Security Policies in Database-backed Applications. In OSDI.   Adam Chlipala. 2010. Static Checking of Dynamically-varying Security Policies in Database-backed Applications. In OSDI."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294265"},{"key":"e_1_2_2_9_1","volume-title":"SIF: Enforcing Confidentiality and Integrity in Web Applications. In USENIX Security Symposium.","author":"Chong Stephen","unstructured":"Stephen Chong , K. Vikram , and Andrew C. Myers . 2007b . SIF: Enforcing Confidentiality and Integrity in Web Applications. In USENIX Security Symposium. Stephen Chong, K. Vikram, and Andrew C. Myers. 2007b. SIF: Enforcing Confidentiality and Integrity in Web Applications. In USENIX Security Symposium."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813684"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559845.1559875"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095813"},{"key":"e_1_2_2_14_1","unstructured":"Esqueleto 2018. Esqueleto: Type-safe EDSL for SQL queries on persistent backends. https:\/\/github.com\/bitemyapp\/esqueleto\/ blob\/master\/docs\/blog_post_2012_08_06 .  Esqueleto 2018. Esqueleto: Type-safe EDSL for SQL queries on persistent backends. https:\/\/github.com\/bitemyapp\/esqueleto\/ blob\/master\/docs\/blog_post_2012_08_06 ."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-15801"},{"key":"e_1_2_2_16_1","volume-title":"Hails: Protecting Data Privacy in Untrusted Web Applications. In OSDI.","author":"Giffin Daniel B.","year":"2012","unstructured":"Daniel B. Giffin , Amit Levy , Deian Stefan , David Terei , David Mazi\u00e8res , John C. Mitchell , and Alejandro Russo . 2012 . Hails: Protecting Data Privacy in Untrusted Web Applications. In OSDI. Daniel B. Giffin, Amit Levy, Deian Stefan, David Terei, David Mazi\u00e8res, John C. Mitchell, and Alejandro Russo. 2012. Hails: Protecting Data Privacy in Untrusted Web Applications. In OSDI."},{"key":"e_1_2_2_17_1","volume-title":"Goguen and Jos\u00c3\u013e Meseguer","author":"Joseph","year":"1982","unstructured":"Joseph A. Goguen and Jos\u00c3\u013e Meseguer . 1982 . Security Policies and Security Models. In S &amp;P. Joseph A. Goguen and Jos\u00c3\u013e Meseguer. 1982. Security Policies and Security Models. In S&amp;P."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-009-0086-1"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-160544"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_2"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737957"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89862-7_4"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294293"},{"key":"e_1_2_2_24_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR.","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino . 2010 . Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR. K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR."},{"key":"e_1_2_2_25_1","volume-title":"Arrows for Secure Information Flow. Theoretical Computer Science 411, 19","author":"Li Peng","year":"2010","unstructured":"Peng Li and Steve Zdancewic . 2010. Arrows for Secure Information Flow. Theoretical Computer Science 411, 19 ( 2010 ). Peng Li and Steve Zdancewic. 2010. Arrows for Secure Information Flow. Theoretical Computer Science 411, 19 (2010)."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-05119-2_11"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676994"},{"key":"e_1_2_2_28_1","volume-title":"USENIX Security Symposium.","author":"Mehta Aastha","year":"2017","unstructured":"Aastha Mehta , Eslam Elnikety , Katura Harvey , Deepak Garg , and Peter Druschel . 2017 . Qapla: Policy compliance for database-backed systems . In USENIX Security Symposium. Aastha Mehta, Eslam Elnikety, Katura Harvey, Deepak Garg, and Peter Druschel. 2017. Qapla: Policy compliance for database-backed systems. In USENIX Security Symposium."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813639"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292561"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542484"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978382"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784756"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411289"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1662658.1662659"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628151"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465351.2465357"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_2_2_41_1","unstructured":"Michael Snoyman. 2018. Yesod Web Framework for Haskell. http:\/\/www.yesodweb.com\/.  Michael Snoyman. 2018. Yesod Web Framework for Haskell. http:\/\/www.yesodweb.com\/."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29615-4_16"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000241"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034675.2034688"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.29"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364524"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897845.2897888"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993608"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122963"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134036"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908098"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103669"},{"key":"e_1_2_2_56_1","unstructured":"Nickolai Zeldovich Silas Boyd-Wickizer Eddie Kohler and David Mazi\u00e8res. 2006. Making Information Flow Explicit in HiStar. In OSDI.   Nickolai Zeldovich Silas Boyd-Wickizer Eddie Kohler and David Mazi\u00e8res. 2006. Making Information Flow Explicit in HiStar. In OSDI."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290388","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290388","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290388","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290388"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290388"],"URL":"https:\/\/doi.org\/10.1145\/3290388","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}