Information flow analysis for a dynamically typed language with staged metaprogramming

Lester, M. ORCID: https://orcid.org/0000-0002-2323-1771, Ong, L. and Schäfer, M. (2016) Information flow analysis for a dynamically typed language with staged metaprogramming. Journal of Computer Security, 24 (5). pp. 541-582. ISSN 0926-227X doi: 10.3233/JCS-160557

Abstract/Summary

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. 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. 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.

Item Type	Article
URI	https://reading-clone.eprints-hosting.org/id/eprint/81998
Item Type	Article
Refereed	Yes
Divisions	No Reading authors. Back catalogue items Science > School of Mathematical, Physical and Computational Sciences > Department of Computer Science
Publisher	IOS Press
Download/View statistics	View download statistics for this item