{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T10:59:59Z","timestamp":1777805999345,"version":"3.51.4"},"reference-count":52,"publisher":"SAGE Publications","issue":"5","license":[{"start":{"date-parts":[[2016,9,5]],"date-time":"2016-09-05T00:00:00Z","timestamp":1473033600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2016,11,8]]},"abstract":"<jats:p>Web applications written in JavaScript are regularly used for dealing with sensitive or personal data. Consequently, reasoning about their security properties has become an important problem, which is made very difficult by the highly dynamic nature of the language, particularly its support for runtime code generation via eval. In order to deal with this, we propose to investigate security analyses for languages with more principled forms of dynamic code generation.<\/jats:p>\n                  <jats:p>To this end, we present a static information flow analysis for a dynamically typed functional language with prototype-based inheritance and staged metaprogramming. We prove its soundness, implement it and test it on various examples designed to show its relevance to proving security properties, such as noninterference, in JavaScript. To demonstrate the applicability of the analysis, we also present a general method for transforming a program using eval into one using staged metaprogramming.<\/jats:p>\n                  <jats:p>To our knowledge, this is the first fully static information flow analysis for a language with staged metaprogramming, and the first formal soundness proof of a CFA-based information flow analysis for a functional programming language.<\/jats:p>","DOI":"10.3233\/jcs-160557","type":"journal-article","created":{"date-parts":[[2016,9,6]],"date-time":"2016-09-06T11:36:53Z","timestamp":1473161813000},"page":"541-582","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["Information flow analysis for a dynamically typed language with staged metaprogramming"],"prefix":"10.1177","volume":"24","author":[{"given":"Martin","family":"Lester","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Parks Road, Oxford, OX1 3QD, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luke","family":"Ong","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Parks Road, Oxford, OX1 3QD, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Max","family":"Sch\u00e4fer","sequence":"additional","affiliation":[{"name":"Semmle Limited, Blue Boar Court, 9 Alfred Street, Oxford, OX1 4EH, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2016,9,5]]},"reference":[{"key":"ref001","doi-asserted-by":"crossref","unstructured":"M.\u00a0Abadi, A.\u00a0Banerjee, N.\u00a0Heintze and J.G.\u00a0Riecke, A core calculus of dependency, in: POPL, 1999, pp.\u00a0147\u2013160.","DOI":"10.1145\/292540.292555"},{"key":"ref002","doi-asserted-by":"crossref","unstructured":"T.H.\u00a0Austin and C.\u00a0Flanagan, Multiple facets for dynamic information flow, in: POPL, 2012, pp.\u00a0165\u2013178.","DOI":"10.1145\/2103656.2103677"},{"key":"ref003","doi-asserted-by":"crossref","unstructured":"M.\u00a0Berger and L.\u00a0Tratt, Program logics for homogeneous meta-programming, in: LPAR (Dakar), E.M.\u00a0Clarke and A.\u00a0Voronkov, eds, Lecture Notes in Computer Science, Vol.\u00a06355, Springer, 2010, pp.\u00a064\u201381.","DOI":"10.1007\/978-3-642-17511-4_5"},{"key":"ref004","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bohannon, B.C.\u00a0Pierce, V.\u00a0Sj\u00f6berg, S.\u00a0Weirich and S.\u00a0Zdancewic, Reactive noninterference, in: Computer and Communications Security, 2009, pp.\u00a079\u201390.","DOI":"10.1145\/1653662.1653673"},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"J.\u00a0Cheney, S.\u00a0Lindley and P.\u00a0Wadler, A practical theory of language-integrated query, in: ACM SIGPLAN International Conference on Functional Programming, ICFP\u201913, Boston, MA, USA, September 25\u201327, 2013, G.\u00a0Morrisett and T.\u00a0Uustalu, eds, ACM, 2013, pp.\u00a0403\u2013416. doi:10.1145\/2500365.2500586.","DOI":"10.1145\/2500365.2500586"},{"key":"ref006","doi-asserted-by":"crossref","unstructured":"T.H.\u00a0Choi, O.\u00a0Lee, H.\u00a0Kim and K.G.\u00a0Doh, A practical string analyzer by the widening approach, in: APLAS, 2006, pp.\u00a0374\u2013388.","DOI":"10.1007\/11924661_23"},{"key":"ref007","doi-asserted-by":"crossref","unstructured":"W.\u00a0Choi, B.\u00a0Aktemur, K.\u00a0Yi and M.\u00a0Tatsuta, Static analysis of multi-staged programs via unstaging translation, in: POPL, 2011, pp.\u00a081\u201392.","DOI":"10.1145\/1925844.1926397"},{"key":"ref008","doi-asserted-by":"crossref","unstructured":"A.S.\u00a0Christensen, A.\u00a0M\u00f8ller and M.I.\u00a0Schwartzbach, Precise analysis of string expressions, in: Proceedings of the Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11\u201313, 2003, R.\u00a0Cousot, ed. Lecture Notes in Computer Science, Vol.\u00a02694, Springer, 2003, pp.\u00a01\u201318.","DOI":"10.1007\/3-540-44898-5_1"},{"key":"ref009","doi-asserted-by":"crossref","unstructured":"R.\u00a0Chugh, J.A.\u00a0Meister, R.\u00a0Jhala and S.\u00a0Lerner, Staged information flow for JavaScript, in: PLDI, 2009, pp.\u00a050\u201362. doi:10.1145\/1542476.1542483.","DOI":"10.1145\/1542476.1542483"},{"key":"ref010","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"ref011","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"ref012","doi-asserted-by":"crossref","unstructured":"K.\u00a0Doh, H.\u00a0Kim and D.A.\u00a0Schmidt, Abstract LR-parsing, in: Formal Modeling: Actors, Open Systems, Biological Systems\u00a0\u2013 Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, G.\u00a0Agha, O.\u00a0Danvy and J.\u00a0Meseguer, eds, Lecture Notes in Computer Science, Vol.\u00a07000, Springer, 2011, pp.\u00a090\u2013109. doi:10.1007\/978-3-642-24933-4_6.","DOI":"10.1007\/978-3-642-24933-4_6"},{"key":"ref013","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/17.2.143"},{"key":"ref014","doi-asserted-by":"crossref","unstructured":"J.\u00a0Field and T.\u00a0Teitelbaum, Incremental reduction in the lambda calculus, in: LISP and Functional Programming, 1990, pp.\u00a0307\u2013322.","DOI":"10.1145\/91556.91679"},{"key":"ref015","doi-asserted-by":"crossref","unstructured":"J.A.\u00a0Goguen and J.\u00a0Meseguer, Security policies and security models, in: IEEE Symposium on Security and Privacy, 1982, pp.\u00a011\u201320.","DOI":"10.1109\/SP.1982.10014"},{"key":"ref016","unstructured":"S.\u00a0Guarnieri and V.B.\u00a0Livshits, GATEKEEPER: Mostly static enforcement of security and reliability policies for JavaScript code, in: Proceedings of the 18th USENIX Security Symposium, Montreal, Canada, August 10\u201314, 2009, F.\u00a0Monrose, ed. USENIX Association, 2009, pp.\u00a0151\u2013168."},{"key":"ref017","doi-asserted-by":"crossref","unstructured":"S.\u00a0Guarnieri, M.\u00a0Pistoia, O.\u00a0Tripp, J.\u00a0Dolby, S.\u00a0Teilhet and R.\u00a0Berg, Saving the world wide web from vulnerable JavaScript, in: Proceedings of the 20th International Symposium on Software Testing and Analysis, ISSTA 2011, Toronto, ON, Canada, July 17\u201321, 2011, M.B.\u00a0Dwyer and F.\u00a0Tip, eds, ACM, 2011, pp.\u00a0177\u2013187. doi:10.1145\/2001420.2001442.","DOI":"10.1145\/2001420.2001442"},{"key":"ref018","doi-asserted-by":"crossref","unstructured":"A.\u00a0Guha, C.\u00a0Saftoiu and S.\u00a0Krishnamurthi, The essence of JavaScript, in: ECOOP, 2010, pp.\u00a0126\u2013150.","DOI":"10.1007\/978-3-642-14107-2_7"},{"key":"ref019","doi-asserted-by":"crossref","unstructured":"D.\u00a0Hedin and A.\u00a0Sabelfeld, Information-flow security for a core of JavaScript, in: CSF, S.\u00a0Chong, ed. IEEE, 2012, pp.\u00a03\u201318.","DOI":"10.1109\/CSF.2012.19"},{"key":"ref020","doi-asserted-by":"crossref","unstructured":"N.\u00a0Heintze and D.A.\u00a0McAllester, On the cubic bottleneck in subtyping and flow analysis, in: LICS, IEEE Computer Society, 1997, pp.\u00a0342\u2013351.","DOI":"10.1109\/LICS.1997.614960"},{"key":"ref021","unstructured":"D.R.\u00a0Hofstadter, Godel, Escher, Bach: An Eternal Golden Braid, Basic Books, Inc., New York, NY, USA, 1979."},{"key":"ref022","unstructured":"D.V.\u00a0Horn and M.\u00a0Might, An analytic framework for JavaScript,\n                      CoRR\n                      , abs\/1109.4467 (2011)."},{"key":"ref023","doi-asserted-by":"crossref","unstructured":"J.\u00a0Inoue and W.\u00a0Taha, Reasoning about multi-stage programs, in: ESOP, 2012.","DOI":"10.1007\/978-3-642-28869-2_18"},{"key":"ref024","doi-asserted-by":"crossref","unstructured":"S.H.\u00a0Jensen, P.A.\u00a0Jonsson and A.\u00a0M\u00f8ller, Remedying the eval that men do, in: ISSTA, 2012, pp.\u00a034\u201344.","DOI":"10.1145\/2338965.2336758"},{"key":"ref025","doi-asserted-by":"crossref","unstructured":"S.\u00a0Just, A.\u00a0Cleary, B.\u00a0Shirley and C.\u00a0Hammer, Information flow analysis for JavaScript, in: PLASTIC, 2011.","DOI":"10.1145\/2093328.2093331"},{"key":"ref026","doi-asserted-by":"crossref","unstructured":"I.S.\u00a0Kim, K.\u00a0Yi and C.\u00a0Calcagno, A polymorphic modal type system for lisp-like multi-staged languages, in: POPL, 2006, pp.\u00a0257\u2013268.","DOI":"10.1145\/1111037.1111060"},{"key":"ref027","unstructured":"T.\u00a0Kim, C.\u00a0Lee, K.\u00a0Lee, S.\u00a0Baik and K.\u00a0Yi, A control flow analysis for 2-staged programming languages, Techreport ROSAEC-2009-005, ROSAEC, 2009."},{"key":"ref028","doi-asserted-by":"crossref","unstructured":"M.\u00a0Lester, L.\u00a0Ong and M.\u00a0Sch\u00e4fer, Information flow analysis for a dynamically typed language with staged metaprogramming, in: CSF, IEEE, 2013, pp.\u00a0209\u2013223.","DOI":"10.1109\/CSF.2013.21"},{"key":"ref029","doi-asserted-by":"crossref","unstructured":"M.M.\u00a0Lester, Position paper: The science of boxing, in: PLAS, P.\u00a0Naldurg and N.\u00a0Swamy, eds, ACM, 2013, pp.\u00a083\u201388.","DOI":"10.1145\/2465106.2465120"},{"key":"ref030","unstructured":"M.M.\u00a0Lester, Verifying information flow and metaprogramming in dynamically typed languages: Mechanised Coq proofs and analysis source code supporting thesis, Oxford University Research Archive, 2015. doi:10.5287\/bodleian:wxdB0NV6k."},{"key":"ref031","doi-asserted-by":"crossref","unstructured":"P.\u00a0Li and S.\u00a0Zdancewic, Downgrading policies and relaxed noninterference, in: POPL, 2005, pp.\u00a0158\u2013170.","DOI":"10.1145\/1047659.1040319"},{"key":"ref032","unstructured":"S.\u00a0Liang and M.\u00a0Might, Hash-flow taint analysis of higher-order programs, in: Proceedings of the 2012 Workshop on Programming Languages and Analysis for Security, PLAS 2012, Beijing, China, June 15, 2012, S.\u00a0Maffeis and T.\u00a0Rezk, eds, ACM, 2012, Article No.\u00a08."},{"key":"ref033","doi-asserted-by":"crossref","unstructured":"S.\u00a0Maffeis, J.C.\u00a0Mitchell and A.\u00a0Taly, An operational semantics for JavaScript, in: APLAS, 2008, pp.\u00a0307\u2013325.","DOI":"10.1007\/978-3-540-89330-1_22"},{"key":"ref034","doi-asserted-by":"crossref","unstructured":"F.\u00a0Meawad, G.\u00a0Richards, F.\u00a0Morandat and J.\u00a0Vitek, Eval begone!: Semi-automated removal of eval from javascript programs, in: OOPSLA, G.T.\u00a0Leavens and M.B.\u00a0Dwyer, eds, ACM, 2012, pp.\u00a0607\u2013620.","DOI":"10.1145\/2384616.2384660"},{"key":"ref035","unstructured":"M.\u00a0Might, Y.\u00a0Smaragdakis and D.V.\u00a0Horn, Resolving and exploiting the\n                      k\n                      -CFA paradox,\n                      CoRR\n                      , abs\/1311.4231 (2013)."},{"key":"ref036","doi-asserted-by":"crossref","unstructured":"F.\u00a0Nielson, H.R.\u00a0Nielson and C.\u00a0Hankin, Principles of Program Analysis, Springer, 1999.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"ref037","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1058"},{"key":"ref038","doi-asserted-by":"crossref","unstructured":"P.H.\u00a0Phung, D.\u00a0Sands and A.\u00a0Chudnov, Lightweight self-protecting JavaScript, in: Proceedings of the 2009 ACM Symposium on Information, Computer and Communications Security, ASIACCS 2009, Sydney, Australia, March 10\u201312, 2009, W.\u00a0Li, W.\u00a0Susilo, U.K.\u00a0Tupakula, R.\u00a0Safavi-Naini and V.\u00a0Varadharajan, eds, ACM, 2009, pp.\u00a047\u201360.","DOI":"10.1145\/1533057.1533067"},{"key":"ref039","doi-asserted-by":"crossref","unstructured":"F.\u00a0Pottier and S.\u00a0Conchon, Information flow inference for free, in: ICFP, 2000.","DOI":"10.1145\/351240.351245"},{"key":"ref040","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"ref041","doi-asserted-by":"crossref","unstructured":"G.\u00a0Richards, C.\u00a0Hammer, B.\u00a0Burg and J.\u00a0Vitek, The eval that men do\u00a0\u2013 A large-scale study of the use of eval in JavaScript applications, in: ECOOP, 2011.","DOI":"10.1007\/978-3-642-22655-7_4"},{"key":"ref042","unstructured":"J.\u00a0Rushby, Noninterference, transitivity, and channel-control security policies, Technical report, December 1992."},{"key":"ref043","doi-asserted-by":"crossref","unstructured":"A.\u00a0Russo and A.\u00a0Sabelfeld, Dynamic vs. static flow-sensitive security analysis, in: CSF, 2010, pp.\u00a0186\u2013199.","DOI":"10.1109\/CSF.2010.20"},{"key":"ref044","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"ref045","doi-asserted-by":"crossref","unstructured":"A.\u00a0Sabelfeld and A.\u00a0Russo, From dynamic to static and back: Riding the roller coaster of information-flow control research, in: Ershov Memorial Conf., 2009.","DOI":"10.1007\/978-3-642-11486-1_30"},{"key":"ref046","doi-asserted-by":"crossref","unstructured":"D.\u00a0Schoepe, D.\u00a0Hedin and A.\u00a0Sabelfeld, SeLINQ: Tracking information across application-database boundaries, in: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 1\u20133, 2014, J.\u00a0Jeuring and M.M.T.\u00a0Chakravarty, eds, ACM, 2014, pp.\u00a025\u201338.","DOI":"10.1145\/2628136.2628151"},{"key":"ref047","doi-asserted-by":"crossref","unstructured":"O.\u00a0Shivers, Control-flow analysis in scheme, in: PLDI, 1988, pp.\u00a0164\u2013174.","DOI":"10.1145\/53990.54007"},{"key":"ref048","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680200463X"},{"key":"ref049","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-140516"},{"key":"ref050","doi-asserted-by":"crossref","unstructured":"D.\u00a0Vardoulakis and O.\u00a0Shivers, CFA2: A context-free approach to control-flow analysis,\n                      Logical Methods in Computer Science\n                      7\n                      (2) (2011). doi:10.2168\/LMCS-7(2:3)2011.","DOI":"10.2168\/LMCS-7(2:3)2011"},{"key":"ref051","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"ref052","unstructured":"S.\u00a0Zdancewic, Programming languages for information security, PhD thesis, Cornell University, 2002."}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-160557","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-160557","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-160557","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:44:59Z","timestamp":1777495499000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-160557"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,5]]},"references-count":52,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,11,8]]}},"alternative-id":["10.3233\/JCS-160557"],"URL":"https:\/\/doi.org\/10.3233\/jcs-160557","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9,5]]}}}